Proof of Theorem pcaddlem
Step | Hyp | Ref
| Expression |
1 | | pcaddlem.4 |
. . . . . . . . 9
|
2 | | eluzel2 9479 |
. . . . . . . . 9
|
3 | 1, 2 | syl 14 |
. . . . . . . 8
|
4 | 3 | zred 9321 |
. . . . . . 7
|
5 | 4 | rexrd 7956 |
. . . . . 6
|
6 | | pnfge 9733 |
. . . . . 6
|
7 | 5, 6 | syl 14 |
. . . . 5
|
8 | | pcaddlem.1 |
. . . . . 6
|
9 | | pc0 12245 |
. . . . . 6
|
10 | 8, 9 | syl 14 |
. . . . 5
|
11 | 7, 10 | breqtrrd 4015 |
. . . 4
|
12 | 11 | adantr 274 |
. . 3
|
13 | | simpr 109 |
. . . 4
|
14 | 13 | oveq2d 5866 |
. . 3
|
15 | 12, 14 | breqtrrd 4015 |
. 2
|
16 | 4 | adantr 274 |
. . . 4
|
17 | | prmnn 12051 |
. . . . . . . . . . . . . 14
|
18 | 8, 17 | syl 14 |
. . . . . . . . . . . . 13
|
19 | 18 | nncnd 8879 |
. . . . . . . . . . . 12
|
20 | 18 | nnap0d 8911 |
. . . . . . . . . . . 12
# |
21 | | eluzelz 9483 |
. . . . . . . . . . . . . 14
|
22 | 1, 21 | syl 14 |
. . . . . . . . . . . . 13
|
23 | 22, 3 | zsubcld 9326 |
. . . . . . . . . . . 12
|
24 | 19, 20, 23 | expclzapd 10601 |
. . . . . . . . . . 11
|
25 | | pcaddlem.7 |
. . . . . . . . . . . . 13
|
26 | 25 | simpld 111 |
. . . . . . . . . . . 12
|
27 | 26 | zcnd 9322 |
. . . . . . . . . . 11
|
28 | | pcaddlem.8 |
. . . . . . . . . . . . 13
|
29 | 28 | simpld 111 |
. . . . . . . . . . . 12
|
30 | 29 | nncnd 8879 |
. . . . . . . . . . 11
|
31 | 29 | nnap0d 8911 |
. . . . . . . . . . 11
# |
32 | 24, 27, 30, 31 | divassapd 8730 |
. . . . . . . . . 10
|
33 | 32 | oveq2d 5866 |
. . . . . . . . 9
|
34 | | pcaddlem.5 |
. . . . . . . . . . . 12
|
35 | 34 | simpld 111 |
. . . . . . . . . . 11
|
36 | 35 | zcnd 9322 |
. . . . . . . . . 10
|
37 | 24, 27 | mulcld 7927 |
. . . . . . . . . 10
|
38 | | pcaddlem.6 |
. . . . . . . . . . . . 13
|
39 | 38 | simpld 111 |
. . . . . . . . . . . 12
|
40 | 39 | nncnd 8879 |
. . . . . . . . . . 11
|
41 | 39 | nnap0d 8911 |
. . . . . . . . . . 11
# |
42 | 40, 41 | jca 304 |
. . . . . . . . . 10
# |
43 | 30, 31 | jca 304 |
. . . . . . . . . 10
# |
44 | | divadddivap 8631 |
. . . . . . . . . 10
#
# |
45 | 36, 37, 42, 43, 44 | syl22anc 1234 |
. . . . . . . . 9
|
46 | 33, 45 | eqtr3d 2205 |
. . . . . . . 8
|
47 | 46 | oveq2d 5866 |
. . . . . . 7
|
48 | 47 | adantr 274 |
. . . . . 6
|
49 | 8 | adantr 274 |
. . . . . . 7
|
50 | 29 | nnzd 9320 |
. . . . . . . . . 10
|
51 | 35, 50 | zmulcld 9327 |
. . . . . . . . 9
|
52 | | uznn0sub 9505 |
. . . . . . . . . . . . . 14
|
53 | 1, 52 | syl 14 |
. . . . . . . . . . . . 13
|
54 | 18, 53 | nnexpcld 10618 |
. . . . . . . . . . . 12
|
55 | 54 | nnzd 9320 |
. . . . . . . . . . 11
|
56 | 55, 26 | zmulcld 9327 |
. . . . . . . . . 10
|
57 | 39 | nnzd 9320 |
. . . . . . . . . 10
|
58 | 56, 57 | zmulcld 9327 |
. . . . . . . . 9
|
59 | 51, 58 | zaddcld 9325 |
. . . . . . . 8
|
60 | 59 | adantr 274 |
. . . . . . 7
|
61 | 19, 20, 3 | expclzapd 10601 |
. . . . . . . . . . . . 13
|
62 | 61 | mul01d 8299 |
. . . . . . . . . . . 12
|
63 | | oveq2 5858 |
. . . . . . . . . . . . 13
|
64 | 63 | eqeq1d 2179 |
. . . . . . . . . . . 12
|
65 | 62, 64 | syl5ibrcom 156 |
. . . . . . . . . . 11
|
66 | 65 | necon3d 2384 |
. . . . . . . . . 10
|
67 | 36, 40, 41 | divclapd 8694 |
. . . . . . . . . . . . 13
|
68 | 27, 30, 31 | divclapd 8694 |
. . . . . . . . . . . . . 14
|
69 | 24, 68 | mulcld 7927 |
. . . . . . . . . . . . 13
|
70 | 61, 67, 69 | adddid 7931 |
. . . . . . . . . . . 12
|
71 | | pcaddlem.2 |
. . . . . . . . . . . . 13
|
72 | | pcaddlem.3 |
. . . . . . . . . . . . . 14
|
73 | 3 | zcnd 9322 |
. . . . . . . . . . . . . . . . . 18
|
74 | 22 | zcnd 9322 |
. . . . . . . . . . . . . . . . . 18
|
75 | 73, 74 | pncan3d 8220 |
. . . . . . . . . . . . . . . . 17
|
76 | 75 | oveq2d 5866 |
. . . . . . . . . . . . . . . 16
|
77 | | expaddzap 10507 |
. . . . . . . . . . . . . . . . 17
#
|
78 | 19, 20, 3, 23, 77 | syl22anc 1234 |
. . . . . . . . . . . . . . . 16
|
79 | 76, 78 | eqtr3d 2205 |
. . . . . . . . . . . . . . 15
|
80 | 79 | oveq1d 5865 |
. . . . . . . . . . . . . 14
|
81 | 61, 24, 68 | mulassd 7930 |
. . . . . . . . . . . . . 14
|
82 | 72, 80, 81 | 3eqtrd 2207 |
. . . . . . . . . . . . 13
|
83 | 71, 82 | oveq12d 5868 |
. . . . . . . . . . . 12
|
84 | 70, 83 | eqtr4d 2206 |
. . . . . . . . . . 11
|
85 | 84 | neeq1d 2358 |
. . . . . . . . . 10
|
86 | 46 | neeq1d 2358 |
. . . . . . . . . 10
|
87 | 66, 85, 86 | 3imtr3d 201 |
. . . . . . . . 9
|
88 | 39, 29 | nnmulcld 8914 |
. . . . . . . . . . . . 13
|
89 | 88 | nncnd 8879 |
. . . . . . . . . . . 12
|
90 | 40, 30, 41, 31 | mulap0d 8563 |
. . . . . . . . . . . 12
# |
91 | 89, 90 | div0apd 8691 |
. . . . . . . . . . 11
|
92 | | oveq1 5857 |
. . . . . . . . . . . 12
|
93 | 92 | eqeq1d 2179 |
. . . . . . . . . . 11
|
94 | 91, 93 | syl5ibrcom 156 |
. . . . . . . . . 10
|
95 | 94 | necon3d 2384 |
. . . . . . . . 9
|
96 | 87, 95 | syld 45 |
. . . . . . . 8
|
97 | 96 | imp 123 |
. . . . . . 7
|
98 | 88 | adantr 274 |
. . . . . . 7
|
99 | | pcdiv 12243 |
. . . . . . 7
|
100 | 49, 60, 97, 98, 99 | syl121anc 1238 |
. . . . . 6
|
101 | 39 | nnne0d 8910 |
. . . . . . . . . . 11
|
102 | 29 | nnne0d 8910 |
. . . . . . . . . . 11
|
103 | | pcmul 12242 |
. . . . . . . . . . 11
|
104 | 8, 57, 101, 50, 102, 103 | syl122anc 1242 |
. . . . . . . . . 10
|
105 | 38 | simprd 113 |
. . . . . . . . . . . . 13
|
106 | | pceq0 12262 |
. . . . . . . . . . . . . 14
|
107 | 8, 39, 106 | syl2anc 409 |
. . . . . . . . . . . . 13
|
108 | 105, 107 | mpbird 166 |
. . . . . . . . . . . 12
|
109 | 28 | simprd 113 |
. . . . . . . . . . . . 13
|
110 | | pceq0 12262 |
. . . . . . . . . . . . . 14
|
111 | 8, 29, 110 | syl2anc 409 |
. . . . . . . . . . . . 13
|
112 | 109, 111 | mpbird 166 |
. . . . . . . . . . . 12
|
113 | 108, 112 | oveq12d 5868 |
. . . . . . . . . . 11
|
114 | | 00id 8047 |
. . . . . . . . . . 11
|
115 | 113, 114 | eqtrdi 2219 |
. . . . . . . . . 10
|
116 | 104, 115 | eqtrd 2203 |
. . . . . . . . 9
|
117 | 116 | oveq2d 5866 |
. . . . . . . 8
|
118 | 117 | adantr 274 |
. . . . . . 7
|
119 | | pczcl 12239 |
. . . . . . . . . 10
|
120 | 49, 60, 97, 119 | syl12anc 1231 |
. . . . . . . . 9
|
121 | 120 | nn0cnd 9177 |
. . . . . . . 8
|
122 | 121 | subid1d 8206 |
. . . . . . 7
|
123 | 118, 122 | eqtrd 2203 |
. . . . . 6
|
124 | 48, 100, 123 | 3eqtrd 2207 |
. . . . 5
|
125 | 124, 120 | eqeltrd 2247 |
. . . 4
|
126 | | nn0addge1 9168 |
. . . 4
|
127 | 16, 125, 126 | syl2anc 409 |
. . 3
|
128 | | nnq 9579 |
. . . . . . . 8
|
129 | 18, 128 | syl 14 |
. . . . . . 7
|
130 | 18 | nnne0d 8910 |
. . . . . . 7
|
131 | | qexpclz 10484 |
. . . . . . 7
|
132 | 129, 130,
3, 131 | syl3anc 1233 |
. . . . . 6
|
133 | 132 | adantr 274 |
. . . . 5
|
134 | 19, 20, 3 | expap0d 10602 |
. . . . . . 7
# |
135 | | 0z 9210 |
. . . . . . . . 9
|
136 | | zq 9572 |
. . . . . . . . 9
|
137 | 135, 136 | mp1i 10 |
. . . . . . . 8
|
138 | | qapne 9585 |
. . . . . . . 8
#
|
139 | 132, 137,
138 | syl2anc 409 |
. . . . . . 7
#
|
140 | 134, 139 | mpbid 146 |
. . . . . 6
|
141 | 140 | adantr 274 |
. . . . 5
|
142 | | znq 9570 |
. . . . . . . 8
|
143 | 35, 39, 142 | syl2anc 409 |
. . . . . . 7
|
144 | | qexpclz 10484 |
. . . . . . . . 9
|
145 | 129, 130,
23, 144 | syl3anc 1233 |
. . . . . . . 8
|
146 | | znq 9570 |
. . . . . . . . 9
|
147 | 26, 29, 146 | syl2anc 409 |
. . . . . . . 8
|
148 | | qmulcl 9583 |
. . . . . . . 8
|
149 | 145, 147,
148 | syl2anc 409 |
. . . . . . 7
|
150 | | qaddcl 9581 |
. . . . . . 7
|
151 | 143, 149,
150 | syl2anc 409 |
. . . . . 6
|
152 | 151 | adantr 274 |
. . . . 5
|
153 | 85, 66 | sylbird 169 |
. . . . . 6
|
154 | 153 | imp 123 |
. . . . 5
|
155 | | pcqmul 12244 |
. . . . 5
|
156 | 49, 133, 141, 152, 154, 155 | syl122anc 1242 |
. . . 4
|
157 | 84 | oveq2d 5866 |
. . . . 5
|
158 | 157 | adantr 274 |
. . . 4
|
159 | | pcid 12264 |
. . . . . . 7
|
160 | 8, 3, 159 | syl2anc 409 |
. . . . . 6
|
161 | 160 | oveq1d 5865 |
. . . . 5
|
162 | 161 | adantr 274 |
. . . 4
|
163 | 156, 158,
162 | 3eqtr3d 2211 |
. . 3
|
164 | 127, 163 | breqtrrd 4015 |
. 2
|
165 | | qmulcl 9583 |
. . . . . . 7
|
166 | 132, 143,
165 | syl2anc 409 |
. . . . . 6
|
167 | 71, 166 | eqeltrd 2247 |
. . . . 5
|
168 | | qexpclz 10484 |
. . . . . . . 8
|
169 | 129, 130,
22, 168 | syl3anc 1233 |
. . . . . . 7
|
170 | | qmulcl 9583 |
. . . . . . 7
|
171 | 169, 147,
170 | syl2anc 409 |
. . . . . 6
|
172 | 72, 171 | eqeltrd 2247 |
. . . . 5
|
173 | | qaddcl 9581 |
. . . . 5
|
174 | 167, 172,
173 | syl2anc 409 |
. . . 4
|
175 | | qdceq 10190 |
. . . 4
DECID |
176 | 174, 137,
175 | syl2anc 409 |
. . 3
DECID |
177 | | dcne 2351 |
. . 3
DECID |
178 | 176, 177 | sylib 121 |
. 2
|
179 | 15, 164, 178 | mpjaodan 793 |
1
|