Metamath Proof Explorer

Theorem pellexlem3

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

Ref Expression
Assertion pellexlem3 
|- ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> { x e. QQ | ( 0 < x /\ ( abs ` ( x - ( sqrt ` D ) ) ) < ( ( denom ` x ) ^ -u 2 ) ) } ~<_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) =/= 0 /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) } )

Proof

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