# Metamath Proof Explorer

## Theorem pellexlem2

Description: Lemma for pellex . Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014)

Ref Expression
Assertion pellexlem2 ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|{{A}}^{2}-{D}{{B}}^{2}\right|<1+2\sqrt{{D}}$

### Proof

Step Hyp Ref Expression
1 simpl3 ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {B}\in ℕ$
2 1 nnred ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {B}\in ℝ$
3 2 resqcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\in ℝ$
4 2 sqge0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0\le {{B}}^{2}$
5 3 4 absidd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|{{B}}^{2}\right|={{B}}^{2}$
6 5 eqcomd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}=\left|{{B}}^{2}\right|$
7 6 oveq2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{\left|{{A}}^{2}-{D}{{B}}^{2}\right|}{{{B}}^{2}}=\frac{\left|{{A}}^{2}-{D}{{B}}^{2}\right|}{\left|{{B}}^{2}\right|}$
8 simpl2 ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {A}\in ℕ$
9 8 nncnd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {A}\in ℂ$
10 9 sqcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{A}}^{2}\in ℂ$
11 simpl1 ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {D}\in ℕ$
12 11 nncnd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {D}\in ℂ$
13 1 nncnd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {B}\in ℂ$
14 13 sqcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\in ℂ$
15 12 14 mulcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {D}{{B}}^{2}\in ℂ$
16 10 15 subcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{A}}^{2}-{D}{{B}}^{2}\in ℂ$
17 1 nnne0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {B}\ne 0$
18 sqne0 ${⊢}{B}\in ℂ\to \left({{B}}^{2}\ne 0↔{B}\ne 0\right)$
19 18 biimpar ${⊢}\left({B}\in ℂ\wedge {B}\ne 0\right)\to {{B}}^{2}\ne 0$
20 13 17 19 syl2anc ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\ne 0$
21 16 14 20 absdivd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\frac{{{A}}^{2}-{D}{{B}}^{2}}{{{B}}^{2}}\right|=\frac{\left|{{A}}^{2}-{D}{{B}}^{2}\right|}{\left|{{B}}^{2}\right|}$
22 7 21 eqtr4d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{\left|{{A}}^{2}-{D}{{B}}^{2}\right|}{{{B}}^{2}}=\left|\frac{{{A}}^{2}-{D}{{B}}^{2}}{{{B}}^{2}}\right|$
23 22 oveq2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\left(\frac{\left|{{A}}^{2}-{D}{{B}}^{2}\right|}{{{B}}^{2}}\right)={{B}}^{2}\left|\frac{{{A}}^{2}-{D}{{B}}^{2}}{{{B}}^{2}}\right|$
24 16 abscld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|{{A}}^{2}-{D}{{B}}^{2}\right|\in ℝ$
25 24 recnd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|{{A}}^{2}-{D}{{B}}^{2}\right|\in ℂ$
26 25 14 20 divcan2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\left(\frac{\left|{{A}}^{2}-{D}{{B}}^{2}\right|}{{{B}}^{2}}\right)=\left|{{A}}^{2}-{D}{{B}}^{2}\right|$
27 10 15 14 20 divsubdird ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{{{A}}^{2}-{D}{{B}}^{2}}{{{B}}^{2}}=\left(\frac{{{A}}^{2}}{{{B}}^{2}}\right)-\left(\frac{{D}{{B}}^{2}}{{{B}}^{2}}\right)$
28 9 13 17 sqdivd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {\left(\frac{{A}}{{B}}\right)}^{2}=\frac{{{A}}^{2}}{{{B}}^{2}}$
29 28 eqcomd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{{{A}}^{2}}{{{B}}^{2}}={\left(\frac{{A}}{{B}}\right)}^{2}$
30 11 nnred ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {D}\in ℝ$
31 11 nnnn0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {D}\in {ℕ}_{0}$
32 31 nn0ge0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0\le {D}$
33 remsqsqrt ${⊢}\left({D}\in ℝ\wedge 0\le {D}\right)\to \sqrt{{D}}\sqrt{{D}}={D}$
34 30 32 33 syl2anc ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \sqrt{{D}}\sqrt{{D}}={D}$
35 30 32 resqrtcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \sqrt{{D}}\in ℝ$
36 35 recnd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \sqrt{{D}}\in ℂ$
37 36 sqvald ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {\sqrt{{D}}}^{2}=\sqrt{{D}}\sqrt{{D}}$
38 12 14 20 divcan4d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{{D}{{B}}^{2}}{{{B}}^{2}}={D}$
39 34 37 38 3eqtr4rd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{{D}{{B}}^{2}}{{{B}}^{2}}={\sqrt{{D}}}^{2}$
40 29 39 oveq12d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\frac{{{A}}^{2}}{{{B}}^{2}}\right)-\left(\frac{{D}{{B}}^{2}}{{{B}}^{2}}\right)={\left(\frac{{A}}{{B}}\right)}^{2}-{\sqrt{{D}}}^{2}$
41 9 13 17 divcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{{A}}{{B}}\in ℂ$
42 subsq ${⊢}\left(\frac{{A}}{{B}}\in ℂ\wedge \sqrt{{D}}\in ℂ\right)\to {\left(\frac{{A}}{{B}}\right)}^{2}-{\sqrt{{D}}}^{2}=\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)$
43 41 36 42 syl2anc ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {\left(\frac{{A}}{{B}}\right)}^{2}-{\sqrt{{D}}}^{2}=\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)$
44 41 36 addcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\in ℂ$
45 8 nnred ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {A}\in ℝ$
46 45 1 nndivred ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{{A}}{{B}}\in ℝ$
47 46 35 resubcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\in ℝ$
48 47 recnd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\in ℂ$
49 44 48 mulcomd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)=\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)$
50 43 49 eqtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {\left(\frac{{A}}{{B}}\right)}^{2}-{\sqrt{{D}}}^{2}=\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)$
51 27 40 50 3eqtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{{{A}}^{2}-{D}{{B}}^{2}}{{{B}}^{2}}=\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)$
52 51 fveq2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\frac{{{A}}^{2}-{D}{{B}}^{2}}{{{B}}^{2}}\right|=\left|\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)\right|$
53 52 oveq2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\left|\frac{{{A}}^{2}-{D}{{B}}^{2}}{{{B}}^{2}}\right|={{B}}^{2}\left|\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)\right|$
54 23 26 53 3eqtr3d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|{{A}}^{2}-{D}{{B}}^{2}\right|={{B}}^{2}\left|\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)\right|$
55 48 44 absmuld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)\right|=\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
56 55 oveq2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\left|\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)\right|={{B}}^{2}\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
57 48 abscld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\in ℝ$
58 44 abscld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℝ$
59 57 58 remulcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℝ$
60 3 59 remulcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℝ$
61 2nn0 ${⊢}2\in {ℕ}_{0}$
62 61 nn0negzi ${⊢}-2\in ℤ$
63 62 a1i ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to -2\in ℤ$
64 2 17 63 reexpclzd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{-2}\in ℝ$
65 64 58 remulcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℝ$
66 3 65 remulcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℝ$
67 1red ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 1\in ℝ$
68 2re ${⊢}2\in ℝ$
69 68 a1i ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 2\in ℝ$
70 69 35 remulcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 2\sqrt{{D}}\in ℝ$
71 67 70 readdcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 1+2\sqrt{{D}}\in ℝ$
72 simpr ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}$
73 8 nngt0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0<{A}$
74 1 nngt0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0<{B}$
75 45 2 73 74 divgt0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0<\frac{{A}}{{B}}$
76 11 nngt0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0<{D}$
77 sqrtgt0 ${⊢}\left({D}\in ℝ\wedge 0<{D}\right)\to 0<\sqrt{{D}}$
78 30 76 77 syl2anc ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0<\sqrt{{D}}$
79 46 35 75 78 addgt0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0<\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}$
80 79 gt0ne0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\ne 0$
81 absgt0 ${⊢}\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\in ℂ\to \left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\ne 0↔0<\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\right)$
82 81 biimpa ${⊢}\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\in ℂ\wedge \left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\ne 0\right)\to 0<\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
83 44 80 82 syl2anc ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0<\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
84 ltmul1 ${⊢}\left(\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\in ℝ\wedge {{B}}^{-2}\in ℝ\wedge \left(\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℝ\wedge 0<\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\right)\right)\to \left(\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}↔\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|<{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\right)$
85 57 64 58 83 84 syl112anc ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}↔\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|<{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\right)$
86 72 85 mpbid ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|<{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
87 2 17 sqgt0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0<{{B}}^{2}$
88 ltmul2 ${⊢}\left(\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℝ\wedge {{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℝ\wedge \left({{B}}^{2}\in ℝ\wedge 0<{{B}}^{2}\right)\right)\to \left(\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|<{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|↔{{B}}^{2}\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|<{{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\right)$
89 59 65 3 87 88 syl112anc ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|<{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|↔{{B}}^{2}\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|<{{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\right)$
90 86 89 mpbid ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|<{{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
91 13 17 63 expclzd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{-2}\in ℂ$
92 58 recnd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℂ$
93 mulass ${⊢}\left({{B}}^{2}\in ℂ\wedge {{B}}^{-2}\in ℂ\wedge \left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℂ\right)\to {{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|={{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
94 93 eqcomd ${⊢}\left({{B}}^{2}\in ℂ\wedge {{B}}^{-2}\in ℂ\wedge \left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\in ℂ\right)\to {{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|={{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
95 14 91 92 94 syl3anc ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|={{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
96 expneg ${⊢}\left({B}\in ℂ\wedge 2\in {ℕ}_{0}\right)\to {{B}}^{-2}=\frac{1}{{{B}}^{2}}$
97 13 61 96 sylancl ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{-2}=\frac{1}{{{B}}^{2}}$
98 97 oveq2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}{{B}}^{-2}={{B}}^{2}\left(\frac{1}{{{B}}^{2}}\right)$
99 14 20 recidd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\left(\frac{1}{{{B}}^{2}}\right)=1$
100 98 99 eqtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}{{B}}^{-2}=1$
101 100 oveq1d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|=1\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
102 92 mulid2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 1\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|=\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
103 95 101 102 3eqtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|=\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|$
104 41 36 addcomd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\frac{{A}}{{B}}\right)+\sqrt{{D}}=\sqrt{{D}}+\left(\frac{{A}}{{B}}\right)$
105 ppncan ${⊢}\left(\sqrt{{D}}\in ℂ\wedge \sqrt{{D}}\in ℂ\wedge \frac{{A}}{{B}}\in ℂ\right)\to \sqrt{{D}}+\sqrt{{D}}+\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)=\sqrt{{D}}+\left(\frac{{A}}{{B}}\right)$
106 105 eqcomd ${⊢}\left(\sqrt{{D}}\in ℂ\wedge \sqrt{{D}}\in ℂ\wedge \frac{{A}}{{B}}\in ℂ\right)\to \sqrt{{D}}+\left(\frac{{A}}{{B}}\right)=\sqrt{{D}}+\sqrt{{D}}+\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)$
107 36 36 41 106 syl3anc ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \sqrt{{D}}+\left(\frac{{A}}{{B}}\right)=\sqrt{{D}}+\sqrt{{D}}+\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)$
108 36 36 addcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \sqrt{{D}}+\sqrt{{D}}\in ℂ$
109 108 48 addcomd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \sqrt{{D}}+\sqrt{{D}}+\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)=\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)+\sqrt{{D}}+\sqrt{{D}}$
110 2times ${⊢}\sqrt{{D}}\in ℂ\to 2\sqrt{{D}}=\sqrt{{D}}+\sqrt{{D}}$
111 110 eqcomd ${⊢}\sqrt{{D}}\in ℂ\to \sqrt{{D}}+\sqrt{{D}}=2\sqrt{{D}}$
112 36 111 syl ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \sqrt{{D}}+\sqrt{{D}}=2\sqrt{{D}}$
113 112 oveq2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)+\sqrt{{D}}+\sqrt{{D}}=\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}+2\sqrt{{D}}$
114 109 113 eqtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \sqrt{{D}}+\sqrt{{D}}+\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)=\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}+2\sqrt{{D}}$
115 104 107 114 3eqtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\frac{{A}}{{B}}\right)+\sqrt{{D}}=\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}+2\sqrt{{D}}$
116 115 fveq2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|=\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}+2\sqrt{{D}}\right|$
117 47 70 readdcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\frac{{A}}{{B}}\right)-\sqrt{{D}}+2\sqrt{{D}}\in ℝ$
118 117 recnd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(\frac{{A}}{{B}}\right)-\sqrt{{D}}+2\sqrt{{D}}\in ℂ$
119 118 abscld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}+2\sqrt{{D}}\right|\in ℝ$
120 70 recnd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 2\sqrt{{D}}\in ℂ$
121 120 abscld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|2\sqrt{{D}}\right|\in ℝ$
122 57 121 readdcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|+\left|2\sqrt{{D}}\right|\in ℝ$
123 48 120 abstrid ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}+2\sqrt{{D}}\right|\le \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|+\left|2\sqrt{{D}}\right|$
124 0le2 ${⊢}0\le 2$
125 124 a1i ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0\le 2$
126 30 32 sqrtge0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0\le \sqrt{{D}}$
127 69 35 125 126 mulge0d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0\le 2\sqrt{{D}}$
128 70 127 absidd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|2\sqrt{{D}}\right|=2\sqrt{{D}}$
129 128 oveq2d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|+\left|2\sqrt{{D}}\right|=\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|+2\sqrt{{D}}$
130 1 nnsqcld ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\in ℕ$
131 130 nnge1d ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 1\le {{B}}^{2}$
132 0lt1 ${⊢}0<1$
133 132 a1i ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to 0<1$
134 lerec ${⊢}\left(\left(1\in ℝ\wedge 0<1\right)\wedge \left({{B}}^{2}\in ℝ\wedge 0<{{B}}^{2}\right)\right)\to \left(1\le {{B}}^{2}↔\frac{1}{{{B}}^{2}}\le \frac{1}{1}\right)$
135 67 133 3 87 134 syl22anc ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left(1\le {{B}}^{2}↔\frac{1}{{{B}}^{2}}\le \frac{1}{1}\right)$
136 131 135 mpbid ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{1}{{{B}}^{2}}\le \frac{1}{1}$
137 1div1e1 ${⊢}\frac{1}{1}=1$
138 136 137 breqtrdi ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \frac{1}{{{B}}^{2}}\le 1$
139 97 138 eqbrtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{-2}\le 1$
140 57 64 67 72 139 ltletrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<1$
141 57 67 140 ltled ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\le 1$
142 57 67 70 141 leadd1dd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|+2\sqrt{{D}}\le 1+2\sqrt{{D}}$
143 129 142 eqbrtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|+\left|2\sqrt{{D}}\right|\le 1+2\sqrt{{D}}$
144 119 122 71 123 143 letrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}+2\sqrt{{D}}\right|\le 1+2\sqrt{{D}}$
145 116 144 eqbrtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\le 1+2\sqrt{{D}}$
146 103 145 eqbrtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}{{B}}^{-2}\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|\le 1+2\sqrt{{D}}$
147 60 66 71 90 146 ltletrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|\left|\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right|<1+2\sqrt{{D}}$
148 56 147 eqbrtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to {{B}}^{2}\left|\left(\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right)\left(\left(\frac{{A}}{{B}}\right)+\sqrt{{D}}\right)\right|<1+2\sqrt{{D}}$
149 54 148 eqbrtrd ${⊢}\left(\left({D}\in ℕ\wedge {A}\in ℕ\wedge {B}\in ℕ\right)\wedge \left|\left(\frac{{A}}{{B}}\right)-\sqrt{{D}}\right|<{{B}}^{-2}\right)\to \left|{{A}}^{2}-{D}{{B}}^{2}\right|<1+2\sqrt{{D}}$