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 A2PellFundA21=A+A21

Proof

Step Hyp Ref Expression
1 rmspecnonsq A2A21
2 eluzelz A2A
3 zsqcl AA2
4 2 3 syl A2A2
5 4 zred A2A2
6 1red A21
7 5 6 resubcld A2A21
8 sq1 12=1
9 8 a1i A212=1
10 eluz2b2 A2A1<A
11 10 simprbi A21<A
12 eluzelre A2A
13 0le1 01
14 13 a1i A201
15 eluzge2nn0 A2A0
16 15 nn0ge0d A20A
17 6 12 14 16 lt2sqd A21<A12<A2
18 11 17 mpbid A212<A2
19 9 18 eqbrtrrd A21<A2
20 6 5 posdifd A21<A20<A21
21 19 20 mpbid A20<A21
22 7 21 elrpd A2A21+
23 22 rpsqrtcld A2A21+
24 23 rpred A2A21
25 24 recnd A2A21
26 25 mulid1d A2A211=A21
27 26 oveq2d A2A+A211=A+A21
28 pell1qrss14 A21Pell1QRA21Pell14QRA21
29 1 28 syl A2Pell1QRA21Pell14QRA21
30 1nn0 10
31 30 a1i A210
32 8 oveq2i A2112=A211
33 7 recnd A2A21
34 33 mulid1d A2A211=A21
35 32 34 eqtrid A2A2112=A21
36 35 oveq2d A2A2A2112=A2A21
37 5 recnd A2A2
38 1cnd A21
39 37 38 nncand A2A2A21=1
40 36 39 eqtrd A2A2A2112=1
41 pellqrexplicit A21A010A2A2112=1A+A211Pell1QRA21
42 1 15 31 40 41 syl31anc A2A+A211Pell1QRA21
43 29 42 sseldd A2A+A211Pell14QRA21
44 27 43 eqeltrrd A2A+A21Pell14QRA21
45 6 24 readdcld A21+A21
46 12 24 readdcld A2A+A21
47 6 23 ltaddrpd A21<1+A21
48 6 12 24 11 ltadd1dd A21+A21<A+A21
49 6 45 46 47 48 lttrd A21<A+A21
50 pellfundlb A21A+A21Pell14QRA211<A+A21PellFundA21A+A21
51 1 44 49 50 syl3anc A2PellFundA21A+A21
52 37 38 npcand A2A2-1+1=A2
53 52 fveq2d A2A2-1+1=A2
54 12 16 sqrtsqd A2A2=A
55 53 54 eqtrd A2A2-1+1=A
56 55 oveq1d A2A2-1+1+A21=A+A21
57 pellfundge A21A2-1+1+A21PellFundA21
58 1 57 syl A2A2-1+1+A21PellFundA21
59 56 58 eqbrtrrd A2A+A21PellFundA21
60 pellfundre A21PellFundA21
61 1 60 syl A2PellFundA21
62 61 46 letri3d A2PellFundA21=A+A21PellFundA21A+A21A+A21PellFundA21
63 51 59 62 mpbir2and A2PellFundA21=A+A21