Step | Hyp | Ref
| Expression |
1 | | elpell14qr 37413 |
. . 3
◻NN Pell14QR
|
2 | 1 | biimpa 501 |
. 2
◻NN Pell14QR
|
3 | | simplrr 801 |
. . . . . . . 8
◻NN
Pell14QR
|
4 | | elznn0 11392 |
. . . . . . . 8
|
5 | 3, 4 | sylib 208 |
. . . . . . 7
◻NN
Pell14QR
|
6 | 5 | simprd 479 |
. . . . . 6
◻NN
Pell14QR
|
7 | | simplr 792 |
. . . . . . . . . . 11
◻NN Pell14QR
|
8 | 7 | ad2antrr 762 |
. . . . . . . . . 10
◻NN Pell14QR
|
9 | | simprl 794 |
. . . . . . . . . . . 12
◻NN Pell14QR
|
10 | 9 | ad2antrr 762 |
. . . . . . . . . . 11
◻NN Pell14QR
|
11 | | simpr 477 |
. . . . . . . . . . 11
◻NN Pell14QR
|
12 | | simplr 792 |
. . . . . . . . . . 11
◻NN Pell14QR
|
13 | | rsp2e 3004 |
. . . . . . . . . . 11
|
14 | 10, 11, 12, 13 | syl3anc 1326 |
. . . . . . . . . 10
◻NN Pell14QR
|
15 | 8, 14 | jca 554 |
. . . . . . . . 9
◻NN Pell14QR
|
16 | 15 | ex 450 |
. . . . . . . 8
◻NN
Pell14QR
|
17 | | elpell1qr 37411 |
. . . . . . . . 9
◻NN Pell1QR
|
18 | 17 | ad4antr 768 |
. . . . . . . 8
◻NN
Pell14QR
Pell1QR
|
19 | 16, 18 | sylibrd 249 |
. . . . . . 7
◻NN
Pell14QR
Pell1QR |
20 | 7 | ad2antrr 762 |
. . . . . . . . . . 11
◻NN Pell14QR
|
21 | | pell14qrne0 37422 |
. . . . . . . . . . . 12
◻NN Pell14QR |
22 | 21 | ad4antr 768 |
. . . . . . . . . . 11
◻NN Pell14QR
|
23 | 20, 22 | rereccld 10852 |
. . . . . . . . . 10
◻NN Pell14QR
|
24 | 9 | ad2antrr 762 |
. . . . . . . . . . 11
◻NN Pell14QR
|
25 | | simpr 477 |
. . . . . . . . . . . 12
◻NN Pell14QR
|
26 | | pell14qrre 37421 |
. . . . . . . . . . . . . . . . . 18
◻NN Pell14QR
|
27 | 26 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
◻NN Pell14QR
|
28 | 27, 21 | reccld 10794 |
. . . . . . . . . . . . . . . 16
◻NN Pell14QR |
29 | 28 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
◻NN
Pell14QR
|
30 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . 18
|
31 | 30 | ad2antrl 764 |
. . . . . . . . . . . . . . . . 17
◻NN Pell14QR
|
32 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . 21
◻NN
|
33 | 32 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
◻NN
|
34 | 33 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
◻NN Pell14QR
|
35 | 34 | sqrtcld 14176 |
. . . . . . . . . . . . . . . . . 18
◻NN Pell14QR
|
36 | | zcn 11382 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 36 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . 19
◻NN Pell14QR
|
38 | 37 | negcld 10379 |
. . . . . . . . . . . . . . . . . 18
◻NN Pell14QR
|
39 | 35, 38 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
◻NN Pell14QR
|
40 | 31, 39 | addcld 10059 |
. . . . . . . . . . . . . . . 16
◻NN Pell14QR
|
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . 15
◻NN
Pell14QR
|
42 | 27 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
◻NN
Pell14QR
|
43 | 21 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
◻NN
Pell14QR
|
44 | 27, 21 | recidd 10796 |
. . . . . . . . . . . . . . . . . 18
◻NN Pell14QR |
45 | 44 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
◻NN
Pell14QR
|
46 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
◻NN
Pell14QR
|
47 | 45, 46 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
◻NN
Pell14QR
|
48 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
◻NN
Pell14QR
|
49 | 35, 37 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . 20
◻NN Pell14QR
|
50 | 49 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
◻NN
Pell14QR
|
51 | | subsq 12972 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 48, 50, 51 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
◻NN
Pell14QR
|
53 | 35, 37 | sqmuld 13020 |
. . . . . . . . . . . . . . . . . . . . 21
◻NN Pell14QR
|
54 | 34 | sqsqrtd 14178 |
. . . . . . . . . . . . . . . . . . . . . 22
◻NN Pell14QR
|
55 | 54 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
◻NN Pell14QR
|
56 | 53, 55 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . 20
◻NN Pell14QR
|
57 | 56 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
◻NN Pell14QR
|
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
◻NN
Pell14QR
|
59 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
◻NN
Pell14QR
|
60 | 35, 37 | mulneg2d 10484 |
. . . . . . . . . . . . . . . . . . . . . 22
◻NN Pell14QR
|
61 | 60 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
◻NN Pell14QR
|
62 | | negsub 10329 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
63 | 62 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
|
64 | 31, 49, 63 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
◻NN Pell14QR
|
65 | 61, 64 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . 20
◻NN Pell14QR
|
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
◻NN
Pell14QR
|
67 | 59, 66 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
◻NN
Pell14QR
|
68 | 52, 58, 67 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . 17
◻NN
Pell14QR
|
69 | 68 | adantrr 753 |
. . . . . . . . . . . . . . . 16
◻NN
Pell14QR
|
70 | 47, 69 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
◻NN
Pell14QR
|
71 | 29, 41, 42, 43, 70 | mulcanad 10662 |
. . . . . . . . . . . . . 14
◻NN
Pell14QR
|
72 | 71 | adantr 481 |
. . . . . . . . . . . . 13
◻NN Pell14QR
|
73 | 37 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
◻NN Pell14QR
|
74 | | sqneg 12923 |
. . . . . . . . . . . . . . . . 17
|
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . 16
◻NN Pell14QR
|
76 | 75 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
◻NN Pell14QR
|
77 | 76 | oveq2d 6666 |
. . . . . . . . . . . . . 14
◻NN Pell14QR
|
78 | | simplrr 801 |
. . . . . . . . . . . . . 14
◻NN Pell14QR
|
79 | 77, 78 | eqtrd 2656 |
. . . . . . . . . . . . 13
◻NN Pell14QR
|
80 | 72, 79 | jca 554 |
. . . . . . . . . . . 12
◻NN Pell14QR
|
81 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
83 | 82 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
84 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
85 | 84 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
86 | 85 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
87 | 86 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
88 | 83, 87 | anbi12d 747 |
. . . . . . . . . . . . 13
|
89 | 88 | rspcev 3309 |
. . . . . . . . . . . 12
|
90 | 25, 80, 89 | syl2anc 693 |
. . . . . . . . . . 11
◻NN Pell14QR
|
91 | | rspe 3003 |
. . . . . . . . . . 11
|
92 | 24, 90, 91 | syl2anc 693 |
. . . . . . . . . 10
◻NN Pell14QR
|
93 | 23, 92 | jca 554 |
. . . . . . . . 9
◻NN Pell14QR
|
94 | 93 | ex 450 |
. . . . . . . 8
◻NN
Pell14QR
|
95 | | elpell1qr 37411 |
. . . . . . . . 9
◻NN Pell1QR
|
96 | 95 | ad4antr 768 |
. . . . . . . 8
◻NN
Pell14QR
Pell1QR
|
97 | 94, 96 | sylibrd 249 |
. . . . . . 7
◻NN
Pell14QR
Pell1QR |
98 | 19, 97 | orim12d 883 |
. . . . . 6
◻NN
Pell14QR
Pell1QR Pell1QR |
99 | 6, 98 | mpd 15 |
. . . . 5
◻NN
Pell14QR
Pell1QR Pell1QR |
100 | 99 | ex 450 |
. . . 4
◻NN Pell14QR
Pell1QR Pell1QR |
101 | 100 | rexlimdvva 3038 |
. . 3
◻NN Pell14QR
Pell1QR Pell1QR |
102 | 101 | expimpd 629 |
. 2
◻NN Pell14QR Pell1QR Pell1QR |
103 | 2, 102 | mpd 15 |
1
◻NN Pell14QR Pell1QR Pell1QR |