Step | Hyp | Ref
| Expression |
1 | | nnex 10903 |
. . . 4
⊢ ℕ
∈ V |
2 | 1, 1 | xpex 6860 |
. . 3
⊢ (ℕ
× ℕ) ∈ V |
3 | | opabssxp 5116 |
. . 3
⊢
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
⊆ (ℕ × ℕ) |
4 | 2, 3 | ssexi 4731 |
. 2
⊢
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∈ V |
5 | | simprl 790 |
. . . . . . . 8
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → 𝑎 ∈ ℚ) |
6 | | simprrl 800 |
. . . . . . . 8
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → 0 < 𝑎) |
7 | | qgt0numnn 15297 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℚ ∧ 0 <
𝑎) →
(numer‘𝑎) ∈
ℕ) |
8 | 5, 6, 7 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → (numer‘𝑎) ∈
ℕ) |
9 | | qdencl 15287 |
. . . . . . . 8
⊢ (𝑎 ∈ ℚ →
(denom‘𝑎) ∈
ℕ) |
10 | 5, 9 | syl 17 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → (denom‘𝑎) ∈
ℕ) |
11 | 8, 10 | jca 553 |
. . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → ((numer‘𝑎) ∈ ℕ ∧
(denom‘𝑎) ∈
ℕ)) |
12 | | simpll 786 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → 𝐷 ∈ ℕ) |
13 | | simplr 788 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → ¬
(√‘𝐷) ∈
ℚ) |
14 | | pellexlem1 36411 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧
(numer‘𝑎) ∈
ℕ ∧ (denom‘𝑎) ∈ ℕ) ∧ ¬
(√‘𝐷) ∈
ℚ) → (((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠ 0) |
15 | 12, 8, 10, 13, 14 | syl31anc 1321 |
. . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → (((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠
0) |
16 | | simprrr 801 |
. . . . . . . 8
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → (abs‘(𝑎 − (√‘𝐷))) < ((denom‘𝑎)↑-2)) |
17 | | qeqnumdivden 15292 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℚ → 𝑎 = ((numer‘𝑎) / (denom‘𝑎))) |
18 | 17 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℚ → (𝑎 − (√‘𝐷)) = (((numer‘𝑎) / (denom‘𝑎)) − (√‘𝐷))) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℚ →
(abs‘(𝑎 −
(√‘𝐷))) =
(abs‘(((numer‘𝑎) / (denom‘𝑎)) − (√‘𝐷)))) |
20 | 19 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℚ →
((abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)
↔ (abs‘(((numer‘𝑎) / (denom‘𝑎)) − (√‘𝐷))) < ((denom‘𝑎)↑-2))) |
21 | 5, 20 | syl 17 |
. . . . . . . 8
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → ((abs‘(𝑎 − (√‘𝐷))) < ((denom‘𝑎)↑-2) ↔
(abs‘(((numer‘𝑎) / (denom‘𝑎)) − (√‘𝐷))) < ((denom‘𝑎)↑-2))) |
22 | 16, 21 | mpbid 221 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) →
(abs‘(((numer‘𝑎) / (denom‘𝑎)) − (√‘𝐷))) < ((denom‘𝑎)↑-2)) |
23 | | pellexlem2 36412 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧
(numer‘𝑎) ∈
ℕ ∧ (denom‘𝑎) ∈ ℕ) ∧
(abs‘(((numer‘𝑎) / (denom‘𝑎)) − (√‘𝐷))) < ((denom‘𝑎)↑-2)) →
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷)))) |
24 | 12, 8, 10, 22, 23 | syl31anc 1321 |
. . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) →
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷)))) |
25 | 11, 15, 24 | jca32 556 |
. . . . 5
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → (((numer‘𝑎) ∈ ℕ ∧
(denom‘𝑎) ∈
ℕ) ∧ ((((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷)))))) |
26 | 25 | ex 449 |
. . . 4
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ((𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))
→ (((numer‘𝑎)
∈ ℕ ∧ (denom‘𝑎) ∈ ℕ) ∧ ((((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷))))))) |
27 | | breq2 4587 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (0 < 𝑥 ↔ 0 < 𝑎)) |
28 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (𝑥 − (√‘𝐷)) = (𝑎 − (√‘𝐷))) |
29 | 28 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → (abs‘(𝑥 − (√‘𝐷))) = (abs‘(𝑎 − (√‘𝐷)))) |
30 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (denom‘𝑥) = (denom‘𝑎)) |
31 | 30 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → ((denom‘𝑥)↑-2) = ((denom‘𝑎)↑-2)) |
32 | 29, 31 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = 𝑎 → ((abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2) ↔ (abs‘(𝑎 − (√‘𝐷))) < ((denom‘𝑎)↑-2))) |
33 | 27, 32 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = 𝑎 → ((0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2)) ↔ (0 < 𝑎 ∧ (abs‘(𝑎 − (√‘𝐷))) < ((denom‘𝑎)↑-2)))) |
34 | 33 | elrab 3331 |
. . . 4
⊢ (𝑎 ∈ {𝑥 ∈ ℚ ∣ (0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))} ↔ (𝑎 ∈ ℚ ∧ (0 <
𝑎 ∧ (abs‘(𝑎 − (√‘𝐷))) < ((denom‘𝑎)↑-2)))) |
35 | | fvex 6113 |
. . . . 5
⊢
(numer‘𝑎)
∈ V |
36 | | fvex 6113 |
. . . . 5
⊢
(denom‘𝑎)
∈ V |
37 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑦 = (numer‘𝑎) → (𝑦 ∈ ℕ ↔ (numer‘𝑎) ∈
ℕ)) |
38 | 37 | anbi1d 737 |
. . . . . 6
⊢ (𝑦 = (numer‘𝑎) → ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ↔ ((numer‘𝑎) ∈ ℕ ∧ 𝑧 ∈
ℕ))) |
39 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑦 = (numer‘𝑎) → (𝑦↑2) = ((numer‘𝑎)↑2)) |
40 | 39 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑦 = (numer‘𝑎) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = (((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) |
41 | 40 | neeq1d 2841 |
. . . . . . 7
⊢ (𝑦 = (numer‘𝑎) → (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ↔ (((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))) ≠ 0)) |
42 | 40 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑦 = (numer‘𝑎) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) = (abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))))) |
43 | 42 | breq1d 4593 |
. . . . . . 7
⊢ (𝑦 = (numer‘𝑎) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))) ↔
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))))) |
44 | 41, 43 | anbi12d 743 |
. . . . . 6
⊢ (𝑦 = (numer‘𝑎) → ((((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))) ↔
((((numer‘𝑎)↑2)
− (𝐷 · (𝑧↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))) |
45 | 38, 44 | anbi12d 743 |
. . . . 5
⊢ (𝑦 = (numer‘𝑎) → (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))
↔ (((numer‘𝑎)
∈ ℕ ∧ 𝑧
∈ ℕ) ∧ ((((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))))))) |
46 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑧 = (denom‘𝑎) → (𝑧 ∈ ℕ ↔ (denom‘𝑎) ∈
ℕ)) |
47 | 46 | anbi2d 736 |
. . . . . 6
⊢ (𝑧 = (denom‘𝑎) → (((numer‘𝑎) ∈ ℕ ∧ 𝑧 ∈ ℕ) ↔
((numer‘𝑎) ∈
ℕ ∧ (denom‘𝑎) ∈ ℕ))) |
48 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑧 = (denom‘𝑎) → (𝑧↑2) = ((denom‘𝑎)↑2)) |
49 | 48 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑧 = (denom‘𝑎) → (𝐷 · (𝑧↑2)) = (𝐷 · ((denom‘𝑎)↑2))) |
50 | 49 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑧 = (denom‘𝑎) → (((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))) = (((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) |
51 | 50 | neeq1d 2841 |
. . . . . . 7
⊢ (𝑧 = (denom‘𝑎) → ((((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ↔ (((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠
0)) |
52 | 50 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑧 = (denom‘𝑎) →
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) = (abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))))) |
53 | 52 | breq1d 4593 |
. . . . . . 7
⊢ (𝑧 = (denom‘𝑎) →
((abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))) ↔
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷))))) |
54 | 51, 53 | anbi12d 743 |
. . . . . 6
⊢ (𝑧 = (denom‘𝑎) → (((((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))) ↔
((((numer‘𝑎)↑2)
− (𝐷 ·
((denom‘𝑎)↑2)))
≠ 0 ∧ (abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷)))))) |
55 | 47, 54 | anbi12d 743 |
. . . . 5
⊢ (𝑧 = (denom‘𝑎) → ((((numer‘𝑎) ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧
((((numer‘𝑎)↑2)
− (𝐷 · (𝑧↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))
↔ (((numer‘𝑎)
∈ ℕ ∧ (denom‘𝑎) ∈ ℕ) ∧ ((((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷))))))) |
56 | 35, 36, 45, 55 | opelopab 4922 |
. . . 4
⊢
(〈(numer‘𝑎), (denom‘𝑎)〉 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
↔ (((numer‘𝑎)
∈ ℕ ∧ (denom‘𝑎) ∈ ℕ) ∧ ((((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷)))))) |
57 | 26, 34, 56 | 3imtr4g 284 |
. . 3
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
→ 〈(numer‘𝑎), (denom‘𝑎)〉 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))})) |
58 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))} ⊆
ℚ |
59 | | simprl 790 |
. . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))})) → 𝑎 ∈ {𝑥 ∈ ℚ ∣ (0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))}) |
60 | 58, 59 | sseldi 3566 |
. . . . 5
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))})) → 𝑎 ∈
ℚ) |
61 | | simprr 792 |
. . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))})) → 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))}) |
62 | 58, 61 | sseldi 3566 |
. . . . 5
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))})) → 𝑏 ∈
ℚ) |
63 | 35, 36 | opth 4871 |
. . . . . . 7
⊢
(〈(numer‘𝑎), (denom‘𝑎)〉 = 〈(numer‘𝑏), (denom‘𝑏)〉 ↔
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) |
64 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
(numer‘𝑎) =
(numer‘𝑏)) |
65 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
(denom‘𝑎) =
(denom‘𝑏)) |
66 | 64, 65 | oveq12d 6567 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
((numer‘𝑎) /
(denom‘𝑎)) =
((numer‘𝑏) /
(denom‘𝑏))) |
67 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
𝑎 ∈
ℚ) |
68 | 67, 17 | syl 17 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
𝑎 = ((numer‘𝑎) / (denom‘𝑎))) |
69 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
𝑏 ∈
ℚ) |
70 | | qeqnumdivden 15292 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ℚ → 𝑏 = ((numer‘𝑏) / (denom‘𝑏))) |
71 | 69, 70 | syl 17 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
𝑏 = ((numer‘𝑏) / (denom‘𝑏))) |
72 | 66, 68, 71 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
𝑎 = 𝑏) |
73 | 72 | ex 449 |
. . . . . . 7
⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) →
(((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏)) →
𝑎 = 𝑏)) |
74 | 63, 73 | syl5bi 231 |
. . . . . 6
⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) →
(〈(numer‘𝑎),
(denom‘𝑎)〉 =
〈(numer‘𝑏),
(denom‘𝑏)〉
→ 𝑎 = 𝑏)) |
75 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (numer‘𝑎) = (numer‘𝑏)) |
76 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (denom‘𝑎) = (denom‘𝑏)) |
77 | 75, 76 | opeq12d 4348 |
. . . . . 6
⊢ (𝑎 = 𝑏 → 〈(numer‘𝑎), (denom‘𝑎)〉 = 〈(numer‘𝑏), (denom‘𝑏)〉) |
78 | 74, 77 | impbid1 214 |
. . . . 5
⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) →
(〈(numer‘𝑎),
(denom‘𝑎)〉 =
〈(numer‘𝑏),
(denom‘𝑏)〉
↔ 𝑎 = 𝑏)) |
79 | 60, 62, 78 | syl2anc 691 |
. . . 4
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))})) →
(〈(numer‘𝑎),
(denom‘𝑎)〉 =
〈(numer‘𝑏),
(denom‘𝑏)〉
↔ 𝑎 = 𝑏)) |
80 | 79 | ex 449 |
. . 3
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ((𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))}) →
(〈(numer‘𝑎),
(denom‘𝑎)〉 =
〈(numer‘𝑏),
(denom‘𝑏)〉
↔ 𝑎 = 𝑏))) |
81 | 57, 80 | dom2d 7882 |
. 2
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ({〈𝑦,
𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∈ V → {𝑥 ∈
ℚ ∣ (0 < 𝑥
∧ (abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
≼ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))})) |
82 | 4, 81 | mpi 20 |
1
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → {𝑥 ∈
ℚ ∣ (0 < 𝑥
∧ (abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
≼ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}) |