Metamath Proof Explorer

Theorem pellexlem5

Description: Lemma for pellex . Invoking fiphp3d , we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014)

Ref Expression
Assertion pellexlem5 
|- ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> E. x e. ZZ ( x =/= 0 /\ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~~ NN ) )

Proof

Step Hyp Ref Expression
1 pellexlem4 
 |-  ( ( 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 ) ) ) ) ) } ~~ NN )
2 fzfi 
 |-  ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) e. Fin
3 diffi 
 |-  ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) e. Fin -> ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) e. Fin )
4 2 3 mp1i 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) e. Fin )
5 elopab 
 |-  ( 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 ) ) ) ) ) } <-> E. y E. z ( a = <. 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 ) ) ) ) ) ) )
6 fveq2 
 |-  ( a = <. y , z >. -> ( 1st ` a ) = ( 1st ` <. y , z >. ) )
7 6 oveq1d 
 |-  ( a = <. y , z >. -> ( ( 1st ` a ) ^ 2 ) = ( ( 1st ` <. y , z >. ) ^ 2 ) )
8 fveq2 
 |-  ( a = <. y , z >. -> ( 2nd ` a ) = ( 2nd ` <. y , z >. ) )
9 8 oveq1d 
 |-  ( a = <. y , z >. -> ( ( 2nd ` a ) ^ 2 ) = ( ( 2nd ` <. y , z >. ) ^ 2 ) )
10 9 oveq2d 
 |-  ( a = <. y , z >. -> ( D x. ( ( 2nd ` a ) ^ 2 ) ) = ( D x. ( ( 2nd ` <. y , z >. ) ^ 2 ) ) )
11 7 10 oveq12d 
 |-  ( a = <. y , z >. -> ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = ( ( ( 1st ` <. y , z >. ) ^ 2 ) - ( D x. ( ( 2nd ` <. y , z >. ) ^ 2 ) ) ) )
12 vex 
 |-  y e. _V
13 vex 
 |-  z e. _V
14 12 13 op1st 
 |-  ( 1st ` <. y , z >. ) = y
15 14 oveq1i 
 |-  ( ( 1st ` <. y , z >. ) ^ 2 ) = ( y ^ 2 )
16 12 13 op2nd 
 |-  ( 2nd ` <. y , z >. ) = z
17 16 oveq1i 
 |-  ( ( 2nd ` <. y , z >. ) ^ 2 ) = ( z ^ 2 )
18 17 oveq2i 
 |-  ( D x. ( ( 2nd ` <. y , z >. ) ^ 2 ) ) = ( D x. ( z ^ 2 ) )
19 15 18 oveq12i 
 |-  ( ( ( 1st ` <. y , z >. ) ^ 2 ) - ( D x. ( ( 2nd ` <. y , z >. ) ^ 2 ) ) ) = ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) )
20 11 19 eqtrdi 
 |-  ( a = <. y , z >. -> ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) )
21 20 ad2antrl 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( a = <. 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 ) ) ) ) ) ) ) -> ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) )
22 simprrl 
 |-  ( ( D e. NN /\ ( a = <. 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 ) ) ) ) ) ) ) -> ( y e. NN /\ z e. NN ) )
23 simpl 
 |-  ( ( D e. NN /\ ( a = <. 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 ) ) ) ) ) ) ) -> D e. NN )
24 simprr 
 |-  ( ( ( 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 ) ) ) ) ) -> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) )
25 24 ad2antll 
 |-  ( ( D e. NN /\ ( a = <. 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 ) ) ) ) ) ) ) -> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) )
26 nnz 
 |-  ( y e. NN -> y e. ZZ )
27 26 ad2antrr 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> y e. ZZ )
28 zsqcl 
 |-  ( y e. ZZ -> ( y ^ 2 ) e. ZZ )
29 27 28 syl 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( y ^ 2 ) e. ZZ )
30 nnz 
 |-  ( D e. NN -> D e. ZZ )
31 30 ad2antrl 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> D e. ZZ )
32 simplr 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> z e. NN )
33 32 nnzd 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> z e. ZZ )
34 zsqcl 
 |-  ( z e. ZZ -> ( z ^ 2 ) e. ZZ )
35 33 34 syl 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( z ^ 2 ) e. ZZ )
36 31 35 zmulcld 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( D x. ( z ^ 2 ) ) e. ZZ )
37 29 36 zsubcld 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ZZ )
38 1re 
 |-  1 e. RR
39 2re 
 |-  2 e. RR
40 nnre 
 |-  ( D e. NN -> D e. RR )
41 40 ad2antrl 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> D e. RR )
42 nnnn0 
 |-  ( D e. NN -> D e. NN0 )
43 42 ad2antrl 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> D e. NN0 )
44 43 nn0ge0d 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> 0 <_ D )
45 41 44 resqrtcld 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( sqrt ` D ) e. RR )
46 remulcl 
 |-  ( ( 2 e. RR /\ ( sqrt ` D ) e. RR ) -> ( 2 x. ( sqrt ` D ) ) e. RR )
47 39 45 46 sylancr 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( 2 x. ( sqrt ` D ) ) e. RR )
48 readdcl 
 |-  ( ( 1 e. RR /\ ( 2 x. ( sqrt ` D ) ) e. RR ) -> ( 1 + ( 2 x. ( sqrt ` D ) ) ) e. RR )
49 38 47 48 sylancr 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( 1 + ( 2 x. ( sqrt ` D ) ) ) e. RR )
50 49 flcld 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. ZZ )
51 50 znegcld 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. ZZ )
52 37 zred 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. RR )
53 50 zred 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. RR )
54 nn0abscl 
 |-  ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ZZ -> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) e. NN0 )
55 37 54 syl 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) e. NN0 )
56 55 nn0zd 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) e. ZZ )
57 56 zred 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) e. RR )
58 peano2re 
 |-  ( ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. RR -> ( ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) + 1 ) e. RR )
59 53 58 syl 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) + 1 ) e. RR )
60 simprr 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) )
61 flltp1 
 |-  ( ( 1 + ( 2 x. ( sqrt ` D ) ) ) e. RR -> ( 1 + ( 2 x. ( sqrt ` D ) ) ) < ( ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) + 1 ) )
62 49 61 syl 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( 1 + ( 2 x. ( sqrt ` D ) ) ) < ( ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) + 1 ) )
63 57 49 59 60 62 lttrd 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) + 1 ) )
64 zleltp1 
 |-  ( ( ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) e. ZZ /\ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. ZZ ) -> ( ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) <_ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) <-> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) + 1 ) ) )
65 56 50 64 syl2anc 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) <_ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) <-> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) + 1 ) ) )
66 63 65 mpbird 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) <_ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) )
67 absle 
 |-  ( ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. RR /\ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. RR ) -> ( ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) <_ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) <-> ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) <_ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) <_ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) ) )
68 67 biimpa 
 |-  ( ( ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. RR /\ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. RR ) /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) <_ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) <_ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) <_ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) )
69 52 53 66 68 syl21anc 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) <_ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) <_ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) )
70 elfz 
 |-  ( ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ZZ /\ -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. ZZ /\ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. ZZ ) -> ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) <-> ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) <_ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) <_ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) ) )
71 70 biimpar 
 |-  ( ( ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ZZ /\ -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. ZZ /\ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) e. ZZ ) /\ ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) <_ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) <_ ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) )
72 37 51 50 69 71 syl31anc 
 |-  ( ( ( y e. NN /\ z e. NN ) /\ ( D e. NN /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) )
73 22 23 25 72 syl12anc 
 |-  ( ( D e. NN /\ ( a = <. 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 ) ) ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) )
74 73 adantlr 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( a = <. 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 ) ) ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) )
75 simprl 
 |-  ( ( ( 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 ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) =/= 0 )
76 75 ad2antll 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( a = <. 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 ) ) ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) =/= 0 )
77 eldifsn 
 |-  ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) <-> ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) =/= 0 ) )
78 74 76 77 sylanbrc 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( a = <. 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 ) ) ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) )
79 21 78 eqeltrd 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( a = <. 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 ) ) ) ) ) ) ) -> ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) )
80 79 ex 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( ( a = <. 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 ) ) ) ) ) ) -> ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) ) )
81 80 exlimdvv 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( E. y E. z ( a = <. 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 ) ) ) ) ) ) -> ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) ) )
82 5 81 biimtrid 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( 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 ) ) ) ) ) } -> ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) ) )
83 82 imp 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ 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 ) ) ) ) ) } ) -> ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) )
84 1 4 83 fiphp3d 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> E. x e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN )
85 eldif 
 |-  ( x e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) <-> ( x e. ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) /\ -. x e. { 0 } ) )
86 elfzelz 
 |-  ( x e. ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> x e. ZZ )
87 simp2 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ x e. ZZ /\ -. x e. { 0 } ) -> x e. ZZ )
88 velsn 
 |-  ( x e. { 0 } <-> x = 0 )
89 88 biimpri 
 |-  ( x = 0 -> x e. { 0 } )
90 89 necon3bi 
 |-  ( -. x e. { 0 } -> x =/= 0 )
91 90 3ad2ant3 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ x e. ZZ /\ -. x e. { 0 } ) -> x =/= 0 )
92 87 91 jca 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ x e. ZZ /\ -. x e. { 0 } ) -> ( x e. ZZ /\ x =/= 0 ) )
93 92 3exp 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( x e. ZZ -> ( -. x e. { 0 } -> ( x e. ZZ /\ x =/= 0 ) ) ) )
94 86 93 syl5 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( x e. ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) -> ( -. x e. { 0 } -> ( x e. ZZ /\ x =/= 0 ) ) ) )
95 94 impd 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( ( x e. ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) /\ -. x e. { 0 } ) -> ( x e. ZZ /\ x =/= 0 ) ) )
96 85 95 biimtrid 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( x e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) -> ( x e. ZZ /\ x =/= 0 ) ) )
97 simp2l 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) /\ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN ) -> x e. ZZ )
98 simp2r 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) /\ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN ) -> x =/= 0 )
99 nnex 
 |-  NN e. _V
100 99 99 xpex 
 |-  ( NN X. NN ) e. _V
101 opabssxp 
 |-  { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } C_ ( NN X. NN )
102 ssdomg 
 |-  ( ( NN X. NN ) e. _V -> ( { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } C_ ( NN X. NN ) -> { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~<_ ( NN X. NN ) ) )
103 100 101 102 mp2 
 |-  { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~<_ ( NN X. NN )
104 xpnnen 
 |-  ( NN X. NN ) ~~ NN
105 domentr 
 |-  ( ( { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~<_ ( NN X. NN ) /\ ( NN X. NN ) ~~ NN ) -> { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~<_ NN )
106 103 104 105 mp2an 
 |-  { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~<_ NN
107 ensym 
 |-  ( { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN -> NN ~~ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } )
108 107 3ad2ant3 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) /\ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN ) -> NN ~~ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } )
109 100 101 ssexi 
 |-  { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } e. _V
110 fveq2 
 |-  ( a = b -> ( 1st ` a ) = ( 1st ` b ) )
111 110 oveq1d 
 |-  ( a = b -> ( ( 1st ` a ) ^ 2 ) = ( ( 1st ` b ) ^ 2 ) )
112 fveq2 
 |-  ( a = b -> ( 2nd ` a ) = ( 2nd ` b ) )
113 112 oveq1d 
 |-  ( a = b -> ( ( 2nd ` a ) ^ 2 ) = ( ( 2nd ` b ) ^ 2 ) )
114 113 oveq2d 
 |-  ( a = b -> ( D x. ( ( 2nd ` a ) ^ 2 ) ) = ( D x. ( ( 2nd ` b ) ^ 2 ) ) )
115 111 114 oveq12d 
 |-  ( a = b -> ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) )
116 115 eqeq1d 
 |-  ( a = b -> ( ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x <-> ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) )
117 116 elrab 
 |-  ( b e. { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } <-> ( b 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 ) ) ) ) ) } /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) )
118 simprl 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) /\ ( b = <. 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 ) ) ) ) ) ) ) -> b = <. y , z >. )
119 simprrl 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) /\ ( b = <. 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 ) ) ) ) ) ) ) -> ( y e. NN /\ z e. NN ) )
120 fveq2 
 |-  ( b = <. y , z >. -> ( 1st ` b ) = ( 1st ` <. y , z >. ) )
121 120 oveq1d 
 |-  ( b = <. y , z >. -> ( ( 1st ` b ) ^ 2 ) = ( ( 1st ` <. y , z >. ) ^ 2 ) )
122 fveq2 
 |-  ( b = <. y , z >. -> ( 2nd ` b ) = ( 2nd ` <. y , z >. ) )
123 122 oveq1d 
 |-  ( b = <. y , z >. -> ( ( 2nd ` b ) ^ 2 ) = ( ( 2nd ` <. y , z >. ) ^ 2 ) )
124 123 oveq2d 
 |-  ( b = <. y , z >. -> ( D x. ( ( 2nd ` b ) ^ 2 ) ) = ( D x. ( ( 2nd ` <. y , z >. ) ^ 2 ) ) )
125 121 124 oveq12d 
 |-  ( b = <. y , z >. -> ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = ( ( ( 1st ` <. y , z >. ) ^ 2 ) - ( D x. ( ( 2nd ` <. y , z >. ) ^ 2 ) ) ) )
126 125 19 eqtr2di 
 |-  ( b = <. y , z >. -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) )
127 126 ad2antrl 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) /\ ( b = <. 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 ) ) ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) )
128 simplr 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) /\ ( b = <. 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 ) ) ) ) ) ) ) -> ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x )
129 127 128 eqtrd 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) /\ ( b = <. 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 ) ) ) ) ) ) ) -> ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x )
130 118 119 129 jca32 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) /\ ( b = <. 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 ) ) ) ) ) ) ) -> ( b = <. y , z >. /\ ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) ) )
131 130 ex 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) -> ( ( b = <. 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 ) ) ) ) ) ) -> ( b = <. y , z >. /\ ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) ) ) )
132 131 2eximdv 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) -> ( E. y E. z ( b = <. 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. y E. z ( b = <. y , z >. /\ ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) ) ) )
133 elopab 
 |-  ( b 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 ) ) ) ) ) } <-> E. y E. z ( b = <. 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 ) ) ) ) ) ) )
134 elopab 
 |-  ( b e. { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } <-> E. y E. z ( b = <. y , z >. /\ ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) ) )
135 132 133 134 3imtr4g 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) -> ( b 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 ) ) ) ) ) } -> b e. { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ) )
136 135 expimpd 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( ( ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x /\ b 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 ) ) ) ) ) } ) -> b e. { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ) )
137 136 ancomsd 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( ( b 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 ) ) ) ) ) } /\ ( ( ( 1st ` b ) ^ 2 ) - ( D x. ( ( 2nd ` b ) ^ 2 ) ) ) = x ) -> b e. { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ) )
138 117 137 biimtrid 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( b e. { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } -> b e. { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ) )
139 138 ssrdv 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) ) -> { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } C_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } )
140 139 3adant3 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) /\ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN ) -> { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } C_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } )
141 ssdomg 
 |-  ( { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } e. _V -> ( { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } C_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } -> { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~<_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ) )
142 109 140 141 mpsyl 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) /\ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN ) -> { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~<_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } )
143 endomtr 
 |-  ( ( NN ~~ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } /\ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~<_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ) -> NN ~<_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } )
144 108 142 143 syl2anc 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) /\ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN ) -> NN ~<_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } )
145 sbth 
 |-  ( ( { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~<_ NN /\ NN ~<_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ) -> { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~~ NN )
146 106 144 145 sylancr 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) /\ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN ) -> { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~~ NN )
147 97 98 146 jca32 
 |-  ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ ( x e. ZZ /\ x =/= 0 ) /\ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN ) -> ( x e. ZZ /\ ( x =/= 0 /\ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~~ NN ) ) )
148 147 3exp 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( ( x e. ZZ /\ x =/= 0 ) -> ( { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN -> ( x e. ZZ /\ ( x =/= 0 /\ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~~ NN ) ) ) ) )
149 96 148 syld 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( x e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) -> ( { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN -> ( x e. ZZ /\ ( x =/= 0 /\ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~~ NN ) ) ) ) )
150 149 impd 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( ( x e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) /\ { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN ) -> ( x e. ZZ /\ ( x =/= 0 /\ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~~ NN ) ) ) )
151 150 reximdv2 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( E. x e. ( ( -u ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ... ( |_ ` ( 1 + ( 2 x. ( sqrt ` D ) ) ) ) ) \ { 0 } ) { 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 ) ) ) ) ) } | ( ( ( 1st ` a ) ^ 2 ) - ( D x. ( ( 2nd ` a ) ^ 2 ) ) ) = x } ~~ NN -> E. x e. ZZ ( x =/= 0 /\ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~~ NN ) ) )
152 84 151 mpd 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> E. x e. ZZ ( x =/= 0 /\ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~~ NN ) )