Step | Hyp | Ref
| Expression |
1 | | ax-1cn 7208 |
. . . . . 6
⊢ 1 ∈
ℂ |
2 | | 1ap0 7834 |
. . . . . 6
⊢ 1 #
0 |
3 | 1, 2 | div0api 7978 |
. . . . 5
⊢ (0 / 1) =
0 |
4 | | 0z 8520 |
. . . . . 6
⊢ 0 ∈
ℤ |
5 | | 1nn 8194 |
. . . . . 6
⊢ 1 ∈
ℕ |
6 | | znq 8867 |
. . . . . 6
⊢ ((0
∈ ℤ ∧ 1 ∈ ℕ) → (0 / 1) ∈
ℚ) |
7 | 4, 5, 6 | mp2an 417 |
. . . . 5
⊢ (0 / 1)
∈ ℚ |
8 | 3, 7 | eqeltrri 2156 |
. . . 4
⊢ 0 ∈
ℚ |
9 | | qapne 8882 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 0 ∈
ℚ) → (𝐴 # 0
↔ 𝐴 ≠
0)) |
10 | 8, 9 | mpan2 416 |
. . 3
⊢ (𝐴 ∈ ℚ → (𝐴 # 0 ↔ 𝐴 ≠ 0)) |
11 | 10 | biimpar 291 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → 𝐴 # 0) |
12 | | elq 8865 |
. . . 4
⊢ (𝐴 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝐴 = (𝑥 / 𝑦)) |
13 | | nnne0 8211 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
14 | 13 | ancli 316 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℕ ∧ 𝑦 ≠ 0)) |
15 | | nnz 8528 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
16 | | zapne 8580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℤ ∧ 0 ∈
ℤ) → (𝑦 # 0
↔ 𝑦 ≠
0)) |
17 | 15, 4, 16 | sylancl 404 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 # 0 ↔ 𝑦 ≠ 0)) |
18 | 17 | adantl 271 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑦 # 0 ↔ 𝑦 ≠ 0)) |
19 | 18 | pm5.32i 442 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) ↔ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0)) |
20 | 19 | anbi1i 446 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) ∧ 𝐴 = (𝑥 / 𝑦)) ↔ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦))) |
21 | | breq1 3809 |
. . . . . . . . . . . . 13
⊢ (𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 ↔ (𝑥 / 𝑦) # 0)) |
22 | | zcn 8514 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
23 | | nncn 8191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
24 | 22, 23 | anim12i 331 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ ℂ ∧ 𝑦 ∈
ℂ)) |
25 | | divap0b 7915 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 # 0) → (𝑥 # 0 ↔ (𝑥 / 𝑦) # 0)) |
26 | 25 | 3expa 1139 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑦 # 0) → (𝑥 # 0 ↔ (𝑥 / 𝑦) # 0)) |
27 | 24, 26 | sylan 277 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) → (𝑥 # 0 ↔ (𝑥 / 𝑦) # 0)) |
28 | 27 | bicomd 139 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) → ((𝑥 / 𝑦) # 0 ↔ 𝑥 # 0)) |
29 | 21, 28 | sylan9bbr 451 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝐴 # 0 ↔ 𝑥 # 0)) |
30 | 20, 29 | sylbir 133 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝐴 # 0 ↔ 𝑥 # 0)) |
31 | | simplll 500 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → 𝑥 ∈ ℤ) |
32 | | zapne 8580 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 0 ∈
ℤ) → (𝑥 # 0
↔ 𝑥 ≠
0)) |
33 | 31, 4, 32 | sylancl 404 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝑥 # 0 ↔ 𝑥 ≠ 0)) |
34 | 30, 33 | bitrd 186 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝐴 # 0 ↔ 𝑥 ≠ 0)) |
35 | | zmulcl 8562 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ) |
36 | 15, 35 | sylan2 280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑥 · 𝑦) ∈ ℤ) |
37 | 36 | adantr 270 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → (𝑥 · 𝑦) ∈ ℤ) |
38 | | msqznn 8605 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) → (𝑥 · 𝑥) ∈ ℕ) |
39 | 38 | adantlr 461 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → (𝑥 · 𝑥) ∈ ℕ) |
40 | 37, 39 | jca 300 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → ((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ)) |
41 | 40 | adantlr 461 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝑥 ≠ 0) → ((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ)) |
42 | 41 | adantlr 461 |
. . . . . . . . . . . 12
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0) → ((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ)) |
43 | 20 | anbi1i 446 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 # 0) ∧
𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 # 0) ↔ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 # 0)) |
44 | 33 | pm5.32i 442 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 # 0) ↔ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0)) |
45 | 43, 44 | bitri 182 |
. . . . . . . . . . . . 13
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 # 0) ∧
𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 # 0) ↔ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0)) |
46 | | oveq2 5573 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 = (𝑥 / 𝑦) → (1 / 𝐴) = (1 / (𝑥 / 𝑦))) |
47 | | dividap 7933 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 # 0) → (𝑥 / 𝑥) = 1) |
48 | 47 | adantr 270 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑥 / 𝑥) = 1) |
49 | 48 | oveq1d 5580 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → ((𝑥 / 𝑥) / (𝑥 / 𝑦)) = (1 / (𝑥 / 𝑦))) |
50 | | simpll 496 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → 𝑥 ∈ ℂ) |
51 | | simpl 107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑥 ∈ ℂ ∧ 𝑥 # 0)) |
52 | | simpr 108 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑦 ∈ ℂ ∧ 𝑦 # 0)) |
53 | | divdivdivap 7945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 # 0)) ∧ ((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0))) → ((𝑥 / 𝑥) / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
54 | 50, 51, 51, 52, 53 | syl22anc 1171 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → ((𝑥 / 𝑥) / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
55 | 49, 54 | eqtr3d 2117 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
56 | 55 | an4s 553 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ (𝑥 # 0 ∧ 𝑦 # 0)) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
57 | 24, 56 | sylan 277 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑥 # 0 ∧ 𝑦 # 0)) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
58 | 57 | anass1rs 536 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) ∧ 𝑥 # 0) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
59 | 46, 58 | sylan9eqr 2137 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 # 0) ∧
𝑥 # 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
60 | 59 | an32s 533 |
. . . . . . . . . . . . 13
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 # 0) ∧
𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 # 0) → (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
61 | 45, 60 | sylbir 133 |
. . . . . . . . . . . 12
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0) → (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
62 | 42, 61 | jca 300 |
. . . . . . . . . . 11
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0) → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))) |
63 | 62 | ex 113 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝑥 ≠ 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))))) |
64 | 34, 63 | sylbid 148 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝐴 # 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))))) |
65 | 64 | ex 113 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) → (𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))))) |
66 | 65 | anasss 391 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ≠ 0)) → (𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))))) |
67 | 14, 66 | sylan2 280 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))))) |
68 | | rspceov 5600 |
. . . . . . . 8
⊢ (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) → ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ (1 / 𝐴) = (𝑧 / 𝑤)) |
69 | 68 | 3expa 1139 |
. . . . . . 7
⊢ ((((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) → ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ (1 / 𝐴) = (𝑧 / 𝑤)) |
70 | | elq 8865 |
. . . . . . 7
⊢ ((1 /
𝐴) ∈ ℚ ↔
∃𝑧 ∈ ℤ
∃𝑤 ∈ ℕ (1
/ 𝐴) = (𝑧 / 𝑤)) |
71 | 69, 70 | sylibr 132 |
. . . . . 6
⊢ ((((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) → (1 / 𝐴) ∈ ℚ) |
72 | 67, 71 | syl8 70 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 → (1 / 𝐴) ∈ ℚ))) |
73 | 72 | rexlimivv 2488 |
. . . 4
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℕ 𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 → (1 / 𝐴) ∈ ℚ)) |
74 | 12, 73 | sylbi 119 |
. . 3
⊢ (𝐴 ∈ ℚ → (𝐴 # 0 → (1 / 𝐴) ∈
ℚ)) |
75 | 74 | imp 122 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 # 0) → (1 / 𝐴) ∈
ℚ) |
76 | 11, 75 | syldan 276 |
1
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℚ) |