# List of theorems

List of theorems in peano_new/arithmetic/complex/division_min.gh:

df-div # <context> # This theorem is part of a series of theorems constructing division # for complex numbers. A complex number is constructed as a pair of real numbers which # represents the real and the imaginary part of the complex number. These theorems demonstrate # that this newly constructed version of complex division has the essential properties of a # division operation. # </context> # <title> Definition of Complex Division </title>
(= (/ A B) (<,> (r./ (r.+ (r.* (head A) (head B)) (r.* (tail A) (tail B))) (r.+ (r.* (head B) (head B)) (r.* (tail B) (tail B)))) (r./ (r.- (r.* (tail A) (head B)) (r.* (head A) (tail B))) (r.+ (r.* (head B) (head B)) (r.* (tail B) (tail B))))))
EqReplaceImp1Eq0 # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (= A C)) , (= A B)(-> ph (= B C))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
diveq1 # <summary> This is used just for convenience to get an empty theorem. </summary>
(-> (= A B) (= (/ A C) (/ B C)))
diveq2bottom # <title> Equality in the Denominator </title>
(-> (/\ (r.= (head A) (head B)) (r.= (tail A) (tail B))) (r.= (r.+ (r.* (head A) (head A)) (r.* (tail A) (tail A))) (r.+ (r.* (head B) (head B)) (r.* (tail B) (tail B)))))
(-> (= A B) (= (/ C A) (/ C B)))
diveq12 # <title> Equivalence for / </title> ##
(-> (/\ (= A B) (= C D)) (= (/ A C) (/ B D)))
EqReplaceEq1 # <title> Substitution </title> # <table> # (= A [ B ] ] ] ) # (= [ B ] [ C ] ) # (= A [ [ [ C ] ) # </table>
(= A B) , (= B C)(= A C)
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
ReqReplaceImp1Not0Req1 # <title> Substitution </title> # <table> # (-> ph (-. (r.= a [ b ] ] ] ))) # (r.= [ b ] [ c ] ) # (-> ph (-. (r.= a [ [ [ c ] ))) # </table>
(-> ph (-. (r.= a b))) , (r.= b c)(-> ph (-. (r.= a c)))
ReqReplaceImp1Not0Req0 # <title> Substitution </title> # <table> # (-> ph (-. (r.= [ a ] ] ] c))) # (r.= [ a ] [ b ] ) # (-> ph (-. (r.= [ [ [ b ] c))) # </table>
(-> ph (-. (r.= a c))) , (r.= a b)(-> ph (-. (r.= b c)))
BiReplaceBi1An0 # <title> Substitution </title> # <table> # (<-> ph (/\ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ [ [ [ ch ] th)) # </table>
(<-> ph (/\ ps th)) , (<-> ps ch)(<-> ph (/\ ch th))
ReqReplaceBi1An0Req1 # <title> Substitution </title> # <table> # (<-> ph (/\ (r.= a [ b ] ] ] ) ps)) # (r.= [ b ] [ c ] ) # (<-> ph (/\ (r.= a [ [ [ c ] ) ps)) # </table>
(<-> ph (/\ (r.= a b) ps)) , (r.= b c)(<-> ph (/\ (r.= a c) ps))
BiReplaceBi1An1 # <title> Substitution </title> # <table> # (<-> ph (/\ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (<-> ph (/\ ps [ [ [ th ] )) # </table>
(<-> ph (/\ ps ch)) , (<-> ch th)(<-> ph (/\ ps th))
ReqReplaceBi1An1Req1 # <title> Substitution </title> # <table> # (<-> ph (/\ ps (r.= a [ b ] ] ] ))) # (r.= [ b ] [ c ] ) # (<-> ph (/\ ps (r.= a [ [ [ c ] ))) # </table>
(<-> ph (/\ ps (r.= a b))) , (r.= b c)(<-> ph (/\ ps (r.= a c)))
EqReplaceBi0Eq1 # <title> Substitution </title> # <table> # (<-> (= A [ B ] ] ] ) ph) # (= [ B ] [ C ] ) # (<-> (= A [ [ [ C ] ) ph) # </table>
(<-> (= A B) ph) , (= B C)(<-> (= A C) ph)
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
absNot0 # <title> Absolute value is only 0 for 0 </title>
(-> (-. (= A (0))) (-. (r.= (r.+ (r.* (head A) (head A)) (r.* (tail A) (tail A))) (r.0))))
ReqReplaceReq1 # <title> Substitution </title> # <table> # (r.= a [ b ] ] ] ) # (r.= [ b ] [ c ] ) # (r.= a [ [ [ c ] ) # </table>
(r.= a b) , (r.= b c)(r.= a c)
ReqReplaceReq1Radd0 # <title> Substitution </title> # <table> # (r.= a (r.+ [ b ] ] ] d)) # (r.= [ b ] [ c ] ) # (r.= a (r.+ [ [ [ c ] d)) # </table>
(r.= a (r.+ b d)) , (r.= b c)(r.= a (r.+ c d))
ReqReplaceReq1Radd1 # <title> Substitution </title> # <table> # (r.= a (r.+ b [ c ] ] ] )) # (r.= [ c ] [ d ] ) # (r.= a (r.+ b [ [ [ d ] )) # </table>
(r.= a (r.+ b c)) , (r.= c d)(r.= a (r.+ b d))
ReqReplaceReq1Radd1Rneg0 # <title> Substitution </title> # <table> # (r.= a (r.+ b (r.-n [ c ] ] ] ))) # (r.= [ c ] [ d ] ) # (r.= a (r.+ b (r.-n [ [ [ d ] ))) # </table>
(r.= a (r.+ b (r.-n c))) , (r.= c d)(r.= a (r.+ b (r.-n d)))
ReqReplaceReq1Radd0Radd0 # <title> Substitution </title> # <table> # (r.= a (r.+ (r.+ [ b ] ] ] d) a')) # (r.= [ b ] [ c ] ) # (r.= a (r.+ (r.+ [ [ [ c ] d) a')) # </table>
(r.= a (r.+ (r.+ b d) a')) , (r.= b c)(r.= a (r.+ (r.+ c d) a'))
ReqReplaceReq1Radd0Radd1 # <title> Substitution </title> # <table> # (r.= a (r.+ (r.+ b [ c ] ] ] ) a')) # (r.= [ c ] [ d ] ) # (r.= a (r.+ (r.+ b [ [ [ d ] ) a')) # </table>
(r.= a (r.+ (r.+ b c) a')) , (r.= c d)(r.= a (r.+ (r.+ b d) a'))
ReqReplaceReq1Radd0Radd1Rmul1 # <title> Substitution </title> # <table> # (r.= a (r.+ (r.+ b (r.* c [ d ] ] ] )) b')) # (r.= [ d ] [ a' ] ) # (r.= a (r.+ (r.+ b (r.* c [ [ [ a' ] )) b')) # </table>
(r.= a (r.+ (r.+ b (r.* c d)) b')) , (r.= d a')(r.= a (r.+ (r.+ b (r.* c a')) b'))
ReqReplaceReq1Radd1Rsub0 # <title> Substitution </title> # <table> # (r.= a (r.+ b (r.- [ c ] ] ] a'))) # (r.= [ c ] [ d ] ) # (r.= a (r.+ b (r.- [ [ [ d ] a'))) # </table>
(r.= a (r.+ b (r.- c a'))) , (r.= c d)(r.= a (r.+ b (r.- d a')))
ReqReplaceReq1Radd1Rsub1 # <title> Substitution </title> # <table> # (r.= a (r.+ b (r.- c [ d ] ] ] ))) # (r.= [ d ] [ a' ] ) # (r.= a (r.+ b (r.- c [ [ [ a' ] ))) # </table>
(r.= a (r.+ b (r.- c d))) , (r.= d a')(r.= a (r.+ b (r.- c a')))
ReqReplaceReq1Radd1Rsub1Rmul1 # <title> Substitution </title> # <table> # (r.= a (r.+ b (r.- c (r.* d [ a' ] ] ] )))) # (r.= [ a' ] [ b' ] ) # (r.= a (r.+ b (r.- c (r.* d [ [ [ b' ] )))) # </table>
(r.= a (r.+ b (r.- c (r.* d a')))) , (r.= a' b')(r.= a (r.+ b (r.- c (r.* d b'))))
ReqReplaceReq1Radd0Radd0Rmul1 # <title> Substitution </title> # <table> # (r.= a (r.+ (r.+ (r.* b [ c ] ] ] ) a') b')) # (r.= [ c ] [ d ] ) # (r.= a (r.+ (r.+ (r.* b [ [ [ d ] ) a') b')) # </table>
(r.= a (r.+ (r.+ (r.* b c) a') b')) , (r.= c d)(r.= a (r.+ (r.+ (r.* b d) a') b'))
ReqReplaceImp1Req1 # <title> Substitution </title> # <table> # (-> ph (r.= a [ b ] ] ] )) # (r.= [ b ] [ c ] ) # (-> ph (r.= a [ [ [ c ] )) # </table>
(-> ph (r.= a b)) , (r.= b c)(-> ph (r.= a c))
(r.= (r.- (r.* a (r.+ (r.* c a) (r.* d b))) (r.* b (r.- (r.* d a) (r.* c b)))) (r.* c (r.+ (r.* a a) (r.* b b))))
(-> (-. (r.= (r.+ (r.* a a) (r.* b b)) (r.0))) (r.= (r.- (r.* a (r./ (r.+ (r.* c a) (r.* d b)) (r.+ (r.* a a) (r.* b b)))) (r.* b (r./ (r.- (r.* d a) (r.* c b)) (r.+ (r.* a a) (r.* b b))))) c))
(r.= (r.+ (r.* b (r.+ (r.* c a) (r.* d b))) (r.* a (r.- (r.* d a) (r.* c b)))) (r.* d (r.+ (r.* a a) (r.* b b))))
(-> (-. (r.= (r.+ (r.* a a) (r.* b b)) (r.0))) (r.= (r.+ (r.* b (r./ (r.+ (r.* c a) (r.* d b)) (r.+ (r.* a a) (r.* b b)))) (r.* a (r./ (r.- (r.* d a) (r.* c b)) (r.+ (r.* a a) (r.* b b))))) d))
(-> (-. (= A (0))) (= (* A (/ B A)) B))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)