Metamath Proof Explorer

Theorem pellex

Description: Every Pell equation has a nontrivial solution. Theorem 62 in vandenDries p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014)

Ref Expression
Assertion pellex 
|- ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 )

Proof

Step Hyp Ref Expression
1 fzfi 
 |-  ( 0 ... ( ( abs ` a ) - 1 ) ) e. Fin
2 xpfi 
 |-  ( ( ( 0 ... ( ( abs ` a ) - 1 ) ) e. Fin /\ ( 0 ... ( ( abs ` a ) - 1 ) ) e. Fin ) -> ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) e. Fin )
3 1 1 2 mp2an 
 |-  ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) e. Fin
4 isfinite 
 |-  ( ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) e. Fin <-> ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ~< _om )
5 3 4 mpbi 
 |-  ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ~< _om
6 nnenom 
 |-  NN ~~ _om
7 6 ensymi 
 |-  _om ~~ NN
8 sdomentr 
 |-  ( ( ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ~< _om /\ _om ~~ NN ) -> ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ~< NN )
9 5 7 8 mp2an 
 |-  ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ~< NN
10 ensym 
 |-  ( { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ~~ NN -> NN ~~ { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } )
11 10 ad2antll 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ ( a =/= 0 /\ { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ~~ NN ) ) -> NN ~~ { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } )
12 sdomentr 
 |-  ( ( ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ~< NN /\ NN ~~ { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ) -> ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ~< { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } )
13 9 11 12 sylancr 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ ( a =/= 0 /\ { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ~~ NN ) ) -> ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ~< { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } )
14 opabssxp 
 |-  { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } C_ ( NN X. NN )
15 14 sseli 
 |-  ( d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } -> d e. ( NN X. NN ) )
16 simprrl 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) ) -> ( 1st ` d ) e. NN )
17 16 nnzd 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) ) -> ( 1st ` d ) e. ZZ )
18 simpllr 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) ) -> a e. ZZ )
19 simplr 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) ) -> a =/= 0 )
20 nnabscl 
 |-  ( ( a e. ZZ /\ a =/= 0 ) -> ( abs ` a ) e. NN )
21 18 19 20 syl2anc 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) ) -> ( abs ` a ) e. NN )
22 zmodfz 
 |-  ( ( ( 1st ` d ) e. ZZ /\ ( abs ` a ) e. NN ) -> ( ( 1st ` d ) mod ( abs ` a ) ) e. ( 0 ... ( ( abs ` a ) - 1 ) ) )
23 17 21 22 syl2anc 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) ) -> ( ( 1st ` d ) mod ( abs ` a ) ) e. ( 0 ... ( ( abs ` a ) - 1 ) ) )
24 simprrr 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) ) -> ( 2nd ` d ) e. NN )
25 24 nnzd 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) ) -> ( 2nd ` d ) e. ZZ )
26 zmodfz 
 |-  ( ( ( 2nd ` d ) e. ZZ /\ ( abs ` a ) e. NN ) -> ( ( 2nd ` d ) mod ( abs ` a ) ) e. ( 0 ... ( ( abs ` a ) - 1 ) ) )
27 25 21 26 syl2anc 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) ) -> ( ( 2nd ` d ) mod ( abs ` a ) ) e. ( 0 ... ( ( abs ` a ) - 1 ) ) )
28 23 27 jca 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) ) -> ( ( ( 1st ` d ) mod ( abs ` a ) ) e. ( 0 ... ( ( abs ` a ) - 1 ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) e. ( 0 ... ( ( abs ` a ) - 1 ) ) ) )
29 28 ex 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) -> ( ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) -> ( ( ( 1st ` d ) mod ( abs ` a ) ) e. ( 0 ... ( ( abs ` a ) - 1 ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) e. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ) )
30 elxp7 
 |-  ( d e. ( NN X. NN ) <-> ( d e. ( _V X. _V ) /\ ( ( 1st ` d ) e. NN /\ ( 2nd ` d ) e. NN ) ) )
31 opelxp 
 |-  ( <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. e. ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) <-> ( ( ( 1st ` d ) mod ( abs ` a ) ) e. ( 0 ... ( ( abs ` a ) - 1 ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) e. ( 0 ... ( ( abs ` a ) - 1 ) ) ) )
32 29 30 31 3imtr4g 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) -> ( d e. ( NN X. NN ) -> <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. e. ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ) )
33 15 32 syl5 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) -> ( d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } -> <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. e. ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) ) )
34 33 imp 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ) -> <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. e. ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) )
35 34 adantlrr 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ ( a =/= 0 /\ { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ~~ NN ) ) /\ d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ) -> <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. e. ( ( 0 ... ( ( abs ` a ) - 1 ) ) X. ( 0 ... ( ( abs ` a ) - 1 ) ) ) )
36 fveq2 
 |-  ( d = e -> ( 1st ` d ) = ( 1st ` e ) )
37 36 oveq1d 
 |-  ( d = e -> ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) )
38 fveq2 
 |-  ( d = e -> ( 2nd ` d ) = ( 2nd ` e ) )
39 38 oveq1d 
 |-  ( d = e -> ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) )
40 37 39 opeq12d 
 |-  ( d = e -> <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. )
41 13 35 40 fphpd 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ ( a =/= 0 /\ { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ~~ NN ) ) -> E. d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } E. e e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) )
42 eleq1w 
 |-  ( b = f -> ( b e. NN <-> f e. NN ) )
43 eleq1w 
 |-  ( c = g -> ( c e. NN <-> g e. NN ) )
44 42 43 bi2anan9 
 |-  ( ( b = f /\ c = g ) -> ( ( b e. NN /\ c e. NN ) <-> ( f e. NN /\ g e. NN ) ) )
45 oveq1 
 |-  ( b = f -> ( b ^ 2 ) = ( f ^ 2 ) )
46 oveq1 
 |-  ( c = g -> ( c ^ 2 ) = ( g ^ 2 ) )
47 46 oveq2d 
 |-  ( c = g -> ( D x. ( c ^ 2 ) ) = ( D x. ( g ^ 2 ) ) )
48 45 47 oveqan12d 
 |-  ( ( b = f /\ c = g ) -> ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) )
49 48 eqeq1d 
 |-  ( ( b = f /\ c = g ) -> ( ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a <-> ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) )
50 44 49 anbi12d 
 |-  ( ( b = f /\ c = g ) -> ( ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) <-> ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) )
51 50 cbvopabv 
 |-  { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } = { <. f , g >. | ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) }
52 51 eleq2i 
 |-  ( e e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } <-> e e. { <. f , g >. | ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) } )
53 52 biimpi 
 |-  ( e e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } -> e e. { <. f , g >. | ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) } )
54 elopab 
 |-  ( d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } <-> E. b E. c ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) )
55 elopab 
 |-  ( e e. { <. f , g >. | ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) } <-> E. f E. g ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) )
56 simp3ll 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) -> b e. NN )
57 56 3expb 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) -> b e. NN )
58 57 3ad2ant1 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> b e. NN )
59 simp3lr 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) -> c e. NN )
60 59 3expb 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) -> c e. NN )
61 60 3ad2ant1 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> c e. NN )
62 simp1lr 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> a e. ZZ )
63 62 3adant1r 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> a e. ZZ )
64 simp-4l 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) -> D e. NN )
65 64 3ad2ant1 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> D e. NN )
66 simp-4r 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) -> -. ( sqrt ` D ) e. QQ )
67 66 3ad2ant1 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> -. ( sqrt ` D ) e. QQ )
68 simp2ll 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> f e. NN )
69 68 3adant2l 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> f e. NN )
70 simp2lr 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> g e. NN )
71 70 3adant2l 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> g e. NN )
72 simp2l 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> e = <. f , g >. )
73 simp1rl 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> d = <. b , c >. )
74 simp3l 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> d =/= e )
75 simp3 
 |-  ( ( e = <. f , g >. /\ d = <. b , c >. /\ d =/= e ) -> d =/= e )
76 simp2 
 |-  ( ( e = <. f , g >. /\ d = <. b , c >. /\ d =/= e ) -> d = <. b , c >. )
77 simp1 
 |-  ( ( e = <. f , g >. /\ d = <. b , c >. /\ d =/= e ) -> e = <. f , g >. )
78 75 76 77 3netr3d 
 |-  ( ( e = <. f , g >. /\ d = <. b , c >. /\ d =/= e ) -> <. b , c >. =/= <. f , g >. )
79 vex 
 |-  b e. _V
80 vex 
 |-  c e. _V
81 79 80 opth 
 |-  ( <. b , c >. = <. f , g >. <-> ( b = f /\ c = g ) )
82 81 necon3abii 
 |-  ( <. b , c >. =/= <. f , g >. <-> -. ( b = f /\ c = g ) )
83 78 82 sylib 
 |-  ( ( e = <. f , g >. /\ d = <. b , c >. /\ d =/= e ) -> -. ( b = f /\ c = g ) )
84 72 73 74 83 syl3anc 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> -. ( b = f /\ c = g ) )
85 simp1lr 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> a =/= 0 )
86 simp1rr 
 |-  ( ( ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a )
87 86 3adant1l 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a )
88 simp2rr 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a )
89 simp3r 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. )
90 simp3 
 |-  ( ( d = <. b , c >. /\ e = <. f , g >. /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. )
91 ovex 
 |-  ( ( 1st ` d ) mod ( abs ` a ) ) e. _V
92 ovex 
 |-  ( ( 2nd ` d ) mod ( abs ` a ) ) e. _V
93 91 92 opth 
 |-  ( <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. <-> ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) )
94 90 93 sylib 
 |-  ( ( d = <. b , c >. /\ e = <. f , g >. /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) )
95 simprl 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) )
96 simpll 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> d = <. b , c >. )
97 96 fveq2d 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( 1st ` d ) = ( 1st ` <. b , c >. ) )
98 79 80 op1st 
 |-  ( 1st ` <. b , c >. ) = b
99 97 98 eqtrdi 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( 1st ` d ) = b )
100 99 oveq1d 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( ( 1st ` d ) mod ( abs ` a ) ) = ( b mod ( abs ` a ) ) )
101 simplr 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> e = <. f , g >. )
102 101 fveq2d 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( 1st ` e ) = ( 1st ` <. f , g >. ) )
103 vex 
 |-  f e. _V
104 vex 
 |-  g e. _V
105 103 104 op1st 
 |-  ( 1st ` <. f , g >. ) = f
106 102 105 eqtrdi 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( 1st ` e ) = f )
107 106 oveq1d 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( ( 1st ` e ) mod ( abs ` a ) ) = ( f mod ( abs ` a ) ) )
108 95 100 107 3eqtr3d 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( b mod ( abs ` a ) ) = ( f mod ( abs ` a ) ) )
109 simprr 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) )
110 96 fveq2d 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( 2nd ` d ) = ( 2nd ` <. b , c >. ) )
111 79 80 op2nd 
 |-  ( 2nd ` <. b , c >. ) = c
112 110 111 eqtrdi 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( 2nd ` d ) = c )
113 112 oveq1d 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( ( 2nd ` d ) mod ( abs ` a ) ) = ( c mod ( abs ` a ) ) )
114 101 fveq2d 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( 2nd ` e ) = ( 2nd ` <. f , g >. ) )
115 103 104 op2nd 
 |-  ( 2nd ` <. f , g >. ) = g
116 114 115 eqtrdi 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( 2nd ` e ) = g )
117 116 oveq1d 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( ( 2nd ` e ) mod ( abs ` a ) ) = ( g mod ( abs ` a ) ) )
118 109 113 117 3eqtr3d 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( c mod ( abs ` a ) ) = ( g mod ( abs ` a ) ) )
119 108 118 jca 
 |-  ( ( ( d = <. b , c >. /\ e = <. f , g >. ) /\ ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) ) -> ( ( b mod ( abs ` a ) ) = ( f mod ( abs ` a ) ) /\ ( c mod ( abs ` a ) ) = ( g mod ( abs ` a ) ) ) )
120 119 ex 
 |-  ( ( d = <. b , c >. /\ e = <. f , g >. ) -> ( ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) -> ( ( b mod ( abs ` a ) ) = ( f mod ( abs ` a ) ) /\ ( c mod ( abs ` a ) ) = ( g mod ( abs ` a ) ) ) ) )
121 120 3adant3 
 |-  ( ( d = <. b , c >. /\ e = <. f , g >. /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> ( ( ( ( 1st ` d ) mod ( abs ` a ) ) = ( ( 1st ` e ) mod ( abs ` a ) ) /\ ( ( 2nd ` d ) mod ( abs ` a ) ) = ( ( 2nd ` e ) mod ( abs ` a ) ) ) -> ( ( b mod ( abs ` a ) ) = ( f mod ( abs ` a ) ) /\ ( c mod ( abs ` a ) ) = ( g mod ( abs ` a ) ) ) ) )
122 94 121 mpd 
 |-  ( ( d = <. b , c >. /\ e = <. f , g >. /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> ( ( b mod ( abs ` a ) ) = ( f mod ( abs ` a ) ) /\ ( c mod ( abs ` a ) ) = ( g mod ( abs ` a ) ) ) )
123 73 72 89 122 syl3anc 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> ( ( b mod ( abs ` a ) ) = ( f mod ( abs ` a ) ) /\ ( c mod ( abs ` a ) ) = ( g mod ( abs ` a ) ) ) )
124 123 simpld 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> ( b mod ( abs ` a ) ) = ( f mod ( abs ` a ) ) )
125 123 simprd 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> ( c mod ( abs ` a ) ) = ( g mod ( abs ` a ) ) )
126 58 61 63 65 67 69 71 84 85 87 88 124 125 pellexlem6 
 |-  ( ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) /\ ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) /\ ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 )
127 126 3exp 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) -> ( ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) -> ( ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 ) ) )
128 127 exlimdvv 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) -> ( E. f E. g ( e = <. f , g >. /\ ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) ) -> ( ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 ) ) )
129 55 128 biimtrid 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) ) -> ( e e. { <. f , g >. | ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) } -> ( ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 ) ) )
130 129 ex 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) -> ( ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) -> ( e e. { <. f , g >. | ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) } -> ( ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 ) ) ) )
131 130 exlimdvv 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) -> ( E. b E. c ( d = <. b , c >. /\ ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) ) -> ( e e. { <. f , g >. | ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) } -> ( ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 ) ) ) )
132 54 131 biimtrid 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) -> ( d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } -> ( e e. { <. f , g >. | ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) } -> ( ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 ) ) ) )
133 132 impd 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) -> ( ( d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } /\ e e. { <. f , g >. | ( ( f e. NN /\ g e. NN ) /\ ( ( f ^ 2 ) - ( D x. ( g ^ 2 ) ) ) = a ) } ) -> ( ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 ) ) )
134 53 133 sylan2i 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) -> ( ( d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } /\ e e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ) -> ( ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 ) ) )
135 134 rexlimdvv 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) -> ( E. d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } E. e e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 ) )
136 135 imp 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ a =/= 0 ) /\ E. d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } E. e e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 )
137 136 adantlrr 
 |-  ( ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ ( a =/= 0 /\ { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ~~ NN ) ) /\ E. d e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } E. e e. { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ( d =/= e /\ <. ( ( 1st ` d ) mod ( abs ` a ) ) , ( ( 2nd ` d ) mod ( abs ` a ) ) >. = <. ( ( 1st ` e ) mod ( abs ` a ) ) , ( ( 2nd ` e ) mod ( abs ` a ) ) >. ) ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 )
138 41 137 mpdan 
 |-  ( ( ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) /\ a e. ZZ ) /\ ( a =/= 0 /\ { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ~~ NN ) ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 )
139 pellexlem5 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> E. a e. ZZ ( a =/= 0 /\ { <. b , c >. | ( ( b e. NN /\ c e. NN ) /\ ( ( b ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = a ) } ~~ NN ) )
140 138 139 r19.29a 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 )