| 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 · ( √ ‘ 𝐷 ) ) ) ) |