Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltaprg GIF version

Theorem ltaprg 6660
 Description: Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by Jim Kingdon, 26-Dec-2019.)
Assertion
Ref Expression
ltaprg ((𝐴P𝐵P𝐶P) → (𝐴<P 𝐵 ↔ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))

Proof of Theorem ltaprg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ltaprlem 6659 . . 3 (𝐶P → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
213ad2ant3 927 . 2 ((𝐴P𝐵P𝐶P) → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
3 ltexpri 6654 . . . . 5 ((𝐶 +P 𝐴)<P (𝐶 +P 𝐵) → ∃𝑥P ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))
43adantl 262 . . . 4 (((𝐴P𝐵P𝐶P) ∧ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)) → ∃𝑥P ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))
5 simpl1 907 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐴P)
6 simprl 483 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝑥P)
7 ltaddpr 6638 . . . . . . 7 ((𝐴P𝑥P) → 𝐴<P (𝐴 +P 𝑥))
85, 6, 7syl2anc 391 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐴<P (𝐴 +P 𝑥))
9 addassprg 6620 . . . . . . . . . . . 12 ((𝐶P𝐴P𝑥P) → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P (𝐴 +P 𝑥)))
1093com12 1108 . . . . . . . . . . 11 ((𝐴P𝐶P𝑥P) → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P (𝐴 +P 𝑥)))
11103expa 1104 . . . . . . . . . 10 (((𝐴P𝐶P) ∧ 𝑥P) → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P (𝐴 +P 𝑥)))
1211adantrr 448 . . . . . . . . 9 (((𝐴P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P (𝐴 +P 𝑥)))
13 simprr 484 . . . . . . . . 9 (((𝐴P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))
1412, 13eqtr3d 2074 . . . . . . . 8 (((𝐴P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → (𝐶 +P (𝐴 +P 𝑥)) = (𝐶 +P 𝐵))
15143adantl2 1061 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → (𝐶 +P (𝐴 +P 𝑥)) = (𝐶 +P 𝐵))
16 simpl3 909 . . . . . . . 8 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐶P)
17 addclpr 6578 . . . . . . . . 9 ((𝐴P𝑥P) → (𝐴 +P 𝑥) ∈ P)
185, 6, 17syl2anc 391 . . . . . . . 8 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → (𝐴 +P 𝑥) ∈ P)
19 simpl2 908 . . . . . . . 8 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐵P)
20 addcanprg 6657 . . . . . . . 8 ((𝐶P ∧ (𝐴 +P 𝑥) ∈ P𝐵P) → ((𝐶 +P (𝐴 +P 𝑥)) = (𝐶 +P 𝐵) → (𝐴 +P 𝑥) = 𝐵))
2116, 18, 19, 20syl3anc 1135 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → ((𝐶 +P (𝐴 +P 𝑥)) = (𝐶 +P 𝐵) → (𝐴 +P 𝑥) = 𝐵))
2215, 21mpd 13 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → (𝐴 +P 𝑥) = 𝐵)
238, 22breqtrd 3784 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐴<P 𝐵)
2423adantlr 446 . . . 4 ((((𝐴P𝐵P𝐶P) ∧ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐴<P 𝐵)
254, 24rexlimddv 2434 . . 3 (((𝐴P𝐵P𝐶P) ∧ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)) → 𝐴<P 𝐵)
2625ex 108 . 2 ((𝐴P𝐵P𝐶P) → ((𝐶 +P 𝐴)<P (𝐶 +P 𝐵) → 𝐴<P 𝐵))
272, 26impbid 120 1 ((𝐴P𝐵P𝐶P) → (𝐴<P 𝐵 ↔ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 885   = wceq 1243   ∈ wcel 1393  ∃wrex 2304   class class class wbr 3760  (class class class)co 5473  Pcnp 6332   +P cpp 6334
 Copyright terms: Public domain W3C validator