Step | Hyp | Ref
| Expression |
1 | | elq 9509 |
. . . . 5
⊢ (𝐴 ∈ ℚ ↔
∃𝑧 ∈ ℤ
∃𝑦 ∈ ℕ
𝐴 = (𝑧 / 𝑦)) |
2 | | rexcom 2618 |
. . . . 5
⊢
(∃𝑧 ∈
ℤ ∃𝑦 ∈
ℕ 𝐴 = (𝑧 / 𝑦) ↔ ∃𝑦 ∈ ℕ ∃𝑧 ∈ ℤ 𝐴 = (𝑧 / 𝑦)) |
3 | 1, 2 | bitri 183 |
. . . 4
⊢ (𝐴 ∈ ℚ ↔
∃𝑦 ∈ ℕ
∃𝑧 ∈ ℤ
𝐴 = (𝑧 / 𝑦)) |
4 | | breq2 3965 |
. . . . . . . . . . 11
⊢ (𝐴 = (𝑧 / 𝑦) → (0 < 𝐴 ↔ 0 < (𝑧 / 𝑦))) |
5 | | zre 9150 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) |
6 | 5 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈
ℝ) |
7 | | nnre 8819 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
8 | 7 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑦 ∈
ℝ) |
9 | | nngt0 8837 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 0 <
𝑦) |
10 | 9 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 0 <
𝑦) |
11 | | gt0div 8720 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 0 <
𝑦) → (0 < 𝑧 ↔ 0 < (𝑧 / 𝑦))) |
12 | 6, 8, 10, 11 | syl3anc 1217 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (0 <
𝑧 ↔ 0 < (𝑧 / 𝑦))) |
13 | 12 | bicomd 140 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (0 <
(𝑧 / 𝑦) ↔ 0 < 𝑧)) |
14 | 4, 13 | sylan9bb 458 |
. . . . . . . . . 10
⊢ ((𝐴 = (𝑧 / 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (0 < 𝐴 ↔ 0 < 𝑧)) |
15 | | elnnz 9156 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ℕ ↔ (𝑧 ∈ ℤ ∧ 0 <
𝑧)) |
16 | 15 | simplbi2 383 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℤ → (0 <
𝑧 → 𝑧 ∈ ℕ)) |
17 | 16 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (0 <
𝑧 → 𝑧 ∈ ℕ)) |
18 | 17 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = (𝑧 / 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (0 < 𝑧 → 𝑧 ∈ ℕ)) |
19 | 18 | imp 123 |
. . . . . . . . . . . 12
⊢ (((𝐴 = (𝑧 / 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) ∧ 0 < 𝑧) → 𝑧 ∈ ℕ) |
20 | | oveq1 5821 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑥 / 𝑦) = (𝑧 / 𝑦)) |
21 | 20 | eqeq2d 2166 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝐴 = (𝑥 / 𝑦) ↔ 𝐴 = (𝑧 / 𝑦))) |
22 | 21 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((((𝐴 = (𝑧 / 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) ∧ 0 < 𝑧) ∧ 𝑥 = 𝑧) → (𝐴 = (𝑥 / 𝑦) ↔ 𝐴 = (𝑧 / 𝑦))) |
23 | | simpll 519 |
. . . . . . . . . . . 12
⊢ (((𝐴 = (𝑧 / 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) ∧ 0 < 𝑧) → 𝐴 = (𝑧 / 𝑦)) |
24 | 19, 22, 23 | rspcedvd 2819 |
. . . . . . . . . . 11
⊢ (((𝐴 = (𝑧 / 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) ∧ 0 < 𝑧) → ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
25 | 24 | ex 114 |
. . . . . . . . . 10
⊢ ((𝐴 = (𝑧 / 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (0 < 𝑧 → ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦))) |
26 | 14, 25 | sylbid 149 |
. . . . . . . . 9
⊢ ((𝐴 = (𝑧 / 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (0 < 𝐴 → ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦))) |
27 | 26 | ex 114 |
. . . . . . . 8
⊢ (𝐴 = (𝑧 / 𝑦) → ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (0 < 𝐴 → ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦)))) |
28 | 27 | com13 80 |
. . . . . . 7
⊢ (0 <
𝐴 → ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝐴 = (𝑧 / 𝑦) → ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦)))) |
29 | 28 | impl 378 |
. . . . . 6
⊢ (((0 <
𝐴 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ ℤ) → (𝐴 = (𝑧 / 𝑦) → ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦))) |
30 | 29 | rexlimdva 2571 |
. . . . 5
⊢ ((0 <
𝐴 ∧ 𝑦 ∈ ℕ) → (∃𝑧 ∈ ℤ 𝐴 = (𝑧 / 𝑦) → ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦))) |
31 | 30 | reximdva 2556 |
. . . 4
⊢ (0 <
𝐴 → (∃𝑦 ∈ ℕ ∃𝑧 ∈ ℤ 𝐴 = (𝑧 / 𝑦) → ∃𝑦 ∈ ℕ ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦))) |
32 | 3, 31 | syl5bi 151 |
. . 3
⊢ (0 <
𝐴 → (𝐴 ∈ ℚ → ∃𝑦 ∈ ℕ ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦))) |
33 | 32 | impcom 124 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 0 <
𝐴) → ∃𝑦 ∈ ℕ ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
34 | | rexcom 2618 |
. 2
⊢
(∃𝑥 ∈
ℕ ∃𝑦 ∈
ℕ 𝐴 = (𝑥 / 𝑦) ↔ ∃𝑦 ∈ ℕ ∃𝑥 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
35 | 33, 34 | sylibr 133 |
1
⊢ ((𝐴 ∈ ℚ ∧ 0 <
𝐴) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |