| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnex 12272 | . . . 4
⊢ ℕ
∈ V | 
| 2 | 1, 1 | xpex 7773 | . . 3
⊢ (ℕ
× ℕ) ∈ V | 
| 3 |  | opabssxp 5778 | . . 3
⊢
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
⊆ (ℕ × ℕ) | 
| 4 | 2, 3 | ssexi 5322 | . 2
⊢
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∈ V | 
| 5 |  | simprl 771 | . . . . . . . 8
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → 𝑎 ∈ ℚ) | 
| 6 |  | simprrl 781 | . . . . . . . 8
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → 0 < 𝑎) | 
| 7 |  | qgt0numnn 16788 | . . . . . . . 8
⊢ ((𝑎 ∈ ℚ ∧ 0 <
𝑎) →
(numer‘𝑎) ∈
ℕ) | 
| 8 | 5, 6, 7 | syl2anc 584 | . . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → (numer‘𝑎) ∈
ℕ) | 
| 9 |  | qdencl 16778 | . . . . . . . 8
⊢ (𝑎 ∈ ℚ →
(denom‘𝑎) ∈
ℕ) | 
| 10 | 5, 9 | syl 17 | . . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → (denom‘𝑎) ∈
ℕ) | 
| 11 | 8, 10 | jca 511 | . . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → ((numer‘𝑎) ∈ ℕ ∧
(denom‘𝑎) ∈
ℕ)) | 
| 12 |  | simpll 767 | . . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → 𝐷 ∈ ℕ) | 
| 13 |  | simplr 769 | . . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → ¬
(√‘𝐷) ∈
ℚ) | 
| 14 |  | pellexlem1 42840 | . . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧
(numer‘𝑎) ∈
ℕ ∧ (denom‘𝑎) ∈ ℕ) ∧ ¬
(√‘𝐷) ∈
ℚ) → (((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠ 0) | 
| 15 | 12, 8, 10, 13, 14 | syl31anc 1375 | . . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → (((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠
0) | 
| 16 |  | simprrr 782 | . . . . . . . 8
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → (abs‘(𝑎 − (√‘𝐷))) < ((denom‘𝑎)↑-2)) | 
| 17 |  | qeqnumdivden 16783 | . . . . . . . . . . . 12
⊢ (𝑎 ∈ ℚ → 𝑎 = ((numer‘𝑎) / (denom‘𝑎))) | 
| 18 | 17 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝑎 ∈ ℚ → (𝑎 − (√‘𝐷)) = (((numer‘𝑎) / (denom‘𝑎)) − (√‘𝐷))) | 
| 19 | 18 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝑎 ∈ ℚ →
(abs‘(𝑎 −
(√‘𝐷))) =
(abs‘(((numer‘𝑎) / (denom‘𝑎)) − (√‘𝐷)))) | 
| 20 | 19 | breq1d 5153 | . . . . . . . . 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 232 | . . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) →
(abs‘(((numer‘𝑎) / (denom‘𝑎)) − (√‘𝐷))) < ((denom‘𝑎)↑-2)) | 
| 23 |  | pellexlem2 42841 | . . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧
(numer‘𝑎) ∈
ℕ ∧ (denom‘𝑎) ∈ ℕ) ∧
(abs‘(((numer‘𝑎) / (denom‘𝑎)) − (√‘𝐷))) < ((denom‘𝑎)↑-2)) →
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷)))) | 
| 24 | 12, 8, 10, 22, 23 | syl31anc 1375 | . . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) →
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷)))) | 
| 25 | 11, 15, 24 | jca32 515 | . . . . 5
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))) → (((numer‘𝑎) ∈ ℕ ∧
(denom‘𝑎) ∈
ℕ) ∧ ((((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷)))))) | 
| 26 | 25 | ex 412 | . . . 4
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ((𝑎 ∈
ℚ ∧ (0 < 𝑎
∧ (abs‘(𝑎 −
(√‘𝐷))) <
((denom‘𝑎)↑-2)))
→ (((numer‘𝑎)
∈ ℕ ∧ (denom‘𝑎) ∈ ℕ) ∧ ((((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷))))))) | 
| 27 |  | breq2 5147 | . . . . . 6
⊢ (𝑥 = 𝑎 → (0 < 𝑥 ↔ 0 < 𝑎)) | 
| 28 |  | fvoveq1 7454 | . . . . . . 7
⊢ (𝑥 = 𝑎 → (abs‘(𝑥 − (√‘𝐷))) = (abs‘(𝑎 − (√‘𝐷)))) | 
| 29 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑥 = 𝑎 → (denom‘𝑥) = (denom‘𝑎)) | 
| 30 | 29 | oveq1d 7446 | . . . . . . 7
⊢ (𝑥 = 𝑎 → ((denom‘𝑥)↑-2) = ((denom‘𝑎)↑-2)) | 
| 31 | 28, 30 | breq12d 5156 | . . . . . 6
⊢ (𝑥 = 𝑎 → ((abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2) ↔ (abs‘(𝑎 − (√‘𝐷))) < ((denom‘𝑎)↑-2))) | 
| 32 | 27, 31 | anbi12d 632 | . . . . 5
⊢ (𝑥 = 𝑎 → ((0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2)) ↔ (0 < 𝑎 ∧ (abs‘(𝑎 − (√‘𝐷))) < ((denom‘𝑎)↑-2)))) | 
| 33 | 32 | elrab 3692 | . . . 4
⊢ (𝑎 ∈ {𝑥 ∈ ℚ ∣ (0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))} ↔ (𝑎 ∈ ℚ ∧ (0 <
𝑎 ∧ (abs‘(𝑎 − (√‘𝐷))) < ((denom‘𝑎)↑-2)))) | 
| 34 |  | fvex 6919 | . . . . 5
⊢
(numer‘𝑎)
∈ V | 
| 35 |  | fvex 6919 | . . . . 5
⊢
(denom‘𝑎)
∈ V | 
| 36 |  | eleq1 2829 | . . . . . . 7
⊢ (𝑦 = (numer‘𝑎) → (𝑦 ∈ ℕ ↔ (numer‘𝑎) ∈
ℕ)) | 
| 37 | 36 | anbi1d 631 | . . . . . 6
⊢ (𝑦 = (numer‘𝑎) → ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ↔ ((numer‘𝑎) ∈ ℕ ∧ 𝑧 ∈
ℕ))) | 
| 38 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑦 = (numer‘𝑎) → (𝑦↑2) = ((numer‘𝑎)↑2)) | 
| 39 | 38 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑦 = (numer‘𝑎) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = (((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) | 
| 40 | 39 | neeq1d 3000 | . . . . . . 7
⊢ (𝑦 = (numer‘𝑎) → (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ↔ (((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))) ≠ 0)) | 
| 41 | 39 | fveq2d 6910 | . . . . . . . 8
⊢ (𝑦 = (numer‘𝑎) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) = (abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))))) | 
| 42 | 41 | breq1d 5153 | . . . . . . 7
⊢ (𝑦 = (numer‘𝑎) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))) ↔
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))))) | 
| 43 | 40, 42 | anbi12d 632 | . . . . . 6
⊢ (𝑦 = (numer‘𝑎) → ((((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))) ↔
((((numer‘𝑎)↑2)
− (𝐷 · (𝑧↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))) | 
| 44 | 37, 43 | anbi12d 632 | . . . . 5
⊢ (𝑦 = (numer‘𝑎) → (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))
↔ (((numer‘𝑎)
∈ ℕ ∧ 𝑧
∈ ℕ) ∧ ((((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))))))) | 
| 45 |  | eleq1 2829 | . . . . . . 7
⊢ (𝑧 = (denom‘𝑎) → (𝑧 ∈ ℕ ↔ (denom‘𝑎) ∈
ℕ)) | 
| 46 | 45 | anbi2d 630 | . . . . . 6
⊢ (𝑧 = (denom‘𝑎) → (((numer‘𝑎) ∈ ℕ ∧ 𝑧 ∈ ℕ) ↔
((numer‘𝑎) ∈
ℕ ∧ (denom‘𝑎) ∈ ℕ))) | 
| 47 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑧 = (denom‘𝑎) → (𝑧↑2) = ((denom‘𝑎)↑2)) | 
| 48 | 47 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑧 = (denom‘𝑎) → (𝐷 · (𝑧↑2)) = (𝐷 · ((denom‘𝑎)↑2))) | 
| 49 | 48 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑧 = (denom‘𝑎) → (((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))) = (((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) | 
| 50 | 49 | neeq1d 3000 | . . . . . . 7
⊢ (𝑧 = (denom‘𝑎) → ((((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ↔ (((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))) ≠
0)) | 
| 51 | 49 | fveq2d 6910 | . . . . . . . 8
⊢ (𝑧 = (denom‘𝑎) →
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) = (abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2))))) | 
| 52 | 51 | breq1d 5153 | . . . . . . 7
⊢ (𝑧 = (denom‘𝑎) →
((abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))) ↔
(abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷))))) | 
| 53 | 50, 52 | anbi12d 632 | . . . . . 6
⊢ (𝑧 = (denom‘𝑎) → (((((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧
(abs‘(((numer‘𝑎)↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))) ↔
((((numer‘𝑎)↑2)
− (𝐷 ·
((denom‘𝑎)↑2)))
≠ 0 ∧ (abs‘(((numer‘𝑎)↑2) − (𝐷 · ((denom‘𝑎)↑2)))) < (1 + (2 ·
(√‘𝐷)))))) | 
| 54 | 46, 53 | anbi12d 632 | . . . . 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 ·
(√‘𝐷))))))) | 
| 55 | 34, 35, 44, 54 | opelopab 5547 | . . . 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 ·
(√‘𝐷)))))) | 
| 56 | 26, 33, 55 | 3imtr4g 296 | . . 3
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
→ 〈(numer‘𝑎), (denom‘𝑎)〉 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))})) | 
| 57 |  | ssrab2 4080 | . . . . . 6
⊢ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))} ⊆
ℚ | 
| 58 |  | simprl 771 | . . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))})) → 𝑎 ∈ {𝑥 ∈ ℚ ∣ (0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))}) | 
| 59 | 57, 58 | sselid 3981 | . . . . 5
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))})) → 𝑎 ∈
ℚ) | 
| 60 |  | simprr 773 | . . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))})) → 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))}) | 
| 61 | 57, 60 | sselid 3981 | . . . . 5
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))})) → 𝑏 ∈
ℚ) | 
| 62 | 34, 35 | opth 5481 | . . . . . . 7
⊢
(〈(numer‘𝑎), (denom‘𝑎)〉 = 〈(numer‘𝑏), (denom‘𝑏)〉 ↔
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) | 
| 63 |  | simprl 771 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
(numer‘𝑎) =
(numer‘𝑏)) | 
| 64 |  | simprr 773 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
(denom‘𝑎) =
(denom‘𝑏)) | 
| 65 | 63, 64 | oveq12d 7449 | . . . . . . . . 9
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
((numer‘𝑎) /
(denom‘𝑎)) =
((numer‘𝑏) /
(denom‘𝑏))) | 
| 66 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
𝑎 ∈
ℚ) | 
| 67 | 66, 17 | syl 17 | . . . . . . . . 9
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
𝑎 = ((numer‘𝑎) / (denom‘𝑎))) | 
| 68 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
𝑏 ∈
ℚ) | 
| 69 |  | qeqnumdivden 16783 | . . . . . . . . . 10
⊢ (𝑏 ∈ ℚ → 𝑏 = ((numer‘𝑏) / (denom‘𝑏))) | 
| 70 | 68, 69 | syl 17 | . . . . . . . . 9
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
𝑏 = ((numer‘𝑏) / (denom‘𝑏))) | 
| 71 | 65, 67, 70 | 3eqtr4d 2787 | . . . . . . . 8
⊢ (((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) ∧
((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏))) →
𝑎 = 𝑏) | 
| 72 | 71 | ex 412 | . . . . . . 7
⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) →
(((numer‘𝑎) =
(numer‘𝑏) ∧
(denom‘𝑎) =
(denom‘𝑏)) →
𝑎 = 𝑏)) | 
| 73 | 62, 72 | biimtrid 242 | . . . . . 6
⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) →
(〈(numer‘𝑎),
(denom‘𝑎)〉 =
〈(numer‘𝑏),
(denom‘𝑏)〉
→ 𝑎 = 𝑏)) | 
| 74 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑎 = 𝑏 → (numer‘𝑎) = (numer‘𝑏)) | 
| 75 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑎 = 𝑏 → (denom‘𝑎) = (denom‘𝑏)) | 
| 76 | 74, 75 | opeq12d 4881 | . . . . . 6
⊢ (𝑎 = 𝑏 → 〈(numer‘𝑎), (denom‘𝑎)〉 = 〈(numer‘𝑏), (denom‘𝑏)〉) | 
| 77 | 73, 76 | impbid1 225 | . . . . 5
⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ) →
(〈(numer‘𝑎),
(denom‘𝑎)〉 =
〈(numer‘𝑏),
(denom‘𝑏)〉
↔ 𝑎 = 𝑏)) | 
| 78 | 59, 61, 77 | syl2anc 584 | . . . 4
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))})) →
(〈(numer‘𝑎),
(denom‘𝑎)〉 =
〈(numer‘𝑏),
(denom‘𝑏)〉
↔ 𝑎 = 𝑏)) | 
| 79 | 78 | ex 412 | . . 3
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ((𝑎 ∈
{𝑥 ∈ ℚ ∣
(0 < 𝑥 ∧
(abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
∧ 𝑏 ∈ {𝑥 ∈ ℚ ∣ (0 <
𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))}) →
(〈(numer‘𝑎),
(denom‘𝑎)〉 =
〈(numer‘𝑏),
(denom‘𝑏)〉
↔ 𝑎 = 𝑏))) | 
| 80 | 56, 79 | dom2d 9033 | . 2
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ({〈𝑦,
𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∈ V → {𝑥 ∈
ℚ ∣ (0 < 𝑥
∧ (abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
≼ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))})) | 
| 81 | 4, 80 | mpi 20 | 1
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → {𝑥 ∈
ℚ ∣ (0 < 𝑥
∧ (abs‘(𝑥 −
(√‘𝐷))) <
((denom‘𝑥)↑-2))}
≼ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}) |