Metamath Proof Explorer

Theorem rmspecnonsq

Description: The discriminant used to define the X and Y sequences is a nonsquare positive integer and thus a valid Pell equation discriminant. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmspecnonsq 
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )

Proof

Step Hyp Ref Expression
1 eluzelz 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
2 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
3 1 2 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A ^ 2 ) e. ZZ )
4 1zzd 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 e. ZZ )
5 3 4 zsubcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ZZ )
6 sq1 
 |-  ( 1 ^ 2 ) = 1
7 eluz2b2 
 |-  ( A e. ( ZZ>= ` 2 ) <-> ( A e. NN /\ 1 < A ) )
8 7 simprbi 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < A )
9 1red 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 e. RR )
10 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
11 0le1 
 |-  0 <_ 1
12 11 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 <_ 1 )
13 eluzge2nn0 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN0 )
14 13 nn0ge0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 <_ A )
15 9 10 12 14 lt2sqd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 < A <-> ( 1 ^ 2 ) < ( A ^ 2 ) ) )
16 8 15 mpbid 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 ^ 2 ) < ( A ^ 2 ) )
17 6 16 eqbrtrrid 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < ( A ^ 2 ) )
18 10 resqcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A ^ 2 ) e. RR )
19 9 18 posdifd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 < ( A ^ 2 ) <-> 0 < ( ( A ^ 2 ) - 1 ) ) )
20 17 19 mpbid 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 < ( ( A ^ 2 ) - 1 ) )
21 elnnz 
 |-  ( ( ( A ^ 2 ) - 1 ) e. NN <-> ( ( ( A ^ 2 ) - 1 ) e. ZZ /\ 0 < ( ( A ^ 2 ) - 1 ) ) )
22 5 20 21 sylanbrc 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. NN )
23 rmspecsqrtnq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
24 23 eldifbd 
 |-  ( A e. ( ZZ>= ` 2 ) -> -. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. QQ )
25 24 intnand 
 |-  ( A e. ( ZZ>= ` 2 ) -> -. ( ( ( A ^ 2 ) - 1 ) e. NN /\ ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. QQ ) )
26 df-squarenn 
 |-  []NN = { a e. NN | ( sqrt ` a ) e. QQ }
27 26 eleq2i 
 |-  ( ( ( A ^ 2 ) - 1 ) e. []NN <-> ( ( A ^ 2 ) - 1 ) e. { a e. NN | ( sqrt ` a ) e. QQ } )
28 fveq2 
 |-  ( a = ( ( A ^ 2 ) - 1 ) -> ( sqrt ` a ) = ( sqrt ` ( ( A ^ 2 ) - 1 ) ) )
29 28 eleq1d 
 |-  ( a = ( ( A ^ 2 ) - 1 ) -> ( ( sqrt ` a ) e. QQ <-> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. QQ ) )
30 29 elrab 
 |-  ( ( ( A ^ 2 ) - 1 ) e. { a e. NN | ( sqrt ` a ) e. QQ } <-> ( ( ( A ^ 2 ) - 1 ) e. NN /\ ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. QQ ) )
31 27 30 bitr2i 
 |-  ( ( ( ( A ^ 2 ) - 1 ) e. NN /\ ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. QQ ) <-> ( ( A ^ 2 ) - 1 ) e. []NN )
32 25 31 sylnib 
 |-  ( A e. ( ZZ>= ` 2 ) -> -. ( ( A ^ 2 ) - 1 ) e. []NN )
33 22 32 eldifd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )