# Metamath Proof Explorer

## Theorem pellexlem3

Description: Lemma for pellex . To each good rational approximation of ( sqrtD ) , there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014)

Ref Expression
Assertion pellexlem3 ${⊢}\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\to \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\preccurlyeq \left\{⟨{y},{z}⟩|\left(\left({y}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({{y}}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right\}$

### Proof

Step Hyp Ref Expression
1 nnex ${⊢}ℕ\in \mathrm{V}$
2 1 1 xpex ${⊢}ℕ×ℕ\in \mathrm{V}$
3 opabssxp ${⊢}\left\{⟨{y},{z}⟩|\left(\left({y}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({{y}}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right\}\subseteq ℕ×ℕ$
4 2 3 ssexi ${⊢}\left\{⟨{y},{z}⟩|\left(\left({y}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({{y}}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right\}\in \mathrm{V}$
5 simprl ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to {a}\in ℚ$
6 simprrl ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to 0<{a}$
7 qgt0numnn ${⊢}\left({a}\in ℚ\wedge 0<{a}\right)\to \mathrm{numer}\left({a}\right)\in ℕ$
8 5 6 7 syl2anc ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to \mathrm{numer}\left({a}\right)\in ℕ$
9 qdencl ${⊢}{a}\in ℚ\to \mathrm{denom}\left({a}\right)\in ℕ$
10 5 9 syl ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to \mathrm{denom}\left({a}\right)\in ℕ$
11 8 10 jca ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to \left(\mathrm{numer}\left({a}\right)\in ℕ\wedge \mathrm{denom}\left({a}\right)\in ℕ\right)$
12 simpll ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to {D}\in ℕ$
13 simplr ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to ¬\sqrt{{D}}\in ℚ$
14 pellexlem1 ${⊢}\left(\left({D}\in ℕ\wedge \mathrm{numer}\left({a}\right)\in ℕ\wedge \mathrm{denom}\left({a}\right)\in ℕ\right)\wedge ¬\sqrt{{D}}\in ℚ\right)\to {\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\ne 0$
15 12 8 10 13 14 syl31anc ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to {\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\ne 0$
16 simprrr ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}$
17 qeqnumdivden ${⊢}{a}\in ℚ\to {a}=\frac{\mathrm{numer}\left({a}\right)}{\mathrm{denom}\left({a}\right)}$
18 17 oveq1d ${⊢}{a}\in ℚ\to {a}-\sqrt{{D}}=\left(\frac{\mathrm{numer}\left({a}\right)}{\mathrm{denom}\left({a}\right)}\right)-\sqrt{{D}}$
19 18 fveq2d ${⊢}{a}\in ℚ\to \left|{a}-\sqrt{{D}}\right|=\left|\left(\frac{\mathrm{numer}\left({a}\right)}{\mathrm{denom}\left({a}\right)}\right)-\sqrt{{D}}\right|$
20 19 breq1d ${⊢}{a}\in ℚ\to \left(\left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}↔\left|\left(\frac{\mathrm{numer}\left({a}\right)}{\mathrm{denom}\left({a}\right)}\right)-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)$
21 5 20 syl ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to \left(\left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}↔\left|\left(\frac{\mathrm{numer}\left({a}\right)}{\mathrm{denom}\left({a}\right)}\right)-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)$
22 16 21 mpbid ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to \left|\left(\frac{\mathrm{numer}\left({a}\right)}{\mathrm{denom}\left({a}\right)}\right)-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}$
23 pellexlem2 ${⊢}\left(\left({D}\in ℕ\wedge \mathrm{numer}\left({a}\right)\in ℕ\wedge \mathrm{denom}\left({a}\right)\in ℕ\right)\wedge \left|\left(\frac{\mathrm{numer}\left({a}\right)}{\mathrm{denom}\left({a}\right)}\right)-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\to \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\right|<1+2\sqrt{{D}}$
24 12 8 10 22 23 syl31anc ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\right|<1+2\sqrt{{D}}$
25 11 15 24 jca32 ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\right)\to \left(\left(\mathrm{numer}\left({a}\right)\in ℕ\wedge \mathrm{denom}\left({a}\right)\in ℕ\right)\wedge \left({\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\ne 0\wedge \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\right|<1+2\sqrt{{D}}\right)\right)$
26 25 ex ${⊢}\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\to \left(\left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)\to \left(\left(\mathrm{numer}\left({a}\right)\in ℕ\wedge \mathrm{denom}\left({a}\right)\in ℕ\right)\wedge \left({\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\ne 0\wedge \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right)$
27 breq2 ${⊢}{x}={a}\to \left(0<{x}↔0<{a}\right)$
28 fvoveq1 ${⊢}{x}={a}\to \left|{x}-\sqrt{{D}}\right|=\left|{a}-\sqrt{{D}}\right|$
29 fveq2 ${⊢}{x}={a}\to \mathrm{denom}\left({x}\right)=\mathrm{denom}\left({a}\right)$
30 29 oveq1d ${⊢}{x}={a}\to {\mathrm{denom}\left({x}\right)}^{-2}={\mathrm{denom}\left({a}\right)}^{-2}$
31 28 30 breq12d ${⊢}{x}={a}\to \left(\left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}↔\left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)$
32 27 31 anbi12d ${⊢}{x}={a}\to \left(\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)↔\left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)$
33 32 elrab ${⊢}{a}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}↔\left({a}\in ℚ\wedge \left(0<{a}\wedge \left|{a}-\sqrt{{D}}\right|<{\mathrm{denom}\left({a}\right)}^{-2}\right)\right)$
34 fvex ${⊢}\mathrm{numer}\left({a}\right)\in \mathrm{V}$
35 fvex ${⊢}\mathrm{denom}\left({a}\right)\in \mathrm{V}$
36 eleq1 ${⊢}{y}=\mathrm{numer}\left({a}\right)\to \left({y}\in ℕ↔\mathrm{numer}\left({a}\right)\in ℕ\right)$
37 36 anbi1d ${⊢}{y}=\mathrm{numer}\left({a}\right)\to \left(\left({y}\in ℕ\wedge {z}\in ℕ\right)↔\left(\mathrm{numer}\left({a}\right)\in ℕ\wedge {z}\in ℕ\right)\right)$
38 oveq1 ${⊢}{y}=\mathrm{numer}\left({a}\right)\to {{y}}^{2}={\mathrm{numer}\left({a}\right)}^{2}$
39 38 oveq1d ${⊢}{y}=\mathrm{numer}\left({a}\right)\to {{y}}^{2}-{D}{{z}}^{2}={\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}$
40 39 neeq1d ${⊢}{y}=\mathrm{numer}\left({a}\right)\to \left({{y}}^{2}-{D}{{z}}^{2}\ne 0↔{\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\ne 0\right)$
41 39 fveq2d ${⊢}{y}=\mathrm{numer}\left({a}\right)\to \left|{{y}}^{2}-{D}{{z}}^{2}\right|=\left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\right|$
42 41 breq1d ${⊢}{y}=\mathrm{numer}\left({a}\right)\to \left(\left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}↔\left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)$
43 40 42 anbi12d ${⊢}{y}=\mathrm{numer}\left({a}\right)\to \left(\left({{y}}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)↔\left({\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)$
44 37 43 anbi12d ${⊢}{y}=\mathrm{numer}\left({a}\right)\to \left(\left(\left({y}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({{y}}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)↔\left(\left(\mathrm{numer}\left({a}\right)\in ℕ\wedge {z}\in ℕ\right)\wedge \left({\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right)$
45 eleq1 ${⊢}{z}=\mathrm{denom}\left({a}\right)\to \left({z}\in ℕ↔\mathrm{denom}\left({a}\right)\in ℕ\right)$
46 45 anbi2d ${⊢}{z}=\mathrm{denom}\left({a}\right)\to \left(\left(\mathrm{numer}\left({a}\right)\in ℕ\wedge {z}\in ℕ\right)↔\left(\mathrm{numer}\left({a}\right)\in ℕ\wedge \mathrm{denom}\left({a}\right)\in ℕ\right)\right)$
47 oveq1 ${⊢}{z}=\mathrm{denom}\left({a}\right)\to {{z}}^{2}={\mathrm{denom}\left({a}\right)}^{2}$
48 47 oveq2d ${⊢}{z}=\mathrm{denom}\left({a}\right)\to {D}{{z}}^{2}={D}{\mathrm{denom}\left({a}\right)}^{2}$
49 48 oveq2d ${⊢}{z}=\mathrm{denom}\left({a}\right)\to {\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}={\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}$
50 49 neeq1d ${⊢}{z}=\mathrm{denom}\left({a}\right)\to \left({\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\ne 0↔{\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\ne 0\right)$
51 49 fveq2d ${⊢}{z}=\mathrm{denom}\left({a}\right)\to \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\right|=\left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\right|$
52 51 breq1d ${⊢}{z}=\mathrm{denom}\left({a}\right)\to \left(\left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}↔\left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\right|<1+2\sqrt{{D}}\right)$
53 50 52 anbi12d ${⊢}{z}=\mathrm{denom}\left({a}\right)\to \left(\left({\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)↔\left({\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\ne 0\wedge \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\right|<1+2\sqrt{{D}}\right)\right)$
54 46 53 anbi12d ${⊢}{z}=\mathrm{denom}\left({a}\right)\to \left(\left(\left(\mathrm{numer}\left({a}\right)\in ℕ\wedge {z}\in ℕ\right)\wedge \left({\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)↔\left(\left(\mathrm{numer}\left({a}\right)\in ℕ\wedge \mathrm{denom}\left({a}\right)\in ℕ\right)\wedge \left({\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\ne 0\wedge \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right)$
55 34 35 44 54 opelopab ${⊢}⟨\mathrm{numer}\left({a}\right),\mathrm{denom}\left({a}\right)⟩\in \left\{⟨{y},{z}⟩|\left(\left({y}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({{y}}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right\}↔\left(\left(\mathrm{numer}\left({a}\right)\in ℕ\wedge \mathrm{denom}\left({a}\right)\in ℕ\right)\wedge \left({\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\ne 0\wedge \left|{\mathrm{numer}\left({a}\right)}^{2}-{D}{\mathrm{denom}\left({a}\right)}^{2}\right|<1+2\sqrt{{D}}\right)\right)$
56 26 33 55 3imtr4g ${⊢}\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\to \left({a}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\to ⟨\mathrm{numer}\left({a}\right),\mathrm{denom}\left({a}\right)⟩\in \left\{⟨{y},{z}⟩|\left(\left({y}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({{y}}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right\}\right)$
57 ssrab2 ${⊢}\left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\subseteq ℚ$
58 simprl ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\wedge {b}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\right)\right)\to {a}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}$
59 57 58 sseldi ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\wedge {b}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\right)\right)\to {a}\in ℚ$
60 simprr ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\wedge {b}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\right)\right)\to {b}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}$
61 57 60 sseldi ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\wedge {b}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\right)\right)\to {b}\in ℚ$
62 34 35 opth ${⊢}⟨\mathrm{numer}\left({a}\right),\mathrm{denom}\left({a}\right)⟩=⟨\mathrm{numer}\left({b}\right),\mathrm{denom}\left({b}\right)⟩↔\left(\mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)\wedge \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)\right)$
63 simprl ${⊢}\left(\left({a}\in ℚ\wedge {b}\in ℚ\right)\wedge \left(\mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)\wedge \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)\right)\right)\to \mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)$
64 simprr ${⊢}\left(\left({a}\in ℚ\wedge {b}\in ℚ\right)\wedge \left(\mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)\wedge \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)\right)\right)\to \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)$
65 63 64 oveq12d ${⊢}\left(\left({a}\in ℚ\wedge {b}\in ℚ\right)\wedge \left(\mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)\wedge \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)\right)\right)\to \frac{\mathrm{numer}\left({a}\right)}{\mathrm{denom}\left({a}\right)}=\frac{\mathrm{numer}\left({b}\right)}{\mathrm{denom}\left({b}\right)}$
66 simpll ${⊢}\left(\left({a}\in ℚ\wedge {b}\in ℚ\right)\wedge \left(\mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)\wedge \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)\right)\right)\to {a}\in ℚ$
67 66 17 syl ${⊢}\left(\left({a}\in ℚ\wedge {b}\in ℚ\right)\wedge \left(\mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)\wedge \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)\right)\right)\to {a}=\frac{\mathrm{numer}\left({a}\right)}{\mathrm{denom}\left({a}\right)}$
68 simplr ${⊢}\left(\left({a}\in ℚ\wedge {b}\in ℚ\right)\wedge \left(\mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)\wedge \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)\right)\right)\to {b}\in ℚ$
69 qeqnumdivden ${⊢}{b}\in ℚ\to {b}=\frac{\mathrm{numer}\left({b}\right)}{\mathrm{denom}\left({b}\right)}$
70 68 69 syl ${⊢}\left(\left({a}\in ℚ\wedge {b}\in ℚ\right)\wedge \left(\mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)\wedge \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)\right)\right)\to {b}=\frac{\mathrm{numer}\left({b}\right)}{\mathrm{denom}\left({b}\right)}$
71 65 67 70 3eqtr4d ${⊢}\left(\left({a}\in ℚ\wedge {b}\in ℚ\right)\wedge \left(\mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)\wedge \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)\right)\right)\to {a}={b}$
72 71 ex ${⊢}\left({a}\in ℚ\wedge {b}\in ℚ\right)\to \left(\left(\mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)\wedge \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)\right)\to {a}={b}\right)$
73 62 72 syl5bi ${⊢}\left({a}\in ℚ\wedge {b}\in ℚ\right)\to \left(⟨\mathrm{numer}\left({a}\right),\mathrm{denom}\left({a}\right)⟩=⟨\mathrm{numer}\left({b}\right),\mathrm{denom}\left({b}\right)⟩\to {a}={b}\right)$
74 fveq2 ${⊢}{a}={b}\to \mathrm{numer}\left({a}\right)=\mathrm{numer}\left({b}\right)$
75 fveq2 ${⊢}{a}={b}\to \mathrm{denom}\left({a}\right)=\mathrm{denom}\left({b}\right)$
76 74 75 opeq12d ${⊢}{a}={b}\to ⟨\mathrm{numer}\left({a}\right),\mathrm{denom}\left({a}\right)⟩=⟨\mathrm{numer}\left({b}\right),\mathrm{denom}\left({b}\right)⟩$
77 73 76 impbid1 ${⊢}\left({a}\in ℚ\wedge {b}\in ℚ\right)\to \left(⟨\mathrm{numer}\left({a}\right),\mathrm{denom}\left({a}\right)⟩=⟨\mathrm{numer}\left({b}\right),\mathrm{denom}\left({b}\right)⟩↔{a}={b}\right)$
78 59 61 77 syl2anc ${⊢}\left(\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\wedge \left({a}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\wedge {b}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\right)\right)\to \left(⟨\mathrm{numer}\left({a}\right),\mathrm{denom}\left({a}\right)⟩=⟨\mathrm{numer}\left({b}\right),\mathrm{denom}\left({b}\right)⟩↔{a}={b}\right)$
79 78 ex ${⊢}\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\to \left(\left({a}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\wedge {b}\in \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\right)\to \left(⟨\mathrm{numer}\left({a}\right),\mathrm{denom}\left({a}\right)⟩=⟨\mathrm{numer}\left({b}\right),\mathrm{denom}\left({b}\right)⟩↔{a}={b}\right)\right)$
80 56 79 dom2d ${⊢}\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\to \left(\left\{⟨{y},{z}⟩|\left(\left({y}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({{y}}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right\}\in \mathrm{V}\to \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\preccurlyeq \left\{⟨{y},{z}⟩|\left(\left({y}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({{y}}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right\}\right)$
81 4 80 mpi ${⊢}\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\to \left\{{x}\in ℚ|\left(0<{x}\wedge \left|{x}-\sqrt{{D}}\right|<{\mathrm{denom}\left({x}\right)}^{-2}\right)\right\}\preccurlyeq \left\{⟨{y},{z}⟩|\left(\left({y}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({{y}}^{2}-{D}{{z}}^{2}\ne 0\wedge \left|{{y}}^{2}-{D}{{z}}^{2}\right|<1+2\sqrt{{D}}\right)\right)\right\}$