# 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 ( ( ( 𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( abs ‘ ( ( 𝐴 / 𝐵 ) − ( √ ‘ 𝐷 ) ) ) < ( 𝐵 ↑ - 2 ) ) → ( abs ‘ ( ( 𝐴 ↑ 2 ) − ( 𝐷 · ( 𝐵 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) )

### Proof

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