Step | Hyp | Ref
| Expression |
1 | | elq 8333 |
. 2
⊢ (A ∈ ℚ ↔
∃x ∈ ℤ ∃y ∈ ℕ A =
(x / y)) |
2 | | elq 8333 |
. 2
⊢ (B ∈ ℚ ↔
∃z ∈ ℤ ∃w ∈ ℕ B =
(z / w)) |
3 | | nnz 8040 |
. . . . . . . . . . . 12
⊢ (w ∈ ℕ →
w ∈
ℤ) |
4 | | zmulcl 8073 |
. . . . . . . . . . . 12
⊢
((x ∈ ℤ ∧
w ∈
ℤ) → (x · w) ∈
ℤ) |
5 | 3, 4 | sylan2 270 |
. . . . . . . . . . 11
⊢
((x ∈ ℤ ∧
w ∈
ℕ) → (x · w) ∈
ℤ) |
6 | 5 | ad2ant2rl 480 |
. . . . . . . . . 10
⊢
(((x ∈ ℤ ∧
y ∈
ℕ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) → (x · w)
∈ ℤ) |
7 | | simpl 102 |
. . . . . . . . . . 11
⊢
((z ∈ ℤ ∧
w ∈
ℕ) → z ∈ ℤ) |
8 | | nnz 8040 |
. . . . . . . . . . . 12
⊢ (y ∈ ℕ →
y ∈
ℤ) |
9 | 8 | adantl 262 |
. . . . . . . . . . 11
⊢
((x ∈ ℤ ∧
y ∈
ℕ) → y ∈ ℤ) |
10 | | zmulcl 8073 |
. . . . . . . . . . 11
⊢
((z ∈ ℤ ∧
y ∈
ℤ) → (z · y) ∈
ℤ) |
11 | 7, 9, 10 | syl2anr 274 |
. . . . . . . . . 10
⊢
(((x ∈ ℤ ∧
y ∈
ℕ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) → (z · y)
∈ ℤ) |
12 | 6, 11 | zaddcld 8140 |
. . . . . . . . 9
⊢
(((x ∈ ℤ ∧
y ∈
ℕ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) → ((x · w) +
(z · y)) ∈
ℤ) |
13 | 12 | adantr 261 |
. . . . . . . 8
⊢
((((x ∈ ℤ ∧
y ∈
ℕ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
(A = (x
/ y) ∧
B = (z
/ w))) → ((x · w) +
(z · y)) ∈
ℤ) |
14 | | nnmulcl 7716 |
. . . . . . . . . 10
⊢
((y ∈ ℕ ∧
w ∈
ℕ) → (y · w) ∈
ℕ) |
15 | 14 | ad2ant2l 477 |
. . . . . . . . 9
⊢
(((x ∈ ℤ ∧
y ∈
ℕ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) → (y · w)
∈ ℕ) |
16 | 15 | adantr 261 |
. . . . . . . 8
⊢
((((x ∈ ℤ ∧
y ∈
ℕ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
(A = (x
/ y) ∧
B = (z
/ w))) → (y · w)
∈ ℕ) |
17 | | oveq12 5464 |
. . . . . . . . 9
⊢
((A = (x / y) ∧ B = (z / w)) →
(A + B)
= ((x / y) + (z /
w))) |
18 | | zcn 8026 |
. . . . . . . . . . . 12
⊢ (x ∈ ℤ →
x ∈
ℂ) |
19 | | zcn 8026 |
. . . . . . . . . . . 12
⊢ (z ∈ ℤ →
z ∈
ℂ) |
20 | 18, 19 | anim12i 321 |
. . . . . . . . . . 11
⊢
((x ∈ ℤ ∧
z ∈
ℤ) → (x ∈ ℂ ∧
z ∈
ℂ)) |
21 | | nncn 7703 |
. . . . . . . . . . . . 13
⊢ (y ∈ ℕ →
y ∈
ℂ) |
22 | | nnap0 7724 |
. . . . . . . . . . . . 13
⊢ (y ∈ ℕ →
y # 0) |
23 | 21, 22 | jca 290 |
. . . . . . . . . . . 12
⊢ (y ∈ ℕ →
(y ∈
ℂ ∧ y # 0)) |
24 | | nncn 7703 |
. . . . . . . . . . . . 13
⊢ (w ∈ ℕ →
w ∈
ℂ) |
25 | | nnap0 7724 |
. . . . . . . . . . . . 13
⊢ (w ∈ ℕ →
w # 0) |
26 | 24, 25 | jca 290 |
. . . . . . . . . . . 12
⊢ (w ∈ ℕ →
(w ∈
ℂ ∧ w # 0)) |
27 | 23, 26 | anim12i 321 |
. . . . . . . . . . 11
⊢
((y ∈ ℕ ∧
w ∈
ℕ) → ((y ∈ ℂ ∧
y # 0) ∧
(w ∈
ℂ ∧ w # 0))) |
28 | | divadddivap 7485 |
. . . . . . . . . . 11
⊢
(((x ∈ ℂ ∧
z ∈
ℂ) ∧ ((y ∈ ℂ ∧ y # 0) ∧ (w ∈ ℂ ∧
w # 0))) → ((x / y) +
(z / w)) = (((x
· w) + (z · y)) /
(y · w))) |
29 | 20, 27, 28 | syl2an 273 |
. . . . . . . . . 10
⊢
(((x ∈ ℤ ∧
z ∈
ℤ) ∧ (y ∈ ℕ ∧ w ∈ ℕ)) → ((x / y) +
(z / w)) = (((x
· w) + (z · y)) /
(y · w))) |
30 | 29 | an4s 522 |
. . . . . . . . 9
⊢
(((x ∈ ℤ ∧
y ∈
ℕ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) → ((x / y) +
(z / w)) = (((x
· w) + (z · y)) /
(y · w))) |
31 | 17, 30 | sylan9eqr 2091 |
. . . . . . . 8
⊢
((((x ∈ ℤ ∧
y ∈
ℕ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
(A = (x
/ y) ∧
B = (z
/ w))) → (A + B) =
(((x · w) + (z ·
y)) / (y · w))) |
32 | | rspceov 5489 |
. . . . . . . . 9
⊢
((((x · w) + (z ·
y)) ∈
ℤ ∧ (y · w)
∈ ℕ ∧
(A + B)
= (((x · w) + (z ·
y)) / (y · w)))
→ ∃v ∈ ℤ ∃u ∈ ℕ (A +
B) = (v
/ u)) |
33 | | elq 8333 |
. . . . . . . . 9
⊢
((A + B) ∈ ℚ
↔ ∃v ∈ ℤ ∃u ∈ ℕ (A +
B) = (v
/ u)) |
34 | 32, 33 | sylibr 137 |
. . . . . . . 8
⊢
((((x · w) + (z ·
y)) ∈
ℤ ∧ (y · w)
∈ ℕ ∧
(A + B)
= (((x · w) + (z ·
y)) / (y · w)))
→ (A + B) ∈
ℚ) |
35 | 13, 16, 31, 34 | syl3anc 1134 |
. . . . . . 7
⊢
((((x ∈ ℤ ∧
y ∈
ℕ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
(A = (x
/ y) ∧
B = (z
/ w))) → (A + B) ∈ ℚ) |
36 | 35 | an4s 522 |
. . . . . 6
⊢
((((x ∈ ℤ ∧
y ∈
ℕ) ∧ A = (x /
y)) ∧
((z ∈
ℤ ∧ w ∈ ℕ) ∧ B = (z / w))) →
(A + B)
∈ ℚ) |
37 | 36 | exp43 354 |
. . . . 5
⊢
((x ∈ ℤ ∧
y ∈
ℕ) → (A = (x / y) →
((z ∈
ℤ ∧ w ∈ ℕ)
→ (B = (z / w) →
(A + B)
∈ ℚ)))) |
38 | 37 | rexlimivv 2432 |
. . . 4
⊢ (∃x ∈ ℤ ∃y ∈ ℕ A =
(x / y)
→ ((z ∈ ℤ ∧
w ∈
ℕ) → (B = (z / w) →
(A + B)
∈ ℚ))) |
39 | 38 | rexlimdvv 2433 |
. . 3
⊢ (∃x ∈ ℤ ∃y ∈ ℕ A =
(x / y)
→ (∃z ∈ ℤ ∃w ∈ ℕ B =
(z / w)
→ (A + B) ∈
ℚ)) |
40 | 39 | imp 115 |
. 2
⊢ ((∃x ∈ ℤ ∃y ∈ ℕ A =
(x / y)
∧ ∃z ∈ ℤ ∃w ∈ ℕ B =
(z / w)) → (A +
B) ∈
ℚ) |
41 | 1, 2, 40 | syl2anb 275 |
1
⊢
((A ∈ ℚ ∧
B ∈
ℚ) → (A + B) ∈
ℚ) |