List of theorems

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

negeqi # <context> # This theorem is part of a series of proofs related to the introduction of # <a href="/wiki/peano/arithmetic/negative-sign">negative numbers</a>. These # theorems apply to integers, rational numbers, and real numbers. # </context>
(= A B)(= (-n A) (-n B))
(-> ph (= A B))(-> ph (= (-n A) (-n 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))
EqReplaceImp1Eq1Add1 # <title> Substitution </title> # <table> # (-> ph (= A (+ B [ C ] ] ] ))) # (= [ C ] [ D ] ) # (-> ph (= A (+ B [ [ [ D ] ))) # </table>
(-> ph (= A (+ B C))) , (= C D)(-> ph (= A (+ B D)))
(<-> (= A B) (= (-n A) (-n B)))
doubleneg # <title> Double Negative </title> # <suggest> right('Simplify', '-') </suggest>
(= (-n (-n A)) A)
EqReplaceBi1Eq1 # <title> Substitution </title> # <table> # (<-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (= A [ [ [ C ] )) # </table>
(<-> ph (= A B)) , (= B C)(<-> ph (= A C))
negeq3 # <title> Negative can switch sides </title> # <suggest> right('Equivalence', '-') left('Equivalence', '-') </suggest>
(<-> (= A (-n B)) (= (-n A) B))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
neg0 # <title> Negative of 0 is 0 </title>
(= (-n (0)) (0))
negcan2 # <title> Cancel using subtraction </title> # <suggest> right('Simplify','0') </suggest>
(= (+ (-n A) A) (0))
df-minus # <title> Definition of Subtraction </title> # <summary> # This is the binary subtraction operation, not to be confused with the # unary <a href="df-neg">negative sign</a> which is used in the definition. # </summary> # <suggest> right('Define', '-') left('Simplify', '-') </suggest>
(= (- A B) (+ A (-n B)))
df-minusr # <title> Minus Definition Reversed </title>
(= (+ A (-n B)) (- A B))
minuseq1 # <title> Equivalence for - </title> ##
(-> (= A C) (= (- A B) (- C B)))
(= A C)(= (- A B) (- C B))
minuseq2 # <title> Equivalence for - </title> ##
(-> (= B C) (= (- A B) (- A C)))
(-> ph (= A C))(-> ph (= (- A B) (- C B)))
(= B C)(= (- A B) (- A C))
(-> ph (= B C))(-> ph (= (- A B) (- A C)))
(-> (/\ (= A B) (= C D)) (= (- A C) (- B D)))
minuseq12i # <title> Equality over Subtraction </title> # <table> # (= A ] ] ] [ B ] ] ) # (= [ [ C ] [ [ [ D) # (= (- A ] [ C ] ) (- [ B ] [ D)) # </table>
(= A B) , (= C D)(= (- A C) (- B D))
minuseq12d # <title> Equality over Subtraction </title>
(-> ph (= A B)) , (-> ph (= C D))(-> ph (= (- A C) (- B D)))
minuscan # <title> Cancel using subtraction </title> # <suggest> right('Simplify','-') </suggest>
(= (- A A) (0))
minuscan2 # <title> Addition is the inverse of Subtraction </title> # <suggest> right('Simplify','-') </suggest>
(= (+ (- A B) B) A)
addcanr # <title> Addition is the inverse of Subtraction </title> # <suggest> right('Simplify','-') </suggest>
(= (- (+ A B) B) A)
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
minusneg # <title> Negative and Subtraction Cancel </title> # <suggest> right('Simplify', '-') </suggest>
(= (- A (-n B)) (+ A B))
minusid # <title> Subtraction Identity </title> # <suggest> right('Simplify', '0') </suggest>
(= (- A (0)) A)
negmul # <title> Negative Multiplication </title> # <suggest> right('Simplify', '-') </suggest>
(= (* (-n A) B) (-n (* A B)))
EqReplaceEq1Neg0 # <title> Substitution </title> # <table> # (= A (-n [ B ] ] ] )) # (= [ B ] [ C ] ) # (= A (-n [ [ [ C ] )) # </table>
(= A (-n B)) , (= B C)(= A (-n C))
negmul2 # <title> Negative Multiplication </title> # <suggest> right('Simplify', '-') </suggest>
(= (* A (-n B)) (-n (* A B)))
mulneg1 # <title> Multiply by Negative 1 </title>
(= (* (-n (1)) A) (-n A))
doublenegmul # <title> Multiply Two Negative Numbers </title> # <suggest> right('Simplify', '-') </suggest>
(= (* (-n A) (-n B)) (* A B))
EqReplaceEq0Mul1 # <title> Substitution </title> # <table> # (= (* A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (= (* A [ [ [ C ] ) D) # </table>
(= (* A B) D) , (= B C)(= (* A C) D)
minusdistr # <title> Distribute Multiplication over Subtraction </title> # <table> # (= (* <c> A (+ B C)) (+ (* <c> A B) (* <c> A C))) # </table> # <suggest> right('Distribute', 'R') left('Distribute', '-R') </suggest>
(= (* A (- B C)) (- (* A B) (* A C)))
EqReplaceEq0Mul0 # <title> Substitution </title> # <table> # (= (* [ A ] ] ] C) D) # (= [ A ] [ B ] ) # (= (* [ [ [ B ] C) D) # </table>
(= (* A C) D) , (= A B)(= (* B C) D)
minusdistl # <title> Distribute Multiplication over Subtraction </title> # <table> # (= (* (+ A B) <c> C) (+ (* A <c> C) (* B <c> C))) # </table> # <suggest> right('Distribute', 'L') left('Distribute', '-L') </suggest>
(= (* (- A B) C) (- (* A C) (* 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))
EqReplaceBi1Lt1Add0 # <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)))
EqReplaceBi1Lt1Add1 # <title> Substitution </title> # <table> # (<-> ph (< A (+ B [ C ] ] ] ))) # (= [ C ] [ D ] ) # (<-> ph (< A (+ B [ [ [ D ] ))) # </table>
(<-> ph (< A (+ B C))) , (= C D)(<-> ph (< A (+ B D)))
(<-> (< A B) (> (-n A) (-n B)))
EqReplaceBi1Gt1 # <title> Substitution </title> # <table> # (<-> ph (> A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (> A [ [ [ C ] )) # </table>
(<-> ph (> A B)) , (= B C)(<-> ph (> A C))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
EqReplaceImp1Gt0 # <title> Substitution </title> # <table> # (-> ph (> [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (> [ [ [ B ] C)) # </table>
(-> ph (> A C)) , (= A B)(-> ph (> B C))
negProduct # <title> Multiply Two Negative Numbers </title>
(-> (/\ (zneg A) (zneg B)) (pos (* A B)))
BiReplaceOr1Or1 # <title> Substitution </title> # <table> # (\/ ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (\/ ph (\/ ps [ [ [ th ] )) # </table>
(\/ ph (\/ ps ch)) , (<-> ch th)(\/ ph (\/ ps th))
0negpos # <title> A number is negative, positive or 0 </title>
(\/ (zneg A) (\/ (= A (0)) (pos A)))
negpos # <title> Nonzero numbers are negative or positive </title>
(-> (-. (= A (0))) (\/ (zneg A) (pos A)))
BiReplaceImp0Not0 # <title> Substitution </title> # <table> # (-> (-. [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (-> (-. [ [ [ ps ] ) ch) # </table>
(-> (-. ph) ch) , (<-> ph ps)(-> (-. ps) ch)
posCases # <title> Positive Proof by Cases </title>
(-> (/\ (-. (zneg A)) (-. (= A (0)))) (pos A))
negCases # <title> Negative Proof by Cases </title>
(-> (/\ (-. (pos A)) (-. (= A (0)))) (zneg A))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
negNotPos # <title> Negative numbers are not positive </title>
(-> (zneg A) (-. (pos A)))
posNotNeg # <title> Positive numbers are not negative </title>
(-> (pos A) (-. (zneg A)))
posSquares # <title> Squares are not negative </title>
(-> (-. (= A (0))) (pos (* A A)))
squareNotNeg # <title> Squares are not negative </title>
(>= (* A A) (0))
(-> (pos (* A B)) (-. (= B (0))))
EqReplaceImp1Lt1 # <title> Substitution </title> # <table> # (-> ph (< A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (< A [ [ [ C ] )) # </table>
(-> ph (< A B)) , (= B C)(-> ph (< A C))
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)
(-> (/\ (zneg A) (pos B)) (zneg (* A B)))
(-> (/\ (pos A) (zneg B)) (zneg (* A B)))
BiReplaceImp1Or1 # <title> Substitution </title> # <table> # (-> ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (\/ ps [ [ [ th ] )) # </table>
(-> ph (\/ ps ch)) , (<-> ch th)(-> ph (\/ ps th))
EqReplaceImp0Not0Zneg0 # <title> Substitution </title> # <table> # (-> (-. (zneg [ A ] ] ] )) ph) # (= [ A ] [ B ] ) # (-> (-. (zneg [ [ [ B ] )) ph) # </table>
(-> (-. (zneg A)) ph) , (= A B)(-> (-. (zneg B)) ph)
BiReplaceBi1Imp0 # <title> Substitution </title> # <table> # (<-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (-> [ [ [ ch ] th)) # </table>
(<-> ph (-> ps th)) , (<-> ps ch)(<-> ph (-> ch th))
ImpReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (-> ch th)(-> ph (-> ps th))
ImpReplaceImp1Or0 # <title> Substitution </title> # <table> # (-> ph (\/ [ ps ] ] ] th)) # (-> [ ps ] [ ch ] ) # (-> ph (\/ [ [ [ ch ] th)) # </table>
(-> ph (\/ ps th)) , (-> ps ch)(-> ph (\/ ch th))
ImpReplaceImp1Or1 # <title> Substitution </title> # <table> # (-> ph (\/ ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (\/ ps [ [ [ th ] )) # </table>
(-> ph (\/ ps ch)) , (-> ch th)(-> ph (\/ ps th))
ImpReplaceImp1Or1Or1 # <title> Substitution </title> # <table> # (-> ph (\/ ps (\/ ch [ th ] ] ] ))) # (-> [ th ] [ ta ] ) # (-> ph (\/ ps (\/ ch [ [ [ ta ] ))) # </table>
(-> ph (\/ ps (\/ ch th))) , (-> th ta)(-> ph (\/ ps (\/ ch ta)))
BiReplaceNot0An1 # <title> Substitution </title> # <table> # (-. (/\ ph [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-. (/\ ph [ [ [ ch ] )) # </table>
(-. (/\ ph ps)) , (<-> ps ch)(-. (/\ ph ch))
(<-> (pos (* A B)) (\/ (/\ (zneg A) (zneg B)) (/\ (pos A) (pos B))))
(-> (pos (* A B)) (<-> (pos A) (pos B)))
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
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)))
(-> (-. (pos A)) (\/ (zneg A) (= A (0))))
negPositive # <title> Negative of a positive number </title>
(<-> (pos (-n A)) (zneg A))
EqReplaceEq0Add1 # <title> Substitution </title> # <table> # (= (+ A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (= (+ A [ [ [ C ] ) D) # </table>
(= (+ A B) D) , (= B C)(= (+ A C) D)
EqReplaceEq0Add0 # <title> Substitution </title> # <table> # (= (+ [ A ] ] ] C) D) # (= [ A ] [ B ] ) # (= (+ [ [ [ B ] C) D) # </table>
(= (+ A C) D) , (= A B)(= (+ B C) D)
0minus # <title> Subtract from 0 </title> # <suggest> right('Simplify', '-') </suggest>
(= (- (0) A) (-n A))
negminus # <title> Negative of Subtraction </title> # <suggest> left('Simplify', '-') </suggest>
(= (- A B) (-n (- B A)))
EqReplaceNot0Eq0 # <title> Substitution </title> # <table> # (-. (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-. (= [ [ [ B ] C)) # </table>
(-. (= A C)) , (= A B)(-. (= B C))
EqReplaceNot0Eq1 # <title> Substitution </title> # <table> # (-. (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-. (= A [ [ [ C ] )) # </table>
(-. (= A B)) , (= B C)(-. (= A C))
neg1ne0 # <title> Negative 1 is not 0 </title>
(-. (= (-n (1)) (0)))
EqReplaceBi1Eq0 # <title> Substitution </title> # <table> # (<-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (= [ [ [ B ] C)) # </table>
(<-> ph (= A C)) , (= A B)(<-> ph (= B C))
BiReplaceBi0Not0 # <title> Substitution </title> # <table> # (<-> (-. [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (<-> (-. [ [ [ ps ] ) ch) # </table>
(<-> (-. ph) ch) , (<-> ph ps)(<-> (-. ps) ch)
negne0 # <title> Negative 1 is not 0 </title>
(<-> (-. (= A (0))) (-. (= (-n A) (0))))
negadd # <title> Negative distributes over addition </title>
(= (- (-n A) B) (-n (+ A B)))
(= (+ (-n A) B) (-n (- A B)))
(= (- (-n A) B) (-n (+ A B)))
EqReplaceImp1Eq0Add1 # <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))
minusValue # <title> Subtraction Value from Addition </title>
(-> (= (+ A B) C) (= A (- C B)))
minusValuei # <title> Subtraction Value from Addition </title> # <table> # (= (+ A <c> B) C) # (= A (- C <c> B ) ) # </table>
(= (+ A B) C)(= A (- C B))
minusValue2i # <title> Subtraction from both sides </title> # <table> # (= (+ A <c> B ) [ C) # (= A (- <c> (-n B ) [ C) ) # </table>
(= (+ A B) C)(= A (+ (-n B) C))
minusValue3i # <title> Subtraction Value from Addition </title> # <table> # (= (+ A B) C) # (= (- C B ) A ) # </table>
(= (+ A B) C)(= (- C B) A)
EqReplaceBi1Gt0 # <title> Substitution </title> # <table> # (<-> ph (> [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (> [ [ [ B ] C)) # </table>
(<-> ph (> A C)) , (= A B)(<-> ph (> B C))
subtractPositive # <title> Positive Number Subtraction </title> # <summary> A number decreases when a positive number is subtracted from it. </summary>
(<-> (> B (0)) (< (- A B) A))
gtdiff # <title> Add or subtract on both sides </title>
(<-> (> A B) (> (- A B) (0)))
EqReplaceBi1Ge1 # <title> Substitution </title> # <table> # (<-> ph (>= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (>= A [ [ [ C ] )) # </table>
(<-> ph (>= A B)) , (= B C)(<-> ph (>= A C))
EqReplaceBi1Ge0 # <title> Substitution </title> # <table> # (<-> ph (>= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (>= [ [ [ B ] C)) # </table>
(<-> ph (>= A C)) , (= A B)(<-> ph (>= B C))
gediff # <title> Add or subtract on both sides </title>
(<-> (>= A B) (>= (- A B) (0)))
(<-> (> (-n A) (0)) (< A (0)))
(<-> (>= (-n A) (0)) (<= A (0)))
EqReplaceBi0Gt0 # <title> Substitution </title> # <table> # (<-> (> [ A ] ] ] C) ph) # (= [ A ] [ B ] ) # (<-> (> [ [ [ B ] C) ph) # </table>
(<-> (> A C) ph) , (= A B)(<-> (> B C) ph)
(<-> (< (-n A) (0)) (> A (0)))
EqReplaceBi0Ge0 # <title> Substitution </title> # <table> # (<-> (>= [ A ] ] ] C) ph) # (= [ A ] [ B ] ) # (<-> (>= [ [ [ B ] C) ph) # </table>
(<-> (>= A C) ph) , (= A B)(<-> (>= B C) ph)
(<-> (>= A (0)) (<= (-n A) (0)))
df-abs # <title> Definition of Absolute Value </title> # <suggest> right('Define', '|x|') left('Simplify', '|x|') </suggest>
(= (abs A) (ifn (>= A (0)) A (-n A)))
abseq # <title> Equivalence for abs </title> ##
(-> (= A B) (= (abs A) (abs B)))
(= A B)(= (abs A) (abs B))
(-> ph (= A B))(-> ph (= (abs A) (abs B)))
dfabs1 # <title> Def. Absolute Value for Positive Numbers </title>
(-> (>= A (0)) (= (abs A) A))
dfabs2 # <title> Def. Absolute Value for Negative Numbers </title>
(-> (< A (0)) (= (abs A) (-n A)))
ImpReplaceImp1An0 # <title> Substitution </title> # <table> # (-> ph (/\ [ ps ] ] ] th)) # (-> [ ps ] [ ch ] ) # (-> ph (/\ [ [ [ ch ] th)) # </table>
(-> ph (/\ ps th)) , (-> ps ch)(-> ph (/\ ch th))
BiReplaceImp1An1 # <title> Substitution </title> # <table> # (-> ph (/\ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (/\ ps [ [ [ th ] )) # </table>
(-> ph (/\ ps ch)) , (<-> ch th)(-> ph (/\ ps th))
absNotNeg # <title> The absolute value is not negative </title>
(>= (abs A) (0))
absidm # <title> The absolute value is idempotent </title>
(= (abs (abs A)) (abs A))
absPosDef # <title> The absolute value is positive definite </title>
(<-> (= A (0)) (= (abs A) (0)))
BiReplaceImp1Bi0 # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
BiReplaceImp1Bi0Not0 # <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))
ImpReplaceImp1An1 # <title> Substitution </title> # <table> # (-> ph (/\ ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (/\ ps [ [ [ th ] )) # </table>
(-> ph (/\ ps ch)) , (-> ch th)(-> ph (/\ ps th))
absTwoValues.1 # <title> Two numbers have the same absolute value </title>
(-> (/\ (\/ (= A (-n B)) (= A B)) (>= B (0))) (= (abs A) B))
(-> (= (abs A) B) (>= B (0)))
BiReplaceImp0An0Or0 # <title> Substitution </title> # <table> # (-> (/\ (\/ [ ph ] ] ] ch) th) ta) # (<-> [ ph ] [ ps ] ) # (-> (/\ (\/ [ [ [ ps ] ch) th) ta) # </table>
(-> (/\ (\/ ph ch) th) ta) , (<-> ph ps)(-> (/\ (\/ ps ch) th) ta)
absTwoValues # <title> Two numbers have the same absolute value </title>
(<-> (= (abs A) B) (/\ (\/ (= A B) (= (-n A) B)) (>= B (0))))
BiReplaceImp1Or0 # <title> Substitution </title> # <table> # (-> ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (\/ [ [ [ ch ] th)) # </table>
(-> ph (\/ ps th)) , (<-> ps ch)(-> ph (\/ ch th))
(\/ (= (abs A) A) (= (abs A) (-n A)))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)