Step | Hyp | Ref
| Expression |
1 | | elq 9581 |
. 2
⊢ (𝐴 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝐴 = (𝑥 / 𝑦)) |
2 | | elq 9581 |
. 2
⊢ (𝐵 ∈ ℚ ↔
∃𝑧 ∈ ℤ
∃𝑤 ∈ ℕ
𝐵 = (𝑧 / 𝑤)) |
3 | | nnz 9231 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ℕ → 𝑤 ∈
ℤ) |
4 | | zmulcl 9265 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 𝑤 ∈ ℤ) → (𝑥 · 𝑤) ∈ ℤ) |
5 | 3, 4 | sylan2 284 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑤 ∈ ℕ) → (𝑥 · 𝑤) ∈ ℤ) |
6 | 5 | ad2ant2rl 508 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → (𝑥 · 𝑤) ∈ ℤ) |
7 | | simpl 108 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ) → 𝑧 ∈
ℤ) |
8 | | nnz 9231 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
9 | 8 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
ℤ) |
10 | | zmulcl 9265 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑧 · 𝑦) ∈ ℤ) |
11 | 7, 9, 10 | syl2anr 288 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → (𝑧 · 𝑦) ∈ ℤ) |
12 | 6, 11 | zaddcld 9338 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → ((𝑥 · 𝑤) + (𝑧 · 𝑦)) ∈ ℤ) |
13 | 12 | adantr 274 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤))) → ((𝑥 · 𝑤) + (𝑧 · 𝑦)) ∈ ℤ) |
14 | | nnmulcl 8899 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 · 𝑤) ∈ ℕ) |
15 | 14 | ad2ant2l 505 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → (𝑦 · 𝑤) ∈ ℕ) |
16 | 15 | adantr 274 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤))) → (𝑦 · 𝑤) ∈ ℕ) |
17 | | oveq12 5862 |
. . . . . . . . 9
⊢ ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (𝐴 + 𝐵) = ((𝑥 / 𝑦) + (𝑧 / 𝑤))) |
18 | | zcn 9217 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
19 | | zcn 9217 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℂ) |
20 | 18, 19 | anim12i 336 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑥 ∈ ℂ ∧ 𝑧 ∈
ℂ)) |
21 | | nncn 8886 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
22 | | nnap0 8907 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 𝑦 # 0) |
23 | 21, 22 | jca 304 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℂ ∧ 𝑦 # 0)) |
24 | | nncn 8886 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℕ → 𝑤 ∈
ℂ) |
25 | | nnap0 8907 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℕ → 𝑤 # 0) |
26 | 24, 25 | jca 304 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ℕ → (𝑤 ∈ ℂ ∧ 𝑤 # 0)) |
27 | 23, 26 | anim12i 336 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → ((𝑦 ∈ ℂ ∧ 𝑦 # 0) ∧ (𝑤 ∈ ℂ ∧ 𝑤 # 0))) |
28 | | divadddivap 8644 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑦 ∈ ℂ ∧ 𝑦 # 0) ∧ (𝑤 ∈ ℂ ∧ 𝑤 # 0))) → ((𝑥 / 𝑦) + (𝑧 / 𝑤)) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤))) |
29 | 20, 27, 28 | syl2an 287 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝑥 / 𝑦) + (𝑧 / 𝑤)) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤))) |
30 | 29 | an4s 583 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → ((𝑥 / 𝑦) + (𝑧 / 𝑤)) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤))) |
31 | 17, 30 | sylan9eqr 2225 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤))) → (𝐴 + 𝐵) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤))) |
32 | | rspceov 5895 |
. . . . . . . . 9
⊢ ((((𝑥 · 𝑤) + (𝑧 · 𝑦)) ∈ ℤ ∧ (𝑦 · 𝑤) ∈ ℕ ∧ (𝐴 + 𝐵) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤))) → ∃𝑣 ∈ ℤ ∃𝑢 ∈ ℕ (𝐴 + 𝐵) = (𝑣 / 𝑢)) |
33 | | elq 9581 |
. . . . . . . . 9
⊢ ((𝐴 + 𝐵) ∈ ℚ ↔ ∃𝑣 ∈ ℤ ∃𝑢 ∈ ℕ (𝐴 + 𝐵) = (𝑣 / 𝑢)) |
34 | 32, 33 | sylibr 133 |
. . . . . . . 8
⊢ ((((𝑥 · 𝑤) + (𝑧 · 𝑦)) ∈ ℤ ∧ (𝑦 · 𝑤) ∈ ℕ ∧ (𝐴 + 𝐵) = (((𝑥 · 𝑤) + (𝑧 · 𝑦)) / (𝑦 · 𝑤))) → (𝐴 + 𝐵) ∈ ℚ) |
35 | 13, 16, 31, 34 | syl3anc 1233 |
. . . . . . 7
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤))) → (𝐴 + 𝐵) ∈ ℚ) |
36 | 35 | an4s 583 |
. . . . . 6
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝐴 = (𝑥 / 𝑦)) ∧ ((𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ) ∧ 𝐵 = (𝑧 / 𝑤))) → (𝐴 + 𝐵) ∈ ℚ) |
37 | 36 | exp43 370 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝐴 = (𝑥 / 𝑦) → ((𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ) → (𝐵 = (𝑧 / 𝑤) → (𝐴 + 𝐵) ∈ ℚ)))) |
38 | 37 | rexlimivv 2593 |
. . . 4
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℕ 𝐴 = (𝑥 / 𝑦) → ((𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ) → (𝐵 = (𝑧 / 𝑤) → (𝐴 + 𝐵) ∈ ℚ))) |
39 | 38 | rexlimdvv 2594 |
. . 3
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℕ 𝐴 = (𝑥 / 𝑦) → (∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤) → (𝐴 + 𝐵) ∈ ℚ)) |
40 | 39 | imp 123 |
. 2
⊢
((∃𝑥 ∈
ℤ ∃𝑦 ∈
ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝐴 + 𝐵) ∈ ℚ) |
41 | 1, 2, 40 | syl2anb 289 |
1
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ) |