Theorem qaddcl 12017

Description: Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)

Assertion

Ref	Expression
qaddcl	⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ)

Proof of Theorem qaddcl

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elq 12003	. 2 ⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
2		elq 12003	. 2 ⊢ (𝐵 ∈ ℚ ↔ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤))
3		nnz 11659	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℤ)
4		zmulcl 11686	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℤ ∧ 𝑤 ∈ ℤ) → (𝑥 · 𝑤) ∈ ℤ)
5	3, 4	sylan2 582	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℤ ∧ 𝑤 ∈ ℕ) → (𝑥 · 𝑤) ∈ ℤ)
6	5	ad2ant2rl 746	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → (𝑥 · 𝑤) ∈ ℤ)
7		simpl 470	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ) → 𝑧 ∈ ℤ)
8		nnz 11659	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
9	8	adantl 469	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ)
10		zmulcl 11686	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑧 · 𝑦) ∈ ℤ)
11	7, 9, 10	syl2anr 586	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → (𝑧 · 𝑦) ∈ ℤ)
12	6, 11	zaddcld 11746	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → ((𝑥 · 𝑤) + (𝑧 · 𝑦)) ∈ ℤ)
13	12	adantr 468	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤))) → ((𝑥 · 𝑤) + (𝑧 · 𝑦)) ∈ ℤ)
14		nnmulcl 11322	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 · 𝑤) ∈ ℕ)
15	14	ad2ant2l 743	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → (𝑦 · 𝑤) ∈ ℕ)
16	15	adantr 468	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤))) → (𝑦 · 𝑤) ∈ ℕ)
17		oveq12 6877	. . . . . . . . 9 ⊢ ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (𝐴 + 𝐵) = ((𝑥 / 𝑦) + (𝑧 / 𝑤)))
18		zcn 11642	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
19		zcn 11642	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℂ)
20	18, 19	anim12i 602	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ))
21		nncn 11307	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
22		nnne0 11333	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0)
23	21, 22	jca 503	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
24		nncn 11307	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
25		nnne0 11333	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ℕ → 𝑤 ≠ 0)
26	24, 25	jca 503	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℕ → (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0))
27	23, 26	anim12i 602	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)))
28		divadddiv 11019	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0))) → ((𝑥 / 𝑦) + (𝑧 / 𝑤)) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤)))
29	20, 27, 28	syl2an 585	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝑥 / 𝑦) + (𝑧 / 𝑤)) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤)))
30	29	an4s 642	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → ((𝑥 / 𝑦) + (𝑧 / 𝑤)) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤)))
31	17, 30	sylan9eqr 2858	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤))) → (𝐴 + 𝐵) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤)))
32		rspceov 6914	. . . . . . . . 9 ⊢ ((((𝑥 · 𝑤) + (𝑧 · 𝑦)) ∈ ℤ ∧ (𝑦 · 𝑤) ∈ ℕ ∧ (𝐴 + 𝐵) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤))) → ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℕ (𝐴 + 𝐵) = (𝑢 / 𝑣))
33		elq 12003	. . . . . . . . 9 ⊢ ((𝐴 + 𝐵) ∈ ℚ ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℕ (𝐴 + 𝐵) = (𝑢 / 𝑣))
34	32, 33	sylibr 225	. . . . . . . 8 ⊢ ((((𝑥 · 𝑤) + (𝑧 · 𝑦)) ∈ ℤ ∧ (𝑦 · 𝑤) ∈ ℕ ∧ (𝐴 + 𝐵) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤))) → (𝐴 + 𝐵) ∈ ℚ)
35	13, 16, 31, 34	syl3anc 1483	. . . . . . 7 ⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤))) → (𝐴 + 𝐵) ∈ ℚ)
36	35	an4s 642	. . . . . 6 ⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝐴 = (𝑥 / 𝑦)) ∧ ((𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ) ∧ 𝐵 = (𝑧 / 𝑤))) → (𝐴 + 𝐵) ∈ ℚ)
37	36	exp43 425	. . . . 5 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝐴 = (𝑥 / 𝑦) → ((𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ) → (𝐵 = (𝑧 / 𝑤) → (𝐴 + 𝐵) ∈ ℚ))))
38	37	rexlimivv 3220	. . . 4 ⊢ (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) → ((𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ) → (𝐵 = (𝑧 / 𝑤) → (𝐴 + 𝐵) ∈ ℚ)))
39	38	rexlimdvv 3221	. . 3 ⊢ (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) → (∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤) → (𝐴 + 𝐵) ∈ ℚ))
40	39	imp 395	. 2 ⊢ ((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝐴 + 𝐵) ∈ ℚ)
41	1, 2, 40	syl2anb 587	1 ⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100   = wceq 1637   ∈ wcel 2155   ≠ wne 2974  ∃wrex 3093  (class class class)co 6868  ℂcc 10213  0cc0 10215   + caddc 10218   · cmul 10220   / cdiv 10963  ℕcn 11299  ℤcz 11637  ℚcq 12001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291  ax-pre-mulgt0 10292

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-om 7290  df-1st 7392  df-2nd 7393  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-er 7973  df-en 8187  df-dom 8188  df-sdom 8189  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-sub 10547  df-neg 10548  df-div 10964  df-nn 11300  df-n0 11554  df-z 11638  df-q 12002

This theorem is referenced by:  qsubcl  12020  qrevaddcl  12023  pcaddlem  15803  pcadd2  15805  qsubdrg  20000  vitalilem1  23583  qaa  24286  padicabv  25527  ostth3  25535  dp2clq  29908  mblfinlem1  33753  rmxyadd  37981  mpaaeu  38215  aacllem  43112