Step | Hyp | Ref
| Expression |
1 | | ax-1cn 7867 |
. . . . . 6
⊢ 1 ∈
ℂ |
2 | | 1ap0 8509 |
. . . . . 6
⊢ 1 #
0 |
3 | 1, 2 | div0api 8663 |
. . . . 5
⊢ (0 / 1) =
0 |
4 | | 0z 9223 |
. . . . . 6
⊢ 0 ∈
ℤ |
5 | | 1nn 8889 |
. . . . . 6
⊢ 1 ∈
ℕ |
6 | | znq 9583 |
. . . . . 6
⊢ ((0
∈ ℤ ∧ 1 ∈ ℕ) → (0 / 1) ∈
ℚ) |
7 | 4, 5, 6 | mp2an 424 |
. . . . 5
⊢ (0 / 1)
∈ ℚ |
8 | 3, 7 | eqeltrri 2244 |
. . . 4
⊢ 0 ∈
ℚ |
9 | | qapne 9598 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 0 ∈
ℚ) → (𝐴 # 0
↔ 𝐴 ≠
0)) |
10 | 8, 9 | mpan2 423 |
. . 3
⊢ (𝐴 ∈ ℚ → (𝐴 # 0 ↔ 𝐴 ≠ 0)) |
11 | 10 | biimpar 295 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → 𝐴 # 0) |
12 | | elq 9581 |
. . . 4
⊢ (𝐴 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝐴 = (𝑥 / 𝑦)) |
13 | | nnne0 8906 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
14 | 13 | ancli 321 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℕ ∧ 𝑦 ≠ 0)) |
15 | | nnz 9231 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
16 | | zapne 9286 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℤ ∧ 0 ∈
ℤ) → (𝑦 # 0
↔ 𝑦 ≠
0)) |
17 | 15, 4, 16 | sylancl 411 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 # 0 ↔ 𝑦 ≠ 0)) |
18 | 17 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑦 # 0 ↔ 𝑦 ≠ 0)) |
19 | 18 | pm5.32i 451 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) ↔ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0)) |
20 | 19 | anbi1i 455 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) ∧ 𝐴 = (𝑥 / 𝑦)) ↔ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦))) |
21 | | breq1 3992 |
. . . . . . . . . . . . 13
⊢ (𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 ↔ (𝑥 / 𝑦) # 0)) |
22 | | zcn 9217 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
23 | | nncn 8886 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
24 | 22, 23 | anim12i 336 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ ℂ ∧ 𝑦 ∈
ℂ)) |
25 | | divap0b 8600 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 # 0) → (𝑥 # 0 ↔ (𝑥 / 𝑦) # 0)) |
26 | 25 | 3expa 1198 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑦 # 0) → (𝑥 # 0 ↔ (𝑥 / 𝑦) # 0)) |
27 | 24, 26 | sylan 281 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) → (𝑥 # 0 ↔ (𝑥 / 𝑦) # 0)) |
28 | 27 | bicomd 140 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) → ((𝑥 / 𝑦) # 0 ↔ 𝑥 # 0)) |
29 | 21, 28 | sylan9bbr 460 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝐴 # 0 ↔ 𝑥 # 0)) |
30 | 20, 29 | sylbir 134 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝐴 # 0 ↔ 𝑥 # 0)) |
31 | | simplll 528 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → 𝑥 ∈ ℤ) |
32 | | zapne 9286 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 0 ∈
ℤ) → (𝑥 # 0
↔ 𝑥 ≠
0)) |
33 | 31, 4, 32 | sylancl 411 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝑥 # 0 ↔ 𝑥 ≠ 0)) |
34 | 30, 33 | bitrd 187 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝐴 # 0 ↔ 𝑥 ≠ 0)) |
35 | | zmulcl 9265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ) |
36 | 15, 35 | sylan2 284 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑥 · 𝑦) ∈ ℤ) |
37 | 36 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → (𝑥 · 𝑦) ∈ ℤ) |
38 | | msqznn 9312 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) → (𝑥 · 𝑥) ∈ ℕ) |
39 | 38 | adantlr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → (𝑥 · 𝑥) ∈ ℕ) |
40 | 37, 39 | jca 304 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → ((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ)) |
41 | 40 | adantlr 474 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝑥 ≠ 0) → ((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ)) |
42 | 41 | adantlr 474 |
. . . . . . . . . . . 12
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0) → ((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ)) |
43 | 20 | anbi1i 455 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 # 0) ∧
𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 # 0) ↔ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 # 0)) |
44 | 33 | pm5.32i 451 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 # 0) ↔ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0)) |
45 | 43, 44 | bitri 183 |
. . . . . . . . . . . . 13
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 # 0) ∧
𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 # 0) ↔ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0)) |
46 | | oveq2 5861 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 = (𝑥 / 𝑦) → (1 / 𝐴) = (1 / (𝑥 / 𝑦))) |
47 | | dividap 8618 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 # 0) → (𝑥 / 𝑥) = 1) |
48 | 47 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑥 / 𝑥) = 1) |
49 | 48 | oveq1d 5868 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → ((𝑥 / 𝑥) / (𝑥 / 𝑦)) = (1 / (𝑥 / 𝑦))) |
50 | | simpll 524 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → 𝑥 ∈ ℂ) |
51 | | simpl 108 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑥 ∈ ℂ ∧ 𝑥 # 0)) |
52 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑦 ∈ ℂ ∧ 𝑦 # 0)) |
53 | | divdivdivap 8630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 # 0)) ∧ ((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0))) → ((𝑥 / 𝑥) / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
54 | 50, 51, 51, 52, 53 | syl22anc 1234 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → ((𝑥 / 𝑥) / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
55 | 49, 54 | eqtr3d 2205 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
56 | 55 | an4s 583 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ (𝑥 # 0 ∧ 𝑦 # 0)) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
57 | 24, 56 | sylan 281 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑥 # 0 ∧ 𝑦 # 0)) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
58 | 57 | anass1rs 566 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 # 0) ∧ 𝑥 # 0) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
59 | 46, 58 | sylan9eqr 2225 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 # 0) ∧
𝑥 # 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
60 | 59 | an32s 563 |
. . . . . . . . . . . . 13
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 # 0) ∧
𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 # 0) → (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
61 | 45, 60 | sylbir 134 |
. . . . . . . . . . . 12
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0) → (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
62 | 42, 61 | jca 304 |
. . . . . . . . . . 11
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0) → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))) |
63 | 62 | ex 114 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝑥 ≠ 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))))) |
64 | 34, 63 | sylbid 149 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝐴 # 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))))) |
65 | 64 | ex 114 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) → (𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))))) |
66 | 65 | anasss 397 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ≠ 0)) → (𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))))) |
67 | 14, 66 | sylan2 284 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))))) |
68 | | rspceov 5895 |
. . . . . . . 8
⊢ (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) → ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ (1 / 𝐴) = (𝑧 / 𝑤)) |
69 | 68 | 3expa 1198 |
. . . . . . 7
⊢ ((((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) → ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ (1 / 𝐴) = (𝑧 / 𝑤)) |
70 | | elq 9581 |
. . . . . . 7
⊢ ((1 /
𝐴) ∈ ℚ ↔
∃𝑧 ∈ ℤ
∃𝑤 ∈ ℕ (1
/ 𝐴) = (𝑧 / 𝑤)) |
71 | 69, 70 | sylibr 133 |
. . . . . 6
⊢ ((((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) → (1 / 𝐴) ∈ ℚ) |
72 | 67, 71 | syl8 71 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 → (1 / 𝐴) ∈ ℚ))) |
73 | 72 | rexlimivv 2593 |
. . . 4
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℕ 𝐴 = (𝑥 / 𝑦) → (𝐴 # 0 → (1 / 𝐴) ∈ ℚ)) |
74 | 12, 73 | sylbi 120 |
. . 3
⊢ (𝐴 ∈ ℚ → (𝐴 # 0 → (1 / 𝐴) ∈
ℚ)) |
75 | 74 | imp 123 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 # 0) → (1 / 𝐴) ∈
ℚ) |
76 | 11, 75 | syldan 280 |
1
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℚ) |