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

Theorem addcomprg 6404
Description: Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
Assertion
Ref Expression
addcomprg ((A P B P) → (A +P B) = (B +P A))

Proof of Theorem addcomprg
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prop 6316 . . . . . . . . 9 (B P → ⟨(1stB), (2ndB)⟩ P)
2 elprnql 6322 . . . . . . . . 9 ((⟨(1stB), (2ndB)⟩ P y (1stB)) → y Q)
31, 2sylan 267 . . . . . . . 8 ((B P y (1stB)) → y Q)
4 prop 6316 . . . . . . . . . . . . 13 (A P → ⟨(1stA), (2ndA)⟩ P)
5 elprnql 6322 . . . . . . . . . . . . 13 ((⟨(1stA), (2ndA)⟩ P z (1stA)) → z Q)
64, 5sylan 267 . . . . . . . . . . . 12 ((A P z (1stA)) → z Q)
7 addcomnqg 6227 . . . . . . . . . . . . 13 ((y Q z Q) → (y +Q z) = (z +Q y))
87eqeq2d 2025 . . . . . . . . . . . 12 ((y Q z Q) → (x = (y +Q z) ↔ x = (z +Q y)))
96, 8sylan2 270 . . . . . . . . . . 11 ((y Q (A P z (1stA))) → (x = (y +Q z) ↔ x = (z +Q y)))
109anassrs 380 . . . . . . . . . 10 (((y Q A P) z (1stA)) → (x = (y +Q z) ↔ x = (z +Q y)))
1110rexbidva 2293 . . . . . . . . 9 ((y Q A P) → (z (1stA)x = (y +Q z) ↔ z (1stA)x = (z +Q y)))
1211ancoms 255 . . . . . . . 8 ((A P y Q) → (z (1stA)x = (y +Q z) ↔ z (1stA)x = (z +Q y)))
133, 12sylan2 270 . . . . . . 7 ((A P (B P y (1stB))) → (z (1stA)x = (y +Q z) ↔ z (1stA)x = (z +Q y)))
1413anassrs 380 . . . . . 6 (((A P B P) y (1stB)) → (z (1stA)x = (y +Q z) ↔ z (1stA)x = (z +Q y)))
1514rexbidva 2293 . . . . 5 ((A P B P) → (y (1stB)z (1stA)x = (y +Q z) ↔ y (1stB)z (1stA)x = (z +Q y)))
16 rexcom 2444 . . . . 5 (y (1stB)z (1stA)x = (z +Q y) ↔ z (1stA)y (1stB)x = (z +Q y))
1715, 16syl6bb 185 . . . 4 ((A P B P) → (y (1stB)z (1stA)x = (y +Q z) ↔ z (1stA)y (1stB)x = (z +Q y)))
1817rabbidv 2519 . . 3 ((A P B P) → {x Qy (1stB)z (1stA)x = (y +Q z)} = {x Qz (1stA)y (1stB)x = (z +Q y)})
19 elprnqu 6323 . . . . . . . . 9 ((⟨(1stB), (2ndB)⟩ P y (2ndB)) → y Q)
201, 19sylan 267 . . . . . . . 8 ((B P y (2ndB)) → y Q)
21 elprnqu 6323 . . . . . . . . . . . . 13 ((⟨(1stA), (2ndA)⟩ P z (2ndA)) → z Q)
224, 21sylan 267 . . . . . . . . . . . 12 ((A P z (2ndA)) → z Q)
2322, 8sylan2 270 . . . . . . . . . . 11 ((y Q (A P z (2ndA))) → (x = (y +Q z) ↔ x = (z +Q y)))
2423anassrs 380 . . . . . . . . . 10 (((y Q A P) z (2ndA)) → (x = (y +Q z) ↔ x = (z +Q y)))
2524rexbidva 2293 . . . . . . . . 9 ((y Q A P) → (z (2ndA)x = (y +Q z) ↔ z (2ndA)x = (z +Q y)))
2625ancoms 255 . . . . . . . 8 ((A P y Q) → (z (2ndA)x = (y +Q z) ↔ z (2ndA)x = (z +Q y)))
2720, 26sylan2 270 . . . . . . 7 ((A P (B P y (2ndB))) → (z (2ndA)x = (y +Q z) ↔ z (2ndA)x = (z +Q y)))
2827anassrs 380 . . . . . 6 (((A P B P) y (2ndB)) → (z (2ndA)x = (y +Q z) ↔ z (2ndA)x = (z +Q y)))
2928rexbidva 2293 . . . . 5 ((A P B P) → (y (2ndB)z (2ndA)x = (y +Q z) ↔ y (2ndB)z (2ndA)x = (z +Q y)))
30 rexcom 2444 . . . . 5 (y (2ndB)z (2ndA)x = (z +Q y) ↔ z (2ndA)y (2ndB)x = (z +Q y))
3129, 30syl6bb 185 . . . 4 ((A P B P) → (y (2ndB)z (2ndA)x = (y +Q z) ↔ z (2ndA)y (2ndB)x = (z +Q y)))
3231rabbidv 2519 . . 3 ((A P B P) → {x Qy (2ndB)z (2ndA)x = (y +Q z)} = {x Qz (2ndA)y (2ndB)x = (z +Q y)})
3318, 32opeq12d 3521 . 2 ((A P B P) → ⟨{x Qy (1stB)z (1stA)x = (y +Q z)}, {x Qy (2ndB)z (2ndA)x = (y +Q z)}⟩ = ⟨{x Qz (1stA)y (1stB)x = (z +Q y)}, {x Qz (2ndA)y (2ndB)x = (z +Q y)}⟩)
34 plpvlu 6380 . . 3 ((B P A P) → (B +P A) = ⟨{x Qy (1stB)z (1stA)x = (y +Q z)}, {x Qy (2ndB)z (2ndA)x = (y +Q z)}⟩)
3534ancoms 255 . 2 ((A P B P) → (B +P A) = ⟨{x Qy (1stB)z (1stA)x = (y +Q z)}, {x Qy (2ndB)z (2ndA)x = (y +Q z)}⟩)
36 plpvlu 6380 . 2 ((A P B P) → (A +P B) = ⟨{x Qz (1stA)y (1stB)x = (z +Q y)}, {x Qz (2ndA)y (2ndB)x = (z +Q y)}⟩)
3733, 35, 363eqtr4rd 2057 1 ((A P B P) → (A +P B) = (B +P A))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1224   wcel 1367  wrex 2277  {crab 2280  cop 3343  cfv 4818  (class class class)co 5425  1st c1st 5677  2nd c2nd 5678  Qcnq 6127   +Q cplq 6129  Pcnp 6138   +P cpp 6140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1310  ax-7 1311  ax-gen 1312  ax-ie1 1356  ax-ie2 1357  ax-8 1369  ax-10 1370  ax-11 1371  ax-i12 1372  ax-bnd 1373  ax-4 1374  ax-13 1378  ax-14 1379  ax-17 1393  ax-i9 1397  ax-ial 1401  ax-i5r 1402  ax-ext 1996  ax-coll 3836  ax-sep 3839  ax-nul 3847  ax-pow 3891  ax-pr 3908  ax-un 4109  ax-setind 4193  ax-iinf 4227
This theorem depends on definitions:  df-bi 110  df-dc 727  df-3or 868  df-3an 869  df-tru 1227  df-fal 1230  df-nf 1324  df-sb 1620  df-eu 1877  df-mo 1878  df-clab 2001  df-cleq 2007  df-clel 2010  df-nfc 2141  df-ne 2180  df-ral 2281  df-rex 2282  df-reu 2283  df-rab 2285  df-v 2529  df-sbc 2734  df-csb 2822  df-dif 2889  df-un 2891  df-in 2893  df-ss 2900  df-nul 3194  df-pw 3326  df-sn 3346  df-pr 3347  df-op 3349  df-uni 3545  df-int 3580  df-iun 3623  df-br 3729  df-opab 3783  df-mpt 3784  df-tr 3819  df-id 3994  df-iord 4042  df-on 4044  df-suc 4047  df-iom 4230  df-xp 4267  df-rel 4268  df-cnv 4269  df-co 4270  df-dm 4271  df-rn 4272  df-res 4273  df-ima 4274  df-iota 4783  df-fun 4820  df-fn 4821  df-f 4822  df-f1 4823  df-fo 4824  df-f1o 4825  df-fv 4826  df-ov 5428  df-oprab 5429  df-mpt2 5430  df-1st 5679  df-2nd 5680  df-recs 5831  df-irdg 5867  df-oadd 5909  df-omul 5910  df-er 6006  df-ec 6008  df-qs 6012  df-ni 6151  df-pli 6152  df-mi 6153  df-plpq 6190  df-enq 6193  df-nqqs 6194  df-plqqs 6195  df-inp 6307  df-iplp 6309
This theorem is referenced by:  addextpr  6443  enrer  6474  addcmpblnr  6478  mulcmpblnrlemg  6479  ltsrprg  6486  addcomsrg  6494  mulcomsrg  6496  mulasssrg  6497  distrsrg  6498  lttrsr  6501  ltposr  6502  ltsosr  6503  0lt1sr  6504  0idsr  6506  1idsr  6507  ltasrg  6509  recexgt0sr  6512  mulgt0sr  6515  aptisr  6516  mulextsr1lem  6517
  Copyright terms: Public domain W3C validator