Step Hyp Ref
Expression 1 oveq2 6304 . . 3
2 1 breq2d 4464 . 2
3 pcaddlem.4 . . . . . . 7
4 eluzel2 11115 . . . . . . 7
5 3 , 4 syl 16 . . . . . 6
6 5 zred 10994 . . . . 5
7 6 adantr 465 . . . 4
8 pcaddlem.1 . . . . . . . . . . . . . 14
9 prmnn 14220 . . . . . . . . . . . . . 14
10 8 , 9 syl 16 . . . . . . . . . . . . 13
11 10 nncnd 10577 . . . . . . . . . . . 12
12 10 nnne0d 10605 . . . . . . . . . . . 12
13 eluzelz 11119 . . . . . . . . . . . . . 14
14 3 , 13 syl 16 . . . . . . . . . . . . 13
15 14 , 5 zsubcld 10999 . . . . . . . . . . . 12
16 11 , 12 , 15 expclzd 12315 . . . . . . . . . . 11
17 pcaddlem.7 . . . . . . . . . . . . 13
18 17 simpld 459 . . . . . . . . . . . 12
19 18 zcnd 10995 . . . . . . . . . . 11
20 pcaddlem.8 . . . . . . . . . . . . 13
21 20 simpld 459 . . . . . . . . . . . 12
22 21 nncnd 10577 . . . . . . . . . . 11
23 21 nnne0d 10605 . . . . . . . . . . 11
24 16 , 19 , 22 , 23 divassd 10380 . . . . . . . . . 10
25 24 oveq2d 6312 . . . . . . . . 9
26 pcaddlem.5 . . . . . . . . . . . 12
27 26 simpld 459 . . . . . . . . . . 11
28 27 zcnd 10995 . . . . . . . . . 10
29 pcaddlem.6 . . . . . . . . . . . 12
30 29 simpld 459 . . . . . . . . . . 11
31 30 nncnd 10577 . . . . . . . . . 10
32 16 , 19 mulcld 9637 . . . . . . . . . 10
33 30 nnne0d 10605 . . . . . . . . . 10
34 28 , 31 , 32 , 22 , 33 , 23 divadddivd 10389 . . . . . . . . 9
35 25 , 34 eqtr3d 2500 . . . . . . . 8
36 35 oveq2d 6312 . . . . . . 7
37 36 adantr 465 . . . . . 6
38 8 adantr 465 . . . . . . 7
39 21 nnzd 10993 . . . . . . . . . 10
40 27 , 39 zmulcld 11000 . . . . . . . . 9
41 uznn0sub 11141 . . . . . . . . . . . . . 14
42 3 , 41 syl 16 . . . . . . . . . . . . 13
43 10 , 42 nnexpcld 12331 . . . . . . . . . . . 12
44 43 nnzd 10993 . . . . . . . . . . 11
45 44 , 18 zmulcld 11000 . . . . . . . . . 10
46 30 nnzd 10993 . . . . . . . . . 10
47 45 , 46 zmulcld 11000 . . . . . . . . 9
48 40 , 47 zaddcld 10998 . . . . . . . 8
49 48 adantr 465 . . . . . . 7
50 11 , 12 , 5 expclzd 12315 . . . . . . . . . . . . 13
51 50 mul01d 9800 . . . . . . . . . . . 12
52 oveq2 6304 . . . . . . . . . . . . 13
53 52 eqeq1d 2459 . . . . . . . . . . . 12
54 51 , 53 syl5ibrcom 222 . . . . . . . . . . 11
55 54 necon3d 2681 . . . . . . . . . 10
56 28 , 31 , 33 divcld 10345 . . . . . . . . . . . . 13
57 19 , 22 , 23 divcld 10345 . . . . . . . . . . . . . 14
58 16 , 57 mulcld 9637 . . . . . . . . . . . . 13
59 50 , 56 , 58 adddid 9641 . . . . . . . . . . . 12
60 pcaddlem.2 . . . . . . . . . . . . 13
61 pcaddlem.3 . . . . . . . . . . . . . 14
62 5 zcnd 10995 . . . . . . . . . . . . . . . . . 18
63 14 zcnd 10995 . . . . . . . . . . . . . . . . . 18
64 62 , 63 pncan3d 9957 . . . . . . . . . . . . . . . . 17
65 64 oveq2d 6312 . . . . . . . . . . . . . . . 16
66 expaddz 12210 . . . . . . . . . . . . . . . . 17
67 11 , 12 , 5 , 15 , 66 syl22anc 1229 . . . . . . . . . . . . . . . 16
68 65 , 67 eqtr3d 2500 . . . . . . . . . . . . . . 15
69 68 oveq1d 6311 . . . . . . . . . . . . . 14
70 50 , 16 , 57 mulassd 9640 . . . . . . . . . . . . . 14
71 61 , 69 , 70 3eqtrd 2502 . . . . . . . . . . . . 13
72 60 , 71 oveq12d 6314 . . . . . . . . . . . 12
73 59 , 72 eqtr4d 2501 . . . . . . . . . . 11
74 73 neeq1d 2734 . . . . . . . . . 10
75 35 neeq1d 2734 . . . . . . . . . 10
76 55 , 74 , 75 3imtr3d 267 . . . . . . . . 9
77 30 , 21 nnmulcld 10608 . . . . . . . . . . . . 13
78 77 nncnd 10577 . . . . . . . . . . . 12
79 77 nnne0d 10605 . . . . . . . . . . . 12
80 78 , 79 div0d 10344 . . . . . . . . . . 11
81 oveq1 6303 . . . . . . . . . . . 12
82 81 eqeq1d 2459 . . . . . . . . . . 11
83 80 , 82 syl5ibrcom 222 . . . . . . . . . 10
84 83 necon3d 2681 . . . . . . . . 9
85 76 , 84 syld 44 . . . . . . . 8
86 85 imp 429 . . . . . . 7
87 77 adantr 465 . . . . . . 7
88 pcdiv 14376 . . . . . . 7
89 38 , 49 , 86 , 87 , 88 syl121anc 1233 . . . . . 6
90 pcmul 14375 . . . . . . . . . . 11
91 8 , 46 , 33 , 39 , 23 , 90 syl122anc 1237 . . . . . . . . . 10
92 29 simprd 463 . . . . . . . . . . . . 13
93 pceq0 14394 . . . . . . . . . . . . . 14
94 8 , 30 , 93 syl2anc 661 . . . . . . . . . . . . 13
95 92 , 94 mpbird 232 . . . . . . . . . . . 12
96 20 simprd 463 . . . . . . . . . . . . 13
97 pceq0 14394 . . . . . . . . . . . . . 14
98 8 , 21 , 97 syl2anc 661 . . . . . . . . . . . . 13
99 96 , 98 mpbird 232 . . . . . . . . . . . 12
100 95 , 99 oveq12d 6314 . . . . . . . . . . 11
101 00id 9776 . . . . . . . . . . 11
102 100 , 101 syl6eq 2514 . . . . . . . . . 10
103 91 , 102 eqtrd 2498 . . . . . . . . 9
104 103 oveq2d 6312 . . . . . . . 8
105 104 adantr 465 . . . . . . 7
106 pczcl 14372 . . . . . . . . . 10
107 38 , 49 , 86 , 106 syl12anc 1226 . . . . . . . . 9
108 107 nn0cnd 10879 . . . . . . . 8
109 108 subid1d 9943 . . . . . . 7
110 105 , 109 eqtrd 2498 . . . . . 6
111 37 , 89 , 110 3eqtrd 2502 . . . . 5
112 111 , 107 eqeltrd 2545 . . . 4
113 nn0addge1 10867 . . . 4
114 7 , 112 , 113 syl2anc 661 . . 3
115 nnq 11224 . . . . . . . 8
116 10 , 115 syl 16 . . . . . . 7
117 qexpclz 12187 . . . . . . 7
118 116 , 12 , 5 , 117 syl3anc 1228 . . . . . 6
119 118 adantr 465 . . . . 5
120 11 , 12 , 5 expne0d 12316 . . . . . 6
121 120 adantr 465 . . . . 5
122 znq 11215 . . . . . . . 8
123 27 , 30 , 122 syl2anc 661 . . . . . . 7
124 qexpclz 12187 . . . . . . . . 9
125 116 , 12 , 15 , 124 syl3anc 1228 . . . . . . . 8
126 znq 11215 . . . . . . . . 9
127 18 , 21 , 126 syl2anc 661 . . . . . . . 8
128 qmulcl 11229 . . . . . . . 8
129 125 , 127 ,
128 syl2anc 661 . . . . . . 7
130 qaddcl 11227 . . . . . . 7
131 123 , 129 ,
130 syl2anc 661 . . . . . 6
132 131 adantr 465 . . . . 5
133 74 , 55 sylbird 235 . . . . . 6
134 133 imp 429 . . . . 5
135 pcqmul 14377 . . . . 5
136 38 , 119 , 121 , 132 , 134 , 135 syl122anc 1237 . . . 4
137 73 oveq2d 6312 . . . . 5
138 137 adantr 465 . . . 4
139 pcid 14396 . . . . . . 7
140 8 , 5 , 139 syl2anc 661 . . . . . 6
141 140 oveq1d 6311 . . . . 5
142 141 adantr 465 . . . 4
143 136 , 138 ,
142 3eqtr3d 2506 . . 3
144 114 , 143 breqtrrd 4478 . 2
145 6 rexrd 9664 . . . 4
146 pnfge 11368 . . . 4
147 145 , 146 syl 16 . . 3
148 pc0 14378 . . . 4
149 8 , 148 syl 16 . . 3
150 147 , 149 breqtrrd 4478 . 2
151 2 , 144 , 150 pm2.61ne 2772 1
