Metamath Proof Explorer

Theorem pellexlem4

Description: Lemma for pellex . Invoking irrapx1 , we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014)

Ref Expression
Assertion 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 )

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 ssdomg 
 |-  ( ( NN X. NN ) e. _V -> ( { <. 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 ) -> { <. 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 X. NN ) ) )
5 2 3 4 mp2 
 |-  { <. 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 X. NN )
6 xpnnen 
 |-  ( NN X. NN ) ~~ NN
7 domentr 
 |-  ( ( { <. 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 X. NN ) /\ ( NN X. NN ) ~~ NN ) -> { <. 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 )
8 5 6 7 mp2an 
 |-  { <. 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
9 nnrp 
 |-  ( D e. NN -> D e. RR+ )
10 9 rpsqrtcld 
 |-  ( D e. NN -> ( sqrt ` D ) e. RR+ )
11 10 anim1i 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( ( sqrt ` D ) e. RR+ /\ -. ( sqrt ` D ) e. QQ ) )
12 eldif 
 |-  ( ( sqrt ` D ) e. ( RR+ \ QQ ) <-> ( ( sqrt ` D ) e. RR+ /\ -. ( sqrt ` D ) e. QQ ) )
13 11 12 sylibr 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> ( sqrt ` D ) e. ( RR+ \ QQ ) )
14 irrapx1 
 |-  ( ( sqrt ` D ) e. ( RR+ \ QQ ) -> { b e. QQ | ( 0 < b /\ ( abs ` ( b - ( sqrt ` D ) ) ) < ( ( denom ` b ) ^ -u 2 ) ) } ~~ NN )
15 ensym 
 |-  ( { b e. QQ | ( 0 < b /\ ( abs ` ( b - ( sqrt ` D ) ) ) < ( ( denom ` b ) ^ -u 2 ) ) } ~~ NN -> NN ~~ { b e. QQ | ( 0 < b /\ ( abs ` ( b - ( sqrt ` D ) ) ) < ( ( denom ` b ) ^ -u 2 ) ) } )
16 13 14 15 3syl 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> NN ~~ { b e. QQ | ( 0 < b /\ ( abs ` ( b - ( sqrt ` D ) ) ) < ( ( denom ` b ) ^ -u 2 ) ) } )
17 pellexlem3 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> { b e. QQ | ( 0 < b /\ ( abs ` ( b - ( sqrt ` D ) ) ) < ( ( denom ` b ) ^ -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 ) ) ) ) ) } )
18 endomtr 
 |-  ( ( NN ~~ { b e. QQ | ( 0 < b /\ ( abs ` ( b - ( sqrt ` D ) ) ) < ( ( denom ` b ) ^ -u 2 ) ) } /\ { b e. QQ | ( 0 < b /\ ( abs ` ( b - ( sqrt ` D ) ) ) < ( ( denom ` b ) ^ -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 ) ) ) ) ) } ) -> NN ~<_ { <. 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 ) ) ) ) ) } )
19 16 17 18 syl2anc 
 |-  ( ( D e. NN /\ -. ( sqrt ` D ) e. QQ ) -> NN ~<_ { <. 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 ) ) ) ) ) } )
20 sbth 
 |-  ( ( { <. 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 /\ NN ~<_ { <. 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 , 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 )
21 8 19 20 sylancr 
 |-  ( ( 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 )