List of theorems

List of theorems in peano_new/arithmetic/naturals/min_mod_div.gh:

BiReplaceImp1Bi0 # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
BiReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> ps th))
ImpReplaceEx1 # <title> Substitution </title> # <table> # (E. x [ ph ] ] ] ) # (-> [ ph ] [ ps ] ) # (E. x [ [ [ ps ] ) # </table>
(E. x ph) , (-> ph ps)(E. x ps)

Divisibility

df-divides-just number 36.5
(<-> (E. x (= (* A x) B)) (E. y (= (* A y) B)))
df-divides # <title> Divides Definition </title> # <suggest> left('Simplify', '|') right('Define', '|') </suggest>
(<-> (| A B) (E. x (= (* A x) B)))
divideseq1 # <title> Equivalence for | </title>
(-> (= A C) (<-> (| A B) (| C B)))
divideseq1i Equality inference for the divides relation. # <title> Equivalence over Divides </title> # <table> # (= A ] ] [ B ] ) # (<-> (| A ] C ] ) (| [ B ] C)) # </table>
(= A B)(<-> (| A C) (| B C))
divideseq1ii Equality inference for the Divides relation. # <title> Equivalence over divides </title> # <table> # (| A ] ] ] [ C) # (= A ] [ B ] ] ) # (| [ [ B ] [ C) # </table>
(| A C) , (= A B)(| B C)
divideseq2 # <title> Equivalence for | </title>
(-> (= B C) (<-> (| A B) (| A C)))
divideseq2i # <title> Equivalence over Divides </title> # <table> # (= [ A ] [ [ B ] ) # (<-> (| C [ A ] ) (| [ C [ B ] )) # </table>
(= A B)(<-> (| C A) (| C B))
divideseq2ii # <title> Equivalence over Divides </title> # <table> # (| C [ A ] ] ) # (= [ A ] [ B) # (| C [ [ [ B) # </table>
(| C A) , (= A B)(| C B)
(-> ph (= A B))(-> ph (<-> (| A C) (| B C)))
(-> ph (= A B))(-> ph (<-> (| C A) (| C B)))
EqReplaceEx1Eq1 # <title> Substitution </title> # <table> # (E. x (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (E. x (= A [ [ [ C ] )) # </table>
(E. x (= A B)) , (= B C)(E. x (= A C))
(= (* A B) C)(| A C)
(-> ph (= (* A B) C))(-> ph (| A C))
BiReplaceImp1Al1 # <title> Substitution </title> # <table> # (-> ph (A. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (A. x [ [ [ ch ] )) # </table>
(-> ph (A. x ps)) , (<-> ps ch)(-> ph (A. x ch))
BiReplaceImp1Al1An0 # <title> Substitution </title> # <table> # (-> ph (A. x (/\ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (-> ph (A. x (/\ [ [ [ ch ] th))) # </table>
(-> ph (A. x (/\ ps th))) , (<-> ps ch)(-> ph (A. x (/\ ch th)))
BiReplaceImp1Al1An0Or1 # <title> Substitution </title> # <table> # (-> ph (A. x (/\ (\/ ps [ ch ] ] ] ) ta))) # (<-> [ ch ] [ th ] ) # (-> ph (A. x (/\ (\/ ps [ [ [ th ] ) ta))) # </table>
(-> ph (A. x (/\ (\/ ps ch) ta))) , (<-> ch th)(-> ph (A. x (/\ (\/ ps th) ta)))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
BiReplaceImp0An0 # <title> Substitution </title> # <table> # (-> (/\ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ [ [ [ ps ] ch) th) # </table>
(-> (/\ ph ch) th) , (<-> ph ps)(-> (/\ ps ch) th)
BiReplaceImp0An1 # <title> Substitution </title> # <table> # (-> (/\ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph [ [ [ ch ] ) th) # </table>
(-> (/\ ph ps) th) , (<-> ps ch)(-> (/\ ph ch) th)
BiReplaceBi1Not0Ex1 # <title> Substitution </title> # <table> # (<-> ph (-. (E. x [ ps ] ] ] ))) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. (E. x [ [ [ ch ] ))) # </table>
(<-> ph (-. (E. x ps))) , (<-> ps ch)(<-> ph (-. (E. x ch)))
ImpReplaceImp1Al1 # <title> Substitution </title> # <table> # (-> ph (A. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (-> ph (A. x [ [ [ ch ] )) # </table>
(-> ph (A. x ps)) , (-> ps ch)(-> ph (A. x ch))
(-> (/\ (< (* A C) B) (< B (* A (+ C (1))))) (-. (| A B)))
dividessym # <title> A number divides itself </title> # <suggest> full('Simplify', 'T') </suggest>
(| A A)
dividesmul number 46.0
(-> (| A B) (| A (* B C)))
(| A B)(| A (* B C))
1plus1 # <title> One-digit Addition </title>
(= (+ (1) (1)) (2))
EqReplaceGt0 # <title> Substitution </title> # <table> # (> [ A ] ] ] C) # (= [ A ] [ B ] ) # (> [ [ [ B ] C) # </table>
(> A C) , (= A B)(> B C)
EqReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (= [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (= B C)(> A C)
2greater1 # <title> One-Digit Inequality </title>
(> (2) (1))
(> (+ A (2)) (1))
(-> (| (+ A (1)) (+ (* (+ A (1)) B) C)) (| (+ A (1)) C))
(-. (| (+ A (2)) (1)))
dividesmul12 number 128.6
(-> (| A B) (| (* A C) (* B C)))
dividestr # <title> Divides relation is transitive </title>
(-> (/\ (| A B) (| B C)) (| A C))
df-min-just # <context> # This theorem is part of a series of theorems that describe the properties # of the minimum number in a set of natural numbers. It is assumed that every # number in this theorem is a natural number. # </context> number 87.0
(= (iota ({|} x (/\ (e. x S) (A. y (-> (e. y S) (<= x y)))))) (iota ({|} x' (/\ (e. x' S) (A. y' (-> (e. y' S) (<= x' y')))))))
(= (min S) (iota ({|} x (/\ (e. x S) (A. y (-> (e. y S) (<= x y)))))))
minseq number 88.0 # <table> # (-> (=_ <r> S <g> T) (= (min <r> S) (min <g> T))) # </table>
(-> (=_ S T) (= (min S) (min T)))
(=_ S T)(= (min S) (min T))
(-> (= y A) (<-> (-> (e. y S) (/\ (e. (min S) S) (<= (min S) y))) (-> (e. A S) (/\ (e. (min S) S) (<= (min S) A)))))
minex.2.1 number 102.0
(-> (/\ (e. B S) (A. w (-> (e. w S) (<= A w)))) (<= A B))
(-> (/\ (e. A S) (A. w (-> (e. w S) (<= A w)))) (= A (min S)))
(-> (/\ (e. w' S) (A. w (-> (e. w S) (<= w' w)))) (= w' (min S)))
(-> (A. w (-> (<= w z) (-> (e. w S) (/\ (e. (min S) S) (<= (min S) w))))) (-> (e. (+ z (1)) S) (/\ (e. (min S) S) (<= (min S) (+ z (1))))))
minex # <title> The minimum of a nonempty set exists </title>
(-> (e. A S) (/\ (e. (min S) S) (<= (min S) A)))
minseqd Equality deduction for set minimum
(-> ph (=_ S T))(-> ph (= (min S) (min T)))
df-mod-just # <context> # This theorem is part of a series of theorems that describe the properties # of the modulo operation. It is assumed that every # number in this theorem is a natural number. # </context> number 89.0
(= (min ({|} x (E. y (= (+ (* B y) x) A)))) (min ({|} x' (E. y' (= (+ (* B y') x') A)))))
(= (mod A B) (min ({|} x (E. y (= (+ (* B y) x) A)))))
(-> (= A B) (= (mod A C) (mod B C)))
modeq2 Equality theorem for mod
(-> (= A B) (= (mod C A) (mod C B)))
(= A B)(= (mod A C) (mod B C))
(-> ph (= A B))(-> ph (= (mod A C) (mod B C)))
(= A B)(= (mod C A) (mod C B))
(-> ph (= A B))(-> ph (= (mod C A) (mod C B)))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
EqReplaceImp1Eq1Add0 # <title> Substitution </title> # <table> # (-> ph (= A (+ [ B ] ] ] D))) # (= [ B ] [ C ] ) # (-> ph (= A (+ [ [ [ C ] D))) # </table>
(-> ph (= A (+ B D))) , (= B C)(-> ph (= A (+ C D)))
mincl # <context> # This theorem is part of a series of theorems that describe the properties # of the minimum number in a set of natural numbers. It is assumed that every # number in this theorem is a natural number. # </context> # <title> A nonempty set minimum is in the set </title>
(-> (E. x (e. x S)) (e. (min S) S))
(= (min ({} A)) A)
SeqReplaceSeq1 # <title> Substitution </title> # <table> # (=_ S [ T ] ] ] ) # (=_ [ T ] [ U ] ) # (=_ S [ [ [ U ] ) # </table>
(=_ S T) , (=_ T U)(=_ S U)
EqReplaceLt0 # <title> Substitution </title> # <table> # (< [ A ] ] ] C) # (= [ A ] [ B ] ) # (< [ [ [ B ] C) # </table>
(< A C) , (= A B)(< B C)
mod0 # <context> # This theorem is part of a series of theorems that describe the properties # of the modulo operation. It is assumed that every # number in this theorem is a natural number. # </context>
(= (mod A (0)) A)
EqReplaceLt0Mod1 # <title> Substitution </title> # <table> # (< (mod A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (< (mod A [ [ [ C ] ) D) # </table>
(< (mod A B) D) , (= B C)(< (mod A C) D)
(-> (/\ (= (+ (* (+ B (1)) D) C) A) (= (+ (* (+ B (1)) D') C') A)) (<-> (< D' D) (< C C')))
(-> (/\ (= (+ (* (+ B (1)) D) C) A) (= (+ (* (+ B (1)) D') C') A)) (-> (< C C') (<= (+ (+ B (1)) C) C')))
(-> (/\ (= (+ (* B D) C) A) (= (+ (* B D') C') A)) (-> (< C C') (<= (+ B C) C')))
minval # <context> # This theorem is part of a series of theorems that describe the properties # of the minimum number in a set of natural numbers. It is assumed that every # number in this theorem is a natural number. # </context> # <summary> Another way of specifying the value of minimum </summary>
(rwff x ph) , (-> (= x A) (<-> ph ps))(-> (/\ ps (A. x (-> ph (<= A x)))) (= A (min ({|} x ph))))
minsetval # <suggest> right('Simplify', 'min') </suggest>
(-> (/\ (e. A S) (A. x (-> (e. x S) (<= A x)))) (= A (min ({|} x (e. x S)))))
minel # <summary> If any number satisfies a predicate, the minimum does </summary>
(rwff x ph) , (-> (= x (min ({|} x ph))) (<-> ph ps))(-> (E. x ph) ps)
minsn2 # <summary> # Combines <a href="minsn">minsn</a> and <a href="snid">snid</a> into the form # <a href="minun">minun</a> expects. # </summary>
(/\ (= A (min ({} A))) (e. A ({} A)))
(-> (e. A S) (<= (min S) A))
BiReplaceImp1Imp0 # <title> Substitution </title> # <table> # (-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (-> [ [ [ ch ] th)) # </table>
(-> ph (-> ps th)) , (<-> ps ch)(-> ph (-> ch th))
EqReplaceImp1Eq0 # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (= A C)) , (= A B)(-> ph (= B C))
minun # <title> Minimum of a Union </title>
(-> (/\ (e. (min S) S) (<= (min S) (min T))) (= (min S) (min (u. S T))))
EqReplaceImp0An0El0 # <title> Substitution </title> # <table> # (-> (/\ (e. [ A ] ] ] S) ph) ps) # (= [ A ] [ B ] ) # (-> (/\ (e. [ [ [ B ] S) ph) ps) # </table>
(-> (/\ (e. A S) ph) ps) , (= A B)(-> (/\ (e. B S) ph) ps)
EqReplaceImp0An1Le0 # <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)
(/\ (= A (min S)) (e. A S)) , (<= A (min T))(/\ (= A (min (u. S T))) (e. A (u. S T)))
modval # <summary> Main theorem giving mod its value </summary>
(-> (/\ (< C B) (E. y (= (+ (* B y) C) A))) (= C (mod A B)))
modvali # <title> Modulo Value </title>
(< C B) , (= (+ (* B D) C) A)(= (mod A B) C)
modid Identity law for modulo
(-> (< A B) (= (mod A B) A))
df-div-just # <context> # This theorem is part of a series of theorems that describe the properties # of whole number division. It is assumed that every number in this theorem # is a natural number. Whole number division gives the result of normal division # without the remainder. # </context> Definition of division using set minimum instead of iota
(= (min ({|} x (= (+ (* B x) (mod A B)) A))) (min ({|} y (= (+ (* B y) (mod A B)) A))))
(= (div A B) (min ({|} x (= (+ (* B x) (mod A B)) A))))
diveq1 # <title> Equivalence for div </title> ##
(-> (= A C) (= (div A B) (div C B)))
(-> (= B C) (= (div A B) (div A C)))
(-> (/\ (= A B) (= C D)) (= (div A C) (div B D)))
diveq1i # <title> Divide both sides of an equation </title> # <table> # (= [ A ] [ C ) # (= (div [ A B) ] (div [ C B)) # </table>
(= A C)(= (div A B) (div C B))
(-> ph (= A C))(-> ph (= (div A B) (div C B)))
(= A B)(= (div C A) (div C B))
(-> ph (= A B))(-> ph (= (div C A) (div C B)))
modex # <context> # This theorem is part of a series of theorems that describe the properties # of set minumum, modulo, and whole number division. It is assumed that every number in this theorem # is a natural number. # </context> number 108.0
(E. y (= (+ (* B y) (mod A B)) A))
modle1 number 107.0
(<= (mod A B) A)
div # <summary> Main theorem about division </summary>
(= (+ (* B (div A B)) (mod A B)) A)
modmin number 109.0
(-> (E. x (= (+ (* A x) B) C)) (<= (mod C A) B))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
modlt2 number 110.0
(< (mod A (+ B (1))) (+ B (1)))
dividesmod # <title> Divides and modulo equivalence </title> # <summary> Divides relation is equivalent to zero remainder </summary>
(<-> (| A B) (= (mod B A) (0)))
BiReplaceImp0Not0 # <title> Substitution </title> # <table> # (-> (-. [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (-> (-. [ [ [ ps ] ) ch) # </table>
(-> (-. ph) ch) , (<-> ph ps)(-> (-. ps) ch)
(-> (< (0) B) (= (div (* B A) B) A))
muldivi # <title> Cancel multiplication for numbers above 0 </title> # <table> # (> <r> A (0)) # (= (div (* <r> A B) <r> A) B) # </table>
(> A (0))(= (div (* A B) A) B)
df-even # <context> # This theorem is part of a series of theorems that describe the properties # of even and odd numbers. # </context> # <title> Even Number Definition </title> # <summary> # An even number is divisible by 2. # </summary> # <suggest> right('Define', 'Ev') left('Simplify', 'Ev') </suggest>
(<-> (even A) (| (2) A))
(-> (= A B) (<-> (even A) (even B)))
(= A B)(<-> (even A) (even B))
(-> ph (= A B))(-> ph (<-> (even A) (even B)))
df-odd # <title> Odd Number Definition </title> # <summary> # An odd number is not divisible by 2. # </summary> # <suggest> right('Define', 'Odd') left('Simplify', 'Odd') </suggest>
(<-> (odd A) (-. (| (2) A)))
oddNotEven # <title> An Odd Number is Not Even </title>
(<-> (-. (even A)) (odd A))
evenNotOdd # <title> An Odd Number is Not Even </title>
(<-> (-. (odd A)) (even A))
0inequalities # <context> # This theorem is part of a series of theorems that describe the properties # of set minumum, modulo, and whole number division. It is assumed that every number in this theorem # is a natural number. # </context> # <title> All nonzero natural numbers are positive </title> # <suggest> right('Equivalence', '<') </suggest>
(<-> (-. (= (0) A)) (< (0) A))
BiReplaceBi0Not0 # <title> Substitution </title> # <table> # (<-> (-. [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (<-> (-. [ [ [ ps ] ) ch) # </table>
(<-> (-. ph) ch) , (<-> ph ps)(<-> (-. ps) ch)
0inequalities2 # <title> All nonzero natural numbers are positive </title> # <suggest> right('Equivalence', '<') </suggest>
(<-> (-. (= A (0))) (> A (0)))
EqReplaceBi1Le0 # <title> Substitution </title> # <table> # (<-> ph (<= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (<= [ [ [ B ] C)) # </table>
(<-> ph (<= A C)) , (= A B)(<-> ph (<= B C))
EqReplaceBi1Lt0 # <title> Substitution </title> # <table> # (<-> ph (< [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (< [ [ [ B ] C)) # </table>
(<-> ph (< A C)) , (= A B)(<-> ph (< B C))
EqReplaceBi1Lt1 # <title> Substitution </title> # <table> # (<-> ph (< A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (< A [ [ [ C ] )) # </table>
(<-> ph (< A B)) , (= B C)(<-> ph (< A C))
EqReplaceImp1Divs1 # <title> Substitution </title> # <table> # (-> ph (| A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (| A [ [ [ C ] )) # </table>
(-> ph (| A B)) , (= B C)(-> ph (| A C))
EqReplaceBi1Le0Add1 # <title> Substitution </title> # <table> # (<-> ph (<= (+ A [ B ] ] ] ) D)) # (= [ B ] [ C ] ) # (<-> ph (<= (+ A [ [ [ C ] ) D)) # </table>
(<-> ph (<= (+ A B) D)) , (= B C)(<-> ph (<= (+ A C) D))
BiReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (<-> ps ch)(-> ph (E. x ch))
BiReplaceImp1Ex1An0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x (/\ [ [ [ ch ] th))) # </table>
(-> ph (E. x (/\ ps th))) , (<-> ps ch)(-> ph (E. x (/\ ch th)))
EqReplaceImp1Ex1An0Le0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ (<= [ A ] ] ] C) ps))) # (= [ A ] [ B ] ) # (-> ph (E. x (/\ (<= [ [ [ B ] C) ps))) # </table>
(-> ph (E. x (/\ (<= A C) ps))) , (= A B)(-> ph (E. x (/\ (<= B C) ps)))
BiReplaceEx1Imp1 # <title> Substitution </title> # <table> # (E. x (-> ph [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (E. x (-> ph [ [ [ ch ] )) # </table>
(E. x (-> ph ps)) , (<-> ps ch)(E. x (-> ph ch))
ImpReplaceImp1An0 # <title> Substitution </title> # <table> # (-> ph (/\ [ ps ] ] ] th)) # (-> [ ps ] [ ch ] ) # (-> ph (/\ [ [ [ ch ] th)) # </table>
(-> ph (/\ ps th)) , (-> ps ch)(-> ph (/\ ch th))
EqReplaceImp1Lt0 # <title> Substitution </title> # <table> # (-> ph (< [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (< [ [ [ B ] C)) # </table>
(-> ph (< A C)) , (= A B)(-> ph (< B C))
EqReplaceImp1Lt1 # <title> Substitution </title> # <table> # (-> ph (< A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (< A [ [ [ C ] )) # </table>
(-> ph (< A B)) , (= B C)(-> ph (< A C))
(-> (< (0) B) (< (mod A B) B))
notDivides2 # <title> A non-multiple occurs between two multiples </title>
(-> (/\ (-. (| A B)) (> A (0))) (E. x (/\ (< (* A x) B) (< B (* A (+ x (1)))))))
notDivides3 # <title> A non-multiple occurs between two multiples </title>
(-> (> A (0)) (<-> (-. (| A B)) (E. x (/\ (< (* A x) B) (< B (* A (+ x (1))))))))
BiReplaceBi1Ex1 # <title> Substitution </title> # <table> # (<-> ph (E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (E. x [ [ [ ch ] )) # </table>
(<-> ph (E. x ps)) , (<-> ps ch)(<-> ph (E. x ch))
BiReplaceBi1Ex1An1 # <title> Substitution </title> # <table> # (<-> ph (E. x (/\ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (E. x (/\ ps [ [ [ th ] ))) # </table>
(<-> ph (E. x (/\ ps ch))) , (<-> ch th)(<-> ph (E. x (/\ ps th)))
EqReplaceBi1Ex1An1Lt1 # <title> Substitution </title> # <table> # (<-> ph (E. x (/\ ps (< A [ B ] ] ] )))) # (= [ B ] [ C ] ) # (<-> ph (E. x (/\ ps (< A [ [ [ C ] )))) # </table>
(<-> ph (E. x (/\ ps (< A B)))) , (= B C)(<-> ph (E. x (/\ ps (< A C))))
BiReplaceBi1Ex1An0 # <title> Substitution </title> # <table> # (<-> ph (E. x (/\ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (<-> ph (E. x (/\ [ [ [ ch ] th))) # </table>
(<-> ph (E. x (/\ ps th))) , (<-> ps ch)(<-> ph (E. x (/\ ch th)))
GtReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (> [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (> B C)(> A C)
2greater0 # <title> One-Digit Inequality </title>
(> (2) (0))
EqReplaceBi1Le1 # <title> Substitution </title> # <table> # (<-> ph (<= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (<= A [ [ [ C ] )) # </table>
(<-> ph (<= A B)) , (= B C)(<-> ph (<= A C))
oddex # <context> # This theorem is part of a series of theorems that describe the properties # of even and odd numbers. It is assumed that every number in this theorem # is a natural number. # </context> # <title> Alternative Odd Number Definition </title>
(<-> (odd A) (E. x (= (+ (* (2) x) (1)) A)))
evensuccessor # <title> Odd Numbers Are Above Even Numbers </title>
(<-> (even A) (odd (+ A (1))))
EqReplaceBi1Ex1Eq0 # <title> Substitution </title> # <table> # (<-> ph (E. x (= [ A ] ] ] C))) # (= [ A ] [ B ] ) # (<-> ph (E. x (= [ [ [ B ] C))) # </table>
(<-> ph (E. x (= A C))) , (= A B)(<-> ph (E. x (= B C)))
EqReplaceBi1Ex1Eq0Add1 # <title> Substitution </title> # <table> # (<-> ph (E. x (= (+ A [ B ] ] ] ) D))) # (= [ B ] [ C ] ) # (<-> ph (E. x (= (+ A [ [ [ C ] ) D))) # </table>
(<-> ph (E. x (= (+ A B) D))) , (= B C)(<-> ph (E. x (= (+ A C) D)))
oddsuccessor # <title> Even Numbers Are Above Odd Numbers </title>
(<-> (odd A) (even (+ A (1))))
consecutiveEven # <title> One of two consecutive numbers is even </title> # <summary> # For two consecutive numbers, one of the numbers is even. # <a href="consecutiveOdd">consecutiveOdd</a> shows that one # of them is odd. # </summary>
(\/ (even A) (even (+ A (1))))
consecutiveOdd # <title> One of two consecutive numbers is odd </title> # <summary> # For two consecutive numbers, one of the numbers is odd. # <a href="consecutiveEven">consecutiveEven</a> shows that one # of them is even. # </summary>
(\/ (odd A) (odd (+ A (1))))
evenmul # <title> Any multiple of an even number is even </title>
(-> (even A) (even (* A B)))
EqReplaceEq1Add0 # <title> Substitution </title> # <table> # (= A (+ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (+ [ [ [ C ] D)) # </table>
(= A (+ B D)) , (= B C)(= A (+ C D))
ImpReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (-> ps ch)(-> ph (E. x ch))
EqReplaceEq1Add1Add1 # <title> Substitution </title> # <table> # (= A (+ B (+ C [ D ] ] ] ))) # (= [ D ] [ A' ] ) # (= A (+ B (+ C [ [ [ A' ] ))) # </table>
(= A (+ B (+ C D))) , (= D A')(= A (+ B (+ C A')))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
ImpReplaceImp1Ex1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y [ ps ] ] ] ))) # (-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y [ [ [ ch ] ))) # </table>
(-> ph (E. x (E. y ps))) , (-> ps ch)(-> ph (E. x (E. y ch)))
EqReplaceEq1Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ B [ C ] ] ] ) A')) # (= [ C ] [ D ] ) # (= A (+ (+ B [ [ [ D ] ) A')) # </table>
(= A (+ (+ B C) A')) , (= C D)(= A (+ (+ B D) A'))
EqReplaceEq1Add1Add0 # <title> Substitution </title> # <table> # (= A (+ B (+ [ C ] ] ] A'))) # (= [ C ] [ D ] ) # (= A (+ B (+ [ [ [ D ] A'))) # </table>
(= A (+ B (+ C A'))) , (= C D)(= A (+ B (+ D A')))
BiReplaceImp1Ex1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y [ ps ] ] ] ))) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y [ [ [ ch ] ))) # </table>
(-> ph (E. x (E. y ps))) , (<-> ps ch)(-> ph (E. x (E. y ch)))
EqReplaceImp1Ex1Ex1Eq0 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (= [ A ] ] ] C)))) # (= [ A ] [ B ] ) # (-> ph (E. x (E. y (= [ [ [ B ] C)))) # </table>
(-> ph (E. x (E. y (= A C)))) , (= A B)(-> ph (E. x (E. y (= B C))))
EqReplaceEq1Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (+ (+ [ [ [ C ] D) A')) # </table>
(= A (+ (+ B D) A')) , (= B C)(= A (+ (+ C D) A'))
ImpReplaceImp1Ex1Ex1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (E. z [ ps ] ] ] )))) # (-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y (E. z [ [ [ ch ] )))) # </table>
(-> ph (E. x (E. y (E. z ps)))) , (-> ps ch)(-> ph (E. x (E. y (E. z ch))))
oddmul # <title> The product of odd numbers is odd </title>
(-> (/\ (odd A) (odd B)) (odd (* A B)))
BiReplaceImp1Or1 # <title> Substitution </title> # <table> # (-> ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (\/ ps [ [ [ th ] )) # </table>
(-> ph (\/ ps ch)) , (<-> ch th)(-> ph (\/ ps th))
EqReplaceImp1Even0 # <title> Substitution </title> # <table> # (-> ph (even [ A ] ] ] )) # (= [ A ] [ B ] ) # (-> ph (even [ [ [ B ] )) # </table>
(-> ph (even A)) , (= A B)(-> ph (even B))
BiReplaceImp1Or0 # <title> Substitution </title> # <table> # (-> ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (\/ [ [ [ ch ] th)) # </table>
(-> ph (\/ ps th)) , (<-> ps ch)(-> ph (\/ ch th))
evenmul2 # <title> Multiplication of Even Numbers </title>
(<-> (even (* A B)) (\/ (even A) (even B)))
evenxxplus1 # <title> Product of consecutive numbers is even </title>
(even (* A (+ A (1))))
div2xxplus1 # <title> Product of consecutive numbers is even </title>
(| (2) (* A (+ A (1))))
df-modcon # <context> # This theorem is part of a series of theorems that describe the properties # of modulo congruence. It is assumed that every number in this theorem # is a natural number. # </context> # <title> Modulo Congruence Definition </title> # <summary> # Two numbers A and B are congruent modulo C if there values # mod C are equal. # </summary>
(<-> (=mod A B C) (= (mod A C) (mod B C)))
(-> (= A D) (<-> (=mod A B C) (=mod D B C)))
(-> (= A D) (<-> (=mod B A C) (=mod B D C)))
(-> (= A B) (<-> (=mod C D A) (=mod C D B)))
(= A D)(<-> (=mod A B C) (=mod D B C))
(-> ph (= A D))(-> ph (<-> (=mod A B C) (=mod D B C)))
(= A D)(<-> (=mod B A C) (=mod B D C))
(-> ph (= A D))(-> ph (<-> (=mod B A C) (=mod B D C)))
(= A B)(<-> (=mod C D A) (=mod C D B))
modconeq12 # <title> Equivalence for =mod </title> ##
(-> (/\ (= A B) (= C D)) (<-> (=mod A C A') (=mod B D A')))
(-> (/\ (= A A') (= C C')) (<-> (=mod A B C) (=mod A' B C')))
(-> (/\ (= A A') (= C C')) (<-> (=mod B A C) (=mod B A' C')))
(-> ph (= A B))(-> ph (<-> (=mod C D A) (=mod C D B)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (<-> (=mod A C A') (=mod B D A')))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (<-> (=mod A A' C) (=mod B A' D)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (<-> (=mod A' A C) (=mod A' B D)))
modconid # <title> Reflexive Property </title>
(=mod A A C)
modconcom # <title> Symmetric Property </title> # <suggest> right('Commute', '=') </suggest>
(<-> (=mod A B C) (=mod B A C))
eqmodcon # <title> Equality Implies Modular Congruence </title>
(-> (= B C) (=mod B C A))
modcontr # <title> Transitive Property </title>
(-> (/\ (=mod A B D) (=mod A C D)) (=mod B C D))
EqReplaceBi1Eq0 # <title> Substitution </title> # <table> # (<-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (= [ [ [ B ] C)) # </table>
(<-> ph (= A C)) , (= A B)(<-> ph (= B C))
EqReplaceBi1Eq1 # <title> Substitution </title> # <table> # (<-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (= A [ [ [ C ] )) # </table>
(<-> ph (= A B)) , (= B C)(<-> ph (= A C))
(<-> (=mod A B (0)) (= A B))
(-> (= C (mod B A)) (E. x (= (+ (* A x) C) B)))
EqReplaceImp1Eq0Add0 # <title> Substitution </title> # <table> # (-> ph (= (+ [ A ] ] ] C) D)) # (= [ A ] [ B ] ) # (-> ph (= (+ [ [ [ B ] C) D)) # </table>
(-> ph (= (+ A C) D)) , (= A B)(-> ph (= (+ B C) D))
(-> (/\ (< A C) (= A (mod B C))) (= A (mod (+ B (* C D)) C)))
ImpReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (-> ch th)(-> ph (-> ps th))
ImpReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (-> ch th)(-> ph (-> ps th))
addmodcon # <title> Add any multiple of the modulus </title>
(-> (< (0) B) (=mod C (+ C (* B D)) B))
addmodcon1 # <title> Add any multiple of the modulus </title>
(=mod C (+ C (* B D)) B)
EqReplaceImp1Modcon1 # <title> Substitution </title> # <table> # (-> ph (=mod A [ B ] ] ] D)) # (= [ B ] [ C ] ) # (-> ph (=mod A [ [ [ C ] D)) # </table>
(-> ph (=mod A B D)) , (= B C)(-> ph (=mod A C D))
(=mod A (+ (* B C) A) B)
(-> (= (+ (* A x) B) (+ (* A y) C)) (=mod C B A))
(-> (E. y (E. x (= (+ (* A x) B) (+ (* A y) C)))) (=mod C B A))
EqReplaceImp1Ex1Eq0 # <title> Substitution </title> # <table> # (-> ph (E. x (= [ A ] ] ] C))) # (= [ A ] [ B ] ) # (-> ph (E. x (= [ [ [ B ] C))) # </table>
(-> ph (E. x (= A C))) , (= A B)(-> ph (E. x (= B C)))
BiReplaceImp1Imp1Ex1 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps (E. x [ [ [ th ] ))) # </table>
(-> ph (-> ps (E. x ch))) , (<-> ch th)(-> ph (-> ps (E. x th)))
EqReplaceImp1Ex1Eq0Add1 # <title> Substitution </title> # <table> # (-> ph (E. x (= (+ A [ B ] ] ] ) D))) # (= [ B ] [ C ] ) # (-> ph (E. x (= (+ A [ [ [ C ] ) D))) # </table>
(-> ph (E. x (= (+ A B) D))) , (= B C)(-> ph (E. x (= (+ A C) D)))
BiReplaceImp1Imp1Ex1Ex1 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x (E. y [ ch ] ] ] )))) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps (E. x (E. y [ [ [ th ] )))) # </table>
(-> ph (-> ps (E. x (E. y ch)))) , (<-> ch th)(-> ph (-> ps (E. x (E. y th))))
EqReplaceImp1Imp1Ex1Ex1Eq1 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x (E. y (= A [ B ] ] ] ))))) # (= [ B ] [ C ] ) # (-> ph (-> ps (E. x (E. y (= A [ [ [ C ] ))))) # </table>
(-> ph (-> ps (E. x (E. y (= A B))))) , (= B C)(-> ph (-> ps (E. x (E. y (= A C)))))
EqReplaceImp1Ex1Ex1Eq1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (= A [ B ] ] ] )))) # (= [ B ] [ C ] ) # (-> ph (E. x (E. y (= A [ [ [ C ] )))) # </table>
(-> ph (E. x (E. y (= A B)))) , (= B C)(-> ph (E. x (E. y (= A C))))
BiReplaceBi0Ex1 # <title> Substitution </title> # <table> # (<-> (E. x [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (<-> (E. x [ [ [ ps ] ) ch) # </table>
(<-> (E. x ph) ch) , (<-> ph ps)(<-> (E. x ps) ch)
BiReplaceBi0Ex1Ex1 # <title> Substitution </title> # <table> # (<-> (E. x (E. y [ ph ] ] ] )) ch) # (<-> [ ph ] [ ps ] ) # (<-> (E. x (E. y [ [ [ ps ] )) ch) # </table>
(<-> (E. x (E. y ph)) ch) , (<-> ph ps)(<-> (E. x (E. y ps)) ch)
modconex # <title> Modulus Congruence using Existence </title>
(<-> (E. x (E. y (= (+ (* A x) B) (+ (* A y) C)))) (=mod B C A))
ImpReplaceImp1Ex1Ex1Ex1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (E. z (E. v [ ps ] ] ] ))))) # (-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y (E. z (E. v [ [ [ ch ] ))))) # </table>
(-> ph (E. x (E. y (E. z (E. v ps))))) , (-> ps ch)(-> ph (E. x (E. y (E. z (E. v ch)))))
BiReplaceImp1Ex1Ex1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (E. z [ ps ] ] ] )))) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y (E. z [ [ [ ch ] )))) # </table>
(-> ph (E. x (E. y (E. z ps)))) , (<-> ps ch)(-> ph (E. x (E. y (E. z ch))))
BiReplaceImp1Ex1Ex1Ex1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (E. z (E. v [ ps ] ] ] ))))) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y (E. z (E. v [ [ [ ch ] ))))) # </table>
(-> ph (E. x (E. y (E. z (E. v ps))))) , (<-> ps ch)(-> ph (E. x (E. y (E. z (E. v ch)))))
ImpReplaceImp1Ex1Ex1Ex1Ex1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (E. z (E. v (E. w' [ ps ] ] ] )))))) # (-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y (E. z (E. v (E. w' [ [ [ ch ] )))))) # </table>
(-> ph (E. x (E. y (E. z (E. v (E. w' ps)))))) , (-> ps ch)(-> ph (E. x (E. y (E. z (E. v (E. w' ch))))))
modaddeq12 # <title> Add congruent numbers </title>
(-> (/\ (=mod A B j) (=mod C D j)) (=mod (+ A C) (+ B D) j))
EqReplaceEq1Add1Add0Mul0 # <title> Substitution </title> # <table> # (= A (+ B (+ (* [ C ] ] ] A') B'))) # (= [ C ] [ D ] ) # (= A (+ B (+ (* [ [ [ D ] A') B'))) # </table>
(= A (+ B (+ (* C A') B'))) , (= C D)(= A (+ B (+ (* D A') B')))
modmuleq12 # <title> Multiply congruent numbers </title>
(-> (/\ (=mod A B j) (=mod C D j)) (=mod (* A C) (* B D) j))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)