Step | Hyp | Ref
| Expression |
1 | | elpell1234qr 37415 |
. . 3
◻NN Pell1234QR
|
2 | | simp-4r 807 |
. . . . . . . . 9
◻NN
|
3 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
4 | 3 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
5 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
6 | 5 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
7 | 6 | eqeq1d 2624 |
. . . . . . . . . . . . 13
|
8 | 4, 7 | anbi12d 747 |
. . . . . . . . . . . 12
|
9 | 8 | rexbidv 3052 |
. . . . . . . . . . 11
|
10 | 9 | rspcev 3309 |
. . . . . . . . . 10
|
11 | 10 | adantll 750 |
. . . . . . . . 9
◻NN
|
12 | | elpell14qr 37413 |
. . . . . . . . . 10
◻NN Pell14QR
|
13 | 12 | ad4antr 768 |
. . . . . . . . 9
◻NN
Pell14QR
|
14 | 2, 11, 13 | mpbir2and 957 |
. . . . . . . 8
◻NN
Pell14QR |
15 | 14 | orcd 407 |
. . . . . . 7
◻NN
Pell14QR Pell14QR |
16 | 15 | exp31 630 |
. . . . . 6
◻NN
Pell14QR Pell14QR |
17 | | simp-5r 809 |
. . . . . . . . . . . 12
◻NN
|
18 | 17 | renegcld 10457 |
. . . . . . . . . . 11
◻NN |
19 | | simpllr 799 |
. . . . . . . . . . . 12
◻NN |
20 | | znegcl 11412 |
. . . . . . . . . . . . 13
|
21 | 20 | ad2antlr 763 |
. . . . . . . . . . . 12
◻NN |
22 | | simprl 794 |
. . . . . . . . . . . . . 14
◻NN
|
23 | 22 | negeqd 10275 |
. . . . . . . . . . . . 13
◻NN |
24 | | zcn 11382 |
. . . . . . . . . . . . . . 15
|
25 | 24 | ad4antlr 769 |
. . . . . . . . . . . . . 14
◻NN |
26 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . 18
◻NN
|
27 | 26 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
◻NN
|
28 | 27 | ad5antr 770 |
. . . . . . . . . . . . . . . 16
◻NN
|
29 | 28 | sqrtcld 14176 |
. . . . . . . . . . . . . . 15
◻NN |
30 | | zcn 11382 |
. . . . . . . . . . . . . . . 16
|
31 | 30 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
◻NN |
32 | 29, 31 | mulcld 10060 |
. . . . . . . . . . . . . 14
◻NN |
33 | 25, 32 | negdid 10405 |
. . . . . . . . . . . . 13
◻NN
|
34 | | mulneg2 10467 |
. . . . . . . . . . . . . . . 16
|
35 | 34 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
|
36 | 29, 31, 35 | syl2anc 693 |
. . . . . . . . . . . . . 14
◻NN |
37 | 36 | oveq2d 6666 |
. . . . . . . . . . . . 13
◻NN
|
38 | 23, 33, 37 | 3eqtrd 2660 |
. . . . . . . . . . . 12
◻NN
|
39 | | sqneg 12923 |
. . . . . . . . . . . . . . 15
|
40 | 25, 39 | syl 17 |
. . . . . . . . . . . . . 14
◻NN |
41 | | sqneg 12923 |
. . . . . . . . . . . . . . . 16
|
42 | 31, 41 | syl 17 |
. . . . . . . . . . . . . . 15
◻NN |
43 | 42 | oveq2d 6666 |
. . . . . . . . . . . . . 14
◻NN |
44 | 40, 43 | oveq12d 6668 |
. . . . . . . . . . . . 13
◻NN
|
45 | | simprr 796 |
. . . . . . . . . . . . 13
◻NN
|
46 | 44, 45 | eqtrd 2656 |
. . . . . . . . . . . 12
◻NN
|
47 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
48 | 47 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
49 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
50 | 49 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
51 | 50 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
52 | 48, 51 | anbi12d 747 |
. . . . . . . . . . . . 13
|
53 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
55 | 54 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
56 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
58 | 57 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
59 | 58 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
60 | 55, 59 | anbi12d 747 |
. . . . . . . . . . . . 13
|
61 | 52, 60 | rspc2ev 3324 |
. . . . . . . . . . . 12
|
62 | 19, 21, 38, 46, 61 | syl112anc 1330 |
. . . . . . . . . . 11
◻NN
|
63 | | elpell14qr 37413 |
. . . . . . . . . . . 12
◻NN Pell14QR
|
64 | 63 | ad5antr 770 |
. . . . . . . . . . 11
◻NN Pell14QR
|
65 | 18, 62, 64 | mpbir2and 957 |
. . . . . . . . . 10
◻NN Pell14QR |
66 | 65 | olcd 408 |
. . . . . . . . 9
◻NN Pell14QR Pell14QR |
67 | 66 | ex 450 |
. . . . . . . 8
◻NN
Pell14QR Pell14QR |
68 | 67 | rexlimdva 3031 |
. . . . . . 7
◻NN
Pell14QR Pell14QR |
69 | 68 | ex 450 |
. . . . . 6
◻NN
Pell14QR Pell14QR |
70 | | elznn0 11392 |
. . . . . . . 8
|
71 | 70 | simprbi 480 |
. . . . . . 7
|
72 | 71 | adantl 482 |
. . . . . 6
◻NN |
73 | 16, 69, 72 | mpjaod 396 |
. . . . 5
◻NN
Pell14QR Pell14QR |
74 | 73 | rexlimdva 3031 |
. . . 4
◻NN
Pell14QR Pell14QR |
75 | 74 | expimpd 629 |
. . 3
◻NN Pell14QR Pell14QR |
76 | 1, 75 | sylbid 230 |
. 2
◻NN Pell1234QR
Pell14QR Pell14QR |
77 | 76 | imp 445 |
1
◻NN Pell1234QR Pell14QR Pell14QR |