Step | Hyp | Ref
| Expression |
1 | | remulcl 10021 |
. . . . . . . . . . 11
|
2 | 1 | ad5antlr 771 |
. . . . . . . . . 10
◻NN |
3 | | simprl 794 |
. . . . . . . . . . . . . 14
◻NN
|
4 | 3 | ad3antrrr 766 |
. . . . . . . . . . . . 13
◻NN |
5 | | simplrl 800 |
. . . . . . . . . . . . 13
◻NN |
6 | 4, 5 | zmulcld 11488 |
. . . . . . . . . . . 12
◻NN |
7 | | eldifi 3732 |
. . . . . . . . . . . . . . . 16
◻NN
|
8 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
◻NN
|
9 | 8 | nnzd 11481 |
. . . . . . . . . . . . . 14
◻NN
|
10 | 9 | ad3antrrr 766 |
. . . . . . . . . . . . 13
◻NN
|
11 | | simplrr 801 |
. . . . . . . . . . . . . 14
◻NN |
12 | | simprr 796 |
. . . . . . . . . . . . . . 15
◻NN
|
13 | 12 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
◻NN |
14 | 11, 13 | zmulcld 11488 |
. . . . . . . . . . . . 13
◻NN |
15 | 10, 14 | zmulcld 11488 |
. . . . . . . . . . . 12
◻NN |
16 | 6, 15 | zaddcld 11486 |
. . . . . . . . . . 11
◻NN |
17 | 4, 11 | zmulcld 11488 |
. . . . . . . . . . . 12
◻NN |
18 | 5, 13 | zmulcld 11488 |
. . . . . . . . . . . 12
◻NN |
19 | 17, 18 | zaddcld 11486 |
. . . . . . . . . . 11
◻NN |
20 | | simprl 794 |
. . . . . . . . . . . . . 14
◻NN
|
21 | 20 | ad2antrr 762 |
. . . . . . . . . . . . 13
◻NN
|
22 | | simprl 794 |
. . . . . . . . . . . . 13
◻NN
|
23 | 21, 22 | oveq12d 6668 |
. . . . . . . . . . . 12
◻NN |
24 | | zcn 11382 |
. . . . . . . . . . . . . . 15
|
25 | 24 | ad2antrl 764 |
. . . . . . . . . . . . . 14
◻NN
|
26 | 25 | ad3antrrr 766 |
. . . . . . . . . . . . 13
◻NN |
27 | 8 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
◻NN
|
28 | 27 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
◻NN
|
29 | 28 | sqrtcld 14176 |
. . . . . . . . . . . . . 14
◻NN |
30 | | zcn 11382 |
. . . . . . . . . . . . . . . 16
|
31 | 30 | ad2antll 765 |
. . . . . . . . . . . . . . 15
◻NN
|
32 | 31 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
◻NN |
33 | 29, 32 | mulcld 10060 |
. . . . . . . . . . . . 13
◻NN |
34 | | zcn 11382 |
. . . . . . . . . . . . . . 15
|
35 | 34 | adantr 481 |
. . . . . . . . . . . . . 14
|
36 | 35 | ad2antlr 763 |
. . . . . . . . . . . . 13
◻NN |
37 | | zcn 11382 |
. . . . . . . . . . . . . . . 16
|
38 | 37 | adantl 482 |
. . . . . . . . . . . . . . 15
|
39 | 38 | ad2antlr 763 |
. . . . . . . . . . . . . 14
◻NN |
40 | 29, 39 | mulcld 10060 |
. . . . . . . . . . . . 13
◻NN |
41 | 26, 33, 36, 40 | muladdd 10489 |
. . . . . . . . . . . 12
◻NN |
42 | 29, 39, 29, 32 | mul4d 10248 |
. . . . . . . . . . . . . . 15
◻NN |
43 | 28 | msqsqrtd 14179 |
. . . . . . . . . . . . . . . 16
◻NN |
44 | 43 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
◻NN |
45 | 42, 44 | eqtrd 2656 |
. . . . . . . . . . . . . 14
◻NN |
46 | 45 | oveq2d 6666 |
. . . . . . . . . . . . 13
◻NN |
47 | 26, 29, 39 | mul12d 10245 |
. . . . . . . . . . . . . . 15
◻NN |
48 | 36, 29, 32 | mul12d 10245 |
. . . . . . . . . . . . . . 15
◻NN |
49 | 47, 48 | oveq12d 6668 |
. . . . . . . . . . . . . 14
◻NN |
50 | 26, 39 | mulcld 10060 |
. . . . . . . . . . . . . . 15
◻NN |
51 | 36, 32 | mulcld 10060 |
. . . . . . . . . . . . . . 15
◻NN |
52 | 29, 50, 51 | adddid 10064 |
. . . . . . . . . . . . . 14
◻NN |
53 | 49, 52 | eqtr4d 2659 |
. . . . . . . . . . . . 13
◻NN |
54 | 46, 53 | oveq12d 6668 |
. . . . . . . . . . . 12
◻NN |
55 | 23, 41, 54 | 3eqtrd 2660 |
. . . . . . . . . . 11
◻NN |
56 | 50, 51 | addcld 10059 |
. . . . . . . . . . . . . . . 16
◻NN |
57 | 29, 56 | sqmuld 13020 |
. . . . . . . . . . . . . . 15
◻NN |
58 | 28 | sqsqrtd 14178 |
. . . . . . . . . . . . . . . 16
◻NN |
59 | 58 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
◻NN |
60 | 57, 59 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
◻NN |
61 | 60 | oveq2d 6666 |
. . . . . . . . . . . . 13
◻NN
|
62 | 26, 36 | mulcld 10060 |
. . . . . . . . . . . . . . 15
◻NN |
63 | 39, 32 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
◻NN |
64 | 28, 63 | mulcld 10060 |
. . . . . . . . . . . . . . 15
◻NN |
65 | 62, 64 | addcld 10059 |
. . . . . . . . . . . . . 14
◻NN |
66 | 29, 56 | mulcld 10060 |
. . . . . . . . . . . . . 14
◻NN |
67 | | subsq 12972 |
. . . . . . . . . . . . . 14
|
68 | 65, 66, 67 | syl2anc 693 |
. . . . . . . . . . . . 13
◻NN |
69 | 41, 54 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
◻NN |
70 | 26, 33, 36, 40 | mulsubd 10490 |
. . . . . . . . . . . . . . 15
◻NN |
71 | 46, 53 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
◻NN |
72 | 70, 71 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
◻NN |
73 | 69, 72 | oveq12d 6668 |
. . . . . . . . . . . . 13
◻NN |
74 | 61, 68, 73 | 3eqtrd 2660 |
. . . . . . . . . . . 12
◻NN
|
75 | 26, 33 | addcld 10059 |
. . . . . . . . . . . . . 14
◻NN |
76 | 36, 40 | addcld 10059 |
. . . . . . . . . . . . . 14
◻NN |
77 | 26, 33 | subcld 10392 |
. . . . . . . . . . . . . 14
◻NN |
78 | 36, 40 | subcld 10392 |
. . . . . . . . . . . . . 14
◻NN |
79 | 75, 76, 77, 78 | mul4d 10248 |
. . . . . . . . . . . . 13
◻NN |
80 | | subsq 12972 |
. . . . . . . . . . . . . . 15
|
81 | 26, 33, 80 | syl2anc 693 |
. . . . . . . . . . . . . 14
◻NN |
82 | | subsq 12972 |
. . . . . . . . . . . . . . 15
|
83 | 36, 40, 82 | syl2anc 693 |
. . . . . . . . . . . . . 14
◻NN |
84 | 81, 83 | oveq12d 6668 |
. . . . . . . . . . . . 13
◻NN |
85 | 29, 32 | sqmuld 13020 |
. . . . . . . . . . . . . . 15
◻NN |
86 | 85 | oveq2d 6666 |
. . . . . . . . . . . . . 14
◻NN |
87 | 29, 39 | sqmuld 13020 |
. . . . . . . . . . . . . . 15
◻NN |
88 | 87 | oveq2d 6666 |
. . . . . . . . . . . . . 14
◻NN |
89 | 86, 88 | oveq12d 6668 |
. . . . . . . . . . . . 13
◻NN |
90 | 79, 84, 89 | 3eqtr2d 2662 |
. . . . . . . . . . . 12
◻NN |
91 | 58 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
◻NN |
92 | 91 | oveq2d 6666 |
. . . . . . . . . . . . . 14
◻NN
|
93 | 58 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
◻NN |
94 | 93 | oveq2d 6666 |
. . . . . . . . . . . . . 14
◻NN
|
95 | 92, 94 | oveq12d 6668 |
. . . . . . . . . . . . 13
◻NN
|
96 | | simprr 796 |
. . . . . . . . . . . . . . 15
◻NN
|
97 | 96 | ad2antrr 762 |
. . . . . . . . . . . . . 14
◻NN
|
98 | | simprr 796 |
. . . . . . . . . . . . . 14
◻NN
|
99 | 97, 98 | oveq12d 6668 |
. . . . . . . . . . . . 13
◻NN
|
100 | | 1t1e1 11175 |
. . . . . . . . . . . . . 14
|
101 | 100 | a1i 11 |
. . . . . . . . . . . . 13
◻NN |
102 | 95, 99, 101 | 3eqtrd 2660 |
. . . . . . . . . . . 12
◻NN |
103 | 74, 90, 102 | 3eqtrd 2660 |
. . . . . . . . . . 11
◻NN
|
104 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
105 | 104 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
106 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
107 | 106 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
108 | 107 | eqeq1d 2624 |
. . . . . . . . . . . . 13
|
109 | 105, 108 | anbi12d 747 |
. . . . . . . . . . . 12
|
110 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
111 | 110 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
112 | 111 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
113 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
114 | 113 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
115 | 114 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
116 | 115 | eqeq1d 2624 |
. . . . . . . . . . . . 13
|
117 | 112, 116 | anbi12d 747 |
. . . . . . . . . . . 12
|
118 | 109, 117 | rspc2ev 3324 |
. . . . . . . . . . 11
|
119 | 16, 19, 55, 103, 118 | syl112anc 1330 |
. . . . . . . . . 10
◻NN
|
120 | 2, 119 | jca 554 |
. . . . . . . . 9
◻NN |
121 | 120 | ex 450 |
. . . . . . . 8
◻NN
|
122 | 121 | rexlimdvva 3038 |
. . . . . . 7
◻NN
|
123 | 122 | ex 450 |
. . . . . 6
◻NN
|
124 | 123 | rexlimdvva 3038 |
. . . . 5
◻NN
|
125 | 124 | impd 447 |
. . . 4
◻NN
|
126 | 125 | expimpd 629 |
. . 3
◻NN
|
127 | | elpell1234qr 37415 |
. . . . 5
◻NN Pell1234QR
|
128 | | elpell1234qr 37415 |
. . . . 5
◻NN Pell1234QR
|
129 | 127, 128 | anbi12d 747 |
. . . 4
◻NN Pell1234QR
Pell1234QR
|
130 | | an4 865 |
. . . 4
|
131 | 129, 130 | syl6bb 276 |
. . 3
◻NN Pell1234QR
Pell1234QR
|
132 | | elpell1234qr 37415 |
. . 3
◻NN Pell1234QR
|
133 | 126, 131,
132 | 3imtr4d 283 |
. 2
◻NN Pell1234QR
Pell1234QR
Pell1234QR |
134 | 133 | 3impib 1262 |
1
◻NN Pell1234QR Pell1234QR Pell1234QR |