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

Theorem ltaprg 7081
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 7080 . . 3 (𝐶P → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
213ad2ant3 962 . 2 ((𝐴P𝐵P𝐶P) → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
3 ltexpri 7075 . . . . 5 ((𝐶 +P 𝐴)<P (𝐶 +P 𝐵) → ∃𝑥P ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))
43adantl 271 . . . 4 (((𝐴P𝐵P𝐶P) ∧ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)) → ∃𝑥P ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))
5 simpl1 942 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐴P)
6 simprl 498 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝑥P)
7 ltaddpr 7059 . . . . . . 7 ((𝐴P𝑥P) → 𝐴<P (𝐴 +P 𝑥))
85, 6, 7syl2anc 403 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐴<P (𝐴 +P 𝑥))
9 addassprg 7041 . . . . . . . . . . . 12 ((𝐶P𝐴P𝑥P) → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P (𝐴 +P 𝑥)))
1093com12 1143 . . . . . . . . . . 11 ((𝐴P𝐶P𝑥P) → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P (𝐴 +P 𝑥)))
11103expa 1139 . . . . . . . . . 10 (((𝐴P𝐶P) ∧ 𝑥P) → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P (𝐴 +P 𝑥)))
1211adantrr 463 . . . . . . . . 9 (((𝐴P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P (𝐴 +P 𝑥)))
13 simprr 499 . . . . . . . . 9 (((𝐴P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))
1412, 13eqtr3d 2117 . . . . . . . 8 (((𝐴P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → (𝐶 +P (𝐴 +P 𝑥)) = (𝐶 +P 𝐵))
15143adantl2 1096 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → (𝐶 +P (𝐴 +P 𝑥)) = (𝐶 +P 𝐵))
16 simpl3 944 . . . . . . . 8 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐶P)
17 addclpr 6999 . . . . . . . . 9 ((𝐴P𝑥P) → (𝐴 +P 𝑥) ∈ P)
185, 6, 17syl2anc 403 . . . . . . . 8 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → (𝐴 +P 𝑥) ∈ P)
19 simpl2 943 . . . . . . . 8 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐵P)
20 addcanprg 7078 . . . . . . . 8 ((𝐶P ∧ (𝐴 +P 𝑥) ∈ P𝐵P) → ((𝐶 +P (𝐴 +P 𝑥)) = (𝐶 +P 𝐵) → (𝐴 +P 𝑥) = 𝐵))
2116, 18, 19, 20syl3anc 1170 . . . . . . 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 3835 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐴<P 𝐵)
2423adantlr 461 . . . 4 ((((𝐴P𝐵P𝐶P) ∧ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)) ∧ (𝑥P ∧ ((𝐶 +P 𝐴) +P 𝑥) = (𝐶 +P 𝐵))) → 𝐴<P 𝐵)
254, 24rexlimddv 2487 . . 3 (((𝐴P𝐵P𝐶P) ∧ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)) → 𝐴<P 𝐵)
2625ex 113 . 2 ((𝐴P𝐵P𝐶P) → ((𝐶 +P 𝐴)<P (𝐶 +P 𝐵) → 𝐴<P 𝐵))
272, 26impbid 127 1 ((𝐴P𝐵P𝐶P) → (𝐴<P 𝐵 ↔ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 920   = wceq 1285  wcel 1434  wrex 2354   class class class wbr 3811  (class class class)co 5591  Pcnp 6753   +P cpp 6755  <P cltp 6757
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3919  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 4000  ax-un 4224  ax-setind 4316  ax-iinf 4366
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2614  df-sbc 2827  df-csb 2920  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-iun 3706  df-br 3812  df-opab 3866  df-mpt 3867  df-tr 3902  df-eprel 4080  df-id 4084  df-po 4087  df-iso 4088  df-iord 4157  df-on 4159  df-suc 4162  df-iom 4369  df-xp 4407  df-rel 4408  df-cnv 4409  df-co 4410  df-dm 4411  df-rn 4412  df-res 4413  df-ima 4414  df-iota 4934  df-fun 4971  df-fn 4972  df-f 4973  df-f1 4974  df-fo 4975  df-f1o 4976  df-fv 4977  df-ov 5594  df-oprab 5595  df-mpt2 5596  df-1st 5846  df-2nd 5847  df-recs 6002  df-irdg 6067  df-1o 6113  df-2o 6114  df-oadd 6117  df-omul 6118  df-er 6222  df-ec 6224  df-qs 6228  df-ni 6766  df-pli 6767  df-mi 6768  df-lti 6769  df-plpq 6806  df-mpq 6807  df-enq 6809  df-nqqs 6810  df-plqqs 6811  df-mqqs 6812  df-1nqqs 6813  df-rq 6814  df-ltnqqs 6815  df-enq0 6886  df-nq0 6887  df-0nq0 6888  df-plq0 6889  df-mq0 6890  df-inp 6928  df-iplp 6930  df-iltp 6932
This theorem is referenced by:  prplnqu  7082  addextpr  7083  caucvgprlemcanl  7106  caucvgprprlemnkltj  7151  caucvgprprlemnbj  7155  caucvgprprlemmu  7157  caucvgprprlemloc  7165  caucvgprprlemexbt  7168  caucvgprprlemexb  7169  caucvgprprlemaddq  7170  caucvgprprlem1  7171  caucvgprprlem2  7172  ltsrprg  7196  gt0srpr  7197  lttrsr  7211  ltsosr  7213  ltasrg  7219  prsrlt  7235
  Copyright terms: Public domain W3C validator