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

 Description: Closure law for addition of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcl 7769 be used later. Instead, in most cases use addcl 7798. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
Assertion
Ref Expression
axaddcl ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxpi 4567 . . . . 5 (𝐴 ∈ (R × R) → ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)))
2 df-c 7679 . . . . 5 ℂ = (R × R)
31, 2eleq2s 2236 . . . 4 (𝐴 ∈ ℂ → ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)))
4 elxpi 4567 . . . . 5 (𝐵 ∈ (R × R) → ∃𝑧𝑤(𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R)))
54, 2eleq2s 2236 . . . 4 (𝐵 ∈ ℂ → ∃𝑧𝑤(𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R)))
63, 5anim12i 336 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ ∃𝑧𝑤(𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))))
7 ee4anv 1908 . . 3 (∃𝑥𝑦𝑧𝑤((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))) ↔ (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ ∃𝑧𝑤(𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))))
86, 7sylibr 133 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃𝑥𝑦𝑧𝑤((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))))
9 simpll 519 . . . . . . 7 (((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))) → 𝐴 = ⟨𝑥, 𝑦⟩)
10 simprl 521 . . . . . . 7 (((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))) → 𝐵 = ⟨𝑧, 𝑤⟩)
119, 10oveq12d 5804 . . . . . 6 (((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))) → (𝐴 + 𝐵) = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))
12 addcnsr 7695 . . . . . . 7 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 +R 𝑧), (𝑦 +R 𝑤)⟩)
1312ad2ant2l 500 . . . . . 6 (((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 +R 𝑧), (𝑦 +R 𝑤)⟩)
1411, 13eqtrd 2174 . . . . 5 (((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))) → (𝐴 + 𝐵) = ⟨(𝑥 +R 𝑧), (𝑦 +R 𝑤)⟩)
15 addclsr 7614 . . . . . . . . 9 ((𝑥R𝑧R) → (𝑥 +R 𝑧) ∈ R)
1615ad2ant2r 501 . . . . . . . 8 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → (𝑥 +R 𝑧) ∈ R)
17 addclsr 7614 . . . . . . . . 9 ((𝑦R𝑤R) → (𝑦 +R 𝑤) ∈ R)
1817ad2ant2l 500 . . . . . . . 8 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → (𝑦 +R 𝑤) ∈ R)
19 opelxpi 4583 . . . . . . . 8 (((𝑥 +R 𝑧) ∈ R ∧ (𝑦 +R 𝑤) ∈ R) → ⟨(𝑥 +R 𝑧), (𝑦 +R 𝑤)⟩ ∈ (R × R))
2016, 18, 19syl2anc 409 . . . . . . 7 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → ⟨(𝑥 +R 𝑧), (𝑦 +R 𝑤)⟩ ∈ (R × R))
2120, 2eleqtrrdi 2235 . . . . . 6 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → ⟨(𝑥 +R 𝑧), (𝑦 +R 𝑤)⟩ ∈ ℂ)
2221ad2ant2l 500 . . . . 5 (((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))) → ⟨(𝑥 +R 𝑧), (𝑦 +R 𝑤)⟩ ∈ ℂ)
2314, 22eqeltrd 2218 . . . 4 (((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))) → (𝐴 + 𝐵) ∈ ℂ)
2423exlimivv 1870 . . 3 (∃𝑧𝑤((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))) → (𝐴 + 𝐵) ∈ ℂ)
2524exlimivv 1870 . 2 (∃𝑥𝑦𝑧𝑤((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥R𝑦R)) ∧ (𝐵 = ⟨𝑧, 𝑤⟩ ∧ (𝑧R𝑤R))) → (𝐴 + 𝐵) ∈ ℂ)
268, 25syl 14 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332  ∃wex 1469   ∈ wcel 1481  ⟨cop 3537   × cxp 4549  (class class class)co 5786  Rcnr 7158   +R cplr 7162  ℂcc 7671   + caddc 7676 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2123  ax-coll 4053  ax-sep 4056  ax-nul 4064  ax-pow 4108  ax-pr 4142  ax-un 4366  ax-setind 4463  ax-iinf 4513 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1738  df-eu 2004  df-mo 2005  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ne 2311  df-ral 2423  df-rex 2424  df-reu 2425  df-rab 2427  df-v 2693  df-sbc 2916  df-csb 3010  df-dif 3080  df-un 3082  df-in 3084  df-ss 3091  df-nul 3371  df-pw 3519  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-int 3782  df-iun 3825  df-br 3940  df-opab 4000  df-mpt 4001  df-tr 4037  df-eprel 4222  df-id 4226  df-po 4229  df-iso 4230  df-iord 4299  df-on 4301  df-suc 4304  df-iom 4516  df-xp 4557  df-rel 4558  df-cnv 4559  df-co 4560  df-dm 4561  df-rn 4562  df-res 4563  df-ima 4564  df-iota 5100  df-fun 5137  df-fn 5138  df-f 5139  df-f1 5140  df-fo 5141  df-f1o 5142  df-fv 5143  df-ov 5789  df-oprab 5790  df-mpo 5791  df-1st 6050  df-2nd 6051  df-recs 6214  df-irdg 6279  df-1o 6325  df-2o 6326  df-oadd 6329  df-omul 6330  df-er 6441  df-ec 6443  df-qs 6447  df-ni 7165  df-pli 7166  df-mi 7167  df-lti 7168  df-plpq 7205  df-mpq 7206  df-enq 7208  df-nqqs 7209  df-plqqs 7210  df-mqqs 7211  df-1nqqs 7212  df-rq 7213  df-ltnqqs 7214  df-enq0 7285  df-nq0 7286  df-0nq0 7287  df-plq0 7288  df-mq0 7289  df-inp 7327  df-iplp 7329  df-enr 7587  df-nr 7588  df-plr 7589  df-c 7679  df-add 7684 This theorem is referenced by:  axaddf  7729
 Copyright terms: Public domain W3C validator