List of theorems

List of theorems in peano_new/arithmetic/common/mulcan.gh:

BiReplaceImp1Bi0 # <context> # This theorem is part of a set of proofs related to the multiplicative # cancelation property. These theorems apply generally to natural # numbers, integers, rational, and real numbers. They do not apply to complex numbers. # </context> # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
EqReplaceImp1Bi0Eq1 # <title> Substitution </title> # <table> # (-> ph (<-> (= A [ B ] ] ] ) ps)) # (= [ B ] [ C ] ) # (-> ph (<-> (= A [ [ [ C ] ) ps)) # </table>
(-> ph (<-> (= A B) ps)) , (= B C)(-> ph (<-> (= A C) ps))
BiReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (<-> ch th)(-> ph (-> ps th))
BiReplaceImp1Imp1Not0 # <title> Substitution </title> # <table> # (-> ph (-> ps (-. [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps (-. [ [ [ th ] ))) # </table>
(-> ph (-> ps (-. ch))) , (<-> ch th)(-> ph (-> ps (-. th)))
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
(-> (-. (= A (0))) (<-> (= (* B A) (0)) (= B (0))))
EqReplaceImp1Imp1Not0Eq0 # <title> Substitution </title> # <table> # (-> ph (-> ps (-. (= [ A ] ] ] C)))) # (= [ A ] [ B ] ) # (-> ph (-> ps (-. (= [ [ [ B ] C)))) # </table>
(-> ph (-> ps (-. (= A C)))) , (= A B)(-> ph (-> ps (-. (= B C))))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
zeroProductz # <title> Zero Product Property </title>
(-> (/\ (-. (= A (0))) (-. (= B (0)))) (-. (= (* A B) (0))))
BiReplaceBi1Not0Or0 # <title> Substitution </title> # <table> # (<-> ph (-. (\/ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. (\/ [ [ [ ch ] th))) # </table>
(<-> ph (-. (\/ ps th))) , (<-> ps ch)(<-> ph (-. (\/ ch th)))
BiReplaceBi1Not0Or1 # <title> Substitution </title> # <table> # (<-> ph (-. (\/ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (-. (\/ ps [ [ [ th ] ))) # </table>
(<-> ph (-. (\/ ps ch))) , (<-> ch th)(<-> ph (-. (\/ ps th)))
zeroFactors # <title> Zero Product Property </title>
(<-> (= (* A B) (0)) (\/ (= A (0)) (= B (0))))
EqReplaceImp1Imp1Eq1 # <title> Substitution </title> # <table> # (-> ph (-> ps (= A [ B ] ] ] ))) # (= [ B ] [ C ] ) # (-> ph (-> ps (= A [ [ [ C ] ))) # </table>
(-> ph (-> ps (= A B))) , (= B C)(-> ph (-> ps (= A C)))
EqReplaceImp1Imp1Eq0 # <title> Substitution </title> # <table> # (-> ph (-> ps (= [ A ] ] ] C))) # (= [ A ] [ B ] ) # (-> ph (-> ps (= [ [ [ B ] C))) # </table>
(-> ph (-> ps (= A C))) , (= A B)(-> ph (-> ps (= B C)))
(-> (-. (= A (0))) (<-> (= B (0)) (= (* A B) (0))))
nonzeroProduct2 # <title> Zero Product Property </title>
(<-> (-. (= (* A B) (0))) (/\ (-. (= A (0))) (-. (= B (0)))))
neqmul # <title> Multiply Nonequal Numbers </title>
(-> (/\ (-. (= A B)) (-. (= C (0)))) (-. (= (* A C) (* B C))))
EqReplaceImp1Bi0Eq0 # <title> Substitution </title> # <table> # (-> ph (<-> (= [ A ] ] ] C) ps)) # (= [ A ] [ B ] ) # (-> ph (<-> (= [ [ [ B ] C) ps)) # </table>
(-> ph (<-> (= A C) ps)) , (= A B)(-> ph (<-> (= B C) ps))
mulcan2 # <title> Cancel Multiplication </title>
(-> (-. (= A (0))) (<-> (= (* A B) (* A C)) (= B C)))
mulcani # <title> Cancel Multiplication </title> # <table> # (-. (= <r> A ] (0))) ] ] # (= (* B ] <r> A ) ] (* [ C <r> A)) # (= B ] ] [ C) # </table>
(-. (= A (0))) , (= (* B A) (* C A))(= B C)
mulcan2i # <title> Cancel Multiplication </title> # <table> # (-. (= <r> A ] ] (0))) ] # (= (* <r> A [ B ) ] (* <r> A [ C )) # (= [ B ] [ C) # </table>
(-. (= A (0))) , (= (* A B) (* A C))(= B C)
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)