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