eqtr.2 Show Code edit
thm (eqtr.2 () () (-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (-> (/\ (= A B) (= B C)) (= A C)))
A B eqtr.1
(-> (= A B) (-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (z.= (top A) (z.0))))
(top A) (z.0) (bottom C) z.muleq1
(-> (z.= (top A) (z.0)) (z.= (z.* (top A) (bottom C)) (z.* (z.0) (bottom C))))
## <d 'Multiply by 0 '>
(bottom C) z.mul0r
(z.= (z.* (z.0) (bottom C)) (z.0))
ZeqReplaceImp1Zeq1
(-> (z.= (top A) (z.0)) (z.= (z.* (top A) (bottom C)) (z.0)))
## </d 'Multiply by 0 '>
ImpReplaceImp1Imp1
(-> (= A B) (-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (z.= (z.* (top A) (bottom C)) (z.0))))
com12
(-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (-> (= A B) (z.= (z.* (top A) (bottom C)) (z.0))))
C B eqtr.1
(-> (= C B) (-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (z.= (top C) (z.0))))
(top C) (z.0) (bottom A) z.muleq1
(-> (z.= (top C) (z.0)) (z.= (z.* (top C) (bottom A)) (z.* (z.0) (bottom A))))
ImpReplaceImp1Imp1
(-> (= C B) (-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (z.= (z.* (top C) (bottom A)) (z.* (z.0) (bottom A)))))
## <d 'Multiply by 0 '>
(bottom A) z.mul0r
(z.= (z.* (z.0) (bottom A)) (z.0))
ZeqReplaceImp1Imp1Zeq1
(-> (= C B) (-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (z.= (z.* (top C) (bottom A)) (z.0))))
## </d 'Multiply by 0 '>
## <d 'Symmetric Property '>
(z.* (top C) (bottom A)) (z.0) z.eqcom
(<-> (z.= (z.* (top C) (bottom A)) (z.0)) (z.= (z.0) (z.* (top C) (bottom A))))
BiReplaceImp1Imp1
(-> (= C B) (-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (z.= (z.0) (z.* (top C) (bottom A)))))
## </d 'Symmetric Property '>
com12
(-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (-> (= C B) (z.= (z.0) (z.* (top C) (bottom A)))))
anim12d
(-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (-> (/\ (= A B) (= C B)) (/\ (z.= (z.* (top A) (bottom C)) (z.0)) (z.= (z.0) (z.* (top C) (bottom A))))))
## <d 'Transitive Property '>
(z.* (top A) (bottom C)) (z.0) (z.* (top C) (bottom A)) z.eqtr
(-> (/\ (z.= (z.* (top A) (bottom C)) (z.0)) (z.= (z.0) (z.* (top C) (bottom A)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))))
ImpReplaceImp1Imp1
(-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (-> (/\ (= A B) (= C B)) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))))
## </d 'Transitive Property '>
## <d>
C B eqcom
(<-> (= C B) (= B C))
BiReplaceImp1Imp0An1
(-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (-> (/\ (= A B) (= B C)) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))))
## </d>
A B C eqtr.0
(-> (/\ (= A B) (= B C)) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0))))
(/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) a1i
(-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (-> (/\ (= A B) (= B C)) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0)))))
jcad
(-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (-> (/\ (= A B) (= B C)) (/\ (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0))))))
## <d 'Definition of Rational Equality '>
A C df-eq bicomi
(<-> (/\ (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0)))) (= A C))
BiReplaceImp1Imp1
(-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (-> (/\ (= A B) (= B C)) (= A C)))
## </d 'Definition of Rational Equality '>
)
edit