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 
|- ( ( ( D e. NN /\ A e. NN /\ B e. NN ) /\ ( abs ` ( ( A / B ) - ( sqrt ` D ) ) ) < ( B ^ -u 2 ) ) -> ( abs ` ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) )

Proof

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