Step | Hyp | Ref
| Expression |
1 | | pcadd.2 |
. . 3
|
2 | | elq 11790 |
. . 3
|
3 | 1, 2 | sylib 208 |
. 2
|
4 | | pcadd.3 |
. . 3
|
5 | | elq 11790 |
. . 3
|
6 | 4, 5 | sylib 208 |
. 2
|
7 | | pcadd.1 |
. . . . . . . 8
|
8 | | pcxcl 15565 |
. . . . . . . 8
|
9 | 7, 1, 8 | syl2anc 693 |
. . . . . . 7
|
10 | | xrleid 11983 |
. . . . . . 7
|
11 | 9, 10 | syl 17 |
. . . . . 6
|
12 | 11 | adantr 481 |
. . . . 5
|
13 | | oveq2 6658 |
. . . . . . 7
|
14 | | qcn 11802 |
. . . . . . . . 9
|
15 | 1, 14 | syl 17 |
. . . . . . . 8
|
16 | 15 | addid1d 10236 |
. . . . . . 7
|
17 | 13, 16 | sylan9eqr 2678 |
. . . . . 6
|
18 | 17 | oveq2d 6666 |
. . . . 5
|
19 | 12, 18 | breqtrrd 4681 |
. . . 4
|
20 | 19 | a1d 25 |
. . 3
|
21 | | reeanv 3107 |
. . . 4
|
22 | | reeanv 3107 |
. . . . . 6
|
23 | 7 | ad3antrrr 766 |
. . . . . . . . 9
|
24 | | prmnn 15388 |
. . . . . . . . . . . . . . . . 17
|
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
|
26 | | simplrl 800 |
. . . . . . . . . . . . . . . . 17
|
27 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . 19
|
28 | 4 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
29 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
30 | | pcqcl 15561 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
31 | 23, 28, 29, 30 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
32 | 31 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
33 | | ltpnf 11954 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
34 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
35 | | pnfxr 10092 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
36 | | xrltnle 10105 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
37 | 34, 35, 36 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
38 | 33, 37 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
|
39 | 32, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
40 | | pc0 15559 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
41 | 23, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
42 | 41 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
|
43 | 39, 42 | mtbird 315 |
. . . . . . . . . . . . . . . . . . . 20
|
44 | | pcadd.4 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
45 | 44 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
|
46 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
47 | 46 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . 22
|
48 | 45, 47 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . . . . 21
|
49 | 48 | necon3bd 2808 |
. . . . . . . . . . . . . . . . . . . 20
|
50 | 43, 49 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 27, 50 | eqnetrrd 2862 |
. . . . . . . . . . . . . . . . . 18
|
52 | | simprll 802 |
. . . . . . . . . . . . . . . . . . . . . 22
|
53 | 52 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . 21
|
54 | 52 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . . 21
|
55 | 53, 54 | div0d 10800 |
. . . . . . . . . . . . . . . . . . . 20
|
56 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | 56 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 55, 57 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 58 | necon3d 2815 |
. . . . . . . . . . . . . . . . . 18
|
60 | 51, 59 | mpd 15 |
. . . . . . . . . . . . . . . . 17
|
61 | | pczcl 15553 |
. . . . . . . . . . . . . . . . 17
|
62 | 23, 26, 60, 61 | syl12anc 1324 |
. . . . . . . . . . . . . . . 16
|
63 | 25, 62 | nnexpcld 13030 |
. . . . . . . . . . . . . . 15
|
64 | 63 | nncnd 11036 |
. . . . . . . . . . . . . 14
|
65 | 64, 53 | mulcomd 10061 |
. . . . . . . . . . . . 13
|
66 | 65 | oveq2d 6666 |
. . . . . . . . . . . 12
|
67 | 26 | zcnd 11483 |
. . . . . . . . . . . . 13
|
68 | 23, 52 | pccld 15555 |
. . . . . . . . . . . . . . 15
|
69 | 25, 68 | nnexpcld 13030 |
. . . . . . . . . . . . . 14
|
70 | 69 | nncnd 11036 |
. . . . . . . . . . . . 13
|
71 | 63 | nnne0d 11065 |
. . . . . . . . . . . . 13
|
72 | 69 | nnne0d 11065 |
. . . . . . . . . . . . 13
|
73 | 67, 64, 53, 70, 71, 72, 54 | divdivdivd 10848 |
. . . . . . . . . . . 12
|
74 | 27 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
75 | | pcdiv 15557 |
. . . . . . . . . . . . . . . . . 18
|
76 | 23, 26, 60, 52, 75 | syl121anc 1331 |
. . . . . . . . . . . . . . . . 17
|
77 | 74, 76 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
78 | 77 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
79 | 25 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
|
80 | 25 | nnne0d 11065 |
. . . . . . . . . . . . . . . 16
|
81 | 68 | nn0zd 11480 |
. . . . . . . . . . . . . . . 16
|
82 | 62 | nn0zd 11480 |
. . . . . . . . . . . . . . . 16
|
83 | 79, 80, 81, 82 | expsubd 13019 |
. . . . . . . . . . . . . . 15
|
84 | 78, 83 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
85 | 84 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
86 | 27 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
87 | 67, 53, 64, 70, 54, 72, 71 | divdivdivd 10848 |
. . . . . . . . . . . . 13
|
88 | 85, 86, 87 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
89 | 66, 73, 88 | 3eqtr4d 2666 |
. . . . . . . . . . 11
|
90 | 89 | oveq2d 6666 |
. . . . . . . . . 10
|
91 | 1 | ad3antrrr 766 |
. . . . . . . . . . . 12
|
92 | 91, 14 | syl 17 |
. . . . . . . . . . 11
|
93 | | pcqcl 15561 |
. . . . . . . . . . . . 13
|
94 | 23, 91, 50, 93 | syl12anc 1324 |
. . . . . . . . . . . 12
|
95 | 79, 80, 94 | expclzd 13013 |
. . . . . . . . . . 11
|
96 | 79, 80, 94 | expne0d 13014 |
. . . . . . . . . . 11
|
97 | 92, 95, 96 | divcan2d 10803 |
. . . . . . . . . 10
|
98 | 90, 97 | eqtr2d 2657 |
. . . . . . . . 9
|
99 | | simplrr 801 |
. . . . . . . . . . . . . . . . 17
|
100 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . 19
|
101 | 100, 29 | eqnetrrd 2862 |
. . . . . . . . . . . . . . . . . 18
|
102 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . . . 22
|
103 | 102 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . 21
|
104 | 102 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . . 21
|
105 | 103, 104 | div0d 10800 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
|
107 | 106 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | 105, 107 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . 19
|
109 | 108 | necon3d 2815 |
. . . . . . . . . . . . . . . . . 18
|
110 | 101, 109 | mpd 15 |
. . . . . . . . . . . . . . . . 17
|
111 | | pczcl 15553 |
. . . . . . . . . . . . . . . . 17
|
112 | 23, 99, 110, 111 | syl12anc 1324 |
. . . . . . . . . . . . . . . 16
|
113 | 25, 112 | nnexpcld 13030 |
. . . . . . . . . . . . . . 15
|
114 | 113 | nncnd 11036 |
. . . . . . . . . . . . . 14
|
115 | 114, 103 | mulcomd 10061 |
. . . . . . . . . . . . 13
|
116 | 115 | oveq2d 6666 |
. . . . . . . . . . . 12
|
117 | 99 | zcnd 11483 |
. . . . . . . . . . . . 13
|
118 | 23, 102 | pccld 15555 |
. . . . . . . . . . . . . . 15
|
119 | 25, 118 | nnexpcld 13030 |
. . . . . . . . . . . . . 14
|
120 | 119 | nncnd 11036 |
. . . . . . . . . . . . 13
|
121 | 113 | nnne0d 11065 |
. . . . . . . . . . . . 13
|
122 | 119 | nnne0d 11065 |
. . . . . . . . . . . . 13
|
123 | 117, 114,
103, 120, 121, 122, 104 | divdivdivd 10848 |
. . . . . . . . . . . 12
|
124 | 100 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
125 | | pcdiv 15557 |
. . . . . . . . . . . . . . . . . 18
|
126 | 23, 99, 110, 102, 125 | syl121anc 1331 |
. . . . . . . . . . . . . . . . 17
|
127 | 124, 126 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
128 | 127 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
129 | 118 | nn0zd 11480 |
. . . . . . . . . . . . . . . 16
|
130 | 112 | nn0zd 11480 |
. . . . . . . . . . . . . . . 16
|
131 | 79, 80, 129, 130 | expsubd 13019 |
. . . . . . . . . . . . . . 15
|
132 | 128, 131 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
133 | 132 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
134 | 100 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
135 | 117, 103,
114, 120, 104, 122, 121 | divdivdivd 10848 |
. . . . . . . . . . . . 13
|
136 | 133, 134,
135 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
137 | 116, 123,
136 | 3eqtr4d 2666 |
. . . . . . . . . . 11
|
138 | 137 | oveq2d 6666 |
. . . . . . . . . 10
|
139 | | qcn 11802 |
. . . . . . . . . . . 12
|
140 | 28, 139 | syl 17 |
. . . . . . . . . . 11
|
141 | 79, 80, 31 | expclzd 13013 |
. . . . . . . . . . 11
|
142 | 79, 80, 31 | expne0d 13014 |
. . . . . . . . . . 11
|
143 | 140, 141,
142 | divcan2d 10803 |
. . . . . . . . . 10
|
144 | 138, 143 | eqtr2d 2657 |
. . . . . . . . 9
|
145 | | eluz 11701 |
. . . . . . . . . . 11
|
146 | 94, 31, 145 | syl2anc 693 |
. . . . . . . . . 10
|
147 | 45, 146 | mpbird 247 |
. . . . . . . . 9
|
148 | | pczdvds 15567 |
. . . . . . . . . . . 12
|
149 | 23, 26, 60, 148 | syl12anc 1324 |
. . . . . . . . . . 11
|
150 | 63 | nnzd 11481 |
. . . . . . . . . . . 12
|
151 | | dvdsval2 14986 |
. . . . . . . . . . . 12
|
152 | 150, 71, 26, 151 | syl3anc 1326 |
. . . . . . . . . . 11
|
153 | 149, 152 | mpbid 222 |
. . . . . . . . . 10
|
154 | | pczndvds2 15571 |
. . . . . . . . . . 11
|
155 | 23, 26, 60, 154 | syl12anc 1324 |
. . . . . . . . . 10
|
156 | 153, 155 | jca 554 |
. . . . . . . . 9
|
157 | | pcdvds 15568 |
. . . . . . . . . . . . 13
|
158 | 23, 52, 157 | syl2anc 693 |
. . . . . . . . . . . 12
|
159 | 69 | nnzd 11481 |
. . . . . . . . . . . . 13
|
160 | 52 | nnzd 11481 |
. . . . . . . . . . . . 13
|
161 | | dvdsval2 14986 |
. . . . . . . . . . . . 13
|
162 | 159, 72, 160, 161 | syl3anc 1326 |
. . . . . . . . . . . 12
|
163 | 158, 162 | mpbid 222 |
. . . . . . . . . . 11
|
164 | 52 | nnred 11035 |
. . . . . . . . . . . 12
|
165 | 69 | nnred 11035 |
. . . . . . . . . . . 12
|
166 | 52 | nngt0d 11064 |
. . . . . . . . . . . 12
|
167 | 69 | nngt0d 11064 |
. . . . . . . . . . . 12
|
168 | 164, 165,
166, 167 | divgt0d 10959 |
. . . . . . . . . . 11
|
169 | | elnnz 11387 |
. . . . . . . . . . 11
|
170 | 163, 168,
169 | sylanbrc 698 |
. . . . . . . . . 10
|
171 | | pcndvds2 15572 |
. . . . . . . . . . 11
|
172 | 23, 52, 171 | syl2anc 693 |
. . . . . . . . . 10
|
173 | 170, 172 | jca 554 |
. . . . . . . . 9
|
174 | | pczdvds 15567 |
. . . . . . . . . . . 12
|
175 | 23, 99, 110, 174 | syl12anc 1324 |
. . . . . . . . . . 11
|
176 | 113 | nnzd 11481 |
. . . . . . . . . . . 12
|
177 | | dvdsval2 14986 |
. . . . . . . . . . . 12
|
178 | 176, 121,
99, 177 | syl3anc 1326 |
. . . . . . . . . . 11
|
179 | 175, 178 | mpbid 222 |
. . . . . . . . . 10
|
180 | | pczndvds2 15571 |
. . . . . . . . . . 11
|
181 | 23, 99, 110, 180 | syl12anc 1324 |
. . . . . . . . . 10
|
182 | 179, 181 | jca 554 |
. . . . . . . . 9
|
183 | | pcdvds 15568 |
. . . . . . . . . . . . 13
|
184 | 23, 102, 183 | syl2anc 693 |
. . . . . . . . . . . 12
|
185 | 119 | nnzd 11481 |
. . . . . . . . . . . . 13
|
186 | 102 | nnzd 11481 |
. . . . . . . . . . . . 13
|
187 | | dvdsval2 14986 |
. . . . . . . . . . . . 13
|
188 | 185, 122,
186, 187 | syl3anc 1326 |
. . . . . . . . . . . 12
|
189 | 184, 188 | mpbid 222 |
. . . . . . . . . . 11
|
190 | 102 | nnred 11035 |
. . . . . . . . . . . 12
|
191 | 119 | nnred 11035 |
. . . . . . . . . . . 12
|
192 | 102 | nngt0d 11064 |
. . . . . . . . . . . 12
|
193 | 119 | nngt0d 11064 |
. . . . . . . . . . . 12
|
194 | 190, 191,
192, 193 | divgt0d 10959 |
. . . . . . . . . . 11
|
195 | | elnnz 11387 |
. . . . . . . . . . 11
|
196 | 189, 194,
195 | sylanbrc 698 |
. . . . . . . . . 10
|
197 | | pcndvds2 15572 |
. . . . . . . . . . 11
|
198 | 23, 102, 197 | syl2anc 693 |
. . . . . . . . . 10
|
199 | 196, 198 | jca 554 |
. . . . . . . . 9
|
200 | 23, 98, 144, 147, 156, 173, 182, 199 | pcaddlem 15592 |
. . . . . . . 8
|
201 | 200 | expr 643 |
. . . . . . 7
|
202 | 201 | rexlimdvva 3038 |
. . . . . 6
|
203 | 22, 202 | syl5bir 233 |
. . . . 5
|
204 | 203 | rexlimdvva 3038 |
. . . 4
|
205 | 21, 204 | syl5bir 233 |
. . 3
|
206 | 20, 205 | pm2.61dane 2881 |
. 2
|
207 | 3, 6, 206 | mp2and 715 |
1
|