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 2 PellFund A 2 1 = A + A 2 1

Proof

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