Metamath Proof Explorer

Theorem rmspecfund

Description: The base of exponent used to define the X and Y sequences is the fundamental solution of the corresponding Pell equation. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmspecfund 
|- ( A e. ( ZZ>= ` 2 ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 rmspecnonsq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
2 eluzelz 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
3 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
4 2 3 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A ^ 2 ) e. ZZ )
5 4 zred 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A ^ 2 ) e. RR )
6 1red 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 e. RR )
7 5 6 resubcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR )
8 sq1 
 |-  ( 1 ^ 2 ) = 1
9 8 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 ^ 2 ) = 1 )
10 eluz2b2 
 |-  ( A e. ( ZZ>= ` 2 ) <-> ( A e. NN /\ 1 < A ) )
11 10 simprbi 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < A )
12 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
13 0le1 
 |-  0 <_ 1
14 13 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 <_ 1 )
15 eluzge2nn0 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN0 )
16 15 nn0ge0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 <_ A )
17 6 12 14 16 lt2sqd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 < A <-> ( 1 ^ 2 ) < ( A ^ 2 ) ) )
18 11 17 mpbid 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 ^ 2 ) < ( A ^ 2 ) )
19 9 18 eqbrtrrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < ( A ^ 2 ) )
20 6 5 posdifd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 < ( A ^ 2 ) <-> 0 < ( ( A ^ 2 ) - 1 ) ) )
21 19 20 mpbid 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 < ( ( A ^ 2 ) - 1 ) )
22 7 21 elrpd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR+ )
23 22 rpsqrtcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. RR+ )
24 23 rpred 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. RR )
25 24 recnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC )
26 25 mulid1d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) = ( sqrt ` ( ( A ^ 2 ) - 1 ) ) )
27 26 oveq2d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
28 pell1qrss14 
 |-  ( ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) -> ( Pell1QR ` ( ( A ^ 2 ) - 1 ) ) C_ ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) )
29 1 28 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( Pell1QR ` ( ( A ^ 2 ) - 1 ) ) C_ ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) )
30 1nn0 
 |-  1 e. NN0
31 30 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 e. NN0 )
32 8 oveq2i 
 |-  ( ( ( A ^ 2 ) - 1 ) x. ( 1 ^ 2 ) ) = ( ( ( A ^ 2 ) - 1 ) x. 1 )
33 7 recnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. CC )
34 33 mulid1d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( ( A ^ 2 ) - 1 ) x. 1 ) = ( ( A ^ 2 ) - 1 ) )
35 32 34 syl5eq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( ( A ^ 2 ) - 1 ) x. ( 1 ^ 2 ) ) = ( ( A ^ 2 ) - 1 ) )
36 35 oveq2d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( 1 ^ 2 ) ) ) = ( ( A ^ 2 ) - ( ( A ^ 2 ) - 1 ) ) )
37 5 recnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A ^ 2 ) e. CC )
38 1cnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 e. CC )
39 37 38 nncand 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - ( ( A ^ 2 ) - 1 ) ) = 1 )
40 36 39 eqtrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( 1 ^ 2 ) ) ) = 1 )
41 pellqrexplicit 
 |-  ( ( ( ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) /\ A e. NN0 /\ 1 e. NN0 ) /\ ( ( A ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( 1 ^ 2 ) ) ) = 1 ) -> ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) e. ( Pell1QR ` ( ( A ^ 2 ) - 1 ) ) )
42 1 15 31 40 41 syl31anc 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) e. ( Pell1QR ` ( ( A ^ 2 ) - 1 ) ) )
43 29 42 sseldd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) )
44 27 43 eqeltrrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) )
45 6 24 readdcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. RR )
46 12 24 readdcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. RR )
47 6 23 ltaddrpd 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < ( 1 + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
48 6 12 24 11 ltadd1dd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) < ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
49 6 45 46 47 48 lttrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
50 pellfundlb 
 |-  ( ( ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) /\ ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) /\ 1 < ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) <_ ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
51 1 44 49 50 syl3anc 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) <_ ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
52 37 38 npcand 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( ( A ^ 2 ) - 1 ) + 1 ) = ( A ^ 2 ) )
53 52 fveq2d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( ( A ^ 2 ) - 1 ) + 1 ) ) = ( sqrt ` ( A ^ 2 ) ) )
54 12 16 sqrtsqd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( A ^ 2 ) ) = A )
55 53 54 eqtrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( ( A ^ 2 ) - 1 ) + 1 ) ) = A )
56 55 oveq1d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( sqrt ` ( ( ( A ^ 2 ) - 1 ) + 1 ) ) + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
57 pellfundge 
 |-  ( ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) -> ( ( sqrt ` ( ( ( A ^ 2 ) - 1 ) + 1 ) ) + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) <_ ( PellFund ` ( ( A ^ 2 ) - 1 ) ) )
58 1 57 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( sqrt ` ( ( ( A ^ 2 ) - 1 ) + 1 ) ) + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) <_ ( PellFund ` ( ( A ^ 2 ) - 1 ) ) )
59 56 58 eqbrtrrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) <_ ( PellFund ` ( ( A ^ 2 ) - 1 ) ) )
60 pellfundre 
 |-  ( ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) e. RR )
61 1 60 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) e. RR )
62 61 46 letri3d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) <-> ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) <_ ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) /\ ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) <_ ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ) ) )
63 51 59 62 mpbir2and 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )