eqtr.3 Show Code edit
thm (eqtr.3 () () (-> (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (-> (/\ (= A B) (= B C)) (= A C)))
A B dfeq1
(-> (= A B) (z.= (z.* (top A) (bottom B)) (z.* (top B) (bottom A))))
B C dfeq1
(-> (= B C) (z.= (z.* (top B) (bottom C)) (z.* (top C) (bottom B))))
anim12i
(-> (/\ (= A B) (= B C)) (/\ (z.= (z.* (top A) (bottom B)) (z.* (top B) (bottom A))) (z.= (z.* (top B) (bottom C)) (z.* (top C) (bottom B)))))
(z.* (top A) (bottom B))
(z.* (top B) (bottom A))
(z.* (top B) (bottom C))
(z.* (top C) (bottom B)) z.muleq12
(-> (/\ (z.= (z.* (top A) (bottom B)) (z.* (top B) (bottom A))) (z.= (z.* (top B) (bottom C)) (z.* (top C) (bottom B)))) (z.= (z.* (z.* (top A) (bottom B)) (z.* (top B) (bottom C))) (z.* (z.* (top B) (bottom A)) (z.* (top C) (bottom B)))))
syl
(-> (/\ (= A B) (= B C)) (z.= (z.* (z.* (top A) (bottom B)) (z.* (top B) (bottom C))) (z.* (z.* (top B) (bottom A)) (z.* (top C) (bottom B)))))
(top A) (bottom B) (top B) (bottom C) z.mul42
(z.= (z.* (z.* (top A) (bottom B)) (z.* (top B) (bottom C))) (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))))
ZeqReplaceImp1Zeq0
(-> (/\ (= A B) (= B C)) (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top B) (bottom A)) (z.* (top C) (bottom B)))))
(top B) (bottom A) (top C) (bottom B) z.mul42
(z.= (z.* (z.* (top B) (bottom A)) (z.* (top C) (bottom B))) (z.* (z.* (top B) (bottom B)) (z.* (top C) (bottom A))))
ZeqReplaceImp1Zeq1
(-> (/\ (= A B) (= B C)) (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top B) (bottom B)) (z.* (top C) (bottom A)))))
## <d 'Commutative Property of Multiplication '>
(z.* (top B) (bottom B)) (z.* (top C) (bottom A)) z.mulcom
(z.= (z.* (z.* (top B) (bottom B)) (z.* (top C) (bottom A))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B))))
ZeqReplaceImp1Zeq1
(-> (/\ (= A B) (= B C)) (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))))
## </d 'Commutative Property of Multiplication '>
(bottom B) (top B) z.zeroProductz
(-> (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (-. (z.= (z.* (bottom B) (top B)) (z.0))))
## <d 'Commutative Property of Multiplication '>
(bottom B) (top B) z.mulcom
(z.= (z.* (bottom B) (top B)) (z.* (top B) (bottom B)))
ZeqReplaceImp1Not0Zeq0
(-> (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (-. (z.= (z.* (top B) (bottom B)) (z.0))))
## </d 'Commutative Property of Multiplication '>
(z.* (top B) (bottom B)) (z.* (top A) (bottom C)) (z.* (top C) (bottom A)) z.mulcan
(-> (-. (z.= (z.* (top B) (bottom B)) (z.0))) (<-> (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))))
syl
(-> (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (<-> (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))))
## <d 'Infer Left to Right '>
(z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))) bi1
(-> (<-> (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))) (-> (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))))
syl
(-> (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (-> (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))))
## </d 'Infer Left to Right '>
anim12i
(-> (/\ (/\ (= A B) (= B C)) (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0))))) (/\ (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (-> (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))))))
## <d 'Introduce conjunct as antecedent '>
(z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))) abai bicomi
(<-> (/\ (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (-> (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))))) (/\ (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))))
sylib
(-> (/\ (/\ (= A B) (= B C)) (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0))))) (/\ (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))))
## </d 'Introduce conjunct as antecedent '>
## <d 'Remove Left Side of AND '>
(z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))) pm3.27
(-> (/\ (z.= (z.* (z.* (top A) (bottom C)) (z.* (top B) (bottom B))) (z.* (z.* (top C) (bottom A)) (z.* (top B) (bottom B)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))))
syl
(-> (/\ (/\ (= A B) (= B C)) (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0))))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))))
## </d 'Remove Left Side of AND '>
## <d 'Commute Conjunction '>
(/\ (= A B) (= B C)) (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) ancom
(<-> (/\ (/\ (= A B) (= B C)) (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0))))) (/\ (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (/\ (= A B) (= B C))))
sylbi2
(-> (/\ (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (/\ (= A B) (= B C))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))))
## </d 'Commute Conjunction '>
## <d 'Import-Export Theorem '>
(/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (/\ (= A B) (= B C)) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))) impexp
(<-> (-> (/\ (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (/\ (= A B) (= B C))) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))) (-> (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (-> (/\ (= A B) (= B C)) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))))))
mpbi
(-> (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (-> (/\ (= A B) (= B C)) (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A)))))
## </d 'Import-Export Theorem '>
A B C eqtr.0
(-> (/\ (= A B) (= B C)) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0))))
(/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) a1i
(-> (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (-> (/\ (= A B) (= B C)) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0)))))
jcad
(-> (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top 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.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (-> (/\ (= A B) (= B C)) (= A C)))
## </d 'Definition of Rational Equality '>
)
edit