SUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUP [SystemQ lemma RemoveOr: ΠA: A ˙∨ A ⊢ A] SystemQ proof of RemoveOr:

L01: Arbitrary ≫  A  ;
L02: Premise ≫  A ˙∨ A  ;
L03: Repetition ⊳ L02 ≫  ˙¬ (A)n ⇒ A  ;
L04: AutoImply ≫  A ⇒ A  ;
L05: FromNegations ⊳ L04 ⊳ L03 ≫ A  □

[SystemQ lemma leqTransitivity: ΠX , Y, Z: X <= Y ⊢ Y <= Z ⊢ X <= Z]

SystemQ proof of leqTransitivity:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X <= Y  ;
L03: Premise ≫  Y <= Z  ;
L04: leqTransitivityAxiom ≫  {X <= Y ⇒ Y <= Z ⇒ X <= \atop Z  ;}
L05: MP2 ⊳ L04 ⊳ L02 ⊳ L03 ≫  X <= Z  □

[SystemQ lemma leqAntisymmetry: ΠX , Y: X <= Y ⊢ Y <= X ⊢ X = Y] SystemQ proof of leqAntisymmetry:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X <= Y  ;
L03: Premise ≫  Y <= X  ;
L04: leqAntisymmetryAxiom ≫  X <= Y ⇒ Y <= X ⇒ X = Y ;
L05: MP2 ⊳ L04 ⊳ L02 ⊳ L03 ≫ X = Y □

[SystemQ lemma leqAddition: ΠX , Y, Z: X <= Y ⊢ (X + Z) <= (Y + Z)] SystemQ proof of leqAddition:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X <= Y  ;
L03: leqAdditionAxiom ≫  X <= Y ⇒ (X +Z) <= (Y+Z) ;
L04: MP ⊳ L03 ⊳ L02 ≫ (X + Z) <= (Y + Z) □

[SystemQ lemma leqMultiplication: ΠX , Y, Z: 0 <= Z ⊢ X <= Y ⊢ (X ∗ Z) <= (Y ∗ Z)]

SystemQ proof of leqMultiplication:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  0 <= Z  ;
L03: Premise ≫  X <= Y  ;
L04: leqMultiplicationAxiom ≫  {0 <= Z ⇒ X <= Y ⇒ (X ∗ \atop Z) <= (Y ∗ Z)  ;}
L05: MP2 ⊳ L04 ⊳ L02 ⊳ L03 ≫  (X ∗ Z) <= (Y ∗ Z)  □

[SystemQ lemma Reciprocal: ΠX: X ≠ 0 ⊢ (X ∗ recX) = 1]

SystemQ proof of Reciprocal:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  X ≠ 0  ;
L03: ReciprocalAxiom ≫  X ≠ 0 ⇒ (X ∗ recX) = 1  ;
L04: MP ⊳ L03 ⊳ L02 ≫  (X ∗ recX) = 1  □

[SystemQ lemma eqLeq: ΠX , Y: X = Y ⊢ X <= Y]

SystemQ proof of eqLeq:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X = Y  ;
L03: EqLeqAxiom ≫  X = Y ⇒ X <= Y  ;
L04: MP ⊳ L03 ⊳ L02 ≫  X <= Y  □

[SystemQ lemma eqAddition: ΠX , Y, Z: X = Y ⊢ (X + Z) = (Y + Z)] SystemQ proof of eqAddition:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: EqAdditionAxiom ≫  X = Y ⇒ (X + Z) = (Y + Z) ;
L04: MP ⊳ L03 ⊳ L02 ≫ (X + Z) = (Y + Z) □

[SystemQ lemma eqMultiplication: ΠX , Y, Z: X = Y ⊢ (X ∗ Z) = (Y ∗ Z)] SystemQ proof of eqMultiplication:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: EqMultiplicationAxiom ≫  X = Y ⇒ (X ∗ Z) = (Y ∗ Z)  ;
L04: MP ⊳ L03 ⊳ L02 ≫  (X ∗ Z) = (Y ∗ Z)  □

[SystemQ lemma Equality: ΠX , Y, Z: X = Y ⊢ X = Z ⊢ Y = Z] SystemQ proof of Equality:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  X = Z  ;
L04: EqualityAxiom ≫  X = Y ⇒ X = Z ⇒ Y = Z  ;
L05: MP2 ⊳ L04 ⊳ L02 ⊳ L03 ≫  Y = Z  □

[SystemQ lemma eqReflexivity: ΠX: X = X]

SystemQ proof of eqReflexivity:

L01: Arbitrary ≫  X  ;
L02: leqReflexivity ≫  X <= X  ;
L03: leqAntisymmetry⊳L02⊳L02 ≫ X = X  □

[SystemQ lemma eqSymmetry: ΠX , Y: X = Y ⊢ Y = X]

SystemQ proof of eqSymmetry:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X = Y  ;
L03: eqReflexivity ≫  X = X  ;
L04: Equality ⊳ L02 ⊳ L03 ≫  Y = X  □

[SystemQ lemma eqTransitivity: ΠX , Y, Z: X = Y ⊢ Y = Z ⊢ X = Z] SystemQ proof of eqTransitivity:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Y = Z  ;
L04: eqSymmetry ⊳ L02 ≫  Y = X  ;
L05: Equality ⊳ L04 ⊳ L03 ≫  X = Z  □

[SystemQ lemma eqTransitivity4: ΠX , Y, Z, U: X = Y ⊢ Y = Z ⊢ Z = U ⊢ X = U]

SystemQ proof of eqTransitivity4:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Y = Z  ;
L04: Premise ≫  Z = U  ;
L05: eqTransitivity ⊳ L02 ⊳ L03 ≫ X = Z  ;
L06: eqTransitivity ⊳ L05 ⊳ L04 ≫ X = U  □

[SystemQ lemma eqTransitivity5: ΠX , Y, Z, U, V: X = Y ⊢ Y = Z ⊢ Z = U ⊢ U = V ⊢ X = V]

SystemQ proof of eqTransitivity5:

L01: Arbitrary ≫  X , Y, Z, U, V  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Y = Z  ;
L04: Premise ≫  Z = U  ;
L05: Premise ≫  U = V  ;

L06: eqTransitivity4 ⊳ L02 ⊳ L03 ⊳

L04 ≫ X = U ;

L07: eqTransitivity ⊳ L06 ⊳ L05 ≫ X = V  □

[SystemQ lemma eqTransitivity6: ΠX , Y, Z, U, V, W: X = Y ⊢ Y = Z ⊢ Z = U ⊢ U = V ⊢ V = W ⊢ X = W]

SystemQ proof of eqTransitivity6:

L01: Arbitrary ≫  X , Y, Z, U, V, W  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Y = Z  ;
L04: Premise ≫  Z = U  ;
L05: Premise ≫  U = V  ;
L06: Premise ≫  V = W  ;

L07: eqTransitivity5 ⊳ L02 ⊳ L03 ⊳

L04 ⊳ L05 ≫ X = V ;

L08: eqTransitivity ⊳ L07 ⊳ L06 ≫ X = W  □

[SystemQ lemma Induction: ΠV_{1}, A, B, C: ⟨B≡A|V_{1}:==0⟩_{Me} ⊢⊢ ⟨C≡A|V_{1}:==(V_{1}+ 1)⟩_{Me} ⊢⊢ B ⊢ A ⇒ C ⊢ A]

SystemQ proof of Induction:

L01: Arbitrary ≫  V_{1}, A, B, C  ;
L02: Side-condition ≫  ⟨B≡A|V_{1}:==0⟩_{Me}  ;
L03: Side-condition ≫  ⟨C≡A|V_{1}:==(V_{1} + 1)⟩_{Me}  ;
L04: Premise ≫  B  ;
L05: Premise ≫  A ⇒ C  ;
L06: Gen ⊳ L05 ≫  ∀V_{1}: (A ⇒ C)  ;

L07: InductionAxiom ⊳ ⊳ L02 ⊳ ⊳

L03 ≫ B ⇒ ∀V_{1}: (A ⇒ C) ⇒ ∀V_{1}: A ;

L08: MP2 ⊳ L07 ⊳ L04 ⊳ L06 ≫  ∀V_{1}: A  ;
L09: A4 @ V_{1} ⊳ L08 ≫  A  □

[SystemQ lemma ToSeries: ΠFX, (SY): ∀(R1ob): ((R1ob) ∈ FX ⇒ IsOrderedPair((R1ob), N, (SY))) ⊢ ∀(F1ob), (F2ob), (F3ob), (F4ob): (OrderedPair((F1ob), (F2ob)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob)) ⊢ ∀(S1ob): ((S1ob) ∈ N ⇒ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ FX) ⊢ IsSeries(FX, (SY))]

SystemQ proof of ToSeries:

L01: Arbitrary ≫ FX, (SY) ;

L02: Premise ≫ ∀(R1ob): ((R1ob) ∈ FX ⇒

IsOrderedPair((R1ob), N, (SY)))

;

L03: Premise ≫ ∀(F1ob), (F2ob), (F3ob), (F4ob): (OrderedPair((F1ob), (F2ob)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob)) ;

L04: Premise ≫ ∀(S1ob): ((S1ob) ∈ N ⇒ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ FX) ;

L05: Repetition ⊳ L02 ≫ IsRelation(FX, N, (SY)) ;

L06: JoinConjuncts ⊳ L05 ⊳ L03 ≫

IsRelation(FX, N, (SY))  ˙∧

∀(F1ob), (F2ob), (F3ob), (F4ob): (OrderedPair((F1ob), (F2ob)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob)) ;

L07: Repetition ⊳ L06 ≫ isFunction(FX, N, (SY)) ;

L08: JoinConjuncts ⊳ L07 ⊳ L04 ≫

isFunction(FX, N, (SY))  ˙∧

∀(S1ob): ((S1ob) ∈ N ⇒ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ FX) ;

L09: Repetition ⊳ L08 ≫ IsSeries(FX, (SY)) □

[SystemQ lemma FromSeries: ΠFX, (SY): IsSeries(FX, (SY)) ⊢ (∀(R1ob): ((R1ob) ∈ FX ⇒ ∃(OP1ob): ∃(OP2ob): (OP1ob) ∈ N ˙∧ (OP2ob) ∈ (SY) ˙∧ (R1ob) = OrderedPair((OP1ob), (OP2ob)))) ˙∧ (∀(F1ob), (F2ob), (F3ob), (F4ob): (OrderedPair((F1ob), (F2ob)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob))) ˙∧ ∀(S1ob): ((S1ob) ∈ N ⇒ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ FX)]

SystemQ proof of FromSeries:

L01: Arbitrary ≫  FX, (SY)  ;
L02: Premise ≫  IsSeries(FX, (SY))  ;

L03: Repetition ⊳ L02 ≫

isFunction(FX, N, (SY))  ˙∧

∀(S1ob): ((S1ob) ∈ N ⇒ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ FX) ; L04: Repetition ⊳ L03 ≫

IsRelation(FX, N, (SY))  ˙∧

(∀(F1ob), (F2ob), (F3ob), (F4ob): (OrderedPair((F1ob), (F2ob)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob))) ˙∧ ∀(S1ob): ((S1ob) ∈ N ⇒ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ FX) ;

L05: Repetition ⊳ L04 ≫ (∀(R1ob): ((R1ob) ∈ FX ⇒ IsOrderedPair((R1ob), N, (SY)))) ˙∧ (∀(F1ob), (F2ob), (F3ob), (F4ob): (OrderedPair((F1ob), (F2ob)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob))) ˙∧ ∀(S1ob): ((S1ob) ∈ N ⇒ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ FX) ;

L06: Repetition ⊳ L05 ≫ (∀(R1ob): ((R1ob) ∈ FX ⇒ ∃(OP1ob): ∃(OP2ob): (OP1ob) ∈

N  ˙∧  (OP2ob)  ∈
(SY)  ˙∧  (R1ob)  =

OrderedPair((OP1ob), (OP2ob)))) ˙∧ (∀(F1ob), (F2ob), (F3ob), (F4ob): (OrderedPair((F1ob), (F2ob)) ∈ FX ⇒ OrderedPair((F3ob), (F4ob)) ∈ FX ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob))) ˙∧ ∀(S1ob): ((S1ob) ∈ N ⇒ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ FX) □

[SystemQ lemma IntroExist(Helper): ΠX , V_{1}, A, B: ⟨ ˙¬ (A)n≡ ˙¬ (B)n|V_{1}:==X ⟩_{Me} ⊢⊢ ∀V_{1}: ˙¬ (B)n ⇒ ˙¬ (A)n]

SystemQ proof of IntroExist(Helper):

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , V_{1}, A, B  ;
L03: Side-condition ≫  ⟨ ˙¬ (A)n≡ ˙¬ (B)n|V_{1}:==X ⟩_{Me}  ;
L04: Premise ≫  ∀V_{1}: ˙¬ (B)n  ;
L05: A4 @ X ⊳ ⊳ L03 ⊳ L04 ≫  ˙¬ (A)n  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  X , V_{1}, A, B  ;

L08: Ded ⊳ L06 ≫

⟨ ˙¬ (A)n≡ ˙¬ (B)n|V_{1}:==X ⟩_{Me} ⊢⊢
∀V_{1}: ˙¬ (B)n ⇒ ˙¬ (A)n □

[SystemQ lemma IntroExist: ΠX , V_{1}, A, B: ⟨ ˙¬ (A)n≡ ˙¬ (B)n|V_{1}:==X ⟩_{Me} ⊢⊢ A ⊢ ∃V_{1}: B]

SystemQ proof of IntroExist:

L01: Arbitrary ≫  X , V_{1}, A, B  ;
L02: Side-condition ≫  ⟨ ˙¬ (A)n≡ ˙¬ (B)n|V_{1}:==X ⟩_{Me}  ;

L03: IntroExist(Helper) @ X ⊳ ⊳

L02 ≫ ∀V_{1}: ˙¬ (B)n ⇒ ˙¬ (A)n ;

L04: Premise ≫  A  ;
L05: AddDoubleNeg ⊳ L04 ≫  ˙¬ ( ˙¬ (A)n)n  ;
L06: MT ⊳ L03 ⊳ L05 ≫  ˙¬ (∀V_{1}: ˙¬ (B)n)n  ;
L07: Repetition ⊳ L06 ≫  ∃V_{1}: B  □

[SystemQ lemma ExistMP: ΠV_{1}, A, B: A ⇒ B ⊢ ∃V_{1}: A ⊢ B]

SystemQ proof of ExistMP:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  V_{1}, A, B  ;
L03: Premise ≫  A ⇒ B  ;
L04: Premise ≫  ∃V_{1}: A  ;
L05: Premise ≫  ˙¬ (B)n  ;
L06: MT ⊳ L03 ⊳ L05 ≫  ˙¬ (A)n  ;
L07: Gen ⊳ L06 ≫  ∀V_{1}: ˙¬ (A)n  ;
L08: Repetition ⊳ L04 ≫  ˙¬ (∀V_{1}: ˙¬ (A)n)n  ;

L09: FromContradiction ⊳ L07 ⊳

L08 ≫ ˙¬ ( ˙¬ (B)n)n ;

L10: Block ≫  End  ;
L11: Arbitrary ≫  V_{1}, A, B  ;
L12: Ded ⊳ L10 ≫  {(A ⇒ B) ⇒ ∃V_{1}: A ⇒ \atop ˙¬ (B)n ⇒ ˙¬ ( ˙¬ (B)n)n  ;}
L04: Premise ≫  A ⇒ B  ;
L03: Premise ≫  ∃V_{1}: A  ;
L05: MP2 ⊳ L12 ⊳ L04 ⊳ L03 ≫  ˙¬ (B)n ⇒ ˙¬ ( ˙¬ (B)n)n  ;

L06: prop lemma imply negation ⊳

L05 ≫ ˙¬ ( ˙¬ (B)n)n ;

L13: RemoveDoubleNeg ⊳ L06 ≫ B □

[SystemQ lemma ExistMP2: ΠV_{1}, V_{2}, A, B, C: A ⇒ B ⇒ C ⊢ ∃V_{1}: A ⊢ ∃V_{2}: B ⊢ C]

SystemQ proof of ExistMP2:

L01: Arbitrary ≫  V_{1}, V_{2}, A, B, C  ;
L02: Premise ≫  A ⇒ B ⇒ C  ;
L03: Premise ≫  ∃V_{1}: A  ;
L04: Premise ≫  ∃V_{2}: B  ;
L05: ExistMP ⊳ L02 ⊳ L03 ≫  B ⇒ C  ;
L06: ExistMP ⊳ L05 ⊳ L04 ≫  C  □

[SystemQ lemma TwiceExistMP: ΠV_{1}, V_{2}, A, B: A ⇒ B ⊢ ∃V_{1}: ∃V_{2}: A ⊢ B]

SystemQ proof of TwiceExistMP:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  V_{2}, A, B  ;
L03: Premise ≫  A ⇒ B  ;
L04: Premise ≫  ∃V_{2}: A  ;
L05: ExistMP ⊳ L03 ⊳ L04 ≫  B  ;
L06: Block ≫  End  ;
L07: Arbitrary ≫  V_{1}, V_{2}, A, B  ;
L03: Ded ⊳ L06 ≫  (A ⇒ B) ⇒ ∃V_{2}: A ⇒ B  ;
L04: Premise ≫  A ⇒ B  ;
L08: Premise ≫  ∃V_{1}: ∃V_{2}: A  ;
L09: MP ⊳ L03 ⊳ L04 ≫  ∃V_{2}: A ⇒ B  ;
L10: ExistMP ⊳ L09 ⊳ L08 ≫  B  □

[SystemQ lemma TwiceExistMP2: ΠV_{1}, V_{2}, V_{3}, V_{4}, A, B, C: A ⇒ B ⇒ C ⊢ ∃V_{1}: ∃V_{2}: A ⊢ ∃V_{3}: ∃V_{4}: B ⊢ C]

SystemQ proof of TwiceExistMP2:

L01: Arbitrary ≫  V_{1}, V_{2}, V_{3}, V_{4}, A, B, C  ;
L02: Premise ≫  A ⇒ B ⇒ C  ;
L03: Premise ≫  ∃V_{1}: ∃V_{2}: A  ;
L04: Premise ≫  ∃V_{3}: ∃V_{4}: B  ;
L05: TwiceExistMP ⊳ L02 ⊳ L03 ≫ B ⇒ C  ;
L06: TwiceExistMP ⊳ L05 ⊳ L04 ≫ C  □

[SystemQ lemma NeqSymmetry: ΠX , Y: X ≠ Y ⊢ Y ≠ X]

SystemQ proof of NeqSymmetry:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  Y = X  ;
L04: eqSymmetry ⊳ L03 ≫  X = Y  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  X , Y  ;
L07: Ded ⊳ L05 ≫  Y = X ⇒ X = Y  ;
L08: Premise ≫  X ≠ Y  ;
L09: MT ⊳ L07 ⊳ L08 ≫  Y ≠ X  □

[SystemQ lemma SubNeqLeft: ΠX , Y, Z: X = Y ⊢ X ≠ Z ⊢ Y ≠ Z] SystemQ proof of SubNeqLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  X ≠ Z  ;
L04: EqualityAxiom ≫  Y = X ⇒ Y = Z ⇒ X = Z  ;
L05: eqSymmetry ⊳ L02 ≫  Y = X  ;
L06: MP ⊳ L04 ⊳ L05 ≫  Y = Z ⇒ X = Z  ;
L07: Contrapositive ⊳ L06 ≫  X ≠ Z ⇒ Y ≠ Z  ;
L08: MP ⊳ L07 ⊳ L03 ≫  Y ≠ Z  □

[SystemQ lemma InPair(1): Π(SX), (SY): (SX) ∈ (p(SX), (SY))]

SystemQ proof of InPair(1):

L01: Arbitrary ≫  (SX), (SY)  ;

L02: eqReflexivity ≫  (SX) = (SX)  ;
L03: WeakenOr2 ⊳ L02 ≫  (SX) = (SX) ˙∨ (SX) = (SY)  ;
L04: Formula2Pair ⊳ L03 ≫  (SX) ∈ (p(SX), (SY))  □

[SystemQ lemma InPair(2): Π(SX), (SY): (SY) ∈ (p(SX), (SY))]

SystemQ proof of InPair(2):

L01: Arbitrary ≫  (SX), (SY)  ;
L02: eqReflexivity ≫  (SY) = (SY)  ;
L03: WeakenOr1 ⊳ L02 ≫  (SY) = (SX) ˙∨ (SY) = (SY)  ;
L04: Formula2Pair ⊳ L03 ≫  (SY) ∈ (p(SX), (SY))  □

[SystemQ lemma FromSingleton: Π(SX), (SY): (SX) ∈ (s(SY)) ⊢ (SX) = (SY)]

SystemQ proof of FromSingleton:

L01: Arbitrary ≫  (SX), (SY)  ;
L02: Premise ≫  (SX) ∈ (s(SY))  ;
L03: Repetition ⊳ L02 ≫  (SX) ∈ (p(SY), (SY))  ;
L04: Pair2Formula ⊳ L03 ≫  (SX) = (SY) ˙∨ (SX) = (SY)  ;
L05: RemoveOr ⊳ L04 ≫  (SX) = (SY)  □

[SystemQ lemma ToSingleton: Π(SX), (SY): (SX) = (SY) ⊢ (SX) ∈ (s(SY))] SystemQ proof of ToSingleton:

L01: Arbitrary ≫  (SX), (SY)  ;
L02: Premise ≫  (SX) = (SY)  ;
L03: WeakenOr1 ⊳ L02 ≫  (SX) = (SY) ˙∨ (SX) = (SY)  ;
L04: Formula2Pair ⊳ L03 ≫  (SX) ∈ (p(SY), (SY))  ;
L05: Repetition ⊳ L04 ≫  (SX) ∈ (s(SY))  □

[SystemQ lemma FromSameSingleton: Π(SX), (SY): (s(SX)) = (s(SY)) ⊢ (SX) = (SY)]

SystemQ proof of FromSameSingleton:

L01: Arbitrary ≫  (SX), (SY)  ;
L02: Premise ≫  (s(SX)) = (s(SY))  ;
L03: eqReflexivity ≫  (SX) = (SX)  ;
L04: ToSingleton ⊳ L03 ≫  (SX) ∈ (s(SX))  ;
L05: SENC1 ⊳ L02 ⊳ L04 ≫  (SX) ∈ (s(SY))  ;
L06: FromSingleton ⊳ L05 ≫  (SX) = (SY)  □

[SystemQ lemma SingletonmembersEqual: Π(SX), (SY), (SZ): (p(SX), (SY)) = (s(SZ)) ⊢ (SX) = (SY)]

SystemQ proof of SingletonmembersEqual:

L01: Arbitrary ≫  (SX), (SY), (SZ)  ;
L02: Premise ≫  (p(SX), (SY)) = (s(SZ))  ;
L03: InPair(1) ≫  (SX) ∈ (p(SX), (SY))  ;
L04: SENC1 ⊳ L02 ⊳ L03 ≫  (SX) ∈ (s(SZ))  ;
L05: FromSingleton ⊳ L04 ≫  (SX) = (SZ)  ;
L06: InPair(2) ≫  (SY) ∈ (p(SX), (SY))  ;
L07: SENC1 ⊳ L02 ⊳ L06 ≫  (SY) ∈ (s(SZ))  ;
L08: FromSingleton ⊳ L07 ≫  (SY) = (SZ)  ;
L09: eqSymmetry ⊳ L08 ≫  (SZ) = (SY)  ;
L10: eqTransitivity ⊳ L05 ⊳ L09 ≫ (SX) = (SY)  □

[SystemQ lemma UnequalsNotInSingleton: Π(SX), (SY), (SZ): (SX) ≠ (SY) ⊢ (p(SX), (SY)) ≠ (s(SZ))]

SystemQ proof of UnequalsNotInSingleton:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  (SX), (SY), (SZ)  ;
L03: Premise ≫  (p(SX), (SY)) = (s(SZ))  ;

L04: SingletonmembersEqual ⊳

L03 ≫ (SX) = (SY) ;

L05: Block ≫  End  ;
L06: Arbitrary ≫  (SX), (SY), (SZ)  ;

L07: Ded ⊳ L05 ≫ (p(SX), (SY)) = (s(SZ)) ⇒ (SX) = (SY) ;

L03: Premise ≫  (SX) ≠ (SY)  ;
L08: MT ⊳ L07 ⊳ L03 ≫  (p(SX), (SY)) ≠ (s(SZ))  □

[SystemQ lemma NonsingletonmembersUnequal: Π(SX), (SY): (p(SX), (SY)) ≠ (s(SX)) ⊢ (SX) ≠ (SY)]

SystemQ proof of NonsingletonmembersUnequal:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  (SX), (SY)  ;
L03: Premise ≫  (SX) = (SY)  ;
L04: eqReflexivity ≫  (SX) = (SX)  ;
L05: SamePair ⊳ L04 ⊳ L03 ≫  (p(SX), (SX)) = (p(SX), (SY)) ;
L06: Repetition ⊳ L05 ≫  (s(SX)) = (p(SX), (SY))  ;
L07: eqSymmetry ⊳ L06 ≫  (p(SX), (SY)) = (s(SX))  ;
L08: Block ≫  End  ;
L09: Arbitrary ≫  (SX), (SY)  ;

L10: Ded ⊳ L08 ≫

(SX)  =  (SY)  ⇒

(p(SX), (SY)) = (s(SX))

;

L03: Premise ≫  (p(SX), (SY)) ≠ (s(SX))  ;
L11: MT ⊳ L10 ⊳ L03 ≫  (SX) ≠ (SY)  □

[SystemQ lemma FromOrderedPair: Π(SX), (SX1), (SY), (SY1): OrderedPair((SX), (SY)) = OrderedPair((SX1), (SY1)) ⊢ (SX) = (SX1) ˙∧ (SY) = (SY1)]

SystemQ proof of FromOrderedPair:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  (SX), (SX1), (SY), (SY1)  ;
L03: Premise ≫  (SX1) = (SY1)  ;
L04: Premise ≫  OrderedPair((SX), (SY))  =

OrderedPair((SX1), (SY1)) ;

L05: Repetition ⊳ L04 ≫ (p(s(SX)), (p(SX), (SY))) = (p(s(SX1)), (p(SX1), (SY1))) ;

L06: eqReflexivity ≫ (SX1) = (SX1) ;

L07: SamePair ⊳ L06 ⊳ L03 ≫ (p(SX1), (SX1)) = (p(SX1), (SY1)) ;

L08: Repetition ⊳ L07 ≫  (s(SX1)) = (p(SX1), (SY1))  ;
L09: eqReflexivity ≫  (s(SX1)) = (s(SX1))  ;

L10: SamePair ⊳ L09 ⊳ L08 ≫ (p(s(SX1)), (s(SX1))) = (p(s(SX1)), (p(SX1), (SY1))) ;

L11: Repetition ⊳ L10 ≫ (s(s(SX1))) = (p(s(SX1)), (p(SX1), (SY1))) ;

L12: eqSymmetry ⊳ L11 ≫ (p(s(SX1)), (p(SX1), (SY1))) = (s(s(SX1))) ;

L13: eqTransitivity ⊳ L05 ⊳ L12 ≫ (p(s(SX)), (p(SX), (SY))) = (s(s(SX1))) ;

L14: InPair(1) ≫ (s(SX)) ∈ (p(s(SX)), (p(SX), (SY)))

;

L15: SENC1 ⊳ L13 ⊳ L14 ≫  (s(SX)) ∈ (s(s(SX1)))  ;
L16: FromSingleton ⊳ L15 ≫  (s(SX)) = (s(SX1))  ;
L17: FromSameSingleton ⊳ L16 ≫ (SX) = (SX1)  ;
L18: eqSymmetry ⊳ L16 ≫  (s(SX1)) = (s(SX))  ;
L19: SameSingleton ⊳ L18 ≫  (s(s(SX1))) = (s(s(SX)))  ;

L20: eqTransitivity ⊳ L13 ⊳ L19 ≫ (p(s(SX)), (p(SX), (SY))) = (s(s(SX))) ;

L21: InPair(2) ≫ (p(SX), (SY)) ∈ (p(s(SX)), (p(SX), (SY)))

;

L22: SENC1 ⊳ L20 ⊳ L21 ≫  (p(SX), (SY)) ∈ (s(s(SX)))  ;
L23: FromSingleton ⊳ L22 ≫  (p(SX), (SY)) = (s(SX))  ;

L24: SingletonmembersEqual ⊳

L23 ≫ (SX) = (SY) ;

L25: eqSymmetry ⊳ L24 ≫ (SY) = (SX) ;

L26: eqTransitivity4 ⊳ L25 ⊳ L17 ⊳

L03 ≫ (SY) = (SY1) ;

L27: JoinConjuncts ⊳ L17 ⊳ L26 ≫ (SX) = (SX1) ˙∧ (SY) = (SY1) ;
L28: Block ≫  End  ;
L29: Block ≫  Begin  ;
L30: Arbitrary ≫  (SX), (SX1), (SY), (SY1)  ;
L03: Premise ≫  (SX1) ≠ (SY1)  ;
L04: Premise ≫  OrderedPair((SX), (SY))  =

OrderedPair((SX1), (SY1)) ;

L05: Repetition ⊳ L04 ≫ (p(s(SX)), (p(SX), (SY))) = (p(s(SX1)), (p(SX1), (SY1))) ;

L06: InPair(1) ≫ (s(SX)) ∈ (p(s(SX)), (p(SX), (SY)))

;

L07: SENC1 ⊳ L05 ⊳ L06 ≫ (s(SX)) ∈ (p(s(SX1)), (p(SX1), (SY1))) ;

L08: Pair2Formula ⊳ L07 ≫ (s(SX)) = (s(SX1)) ˙∨ (s(SX)) = (p(SX1), (SY1))

;

L09: UnequalsNotInSingleton ⊳ L03 ≫ (p(SX1), (SY1)) ≠ (s(SX)) ;

L10: NeqSymmetry ⊳ L09 ≫  (s(SX)) ≠ (p(SX1), (SY1))  ;
L11: NegateDisjunct2⊳L08⊳L10 ≫ (s(SX)) = (s(SX1))  ;
L12: FromSameSingleton ⊳ L11 ≫ (SX) = (SX1)  ;

L14: InPair(2) ≫ (p(SX1), (SY1)) ∈ (p(s(SX1)), (p(SX1), (SY1))) ;

L15: SENC2 ⊳ L05 ⊳ L14 ≫ (p(SX1), (SY1)) ∈ (p(s(SX)), (p(SX), (SY)))

;

L16: Pair2Formula ⊳ L15 ≫ (p(SX1), (SY1)) = (s(SX)) ˙∨ (p(SX1), (SY1)) = (p(SX), (SY)) ;

L18: NegateDisjunct1⊳L16⊳L09 ≫

(p(SX1), (SY1)) =
(p(SX), (SY)) ;
L19: InPair(2) ≫  (SY) ∈ (p(SX), (SY))  ;
L20: SENC2 ⊳ L18 ⊳ L19 ≫  (SY) ∈ (p(SX1), (SY1))  ;
L21: Pair2Formula ⊳ L20 ≫  (SY) = (SX1) ˙∨ (SY) = (SY1) ;

L22: UnequalsNotInSingleton ⊳ L03 ≫

(p(SX1), (SY1)) ≠ (s(SX)) ;

L23: SubNeqLeft ⊳ L18 ⊳ L22 ≫ (p(SX), (SY)) ≠ (s(SX)) ;

L24: NonsingletonmembersUnequal⊳

L23 ≫ (SX) ≠ (SY) ;

L25: SubNeqLeft ⊳ L12 ⊳ L24 ≫  (SX1) ≠ (SY)  ;
L26: NeqSymmetry ⊳ L25 ≫  (SY) ≠ (SX1)  ;
L31: NegateDisjunct1⊳L21⊳L26 ≫ (SY) = (SY1)  ;
L32: JoinConjuncts ⊳ L12 ⊳ L31 ≫ (SX) = (SX1) ˙∧ (SY) = (SY1) ;
L33: Block ≫  End  ;
L34: Arbitrary ≫  (SX), (SX1), (SY), (SY1)  ;

L35: Ded ⊳ L28 ≫

(SX1)  =  (SY1)  ⇒

OrderedPair((SX), (SY)) = OrderedPair((SX1), (SY1)) ⇒ (SX) = (SX1) ˙∧ (SY) = (SY1) ;

L36: Ded ⊳ L33 ≫

(SX1)  ≠  (SY1)  ⇒

OrderedPair((SX), (SY)) = OrderedPair((SX1), (SY1)) ⇒ (SX) = (SX1) ˙∧ (SY) = (SY1) ;

L03: Premise ≫ OrderedPair((SX), (SY)) =

OrderedPair((SX1), (SY1)) ;

L04: FromNegations ⊳ L35 ⊳ L36 ≫ OrderedPair((SX), (SY)) = OrderedPair((SX1), (SY1)) ⇒ (SX) = (SX1) ˙∧ (SY) = (SY1) ;

L37: MP ⊳ L04 ⊳ L03 ≫  (SX) = (SX1) ˙∧ (SY) = (SY1) □

[SystemQ lemma FromOrderedPair(1): Π(SX), (SX1), (SY), (SY1): OrderedPair((SX), (SY)) = OrderedPair((SX1), (SY1)) ⊢ (SX) = (SX1)]

SystemQ proof of FromOrderedPair(1):

L01: Arbitrary ≫  (SX), (SX1), (SY), (SY1)  ;
L02: Premise ≫  OrderedPair((SX), (SY))  =

OrderedPair((SX1), (SY1)) ;

L03: FromOrderedPair ⊳ L02 ≫  (SX) = (SX1) ˙∧ (SY) = (SY1) ;
L04: FirstConjunct ⊳ L03 ≫ (SX) = (SX1) □

[SystemQ lemma FromOrderedPair(2): Π(SX), (SX1), (SY), (SY1): OrderedPair((SX), (SY)) = OrderedPair((SX1), (SY1)) ⊢ (SY) = (SY1)]

SystemQ proof of FromOrderedPair(2):

L01: Arbitrary ≫  (SX), (SX1), (SY), (SY1)  ;
L02: Premise ≫  OrderedPair((SX), (SY))  =

OrderedPair((SX1), (SY1)) ;

L03: FromOrderedPair ⊳ L02 ≫  (SX) = (SX1) ˙∧ (SY) = (SY1) ;
L04: SecondConjunct ⊳ L03 ≫ (SY) = (SY1) □

[SystemQ lemma SameMember(2): Π(SX), (SY), (SZ): (SX) = (SY) ⊢ (SY) ∈ (SZ) ⊢ (SX) ∈ (SZ)]

SystemQ proof of SameMember(2):

L01: Arbitrary ≫  (SX), (SY), (SZ)  ;
L02: Premise ≫  (SX) = (SY)  ;
L03: Premise ≫  (SY) ∈ (SZ)  ;
L04: eqSymmetry ⊳ L02 ≫  (SY) = (SX)  ;
L05: SameMember ⊳ L04 ⊳ L03 ≫ (SX) ∈ (SZ)  □

[SystemQ lemma ToBinaryUnion(1): Π(SX), (SY), (SZ), (SU): (SX) ∈ (SY) ⊢ (SX) ∈ binaryUnion((SY), (SZ))]

SystemQ proof of ToBinaryUnion(1):

L01: Arbitrary ≫  (SX), (SY), (SZ), (SU)  ;
L02: Premise ≫  (SX) ∈ (SY)  ;
L03: InPair(1) ≫  (SY) ∈ (p(SY), (SZ))  ;

L04: JoinConjuncts ⊳ L02 ⊳ L03 ≫

(SX) ∈ (SY) ˙∧ (SY) ∈
(p(SY), (SZ)) ;

L05: IntroExist @(SY) ⊳ L04 ≫ ∃(SU): (SX) ∈ (SU) ˙∧ (SU) ∈ (p(SY), (SZ)) ;

L06: Formula2Union ⊳ L05 ≫ (SX) ∈ Union((p(SY), (SZ))) ;

L07: Repetition ⊳ L06 ≫ (SX) ∈ binaryUnion((SY), (SZ)) □

[SystemQ lemma ToBinaryUnion(2): Π(SX), (SY), (SZ), (SU): (SX) ∈ (SZ) ⊢ (SX) ∈ binaryUnion((SY), (SZ))]

SystemQ proof of ToBinaryUnion(2):

L01: Arbitrary ≫  (SX), (SY), (SZ), (SU)  ;
L02: Premise ≫  (SX) ∈ (SZ)  ;
L03: InPair(2) ≫  (SZ) ∈ (p(SY), (SZ))  ;

L04: JoinConjuncts ⊳ L02 ⊳ L03 ≫

(SX) ∈ (SZ) ˙∧ (SZ) ∈
(p(SY), (SZ)) ;

L05: IntroExist @(SZ) ⊳ L04 ≫ ∃(SU): (SX) ∈ (SU) ˙∧ (SU) ∈ (p(SY), (SZ)) ;

L06: Formula2Union ⊳ L05 ≫ (SX) ∈ Union((p(SY), (SZ))) ;

L07: Repetition ⊳ L06 ≫ (SX) ∈ binaryUnion((SY), (SZ)) □

[SystemQ lemma FromOrderedPair(TwoLevels): Π(SX), (SY), (SZ), (SU): (SX) ∈ (SY) ⊢ (SY) ∈ OrderedPair((SZ), (SU)) ⊢ (SX) = (SZ) ˙∨ (SX) = (SU)]

SystemQ proof of FromOrderedPair(TwoLevels):

L01: Arbitrary ≫  (SX), (SY), (SZ), (SU)  ;
L02: Premise ≫  (SX) ∈ (SY)  ;
L03: Premise ≫  (SY)  ∈

OrderedPair((SZ), (SU)) ;

L04: Repetition ⊳ L03 ≫ (SY) ∈ (p(s(SZ)), (p(SZ), (SU))) ;

L05: Pair2Formula ⊳ L04 ≫

(SY) = (s(SZ)) ˙∨ (SY) =
(p(SZ), (SU)) ;
L06: Block ≫  Begin  ;
L07: Arbitrary ≫  (SX), (SY), (SZ), (SU)  ;
L03: Premise ≫  (SY) = (s(SZ))  ;
L02: Premise ≫  (SX) ∈ (SY)  ;
L04: SENC1 ⊳ L03 ⊳ L02 ≫  (SX) ∈ (s(SZ))  ;
L05: FromSingleton ⊳ L04 ≫  (SX) = (SZ)  ;
L08: WeakenOr2 ⊳ L05 ≫  (SX) = (SZ) ˙∨ (SX) = (SU)  ;
L09: Block ≫  End  ;
L10: Block ≫  Begin  ;
L11: Arbitrary ≫  (SX), (SY), (SZ), (SU)  ;
L03: Premise ≫  (SY) = (p(SZ), (SU))  ;
L02: Premise ≫  (SX) ∈ (SY)  ;
L04: SENC1 ⊳ L03 ⊳ L02 ≫  (SX) ∈ (p(SZ), (SU))  ;
L12: Pair2Formula ⊳ L04 ≫  (SX) = (SZ) ˙∨ (SX) = (SU)  ;
L13: Block ≫  End  ;

L14: Ded ⊳ L09 ≫ (SY) = (s(SZ)) ⇒ (SX) ∈ (SY) ⇒ (SX) = (SZ) ˙∨ (SX) = (SU) ;

L15: Ded ⊳ L13 ≫ (SY) = (p(SZ), (SU)) ⇒ (SX) ∈ (SY) ⇒ (SX) = (SZ) ˙∨ (SX) = (SU) ;

L16: FromDisjuncts ⊳ L05 ⊳ L14 ⊳

L15 ≫ (SX) ∈ (SY) ⇒ (SX) = (SZ) ˙∨

(SX) = (SU) ;

L17: MP ⊳ L16 ⊳ L02 ≫ (SX) = (SZ) ˙∨ (SX) = (SU) □

[SystemQ lemma CartProdIsRelation: Π(SX), (SY): IsRelation(cartProd((SX)), (SX), (SY))] SystemQ proof of CartProdIsRelation:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  (SX), (SY)  ;
L03: Premise ≫  (R1ob) ∈ cartProd((SX))  ;

L04: Sep2Formula ⊳ L03 ≫ (R1ob) ∈ Power(Power(binaryUnion((SX), (SY)))) ˙∧ IsOrderedPair((R1ob), (SX), (SY))

;

L05: SecondConjunct ⊳ L04 ≫ IsOrderedPair((R1ob), (SX), (SY))

;

L06: Block ≫  End  ;

L07: Arbitrary ≫  (SX), (SY)  ;

L03: Ded ⊳ L06 ≫ (R1ob) ∈ cartProd((SX)) ⇒ IsOrderedPair((R1ob), (SX), (SY))

;

L04: Gen ⊳ L03 ≫ ∀(R1ob): ((R1ob) ∈ cartProd((SX)) ⇒ IsOrderedPair((R1ob), (SX), (SY)))

;

L08: Repetition ⊳ L04 ≫ IsRelation(cartProd((SX)), (SX), (SY)) □

[SystemQ lemma FromSubset: Π(SX), (SY), (SZ): IsSubset((SX), (SY)) ⊢ (SZ) ∈ (SX) ⊢ (SZ) ∈ (SY)]

SystemQ proof of FromSubset:

L01: Arbitrary ≫  (SX), (SY), (SZ)  ;
L02: Premise ≫  IsSubset((SX), (SY))  ;
L03: Premise ≫  (SZ) ∈ (SX)  ;

L04: Repetition ⊳ L02 ≫ ∀(S1ob): ((S1ob) ∈ (SX) ⇒ (S1ob) ∈ (SY)) ;

L05: A4 @(SZ) ⊳ L04 ≫  (SZ) ∈ (SX) ⇒ (SZ) ∈ (SY)  ;
L06: MP ⊳ L05 ⊳ L03 ≫  (SZ) ∈ (SY)  □

[SystemQ lemma SubsetIsRelation: Π(SX), (SY), (SZ), (SU): IsRelation((SX), (SZ), (SU)) ⊢ IsSubset((SY), (SX)) ⊢ IsRelation((SY), (SZ), (SU))]

SystemQ proof of SubsetIsRelation:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  (SX), (SY), (SZ), (SU)  ;
L03: Premise ≫  IsRelation((SX), (SZ), (SU))  ;
L04: Premise ≫  IsSubset((SY), (SX))  ;
L05: Premise ≫  (R1ob) ∈ (SY)  ;

L06: Repetition ⊳ L03 ≫ ∀(R1ob): ((R1ob) ∈ (SX) ⇒ IsOrderedPair((R1ob), (SZ), (SU)))

;

L07: A4 @(R1ob) ⊳ L06 ≫

(R1ob)  ∈  (SX)  ⇒

IsOrderedPair((R1ob), (SZ), (SU))

;

L08: FromSubset ⊳ L04 ⊳ L05 ≫ (R1ob) ∈ (SX) ;

L09: MP ⊳ L07 ⊳ L08 ≫ IsOrderedPair((R1ob), (SZ), (SU))

;

L10: Block ≫  End  ;
L11: Arbitrary ≫  (SX), (SY), (SZ), (SU)  ;

L12: Ded ⊳ L10 ≫ IsRelation((SX), (SZ), (SU)) ⇒ IsSubset((SY), (SX)) ⇒ (R1ob) ∈ (SY) ⇒ IsOrderedPair((R1ob), (SZ), (SU))

;

L03: Premise ≫  IsRelation((SX), (SZ), (SU))  ;
L04: Premise ≫  IsSubset((SY), (SX))  ;

L05: MP2 ⊳ L12 ⊳ L03 ⊳ L04 ≫

(R1ob)  ∈  (SY)  ⇒

IsOrderedPair((R1ob), (SZ), (SU))

;

L06: Gen ⊳ L05 ≫ ∀(R1ob): ((R1ob) ∈ (SY) ⇒ IsOrderedPair((R1ob), (SZ), (SU)))

;

L13: Repetition ⊳ L06 ≫ IsRelation((SY), (SZ), (SU)) □

[SystemQ lemma CPseparationIsRelation: ΠA, (SX), (SY): IsRelation({ph ∈ cartProd((SX)) | A}, (SX), (SY))]

SystemQ proof of CPseparationIsRelation:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  A, (SX), (SY)  ;
L03: Premise ≫  (S1ob)  ∈  {ph  ∈

cartProd((SX)) | A} ;

L04: Separation2formula(1)⊳L03 ≫ (S1ob) ∈ cartProd((SX))  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  A, (SX), (SY)  ;

L07: Ded ⊳ L05 ≫ ∀(S1ob): ((S1ob) ∈ {ph ∈ cartProd((SX)) | A} ⇒ (S1ob) ∈ cartProd((SX))) ;

L08: Repetition ⊳ L07 ≫ IsSubset({ph ∈ cartProd((SX)) | A}, cartProd((SX))) ;

L09: CartProdIsRelation ≫ IsRelation(cartProd((SX)), (SX), (SY))

;

L10: SubsetIsRelation⊳L09⊳L08 ≫ IsRelation({ph ∈ cartProd((SX)) | A}, (SX), (SY)) □

[SystemQ lemma ToCartProd(Helper): Π(SX), (SX1), (SY), (SY1), (SZ): (SX) ∈ (SX1) ⊢ (SY) ∈ (SY1) ⊢ (SZ) ∈ OrderedPair((SX), (SY)) ⊢ IsSubset((SZ), binaryUnion((SX1), (SY1)))]

SystemQ proof of ToCartProd(Helper):

L01: Block ≫ Begin ;
L02: Arbitrary ≫  (SX), (SX1), (SY), (SY1), (SZ) ;
L03: Premise ≫  (SX) ∈ (SX1)  ;
L04: Premise ≫  (SY) ∈ (SY1)  ;
L05: Premise ≫  (SZ)  ∈

OrderedPair((SX), (SY)) ;

L06: Premise ≫ (S1ob) ∈ (SZ) ;

L07: FromOrderedPair(TwoLevels)⊳

L06 ⊳ L05 ≫ (S1ob) = (SX) ˙∨ (S1ob) =

(SY) ;

L08: Block ≫  Begin  ;
L09: Arbitrary ≫  (SX), (SX1), (SY1)  ;
L04: Premise ≫  (SX) ∈ (SX1)  ;
L03: Premise ≫  (S1ob) = (SX)  ;
L05: SameMember(2)⊳L03⊳L04 ≫ (S1ob) ∈ (SX1)  ;

L10: ToBinaryUnion(1) ⊳ L05 ≫ (S1ob) ∈ binaryUnion((SX1), (SY1))

;

L11: Block ≫  End  ;
L12: Block ≫  Begin  ;
L13: Arbitrary ≫  (SX1), (SY), (SY1)  ;
L04: Premise ≫  (SY) ∈ (SY1)  ;
L03: Premise ≫  (S1ob) = (SY)  ;
L05: SameMember(2)⊳L03⊳L04 ≫ (S1ob) ∈ (SY1)  ;

L14: ToBinaryUnion(2) ⊳ L05 ≫ (S1ob) ∈ binaryUnion((SX1), (SY1))

;

L15: Block ≫ End ;

L16: Ded ⊳ L11 ≫ (SX) ∈ (SX1) ⇒ (S1ob) = (SX) ⇒ (S1ob) ∈ binaryUnion((SX1), (SY1))

;

L17: MP ⊳ L16 ⊳ L03 ≫ (S1ob) = (SX) ⇒ (S1ob) ∈ binaryUnion((SX1), (SY1)) ;

L18: Ded ⊳ L15 ≫ (SY) ∈ (SY1) ⇒ (S1ob) = (SY) ⇒ (S1ob) ∈ binaryUnion((SX1), (SY1))

;

L19: MP ⊳ L18 ⊳ L04 ≫ (S1ob) = (SY) ⇒ (S1ob) ∈ binaryUnion((SX1), (SY1)) ;

L20: FromDisjuncts ⊳ L07 ⊳ L17 ⊳

L19 ≫ (S1ob) ∈

binaryUnion((SX1), (SY1))

;

L21: Block ≫ End ;
L22: Arbitrary ≫  (SX), (SX1), (SY), (SY1), (SZ) ;

L23: Ded ⊳ L21 ≫

(SX)  ∈  (SX1)  ⇒

(SY) ∈ (SY1) ⇒ (SZ) ∈ OrderedPair((SX), (SY)) ⇒ (S1ob) ∈ (SZ) ⇒ (S1ob) ∈ binaryUnion((SX1), (SY1)) ;

L03: Premise ≫  (SX) ∈ (SX1)  ;
L04: Premise ≫  (SY) ∈ (SY1)  ;
L05: Premise ≫  (SZ)  ∈

OrderedPair((SX), (SY)) ;

L06: MP3⊳L23⊳L03⊳L04⊳L05 ≫ (S1ob) ∈ (SZ) ⇒ (S1ob) ∈ binaryUnion((SX1), (SY1)) ;

L07: Gen ⊳ L06 ≫ ∀(S1ob): ((S1ob) ∈ (SZ) ⇒ (S1ob) ∈ binaryUnion((SX1), (SY1)))

; L24: Repetition ⊳ L07 ≫ IsSubset((SZ), binaryUnion((SX1), (SY1))) □

[SystemQ lemma ToCartProd: Π(SX), (SX1), (SY), (SY1): (SX) ∈ (SX1) ⊢ (SY) ∈ (SY1) ⊢ OrderedPair((SX), (SY)) ∈ cartProd((SX1))]

SystemQ proof of ToCartProd:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  (SX), (SX1), (SY), (SY1)  ;
L03: Premise ≫  (SX) ∈ (SX1)  ;
L04: Premise ≫  (SY) ∈ (SY1)  ;
L05: Premise ≫  (S1ob)  ∈

OrderedPair((SX), (SY)) ;

L06: ToCartProd(Helper) ⊳ L03 ⊳

L04 ⊳ L05 ≫ IsSubset((S1ob), binaryUnion((SX1), (SY1)))

;

L07: Formula2Power ⊳ L06 ≫ (S1ob) ∈ Power(binaryUnion((SX1), (SY1)))

;

L08: Block ≫  End  ;
L09: Arbitrary ≫  (SX), (SX1), (SY), (SY1)  ;

L10: Ded ⊳ L08 ≫ (SX) ∈ (SX1) ⇒ (SY) ∈ (SY1) ⇒ (S1ob) ∈ OrderedPair((SX), (SY)) ⇒ (S1ob) ∈ Power(binaryUnion((SX1), (SY1)))

;

L03: Premise ≫  (SX) ∈ (SX1)  ;
L04: Premise ≫  (SY) ∈ (SY1)  ;

L06: MP2 ⊳ L10 ⊳ L03 ⊳ L04 ≫ (S1ob) ∈ OrderedPair((SX), (SY)) ⇒ (S1ob) ∈ Power(binaryUnion((SX1), (SY1)))

;

L11: Gen ⊳ L06 ≫ ∀(S1ob): ((S1ob) ∈ OrderedPair((SX), (SY)) ⇒ (S1ob) ∈ Power(binaryUnion((SX1), (SY1))))

;

L12: Repetition ⊳ L11 ≫ IsSubset(OrderedPair((SX), (SY)), Power(binaryUnion((SX1), (SY1))))

;

L13: Formula2Power ⊳ L12 ≫ OrderedPair((SX), (SY)) ∈ Power(Power(binaryUnion((SX1), (SY1))))

;

L14: eqReflexivity ≫ OrderedPair((SX), (SY)) = OrderedPair((SX), (SY)) ;

L15: JoinConjuncts ⊳ L03 ⊳ L04 ≫ (SX) ∈ (SX1) ˙∧ (SY) ∈ (SY1) ;

L16: JoinConjuncts ⊳ L15 ⊳ L14 ≫

(SX)  ∈  (SX1)  ˙∧
(SY)  ∈  (SY1)  ˙∧

OrderedPair((SX), (SY)) = OrderedPair((SX), (SY)) ;

L17: IntroExist @(SY) ⊳ L16 ≫ ∃(OP2ob): (SX) ∈ (SX1) ˙∧ (OP2ob) ∈ (SY1) ˙∧ OrderedPair((SX), (SY)) = OrderedPair((SX), (OP2ob)) ;

L18: IntroExist @(SX) ⊳ L17 ≫ ∃(OP1ob): ∃(OP2ob): (OP1ob) ∈ (SX1) ˙∧ (OP2ob) ∈ (SY1) ˙∧ OrderedPair((SX), (SY)) = OrderedPair((OP1ob), (OP2ob))

;

L19: Repetition ⊳ L18 ≫ IsOrderedPair(OrderedPair((SX), (SY)), (SX1), (SY1))

;

L20: Formula2Sep ⊳ L13 ⊳ L19 ≫ OrderedPair((SX), (SY)) ∈ {ph ∈ Power(Power(binaryUnion((SX1), (SY1)))) | IsOrderedPair(ph_{1}, (SX1), (SY1))}

;

L21: Repetition ⊳ L20 ≫ OrderedPair((SX), (SY)) ∈ cartProd((SX1)) □

[SystemQ lemma CrsIsRelation: ΠX: IsRelation(constantRationalSeries(X), N, Q)] SystemQ proof of CrsIsRelation:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X  ;
L03: Premise ≫  (S1ob)  ∈

constantRationalSeries(X)

;

L04: Repetition ⊳ L03 ≫ (S1ob) ∈ {ph ∈ cartProd(N) | ∃(CRS1ob): ph_{3} = OrderedPair((CRS1ob), X)} ;

L05: Sep2Formula ⊳ L04 ≫ (S1ob) ∈ cartProd(N) ˙∧ ∃(CRS1ob): (S1ob) = OrderedPair((CRS1ob), X)

;

L06: FirstConjunct ⊳ L05 ≫  (S1ob) ∈ cartProd(N)  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  X  ;

L03: Ded ⊳ L07 ≫ (S1ob) ∈ constantRationalSeries(X) ⇒ (S1ob) ∈ cartProd(N) ;

L04: Gen ⊳ L03 ≫ ∀(S1ob): ((S1ob) ∈ constantRationalSeries(X) ⇒ (S1ob) ∈ cartProd(N)) ;

L05: Repetition ⊳ L04 ≫ IsSubset(constantRationalSeries(X), cartProd(N))

;

L09: CartProdIsRelation ≫  IsRelation(cartProd(N), N, Q) ;

L10: SubsetIsRelation⊳L09⊳L05 ≫ IsRelation(constantRationalSeries(X), N, Q) □

[SystemQ lemma CrsIsFunction: ΠX: isFunction(constantRationalSeries(X), N, Q)] SystemQ proof of CrsIsFunction:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X  ;

L03: Premise ≫ OrderedPair((F1ob), (F2ob)) =

OrderedPair((CRS1ob), X) ;

L04: Premise ≫ OrderedPair((F3ob), (F4ob)) =

OrderedPair((CRS1ob), X) ;

L05: FromOrderedPair ⊳ L03 ≫ (F1ob) = (CRS1ob) ˙∧ (F2ob) = X ;

L06: SecondConjunct ⊳ L05 ≫ (F2ob) = X ;

L07: FromOrderedPair ⊳ L04 ≫ (F3ob) = (CRS1ob) ˙∧ (F4ob) = X ;

L08: SecondConjunct ⊳ L07 ≫  (F4ob) = X  ;
L09: eqSymmetry ⊳ L08 ≫  X = (F4ob)  ;
L10: eqTransitivity ⊳ L06 ⊳ L09 ≫ (F2ob) = (F4ob)  ;
L11: Block ≫  End  ;
L12: Block ≫  Begin  ;
L13: Arbitrary ≫  X  ;

L14: Ded ⊳ L11 ≫ OrderedPair((F1ob), (F2ob)) = OrderedPair((CRS1ob), X) ⇒ OrderedPair((F3ob), (F4ob)) = OrderedPair((CRS1ob), X) ⇒ (F2ob) = (F4ob) ;

L03: Premise ≫ OrderedPair((F1ob), (F2ob)) ∈

constantRationalSeries(X) ;

L04: Premise ≫ OrderedPair((F3ob), (F4ob)) ∈

constantRationalSeries(X) ;

L05: Premise ≫ (F1ob) = (F3ob) ;

L06: Sep2Formula ⊳ L03 ≫ OrderedPair((F1ob), (F2ob)) ∈ cartProd(N) ˙∧ ∃(CRS1ob): OrderedPair((F1ob), (F2ob)) = OrderedPair((CRS1ob), X) ;

L07: SecondConjunct ⊳ L06 ≫ ∃(CRS1ob): OrderedPair((F1ob), (F2ob)) = OrderedPair((CRS1ob), X) ;

L08: Sep2Formula ⊳ L04 ≫ OrderedPair((F3ob), (F4ob)) ∈ cartProd(N) ˙∧ ∃(CRS1ob): OrderedPair((F3ob), (F4ob)) = OrderedPair((CRS1ob), X) ;

L09: SecondConjunct ⊳ L08 ≫ ∃(CRS1ob): OrderedPair((F3ob), (F4ob)) = OrderedPair((CRS1ob), X) ;

L15: ExistMP2⊳L14⊳L07⊳L09 ≫ (F2ob) = (F4ob)  ;
L16: Block ≫  End  ;
L17: Arbitrary ≫  X  ;

L03: Ded ⊳ L16 ≫ ∀(F1ob), (F2ob), (F3ob), (F4ob): (OrderedPair((F1ob), (F2ob)) ∈ constantRationalSeries(X) ⇒ OrderedPair((F3ob), (F4ob)) ∈ constantRationalSeries(X) ⇒ (F1ob) = (F3ob) ⇒ (F2ob) = (F4ob)) ;

L04: CrsIsRelation ≫ IsRelation(constantRationalSeries(X), N, Q)

;

L18: JoinConjuncts ⊳ L04 ⊳ L03 ≫ isFunction(constantRationalSeries(X), N, Q) □

[SystemQ lemma CrsIsTotal: ΠM, X: TypeRational(X) ⊢⊢ M ∈ N ⊢ OrderedPair(M, X) ∈ constantRationalSeries(X)]

SystemQ proof of CrsIsTotal:

L01: Arbitrary ≫  M, X  ;
L02: Side-condition ≫  TypeRational(X)  ;
L03: Premise ≫  M ∈ N  ;
L04: RationalType ⊳ ⊳ L02 ≫  X ∈ Q  ;

L05: ToCartProd ⊳ L03 ⊳ L04 ≫ OrderedPair(M, X) ∈ cartProd(N) ;

L06: eqReflexivity ≫ OrderedPair(M, X) = OrderedPair(M, X) ;

L07: IntroExist @ M ⊳ L06 ≫ ∃(CRS1ob): OrderedPair(M, X) = OrderedPair((CRS1ob), X) ;

L08: Formula2Sep ⊳ L05 ⊳ L07 ≫ OrderedPair(M, X) ∈ constantRationalSeries(X) □

[SystemQ lemma CrsIsSeries: ΠX: IsSeries(constantRationalSeries(X), Q)] SystemQ proof of CrsIsSeries:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X  ;
L03: Premise ≫  (S1ob) ∈ N  ;

L04: CrsIsTotal ⊳ L03 ≫ OrderedPair((S1ob), X) ∈ constantRationalSeries(X) ;

L05: IntroExist @ X ⊳ L03 ≫ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ constantRationalSeries(X) ;

L06: Block ≫  End  ;
L07: Arbitrary ≫  X  ;

L03: Ded ⊳ L06 ≫

(S1ob)  ∈  N  ⇒

∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ constantRationalSeries(X) ;

L08: Gen ⊳ L03 ≫ ∀(S1ob): ((S1ob) ∈ N ⇒ ∃(S2ob): OrderedPair((S1ob), (S2ob)) ∈ constantRationalSeries(X)) ;

L09: CrsIsFunction ≫ isFunction(constantRationalSeries(X), N, Q)

; L10: JoinConjuncts ⊳ L09 ⊳ L08 ≫ IsSeries(constantRationalSeries(X), Q) □

[SystemQ lemma CrsLookup: ΠM, X: M ∈ N ⊢ constantRationalSeries(X)[M] = X]

SystemQ proof of CrsLookup:

L01: Arbitrary ≫  M, X  ;
L02: Premise ≫  M ∈ N  ;

L03: CrsIsSeries ≫ IsSeries(constantRationalSeries(X), Q)

;

L04: MemberOfSeries⊳L02⊳L03 ≫ OrderedPair(M, constantRationalSeries(X)[M]) ∈ constantRationalSeries(X) ;

L05: CrsIsTotal ⊳ L02 ≫ OrderedPair(M, X) ∈ constantRationalSeries(X)

;

L06: eqReflexivity ≫ M = M ;

L07: UniqueMember ⊳ L03 ⊳ L04 ⊳

L05 ⊳ L06 ≫ constantRationalSeries(X)[M] =

X □

[SystemQ lemma 0f: ΠM: M ∈ N ⊢ 0f[M] = 0]

SystemQ proof of 0f:

L01: Arbitrary ≫  M  ;
L02: Premise ≫  M ∈ N  ;

L03: CrsLookup ⊳ L02 ≫ constantRationalSeries(0)[M] = 0 ;

L04: Repetition ⊳ L03 ≫ 0f[M] = 0 □

[SystemQ lemma 1f: ΠM: M ∈ N ⊢ 1f[M] = 1]

SystemQ proof of 1f:

L01: Arbitrary ≫  M  ;
L02: Premise ≫  M ∈ N  ;

L03: CrsLookup ⊳ L02 ≫ constantRationalSeries(1)[M] = 1 ;

L04: Repetition ⊳ L03 ≫ 1f[M] = 1 □

——-(6.11.06, lemmaer fra kvanti, mod kronologien)

[SystemQ lemma DistributionOut: ΠX , Y, Z: ((X ∗ Y) + (X ∗ Z)) = (X ∗ ((Y + Z)))]

SystemQ proof of DistributionOut:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Distribution ≫  {(X ∗ ((Y + Z))) = ((X ∗ Y) + \atop (X ∗ Z))  ;}
L03: eqSymmetry ⊳ L02 ≫  {((X ∗Y)+(X ∗Z)) = (X ∗((Y + \atop Z)))  □}

[SystemQ lemma Three2twoTerms: ΠX , Y, Z, U: (Y + Z) = U ⊢ ((X + Y) + Z) = (X + U)]

SystemQ proof of Three2twoTerms:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  (Y + Z) = U  ;
L03: lemma eqAdditionLeft⊳L02 ≫ (X + ((Y + Z))) = (X + U)  ;

L04: plusAssociativity ≫  ((X +Y)+Z) = (X +((Y +Z))) ;
L05: eqTransitivity ⊳ L04 ⊳ L03 ≫ ((X + Y) + Z) = (X + U)  □

[SystemQ lemma Three2threeTerms: ΠX , Y, Z: ((X +Y)+Z) = ((X +Z)+ Y)]

SystemQ proof of Three2threeTerms:

L01: Arbitrary ≫  X , Y, Z  ;
L02: plusCommutativity ≫  (Y + Z) = (Z + Y)  ;
L03: Three2twoTerms ⊳ L02 ≫  ((X +Y)+Z) = (X +((Z +Y))) ;
L04: plusAssociativity ≫  ((X +Z)+Y) = (X +((Z +Y))) ;
L05: eqSymmetry ⊳ L04 ≫  (X +((Z +Y))) = ((X +Z)+Y) ;
L06: eqTransitivity ⊳ L03 ⊳ L05 ≫ ((X + Y) + Z) = ((X + Z) + Y) □

[SystemQ lemma Three2twoFactors: ΠX , Y, Z, U: (Y ∗ Z) = U ⊢ ((X ∗ Y) ∗ Z) = (X ∗ U)]

SystemQ proof of Three2twoFactors:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  (Y ∗ Z) = U  ;

L03: lemma eqMultiplicationLeft ⊳

L02 ≫ (X ∗ ((Y ∗ Z))) = (X ∗ U) ;

L04: timesAssociativity ≫  ((X ∗ Y) ∗ Z) = (X ∗ ((Y ∗ Z))) ;
L05: eqTransitivity ⊳ L04 ⊳ L03 ≫ ((X ∗ Y) ∗ Z) = (X ∗ U)  □

[SystemQ lemma x = x + (y − y): ΠX , Y: X = (X + ((Y − Y)))] SystemQ proof of x = x + (y − y):

L01: Arbitrary ≫  X , Y  ;
L02: plus0 ≫  (X + 0) = X  ;
L03: Negative ≫  (Y − Y) = 0  ;
L04: eqSymmetry ⊳ L03 ≫  0 = (Y − Y)  ;
L05: lemma eqAdditionLeft⊳L04 ≫ (X + 0) = (X + ((Y − Y)))  ;
L06: Equality ⊳ L02 ⊳ L05 ≫ X = (X + ((Y − Y))) □

[SystemQ lemma x = x + y − y: ΠX , Y: X = ((X + Y) − Y)]

SystemQ proof of x = x + y − y:

L01: Arbitrary ≫  X , Y  ;
L02: x = x + (y − y) ≫  X = (X + ((Y − Y)))  ;
L03: plusAssociativity ≫  ((X +Y)−Y) = (X +((Y −Y))) ;
L04: eqSymmetry ⊳ L03 ≫  (X +((Y −Y))) = ((X +Y)−Y) ;
L05: eqTransitivity ⊳ L02 ⊳ L04 ≫ X = ((X + Y) − Y)  □

[SystemQ lemma x = x ∗ y ∗ (1/y): ΠX , Y: Y ≠ 0 ⊢ X = ((X ∗ Y) ∗ recY)] SystemQ proof of x = x ∗ y ∗ (1/y):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  Y ≠ 0  ;
L03: times1 ≫  (X ∗ 1) = X  ;
L04: Reciprocal ⊳ L02 ≫  (Y ∗ recY) = 1  ;
L05: Three2twoFactors ⊳ L04 ≫  ((X ∗ Y) ∗ recY) = (X ∗ 1)  ;
L06: eqTransitivity ⊳ L05 ⊳ L03 ≫ ((X ∗ Y) ∗ recY) = X  ;
L07: eqSymmetry ⊳ L06 ≫ X = ((X ∗ Y) ∗ recY) □

[SystemQ lemma x ∗ 0 + x = x: ΠX: ((X ∗ 0) + X) = X]

SystemQ proof of x ∗ 0 + x = x:

L01: Arbitrary ≫  X  ;
L02: times1 ≫  (X ∗ 1) = X  ;
L03: eqSymmetry ⊳ L02 ≫  X = (X ∗ 1)  ;
L04: lemma eqAdditionLeft⊳L03 ≫ ((X ∗0)+X) = ((X ∗0)+(X ∗1)) ;
L05: Distribution ≫  (X ∗((0+1))) = ((X ∗0)+(X ∗1)) ;
L06: eqSymmetry ⊳ L05 ≫  ((X ∗0)+(X ∗1)) = (X ∗((0+1))) ;
L07: lemma plus0Left ≫ (0 + 1) = 1 ;

L08: lemma eqMultiplicationLeft ⊳

L07 ≫ (X ∗ ((0 + 1))) = (X ∗ 1) ;

L09: eqTransitivity5 ⊳ L04 ⊳ L06 ⊳

L08 ⊳ L02 ≫ ((X ∗ 0) + X) = X □

[SystemQ lemma x ∗ 0 = 0: ΠX: (X ∗ 0) = 0]

SystemQ proof of x ∗ 0 = 0:

L01: Arbitrary ≫ X ;
L02: x = x + (y − y) ≫  (X ∗ 0) = ((X ∗ 0) + ((X − X))) ;
L03: plusAssociativity ≫  {(((X ∗ 0) + X) − X) = ((X ∗ 0) + \atop ((X − X)))  ;}
L04: eqSymmetry ⊳ L03 ≫  {((X ∗ 0) + ((X − X))) = (((X ∗ \atop 0) + X) − X)  ;}
L05: x ∗ 0 + x = x ≫  ((X ∗ 0) + X) = X  ;
L06: eqAddition ⊳ L05 ≫  (((X ∗ 0) + X) − X) = (X − X) ;
L07: Negative ≫ (X − X) = 0 ;

L08: eqTransitivity5 ⊳ L02 ⊳ L04 ⊳

L06 ⊳ L07 ≫ (X ∗ 0) = 0 □

[SystemQ lemma (−1)∗(−1)+(−1)∗1 = 0: (((−1)∗(−1))+((−1)∗1)) = 0] SystemQ proof of (−1) ∗ (−1) + (−1) ∗ 1 = 0:

L01: DistributionOut ≫  {(((−1) ∗ (−1)) + ((−1) ∗ 1)) = \atop ((−1) ∗ (((−1) + 1)))  ;}
L02: Negative ≫  (1 + (−1)) = 0  ;
L03: plusCommutativity ≫  ((−1) + 1) = (1 + (−1))  ;
L04: eqTransitivity ⊳ L03 ⊳ L02 ≫ ((−1) + 1) = 0  ;

L05: lemma eqMultiplicationLeft ⊳

L04 ≫ ((−1)∗(((−1)+1))) = ((−1)∗0) ;

L06: x ∗ 0 = 0 ≫ ((−1) ∗ 0) = 0 ;

L07: eqTransitivity4 ⊳ L01 ⊳ L05 ⊳

L06 ≫ (((−1) ∗ (−1)) + ((−1) ∗ 1)) = 0 □

[SystemQ lemma (−1) ∗ (−1) = 1: ((−1) ∗ (−1)) = 1]

SystemQ proof of (−1) ∗ (−1) = 1:

L01: x = x + (y − y) ≫  {((−1)∗(−1)) = (((−1)∗(−1))+ \atop ((1 − 1)))  ;}
L02: times1 ≫  ((−1) ∗ 1) = (−1)  ;
L03: eqSymmetry ⊳ L02 ≫  (−1) = ((−1) ∗ 1)  ;
L04: lemma eqAdditionLeft⊳L03 ≫ (1 − 1) = (1 + ((−1) ∗ 1))  ;
L05: lemma eqAdditionLeft⊳L04 ≫ {(((−1) ∗ (−1)) + ((1 − 1))) = \atop (((−1)∗(−1))+((1+((−1)∗1)))) ;}
L06: plusCommutativity ≫  (1+((−1)∗1)) = (((−1)∗1)+1) ;

L07: lemma eqAdditionLeft⊳L06 ≫ (((−1) ∗ (−1)) + ((1 + ((−1) ∗ ; 1)))) = (((−1)∗(−1))+((((−1)∗ ; 1) + 1)))  ;

L08: plusAssociativity ≫  ((((−1) ∗ (−1)) + ((−1) ∗ 1)) + ; 1) = (((−1) ∗ (−1)) + ((((−1) ∗ ; 1) + 1)))  ;

L09: eqSymmetry ⊳ L08 ≫  (((−1) ∗ (−1)) + ((((−1) ∗ 1) + ; 1))) = ((((−1) ∗ (−1)) + ((−1) ∗ ; 1)) + 1)  ;

L10: (−1) ∗ (−1) + (−1) ∗ 1 = 0 ≫ (((−1) ∗ (−1)) + ((−1) ∗ 1)) = 0 ;
L11: eqAddition ⊳ L10 ≫  {((((−1) ∗ (−1)) + ((−1) ∗ 1)) + \atop 1) = (0 + 1)  ;}
L12: lemma plus0Left ≫  (0 + 1) = 1  ;

L13: eqTransitivity5 ⊳ L01 ⊳ L05 ⊳

L07 ⊳ L09 ≫ ((−1)∗(−1)) = ((((−1)∗(−1))+ ((−1) ∗ 1)) + 1) ;

L14: eqTransitivity4 ⊳ L13 ⊳ L11 ⊳

L12 ≫ ((−1) ∗ (−1)) = 1 □

[SystemQ lemma subLeqRight: ΠX , Y, Z: X = Y ⊢ Z <= X ⊢ Z <= Y] SystemQ proof of subLeqRight:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Z <= X  ;
L04: eqLeq ⊳ L02 ≫  X <= Y  ;
L05: leqTransitivity ⊳ L03 ⊳ L04 ≫ Z <= Y  □

[SystemQ lemma subLeqLeft: ΠX , Y, Z: X = Y ⊢ X <= Z ⊢ Y <= Z] SystemQ proof of subLeqLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  X <= Z  ;
L04: eqSymmetry ⊳ L02 ≫  Y = X  ;
L05: eqLeq ⊳ L04 ≫  Y <= X  ;
L06: leqTransitivity ⊳ L05 ⊳ L03 ≫ Y <= Z  □

[SystemQ lemma 0 < 1Helper: 1 <= 0 ⇒ 0 <= 1]

SystemQ proof of 0 < 1Helper:

L01: Block ≫  Begin  ;
L02: Premise ≫  1 <= 0  ;
L03: leqAddition ⊳ L02 ≫  (1 + (−1)) <= (0 + (−1))  ;
L04: Negative ≫  (1 + (−1)) = 0  ;
L05: subLeqLeft ⊳ L04 ⊳ L03 ≫  0 <= (0 + (−1))  ;
L06: lemma plus0Left ≫  (0 + (−1)) = (−1)  ;
L07: subLeqRight ⊳ L06 ⊳ L05 ≫  0 <= (−1)  ;
L08: leqMultiplication⊳L07⊳L07 ≫ (0 ∗ (−1)) <= ((−1) ∗ (−1))  ;
L09: x ∗ 0 = 0 ≫  ((−1) ∗ 0) = 0  ;
L10: timesCommutativity ≫  (0 ∗ (−1)) = ((−1) ∗ 0)  ;

L11: eqTransitivity ⊳ L10 ⊳ L09 ≫ (0 ∗ (−1)) = 0  ;
L12: subLeqLeft ⊳ L11 ⊳ L08 ≫  0 <= ((−1) ∗ (−1))  ;
L13: (−1) ∗ (−1) = 1 ≫  ((−1) ∗ (−1)) = 1  ;
L14: subLeqRight ⊳ L13 ⊳ L12 ≫  0 <= 1  ;
L15: Block ≫  End  ;
L16: Ded ⊳ L15 ≫  1 <= 0 ⇒ 0 <= 1  □

[SystemQ lemma 0 < 1: 0 < 1]

SystemQ proof of 0 < 1:

L01: leqTotality ≫  0 <= 1 ˙∨ 1 <= 0  ;
L02: AutoImply ≫  0 <= 1 ⇒ 0 <= 1  ;
L03: 0 < 1Helper ≫  1 <= 0 ⇒ 0 <= 1  ;

L04: FromDisjuncts ⊳ L01 ⊳ L02 ⊳

L03 ≫ 0 <= 1 ;

L05: 0not1 ≫ 0 ≠ 1 ;
L06: JoinConjuncts ⊳ L04 ⊳ L05 ≫ 0 < 1  □

[SystemQ lemma AddEquations: ΠX , Y, Z, U: X = Y ⊢ Z = U ⊢ (X +Z) = (Y + U)]

SystemQ proof of AddEquations:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Z = U  ;
L04: eqAddition ⊳ L02 ≫  (X + Z) = (Y + Z)  ;
L05: lemma eqAdditionLeft⊳L03 ≫ (Y + Z) = (Y + U)  ;
L06: eqTransitivity ⊳ L04 ⊳ L05 ≫ (X + Z) = (Y + U)  □

[SystemQ lemma SubtractEquations: ΠX , Y, Z, U: (X + Z) = (Y + U) ⊢ Z = U ⊢ X = Y]

SystemQ proof of SubtractEquations:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  (X + Z) = (Y + U)  ;
L03: Premise ≫  Z = U  ;
L04: eqAddition ⊳ L02 ≫  ((X + Z) − Z) = ((Y + U) − Z) ;
L05: lemma plus0Left ≫ (0 + Z) = Z ;
L06: eqTransitivity ⊳ L05 ⊳ L03 ≫ (0 + Z) = U  ;
L07: PositiveToRight(Eq) ⊳ L06 ≫ 0 = (U − Z)  ;
L08: eqSymmetry ⊳ L07 ≫ (U − Z) = 0 ;
L09: lemma eqAdditionLeft⊳L08 ≫ (Y + ((U − Z))) = (Y + 0)  ;
L10: plusAssociativity ≫  ((Y +U)−Z) = (Y +((U −Z))) ;
L11: plus0 ≫ (Y + 0) = Y ;

L12: eqTransitivity4 ⊳ L10 ⊳ L09 ⊳

L11 ≫ ((Y + U) − Z) = Y ;

L13: x = x + y − y ≫ X = ((X + Z) − Z) ;

L14: eqTransitivity4 ⊳ L13 ⊳ L04 ⊳

L12 ≫ X = Y □

[SystemQ lemma SubtractEquationsLeft: ΠX , Y, Z, U: (X +Z) = (Y +U) ⊢ X = Y ⊢ Z = U]

SystemQ proof of SubtractEquationsLeft:

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  (X + Z) = (Y + U)  ;
L03: Premise ≫  X = Y  ;
L04: plusCommutativity ≫  (Z + X) = (X + Z)  ;
L05: plusCommutativity ≫  (Y + U) = (U + Y)  ;

L06: eqTransitivity4 ⊳ L04 ⊳ L02 ⊳

L05 ≫ (Z + X) = (U + Y) ;

L07: SubtractEquations ⊳ L06 ⊳

L03 ≫ Z = U □

[SystemQ lemma EqNegated: ΠX , Y: X = Y ⊢ (−uX) = (−uY)] SystemQ proof of EqNegated:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X = Y  ;
L03: Negative ≫  (X − X) = 0  ;
L04: Negative ≫  (Y − Y) = 0  ;
L05: eqSymmetry ⊳ L04 ≫  0 = (Y − Y)  ;
L06: eqTransitivity ⊳ L03 ⊳ L05 ≫ (X − X) = (Y − Y)  ;

L07: SubtractEquationsLeft ⊳ L06 ⊳

L02 ≫ (−uX) = (−uY) □

[SystemQ lemma PositiveToRight(Eq): ΠX , Y, Z: (X +Y) = Z ⊢ X = (Z − Y)]

SystemQ proof of PositiveToRight(Eq):

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  (X + Y) = Z  ;
L03: eqAddition ⊳ L02 ≫  ((X + Y) − Y) = (Z − Y)  ;
L04: x = x + y − y ≫  X = ((X + Y) − Y)  ;
L05: eqTransitivity ⊳ L04 ⊳ L03 ≫ X = (Z − Y)  □

[SystemQ lemma PositiveToLeft(Eq)(1term): ΠX , Y: X = Y ⊢ (X −Y) = 0] SystemQ proof of PositiveToLeft(Eq)(1term):

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X = Y  ;
L03: eqAddition ⊳ L02 ≫  (X − Y) = (Y − Y)  ;
L04: Negative ≫  (Y − Y) = 0  ;
L05: eqTransitivity ⊳ L03 ⊳ L04 ≫ (X − Y) = 0  □

[SystemQ lemma PositiveToRight(Leq): ΠX , Y, Z: (X + Y) <= Z ⊢ X <= (Z − Y)]

SystemQ proof of PositiveToRight(Leq):

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  (X + Y) <= Z  ;
L03: leqAddition ⊳ L02 ≫  ((X + Y) − Y) <= (Z − Y)  ;
L04: x = x + y − y ≫  X = ((X + Y) − Y)  ;
L05: eqSymmetry ⊳ L04 ≫  ((X + Y) − Y) = X  ;
L06: subLeqLeft ⊳ L05 ⊳ L03 ≫  X <= (Z − Y)  □

[SystemQ lemma PositiveToRight(Leq)(1term): ΠY, Z: Y <= Z ⊢ 0 <= (Z − Y)]

SystemQ proof of PositiveToRight(Leq)(1term):

L01: Arbitrary ≫  Y, Z  ;
L02: Premise ≫  Y <= Z  ;
L03: lemma plus0Left ≫  (0 + Y) = Y  ;
L04: eqSymmetry ⊳ L03 ≫  Y = (0 + Y)  ;
L05: subLeqLeft ⊳ L04 ⊳ L02 ≫  (0 + Y) <= Z  ;
L06: PositiveToRight(Leq) ⊳ L05 ≫ 0 <= (Z − Y)  □

[SystemQ lemma NegativeToLeft(Eq): ΠX , Y, Z: X = (Y −Z) ⊢ (X +Z) = Y]

SystemQ proof of NegativeToLeft(Eq):

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = (Y − Z)  ;
L03: eqAddition ⊳ L02 ≫  (X + Z) = ((Y − Z) + Z)  ;
L04: Three2threeTerms ≫  ((Y − Z) + Z) = ((Y + Z) − Z) ;
L05: x = x + y − y ≫  Y = ((Y + Z) − Z)  ;
L06: eqSymmetry ⊳ L05 ≫  ((Y + Z) − Z) = Y  ;

L07: eqTransitivity4 ⊳ L03 ⊳ L04 ⊳

L06 ≫ (X + Z) = Y □

(*** NO EQUALITY ***)

[SystemQ lemma LessNeq: ΠX , Y: X < Y ⊢ X ≠ Y]

SystemQ proof of LessNeq:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X < Y  ;
L03: Repetition ⊳ L02 ≫  X <= Y ˙∧ ˙¬ ((X = Y))n  ;
L04: SecondConjunct ⊳ L03 ≫  X ≠ Y  □

[SystemQ lemma x + y = zBackwards: ΠX , Y, Z: (X + Y) = Z ⊢ Z = (Y + X)]

SystemQ proof of x + y = zBackwards:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  (X + Y) = Z  ;
L03: plusCommutativity ≫  (X + Y) = (Y + X)  ;
L04: Equality ⊳ L02 ≫  Z = (Y + X)  □

[SystemQ lemma x∗y = zBackwards: ΠX , Y, Z: (X ∗Y) = Z ⊢ Z = (Y ∗X)] SystemQ proof of x ∗ y = zBackwards:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  (X ∗ Y) = Z  ;
L03: timesCommutativity ≫  (X ∗ Y) = (Y ∗ X)  ;
L04: Equality ⊳ L02 ≫  Z = (Y ∗ X)  □

[SystemQ lemma DoubleMinus: ΠX: (−u(−uX)) = X]

SystemQ proof of DoubleMinus:

L01: Arbitrary ≫  X  ;
L02: Negative ≫  ((−uX) − (−uX)) = 0  ;
L03: x + y = zBackwards ⊳ L02 ≫ 0 = ((−u(−uX)) − X)  ;
L04: NegativeToLeft(Eq) ⊳ L03 ≫ (0 + X) = (−u(−uX))  ;
L05: lemma plus0Left ≫  (0 + X) = X  ;
L06: Equality ⊳ L04 ⊳ L05 ≫  (−u(−uX)) = X  □

[SystemQ lemma NeqNegated: ΠX , Y: X ≠ Y ⊢ (−uX) ≠ (−uY)]

SystemQ proof of NeqNegated:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  X ≠ Y  ;
L04: Premise ≫  (−uX) = (−uY)  ;
L05: EqNegated ⊳ L04 ≫  (−u(−uX)) = (−u(−uY))  ;
L06: DoubleMinus ≫  (−u(−uX)) = X  ;
L07: eqSymmetry ⊳ L06 ≫  X = (−u(−uX))  ;
L08: DoubleMinus ≫  (−u(−uY)) = Y  ;

L09: eqTransitivity4 ⊳ L07 ⊳ L05 ⊳

L08 ≫ X = Y ;

L10: FromContradiction ⊳ L09 ⊳

L03 ≫ (−uX) ≠ (−uY) ;

L11: Block ≫  End  ;
L12: Arbitrary ≫  X , Y  ;
L13: Ded ⊳ L11 ≫  {X ≠ Y ⇒ (−uX) = (−uY) ⇒ \atop ˙¬ ((−uX) = (−uY))n  ;}
L14: Premise ≫  X ≠ Y  ;
L15: MP ⊳ L13 ⊳ L14 ≫  {(−uX)  =  (−uY)  ⇒ \atop ˙¬ ((−uX) = (−uY))n  ;}

L16: prop lemma imply negation ⊳

L15 ≫ ˙¬ ((−uX) = (−uY))n □

[SystemQ lemma SubNeqRight: ΠX , Y, Z: X = Y ⊢ Z ≠ X ⊢ Z ≠ Y] SystemQ proof of SubNeqRight:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Z ≠ X  ;
L04: NeqSymmetry ⊳ L03 ≫  X ≠ Z  ;
L05: SubNeqLeft ⊳ L02 ⊳ L04 ≫  Y ≠ Z  ;
L06: NeqSymmetry ⊳ L05 ≫  Z ≠ Y  □

[SystemQ lemma NeqAddition: ΠX , Y, Z: X ≠ Y ⊢ (X + Z) ≠ (Y + Z)] SystemQ proof of NeqAddition:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y, Z  ;
L03: Premise ≫  X ≠ Y  ;
L04: Premise ≫  (X + Z) = (Y + Z)  ;
L05: eqReflexivity ≫  Z = Z  ;

L06: SubtractEquations ⊳ L04 ⊳

L05 ≫ X = Y ;

L07: FromContradiction ⊳ L06 ⊳

L03 ≫ (X + Z) ≠ (Y + Z) ;

L08: Block ≫  End  ;
L09: Arbitrary ≫  X , Y, Z  ;
L10: Ded ⊳ L08 ≫  {X ≠ Y ⇒ (X +Z) = (Y +Z) ⇒ \atop (X + Z) ≠ (Y + Z)  ;}
L11: Premise ≫  X ≠ Y  ;

L12: MP ⊳ L10 ⊳ L11 ≫  {(X +Z) = (Y +Z) ⇒ (X +Z) ≠ \atop (Y + Z)  ;}

L13: prop lemma imply negation ⊳

L12 ≫ (X + Z) ≠ (Y + Z) □

[SystemQ lemma NeqMultiplication: ΠX , Y, Z: Z ≠ 0 ⊢ X ≠ Y ⊢ (X ∗Z) ≠ (Y ∗ Z)]

SystemQ proof of NeqMultiplication:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y, Z  ;
L03: Premise ≫  Z ≠ 0  ;
L04: Premise ≫  X ≠ Y  ;
L05: Premise ≫  (X ∗ Z) = (Y ∗ Z)  ;
L06: x = x ∗ y ∗ (1/y) ⊳ L03 ≫  X = ((X ∗ Z) ∗ recZ)  ;
L07: eqMultiplication ⊳ L05 ≫  {((X ∗ Z) ∗ recZ) = ((Y ∗ Z) ∗ \atop recZ)  ;}
L08: x = x ∗ y ∗ (1/y) ⊳ L03 ≫  Y = ((Y ∗ Z) ∗ recZ)  ;
L09: eqSymmetry ⊳ L08 ≫  ((Y ∗ Z) ∗ recZ) = Y  ;

L10: eqTransitivity4 ⊳ L06 ⊳ L07 ⊳

L09 ≫ X = Y ;

L11: FromContradiction ⊳ L10 ⊳

L04 ≫ (X ∗ Z) ≠ (Y ∗ Z) ;

L12: Block ≫  End  ;
L13: Arbitrary ≫  X , Y, Z  ;
L14: Ded ⊳ L12 ≫  {Z ≠ 0 ⇒ X ≠ Y ⇒ (X ∗ Z) = \atop (Y ∗ Z) ⇒ (X ∗ Z) ≠ (Y ∗ Z) ;}
L15: Premise ≫  Z ≠ 0  ;
L16: Premise ≫  X ≠ Y  ;
L17: MP2 ⊳ L14 ⊳ L15 ⊳ L16 ≫  {(X ∗ Z) = (Y ∗ Z) ⇒ (X ∗ Z) ≠ \atop (Y ∗ Z)  ;}

L18: prop lemma imply negation ⊳

L17 ≫ (X ∗ Z) ≠ (Y ∗ Z) □

(*** NEGATIVE ***)

[SystemQ lemma UniqueNegative: ΠX , Y, Z: (X + Y) = 0 ⊢ (X + Z) = 0 ⊢ Y = Z]

SystemQ proof of UniqueNegative:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  (X + Y) = 0  ;
L03: Premise ≫  (X + Z) = 0  ;
L04: plusCommutativity ≫  (Y + X) = (X + Y)  ;
L05: eqTransitivity ⊳ L04 ⊳ L02 ≫ (Y + X) = 0  ;
L06: PositiveToRight(Eq) ⊳ L05 ≫ Y = (0 − X)  ;
L07: plusCommutativity ≫ (Z + X) = (X + Z) ;
L08: eqTransitivity ⊳ L07 ⊳ L03 ≫ (Z + X) = 0  ;
L09: PositiveToRight(Eq) ⊳ L08 ≫ Z = (0 − X)  ;
L10: eqSymmetry ⊳ L09 ≫ (0 − X) = Z ;
L11: eqTransitivity ⊳ L06 ⊳ L10 ≫ Y = Z  □

[SystemQ lemma FromLess: ΠX , Y: X < Y ⊢ ˙¬ (Y <= X)n] SystemQ proof of FromLess:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  Y <= X  ;
L04: toNotLess ⊳ L03 ≫  ˙¬ (X < Y)n  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  X , Y  ;
L07: Ded ⊳ L05 ≫  Y <= X ⇒ ˙¬ (X < Y)n  ;
L08: Premise ≫  X < Y  ;
L09: AddDoubleNeg ⊳ L08 ≫  ˙¬ ( ˙¬ (X < Y)n)n  ;
L10: MT ⊳ L07 ⊳ L09 ≫  ˙¬ (Y <= X)n  □

[SystemQ lemma ToLess: ΠX , Y: ˙¬ (X <= Y)n ⊢ Y < X] SystemQ proof of ToLess:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  ˙¬ (Y < X)n  ;
L04: fromNotLess ⊳ L03 ≫  X <= Y  ;
L05: Block ≫  End  ;
L06: Arbitrary ≫  X , Y  ;
L07: Ded ⊳ L05 ≫  ˙¬ (Y < X)n ⇒ X <= Y  ;
L08: Premise ≫  ˙¬ (X <= Y)n  ;
L09: NegativeMT ⊳ L07 ⊳ L08 ≫  Y < X  □

[SystemQ lemma fromNotLess: ΠX , Y: ˙¬ ((X < Y))n ⊢ Y <= X] SystemQ proof of fromNotLess:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  ˙¬ ((X < Y))n  ;
L04: Premise ≫  X <= Y  ;
L05: Repetition ⊳ L03 ≫  {˙¬ ( ˙¬ ((X <= Y ⇒ ˙¬ (X ≠ \atop Y)n))n)n  ;}
L06: RemoveDoubleNeg ⊳ L05 ≫  X <= Y ⇒ ˙¬ (X ≠ Y)n  ;
L07: MP ⊳ L06 ⊳ L04 ≫  ˙¬ (X ≠ Y)n  ;
L08: RemoveDoubleNeg ⊳ L07 ≫  X = Y  ;
L09: eqSymmetry ⊳ L08 ≫  Y = X  ;
L10: eqLeq ⊳ L09 ≫  Y <= X  ;
L11: Block ≫  End  ;
L12: Arbitrary ≫  X , Y  ;
L13: Ded ⊳ L11 ≫  {˙¬ (X < Y)n ⇒ X <= Y ⇒ \atop Y <= X  ;}
L14: Premise ≫  ˙¬ (X < Y)n  ;
L15: MP ⊳ L13 ⊳ L14 ≫  X <= Y ⇒ Y <= X  ;
L16: AutoImply ≫  Y <= X ⇒ Y <= X  ;
L17: leqTotality ≫  X <= Y ˙∨ Y <= X  ;

L18: FromDisjuncts ⊳ L17 ⊳ L15 ⊳

L16 ≫ Y <= X □

[SystemQ lemma toNotLess: ΠX , Y: X <= Y ⊢ ˙¬ (Y < X)n]

SystemQ proof of toNotLess:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  X <= Y  ;
L04: Premise ≫  Y <= X  ;
L05: leqAntisymmetry⊳L04⊳L03 ≫ Y = X  ;
L06: AddDoubleNeg ⊳ L05 ≫  ˙¬ ( ˙¬ (Y = X)n)n  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  X , Y  ;
L09: Ded ⊳ L07 ≫  {X <= Y ⇒ Y <= X ⇒ \atop ˙¬ ( ˙¬ (Y = X)n)n  ;}
L10: Premise ≫  X <= Y  ;
L11: MP ⊳ L09 ⊳ L10 ≫  Y <= X ⇒ ˙¬ ( ˙¬ (Y = X)n)n  ;
L12: AddDoubleNeg ⊳ L11 ≫  {˙¬ ( ˙¬ ((Y <= X ⇒ ˙¬ ( ˙¬ (Y = \atop X)n)n))n)n  ;}
L13: Repetition ⊳ L12 ≫  ˙¬ ((Y <= X ˙∧ ˙¬ (Y = X)n))n ;
L14: Repetition ⊳ L13 ≫  ˙¬ (Y < X)n  □

(*** LEQ ***)

[SystemQ lemma LeqLessEq: ΠX , Y: X <= Y ⊢ X < Y ˙∨ X = Y] SystemQ proof of LeqLessEq:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  X <= Y  ;
L04: Premise ≫  ˙¬ (X < Y)n  ;
L05: fromNotLess ⊳ L04 ≫  Y <= X  ;
L06: leqAntisymmetry⊳L03⊳L05 ≫ X = Y  ;
L07: Block ≫  End  ;
L08: Arbitrary ≫  X , Y  ;
L09: Ded ⊳ L07 ≫  {X <= Y ⇒ ˙¬ (X < Y)n ⇒ \atop X = Y  ;}
L10: Premise ≫  X <= Y  ;
L11: MP ⊳ L09 ⊳ L10 ≫  ˙¬ (X < Y)n ⇒ X = Y  ;
L12: Repetition ⊳ L11 ≫  X < Y ˙∨ X = Y  □

[SystemQ lemma LessLeq: ΠX , Y: X < Y ⊢ X <= Y]

SystemQ proof of LessLeq:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X < Y  ;
L03: Repetition ⊳ L02 ≫  X <= Y ˙∧ ˙¬ ((X = Y))n  ;
L04: FirstConjunct ⊳ L03 ≫  X <= Y  □

[SystemQ lemma FromLeqGeq: ΠA, X , Y: X <= Y ⇒ A ⊢ Y <= X ⇒ A ⊢ A]

SystemQ proof of FromLeqGeq:

L01: Arbitrary ≫  A, X , Y  ;

L02: Premise ≫  X <= Y ⇒ A  ;
L03: Premise ≫  Y <= X ⇒ A  ;
L04: leqTotality ≫  X <= Y ˙∨ Y <= X  ;

L05: FromDisjuncts ⊳ L04 ⊳ L02 ⊳

L03 ≫ A □

[SystemQ lemma SubLessRight: ΠX , Y, Z: X = Y ⊢ Z < X ⊢ Z < Y] SystemQ proof of SubLessRight:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  Z < X  ;
L04: Repetition ⊳ L03 ≫  Z <= X ˙∧ Z ≠ X  ;
L05: FirstConjunct ⊳ L04 ≫  Z <= X  ;
L06: subLeqRight ⊳ L02 ⊳ L05 ≫  Z <= Y  ;
L07: SecondConjunct ⊳ L04 ≫  Z ≠ X  ;
L08: SubNeqRight ⊳ L02 ⊳ L07 ≫  Z ≠ Y  ;
L09: JoinConjuncts ⊳ L06 ⊳ L08 ≫ Z < Y  □

[SystemQ lemma SubLessLeft: ΠX , Y, Z: X = Y ⊢ X < Z ⊢ Y < Z] SystemQ proof of SubLessLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X = Y  ;
L03: Premise ≫  X < Z  ;
L04: Repetition ⊳ L03 ≫  X <= Z ˙∧ X ≠ Z  ;
L05: FirstConjunct ⊳ L04 ≫  X <= Z  ;
L06: subLeqLeft ⊳ L02 ⊳ L05 ≫  Y <= Z  ;
L07: SecondConjunct ⊳ L04 ≫  X ≠ Z  ;
L08: SubNeqLeft ⊳ L02 ⊳ L07 ≫  Y ≠ Z  ;
L09: JoinConjuncts ⊳ L06 ⊳ L08 ≫ Y < Z  □

[SystemQ lemma leqLessTransitivity: ΠX , Y, Z: X <= Y ⊢ Y < Z ⊢ X < Z]

SystemQ proof of leqLessTransitivity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y, Z  ;
L03: Premise ≫  X <= Y  ;
L04: Premise ≫  Y < Z  ;
L05: Premise ≫  X = Z  ;
L06: FirstConjunct ⊳ L04 ≫  Y <= Z  ;
L07: SecondConjunct ⊳ L04 ≫  Y ≠ Z  ;
L08: subLeqLeft ⊳ L05 ⊳ L03 ≫  Z <= Y  ;
L09: leqAntisymmetry⊳L06⊳L08 ≫ Y = Z  ;

L10: FromContradiction ⊳ L09 ⊳

L07 ≫ X ≠ Z ;

L11: Block ≫  End  ;
L12: Arbitrary ≫  X , Y, Z  ;
L13: Ded ⊳ L11 ≫  {X <= Y ⇒ Y < Z ⇒ X = \atop Z ⇒ X ≠ Z  ;}

L14: Premise ≫  X <= Y  ;
L15: Premise ≫  Y < Z  ;
L16: MP2 ⊳ L13 ⊳ L14 ⊳ L15 ≫  X = Z ⇒ X ≠ Z  ;

L17: prop lemma imply negation ⊳

L16 ≫ X ≠ Z ;

L18: FirstConjunct ⊳ L15 ≫ Y <= Z ;
L19: leqTransitivity ⊳ L14 ⊳ L18 ≫ X <= Z  ;
L20: JoinConjuncts ⊳ L19 ⊳ L17 ≫ X < Z  □

[SystemQ lemma LessAddition: ΠX , Y, Z: X < Y ⊢ (X + Z) < (Y + Z)] SystemQ proof of LessAddition:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X < Y  ;
L03: LessLeq ⊳ L02 ≫  X <= Y  ;
L04: leqAddition ⊳ L03 ≫  (X + Z) <= (Y + Z)  ;
L05: LessNeq ⊳ L02 ≫  X ≠ Y  ;
L06: NeqAddition ⊳ L05 ≫  (X + Z) ≠ (Y + Z)  ;
L07: JoinConjuncts ⊳ L04 ⊳ L06 ≫ (X + Z) < (Y + Z)  □

[SystemQ lemma LessAdditionLeft: ΠX , Y, Z: X < Y ⊢ (Z +X) < (Z +Y)] SystemQ proof of LessAdditionLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X < Y  ;
L03: LessAddition ⊳ L02 ≫  (X + Z) < (Y + Z)  ;
L04: plusCommutativity ≫  (X + Z) = (Z + X)  ;
L05: SubLessLeft ⊳ L04 ⊳ L03 ≫  (Z + X) < (Y + Z)  ;
L06: plusCommutativity ≫  (Y + Z) = (Z + Y)  ;
L07: SubLessRight ⊳ L06 ⊳ L05 ≫ (Z + X) < (Z + Y)  □

[SystemQ lemma Leq + 1: ΠX , Y: X <= Y ⊢ X < (Y + 1)]

SystemQ proof of Leq + 1:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X <= Y  ;
L03: 0 < 1 ≫  0 < 1  ;
L04: LessAdditionLeft ⊳ L03 ≫  (Y + 0) < (Y + 1)  ;
L05: plus0 ≫  (Y + 0) = Y  ;
L06: SubLessLeft ⊳ L05 ⊳ L04 ≫  Y < (Y + 1)  ;

L07: leqLessTransitivity ⊳ L02 ⊳

L06 ≫ X < (Y + 1) □

[SystemQ lemma LeqAdditionLeft: ΠX , Y, Z: X <= Y ⊢ (Z + X) <= (Z + Y)]

SystemQ proof of LeqAdditionLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X <= Y  ;
L03: leqAddition ⊳ L02 ≫  (X + Z) <= (Y + Z)  ;
L04: plusCommutativity ≫  (X + Z) = (Z + X)  ;
L05: plusCommutativity ≫  (Y + Z) = (Z + Y)  ;
L06: subLeqLeft ⊳ L04 ⊳ L03 ≫  (Z + X) <= (Y + Z)  ;
L07: subLeqRight ⊳ L05 ⊳ L06 ≫  (Z + X) <= (Z + Y)  □

[SystemQ lemma leqSubtraction: ΠX , Y, Z: (X + Z) <= (Y + Z) ⊢ X <= Y]

SystemQ proof of leqSubtraction:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  (X + Z) <= (Y + Z)  ;
L03: leqAddition ⊳ L02 ≫  ((X +Z)−Z) <= ((Y +Z)−Z) ;
L04: x = x + y − y ≫  X = ((X + Z) − Z)  ;
L05: eqSymmetry ⊳ L04 ≫  ((X + Z) − Z) = X  ;
L06: x = x + y − y ≫  Y = ((Y + Z) − Z)  ;
L07: eqSymmetry ⊳ L06 ≫  ((Y + Z) − Z) = Y  ;
L08: subLeqLeft ⊳ L05 ⊳ L03 ≫  X <= ((Y + Z) − Z)  ;
L09: subLeqRight ⊳ L07 ⊳ L08 ≫  X <= Y  □

[SystemQ lemma leqSubtractionLeft: ΠX , Y, Z: (Z + X) <= (Z + Y) ⊢ X <= Y]

SystemQ proof of leqSubtractionLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  (Z + X) <= (Z + Y)  ;
L03: plusCommutativity ≫  (Z + X) = (X + Z)  ;
L04: plusCommutativity ≫  (Z + Y) = (Y + Z)  ;
L05: subLeqLeft ⊳ L03 ⊳ L02 ≫  (X + Z) <= (Z + Y)  ;
L06: subLeqRight ⊳ L04 ⊳ L05 ≫  (X + Z) <= (Y + Z)  ;
L07: leqSubtraction ⊳ L06 ≫  X <= Y  □

[SystemQ lemma negativeToLeft(Leq): ΠX , Y, Z: X <= (Y − Z) ⊢ (X + Z) <= Y]

SystemQ proof of negativeToLeft(Leq):

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X <= (Y − Z)  ;
L03: leqAddition ⊳ L02 ≫  (X + Z) <= ((Y − Z) + Z)  ;
L04: x = x + y − y ≫  Y = ((Y + Z) − Z)  ;
L05: Three2threeTerms ≫  ((Y + Z) − Z) = ((Y − Z) + Z) ;
L06: eqTransitivity ⊳ L04 ⊳ L05 ≫ Y = ((Y − Z) + Z)  ;
L07: eqSymmetry ⊳ L06 ≫  ((Y − Z) + Z) = Y  ;
L08: subLeqRight ⊳ L07 ⊳ L03 ≫  (X + Z) <= Y  □

[SystemQ lemma thirdGeq: ΠX , Y: X <= Ex3 ˙∧ Y <= Ex3]

SystemQ proof of thirdGeq:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  X <= Y  ;
L04: leqReflexivity ≫  Y <= Y  ;
L05: JoinConjuncts ⊳ L03 ⊳ L04 ≫ X <= Y ˙∧ Y <= Y  ;
L06: ExistIntro @ Ex3 @ Y ⊳ L05 ≫ X <= Ex3 ˙∧ Y <= Ex3  ;
L07: Block ≫  End  ;
L08: Block ≫  Begin  ;
L09: Arbitrary ≫  X , Y  ;
L10: Premise ≫  Y <= X  ;
L11: leqReflexivity ≫  X <= X  ;

L12: JoinConjuncts ⊳ L11 ⊳ L10 ≫ X <= X ˙∧ Y <= X  ;
L13: ExistIntro @ Ex3 @ X ⊳ L12 ≫ X <= Ex3 ˙∧ Y <= Ex3  ;
L14: Block ≫  End  ;
L15: Arbitrary ≫  X , Y  ;
L16: Ded ⊳ L07 ≫  {X <= Y ⇒ X <= Ex3 ˙∧ Y <= \atop Ex3  ;}
L17: Ded ⊳ L14 ≫  {Y <= X ⇒ X <= Ex3 ˙∧ Y <= \atop Ex3  ;}
L18: leqTotality ≫  X <= Y ˙∨ Y <= X  ;

L19: FromDisjuncts ⊳ L18 ⊳ L16 ⊳

L17 ≫ X <= Ex3 ˙∧ Y <= Ex3 □

[SystemQ lemma LeqNegated: ΠX , Y: X <= Y ⊢ (−uY) <= (−uX)] SystemQ proof of LeqNegated:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X <= Y  ;
L03: leqAddition ⊳ L02 ≫  (X − X) <= (Y − X)  ;
L04: Negative ≫  (X − X) = 0  ;
L05: subLeqLeft ⊳ L04 ⊳ L03 ≫  0 <= (Y − X)  ;
L06: plusCommutativity ≫  (Y − X) = ((−uX) + Y)  ;
L07: subLeqRight ⊳ L06 ⊳ L05 ≫  0 <= ((−uX) + Y)  ;
L08: leqAddition ⊳ L07 ≫  (0 − Y) <= (((−uX) + Y) − Y) ;
L09: lemma plus0Left ≫  (0 − Y) = (−uY)  ;
L10: x = x + y − y ≫  (−uX) = (((−uX) + Y) − Y)  ;
L11: eqSymmetry ⊳ L10 ≫  (((−uX) + Y) − Y) = (−uX)  ;
L12: subLeqLeft ⊳ L09 ⊳ L08 ≫  (−uY) <= (((−uX) + Y) − Y) ;
L13: subLeqRight ⊳ L11 ⊳ L12 ≫ (−uY) <= (−uX) □

[SystemQ lemma AddEquations(Leq): ΠX , Y, Z, U: X <= Y ⊢ Z <= U ⊢ (X + Z) <= (Y + U)]

SystemQ proof of AddEquations(Leq):

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  X <= Y  ;
L03: Premise ≫  Z <= U  ;
L04: leqAddition ⊳ L02 ≫  (X + Z) <= (Y + Z)  ;
L05: LeqAdditionLeft ⊳ L03 ≫  (Y + Z) <= (Y + U)  ;
L06: leqTransitivity ⊳ L04 ⊳ L05 ≫ (X + Z) <= (Y + U)  □

(*** LESS ***)

[SystemQ lemma LeqNeqLess: ΠX , Y: X <= Y ⊢ X ≠ Y ⊢ X < Y] SystemQ proof of LeqNeqLess:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X <= Y  ;
L03: Premise ≫  X ≠ Y  ;
L04: JoinConjuncts ⊳ L02 ⊳ L03 ≫ X <= Y ˙∧ X ≠ Y  ;
L05: Repetition ⊳ L04 ≫ X < Y □

[SystemQ lemma LessMultiplication: ΠX , Y, Z: 0 < Z ⊢ X < Y ⊢ (X ∗ Z) < (Y ∗ Z)]

SystemQ proof of LessMultiplication:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  0 < Z  ;
L03: Premise ≫  X < Y  ;
L04: LessLeq ⊳ L03 ≫  X <= Y  ;
L05: LessLeq ⊳ L02 ≫  0 <= Z  ;
L06: leqMultiplication⊳L05⊳L04 ≫ (X ∗ Z) <= (Y ∗ Z)  ;
L07: LessNeq ⊳ L03 ≫  X ≠ Y  ;
L08: LessNeq ⊳ L02 ≫  0 ≠ Z  ;
L09: NeqSymmetry ⊳ L08 ≫  Z ≠ 0  ;

L10: NeqMultiplication ⊳ L09 ⊳

L07 ≫ (X ∗ Z) ≠ (Y ∗ Z) ;

L11: LeqNeqLess ⊳ L06 ⊳ L10 ≫ (X ∗ Z) < (Y ∗ Z) □

[SystemQ lemma LessMultiplicationLeft: ΠX , Y, Z: 0 < Z ⊢ X < Y ⊢ (Z ∗ X) < (Z ∗ Y)]

SystemQ proof of LessMultiplicationLeft:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  0 < Z  ;
L03: Premise ≫  X < Y  ;

L04: LessMultiplication ⊳ L02 ⊳

L03 ≫ (X ∗ Z) < (Y ∗ Z) ;

L05: timesCommutativity ≫  (X ∗ Z) = (Z ∗ X)  ;
L06: timesCommutativity ≫  (Y ∗ Z) = (Z ∗ Y)  ;
L07: SubLessLeft ⊳ L05 ⊳ L04 ≫  (Z ∗ X) < (Y ∗ Z)  ;
L08: SubLessRight ⊳ L06 ⊳ L07 ≫ (Z ∗ X) < (Z ∗ Y)  □

[SystemQ lemma LessDivision: ΠX , Y, Z: 0 <= Z ⊢ (X ∗ Z) < (Y ∗ Z) ⊢ X < Y]

SystemQ proof of LessDivision:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  0 <= Z  ;
L03: Premise ≫  (X ∗ Z) < (Y ∗ Z)  ;
L04: FromLess ⊳ L03 ≫  ˙¬ ((Y ∗ Z) <= (X ∗ Z))n  ;
L05: leqMultiplicationAxiom ≫  {0 <= Z ⇒ Y <= X ⇒ (Y ∗ \atop Z) <= (X ∗ Z)  ;}
L06: MP ⊳ L05 ⊳ L02 ≫  Y <= X ⇒ (Y ∗ Z) <= (X ∗ Z) ;
L07: Contrapositive ⊳ L06 ≫  {˙¬ ((Y ∗ Z) <= (X ∗ Z))n ⇒ \atop ˙¬ (Y <= X)n  ;}
L08: MP ⊳ L07 ⊳ L04 ≫  ˙¬ (Y <= X)n  ;
L09: ToLess ⊳ L08 ≫  X < Y  □

[SystemQ lemma LessLeqTransitivity: ΠX , Y, Z: X < Y ⊢ Y <= Z ⊢ X < Z]

SystemQ proof of LessLeqTransitivity:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y, Z  ;
L03: Premise ≫  X < Y  ;
L04: Premise ≫  Y <= Z  ;

L05: Premise ≫  Z = X  ;
L06: FirstConjunct ⊳ L03 ≫  X <= Y  ;
L07: SecondConjunct ⊳ L03 ≫  X ≠ Y  ;
L08: subLeqRight ⊳ L05 ⊳ L04 ≫  Y <= X  ;
L09: leqAntisymmetry⊳L06⊳L08 ≫ X = Y  ;

L10: FromContradiction ⊳ L09 ⊳

L07 ≫ Z ≠ X ;

L11: Block ≫  End  ;
L12: Arbitrary ≫  X , Y, Z  ;
L13: Ded ⊳ L11 ≫  {X < Y ⇒ Y <= Z ⇒ Z = \atop X ⇒ Z ≠ X  ;}
L14: Premise ≫  X < Y  ;
L15: Premise ≫  Y <= Z  ;
L16: MP2 ⊳ L13 ⊳ L14 ⊳ L15 ≫  Z = X ⇒ Z ≠ X  ;

L17: prop lemma imply negation ⊳

L16 ≫ Z ≠ X ;

L18: NeqSymmetry ⊳ L17 ≫  X ≠ Z  ;
L19: FirstConjunct ⊳ L14 ≫  X <= Y  ;
L20: leqTransitivity ⊳ L19 ⊳ L15 ≫ X <= Z  ;
L21: JoinConjuncts ⊳ L20 ⊳ L18 ≫ X < Z  □

[SystemQ lemma LessTransitivity: ΠX , Y, Z: X < Y ⊢ Y < Z ⊢ X < Z] SystemQ proof of LessTransitivity:

L01: Arbitrary ≫  X , Y, Z  ;
L02: Premise ≫  X < Y  ;
L03: Premise ≫  Y < Z  ;
L04: FirstConjunct ⊳ L03 ≫  Y <= Z  ;

L05: LessLeqTransitivity ⊳ L02 ⊳

L04 ≫ X < Z □

[SystemQ lemma AddEquations(Less): ΠX , Y, Z, U: X < Y ⊢ Z < U ⊢ (X + Z) < (Y + U)]

SystemQ proof of AddEquations(Less):

L01: Arbitrary ≫  X , Y, Z, U  ;
L02: Premise ≫  X < Y  ;
L03: Premise ≫  Z < U  ;
L04: LessAddition ⊳ L02 ≫  (X + Z) < (Y + Z)  ;
L05: LessAdditionLeft ⊳ L03 ≫  (Y + Z) < (Y + U)  ;
L06: LessTransitivity⊳L04⊳L05 ≫ (X + Z) < (Y + U)  □

[SystemQ lemma LessTotality: ΠX , Y: X < Y ˙∨ X = Y ˙∨ Y < X] SystemQ proof of LessTotality:

L01: Block ≫  Begin  ;
L02: Arbitrary ≫  X , Y  ;
L03: Premise ≫  ˙¬ (X < Y)n  ;
L04: Premise ≫  X ≠ Y  ;
L05: fromNotLess ⊳ L03 ≫  Y <= X  ;
L06: NeqSymmetry ⊳ L04 ≫  Y ≠ X  ;

L07: LeqNeqLess ⊳ L05 ⊳ L06 ≫  Y < X  ;
L08: Block ≫  End  ;
L09: Arbitrary ≫  X , Y  ;
L10: Ded ⊳ L08 ≫  {˙¬ (X < Y)n ⇒ X ≠ Y ⇒ Y < \atop X  ;}
L11: Repetition ⊳ L10 ≫  X < Y ˙∨ X = Y ˙∨ Y < X  □

[SystemQ lemma NegativeLessPositive: ΠX: 0 < X ⊢ (−uX) < X] SystemQ proof of NegativeLessPositive:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 < X  ;
L03: FirstConjunct ⊳ L02 ≫  0 <= X  ;
L04: leqAddition ⊳ L03 ≫  (0 − X) <= (X − X)  ;
L05: lemma plus0Left ≫  (0 − X) = (−uX)  ;
L06: Negative ≫  (X − X) = 0  ;
L07: subLeqLeft ⊳ L05 ⊳ L04 ≫  (−uX) <= (X − X)  ;
L08: subLeqRight ⊳ L06 ⊳ L07 ≫  (−uX) <= 0  ;

L09: leqLessTransitivity ⊳ L08 ⊳

L02 ≫ (−uX) < X □

[SystemQ lemma LessNegated: ΠX , Y: X < Y ⊢ (−uY) < (−uX)] SystemQ proof of LessNegated:

L01: Arbitrary ≫  X , Y  ;
L02: Premise ≫  X < Y  ;
L03: LessLeq ⊳ L02 ≫  X <= Y  ;
L04: LeqNegated ⊳ L03 ≫  (−uY) <= (−uX)  ;
L05: LessNeq ⊳ L02 ≫  X ≠ Y  ;
L06: NeqNegated ⊳ L05 ≫  ˙¬ ((−uX) = (−uY))n  ;
L07: NeqSymmetry ⊳ L06 ≫  ˙¬ ((−uY) = (−uX))n  ;
L08: LeqNeqLess ⊳ L04 ⊳ L07 ≫  (−uY) < (−uX)  □

[SystemQ lemma − 0 = 0: (−u0) = 0]

SystemQ proof of − 0 = 0:

L01: Negative ≫  (0 − 0) = 0  ;
L02: plus0 ≫  (0 + 0) = 0  ;
L03: UniqueNegative ⊳ L01 ⊳ L02 ≫ (−u0) = 0  □

[SystemQ lemma PositiveNegated: ΠX: 0 < X ⊢ (−uX) < 0] SystemQ proof of PositiveNegated:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 < X  ;
L03: LessNegated ⊳ L02 ≫  (−uX) < (−u0)  ;
L04: −0 = 0 ≫  (−u0) = 0  ;
L05: SubLessRight ⊳ L04 ⊳ L03 ≫ (−uX) < 0  □

[SystemQ lemma NonpositiveNegated: ΠX: X <= 0 ⊢ 0 <= (−uX)] SystemQ proof of NonpositiveNegated:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  X <= 0  ;
L03: LeqNegated ⊳ L02 ≫  (−u0) <= (−uX)  ;
L04: −0 = 0 ≫  (−u0) = 0  ;

L05: subLeqLeft ⊳ L04 ⊳ L03 ≫  0 <= (−uX)  □

[SystemQ lemma NegativeNegated: ΠX: X < 0 ⊢ 0 < (−uX)] SystemQ proof of NegativeNegated:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  X < 0  ;
L03: LessNegated ⊳ L02 ≫  (−u0) < (−uX)  ;
L04: −0 = 0 ≫  (−u0) = 0  ;
L05: SubLessLeft ⊳ L04 ⊳ L03 ≫  0 < (−uX)  □

[SystemQ lemma NonnegativeNegated: ΠX: 0 <= X ⊢ (−uX) <= 0] SystemQ proof of NonnegativeNegated:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 <= X  ;
L03: LeqNegated ⊳ L02 ≫  (−uX) <= (−u0)  ;
L04: −0 = 0 ≫  (−u0) = 0  ;
L05: subLeqRight ⊳ L04 ⊳ L03 ≫  (−uX) <= 0  □

[SystemQ lemma 0 < 2: 0 < 2]

SystemQ proof of 0 < 2:

L01: 0 < 1 ≫  0 < 1  ;
L02: LessAddition ⊳ L01 ≫  (0 + 1) < (1 + 1)  ;
L03: lemma plus0Left ≫  (0 + 1) = 1  ;
L04: SubLessLeft ⊳ L03 ⊳ L02 ≫  1 < (1 + 1)  ;
L05: LessTransitivity⊳L01⊳L04 ≫ 0 < 2  □

[SystemQ lemma 0 < 1/2: 0 < 1/2]

SystemQ proof of 0 < 1/2:

L01: 0 < 2 ≫  0 < 2  ;
L02: FirstConjunct ⊳ L01 ≫  0 <= 2  ;
L03: SecondConjunct ⊳ L01 ≫  0 ≠ 2  ;
L04: NeqSymmetry ⊳ L03 ≫  2 ≠ 0  ;
L05: 0 < 1 ≫  0 < 1  ;
L06: x ∗ 0 = 0 ≫  (2 ∗ 0) = 0  ;
L07: x ∗ y = zBackwards ⊳ L06 ≫  0 = (0 ∗ 2)  ;
L08: SubLessLeft ⊳ L07 ⊳ L05 ≫  (0 ∗ 2) < 1  ;
L09: Reciprocal ⊳ L04 ≫  (2 ∗ 1/2) = 1  ;
L10: x ∗ y = zBackwards ⊳ L09 ≫  1 = (1/2 ∗ 2)  ;
L11: SubLessRight ⊳ L10 ⊳ L08 ≫ (0 ∗ 2) < (1/2 ∗ 2)  ;
L12: LessDivision ⊳ L02 ⊳ L11 ≫ 0 < 1/2 □

[SystemQ lemma PositiveHalved: ΠX: 0 < X ⊢ 0 < (1/2 ∗ X)] SystemQ proof of PositiveHalved:

L01: Arbitrary ≫  X  ;
L02: Premise ≫  0 < X  ;
L03: 0 < 1/2 ≫  0 < 1/2  ;

L04: LessMultiplicationLeft ⊳ L03 ⊳

L02 ≫ (1/2 ∗ 0) < (1/2 ∗ X) ;

L05: x ∗ 0 = 0 ≫  (1/2 ∗ 0) = 0  ;
L06: SubLessLeft ⊳ L05 ⊳ L04 ≫  0 < (1/2 ∗ X)  □