Step Hyp Ref
Expression 1 pcadd.2 . . 3
2 elq 11213 . . 3
3 1 , 2 sylib 196 . 2
4 pcadd.3 . . 3
5 elq 11213 . . 3
6 4 , 5 sylib 196 . 2
7 pcadd.1 . . . . . . . 8
8 pcxcl 14384 . . . . . . . 8
9 7 , 1 , 8 syl2anc 661 . . . . . . 7
10 xrleid 11385 . . . . . . 7
11 9 , 10 syl 16 . . . . . 6
12 11 adantr 465 . . . . 5
13 oveq2 6304 . . . . . . 7
14 qcn 11225 . . . . . . . . 9
15 1 , 14 syl 16 . . . . . . . 8
16 15 addid1d 9801 . . . . . . 7
17 13 , 16 sylan9eqr 2520 . . . . . 6
18 17 oveq2d 6312 . . . . 5
19 12 , 18 breqtrrd 4478 . . . 4
20 19 a1d 25 . . 3
21 reeanv 3025 . . . 4
22 reeanv 3025 . . . . . 6
23 7 ad3antrrr 729 . . . . . . . . 9
24 prmnn 14220 . . . . . . . . . . . . . . . . 17
25 23 , 24 syl 16 . . . . . . . . . . . . . . . 16
26 simplrl 761 . . . . . . . . . . . . . . . . 17
27 simprrl 765 . . . . . . . . . . . . . . . . . . 19
28 4 ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . 24
29 simpllr 760 . . . . . . . . . . . . . . . . . . . . . . . 24
30 pcqcl 14380 . . . . . . . . . . . . . . . . . . . . . . . 24
31 23 , 28 , 29 , 30 syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . . 23
32 31 zred 10994 . . . . . . . . . . . . . . . . . . . . . 22
33 ltpnf 11360 . . . . . . . . . . . . . . . . . . . . . . 23
34 rexr 9660 . . . . . . . . . . . . . . . . . . . . . . . 24
35 pnfxr 11350 . . . . . . . . . . . . . . . . . . . . . . . 24
36 xrltnle 9674 . . . . . . . . . . . . . . . . . . . . . . . 24
37 34 , 35 , 36 sylancl 662 . . . . . . . . . . . . . . . . . . . . . . 23
38 33 , 37 mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22
39 32 , 38 syl 16 . . . . . . . . . . . . . . . . . . . . 21
40 pc0 14378 . . . . . . . . . . . . . . . . . . . . . . 23
41 23 , 40 syl 16 . . . . . . . . . . . . . . . . . . . . . 22
42 41 breq1d 4462 . . . . . . . . . . . . . . . . . . . . 21
43 39 , 42 mtbird 301 . . . . . . . . . . . . . . . . . . . 20
44 pcadd.4 . . . . . . . . . . . . . . . . . . . . . . 23
45 44 ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22
46 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . 23
47 46 breq1d 4462 . . . . . . . . . . . . . . . . . . . . . 22
48 45 , 47 syl5ibcom 220 . . . . . . . . . . . . . . . . . . . . 21
49 48 necon3bd 2669 . . . . . . . . . . . . . . . . . . . 20
50 43 , 49 mpd 15 . . . . . . . . . . . . . . . . . . 19
51 27 , 50 eqnetrrd 2751 . . . . . . . . . . . . . . . . . 18
52 simprll 763 . . . . . . . . . . . . . . . . . . . . . 22
53 52 nncnd 10577 . . . . . . . . . . . . . . . . . . . . 21
54 52 nnne0d 10605 . . . . . . . . . . . . . . . . . . . . 21
55 53 , 54 div0d 10344 . . . . . . . . . . . . . . . . . . . 20
56 oveq1 6303 . . . . . . . . . . . . . . . . . . . . 21
57 56 eqeq1d 2459 . . . . . . . . . . . . . . . . . . . 20
58 55 , 57 syl5ibrcom 222 . . . . . . . . . . . . . . . . . . 19
59 58 necon3d 2681 . . . . . . . . . . . . . . . . . 18
60 51 , 59 mpd 15 . . . . . . . . . . . . . . . . 17
61 pczcl 14372 . . . . . . . . . . . . . . . . 17
62 23 , 26 , 60 , 61 syl12anc 1226 . . . . . . . . . . . . . . . 16
63 25 , 62 nnexpcld 12331 . . . . . . . . . . . . . . 15
64 63 nncnd 10577 . . . . . . . . . . . . . 14
65 64 , 53 mulcomd 9638 . . . . . . . . . . . . 13
66 65 oveq2d 6312 . . . . . . . . . . . 12
67 26 zcnd 10995 . . . . . . . . . . . . 13
68 23 , 52 pccld 14374 . . . . . . . . . . . . . . 15
69 25 , 68 nnexpcld 12331 . . . . . . . . . . . . . 14
70 69 nncnd 10577 . . . . . . . . . . . . 13
71 63 nnne0d 10605 . . . . . . . . . . . . 13
72 69 nnne0d 10605 . . . . . . . . . . . . 13
73 67 , 64 , 53 , 70 , 71 , 72 , 54 divdivdivd 10392 . . . . . . . . . . . 12
74 27 oveq2d 6312 . . . . . . . . . . . . . . . . 17
75 pcdiv 14376 . . . . . . . . . . . . . . . . . 18
76 23 , 26 , 60 , 52 , 75 syl121anc 1233 . . . . . . . . . . . . . . . . 17
77 74 , 76 eqtrd 2498 . . . . . . . . . . . . . . . 16
78 77 oveq2d 6312 . . . . . . . . . . . . . . 15
79 25 nncnd 10577 . . . . . . . . . . . . . . . 16
80 25 nnne0d 10605 . . . . . . . . . . . . . . . 16
81 68 nn0zd 10992 . . . . . . . . . . . . . . . 16
82 62 nn0zd 10992 . . . . . . . . . . . . . . . 16
83 79 , 80 , 81 , 82 expsubd 12321 . . . . . . . . . . . . . . 15
84 78 , 83 eqtrd 2498 . . . . . . . . . . . . . 14
85 84 oveq2d 6312 . . . . . . . . . . . . 13
86 27 oveq1d 6311 . . . . . . . . . . . . 13
87 67 , 53 , 64 , 70 , 54 , 72 , 71 divdivdivd 10392 . . . . . . . . . . . . 13
88 85 , 86 , 87 3eqtrd 2502 . . . . . . . . . . . 12
89 66 , 73 , 88 3eqtr4d 2508 . . . . . . . . . . 11
90 89 oveq2d 6312 . . . . . . . . . 10
91 1 ad3antrrr 729 . . . . . . . . . . . 12
92 91 , 14 syl 16 . . . . . . . . . . 11
93 pcqcl 14380 . . . . . . . . . . . . 13
94 23 , 91 , 50 , 93 syl12anc 1226 . . . . . . . . . . . 12
95 79 , 80 , 94 expclzd 12315 . . . . . . . . . . 11
96 79 , 80 , 94 expne0d 12316 . . . . . . . . . . 11
97 92 , 95 , 96 divcan2d 10347 . . . . . . . . . 10
98 90 , 97 eqtr2d 2499 . . . . . . . . 9
99 simplrr 762 . . . . . . . . . . . . . . . . 17
100 simprrr 766 . . . . . . . . . . . . . . . . . . 19
101 100 , 29 eqnetrrd 2751 . . . . . . . . . . . . . . . . . 18
102 simprlr 764 . . . . . . . . . . . . . . . . . . . . . 22
103 102 nncnd 10577 . . . . . . . . . . . . . . . . . . . . 21
104 102 nnne0d 10605 . . . . . . . . . . . . . . . . . . . . 21
105 103 , 104 div0d 10344 . . . . . . . . . . . . . . . . . . . 20
106 oveq1 6303 . . . . . . . . . . . . . . . . . . . . 21
107 106 eqeq1d 2459 . . . . . . . . . . . . . . . . . . . 20
108 105 , 107 syl5ibrcom 222 . . . . . . . . . . . . . . . . . . 19
109 108 necon3d 2681 . . . . . . . . . . . . . . . . . 18
110 101 , 109 mpd 15 . . . . . . . . . . . . . . . . 17
111 pczcl 14372 . . . . . . . . . . . . . . . . 17
112 23 , 99 , 110 , 111 syl12anc 1226 . . . . . . . . . . . . . . . 16
113 25 , 112 nnexpcld 12331 . . . . . . . . . . . . . . 15
114 113 nncnd 10577 . . . . . . . . . . . . . 14
115 114 , 103 mulcomd 9638 . . . . . . . . . . . . 13
116 115 oveq2d 6312 . . . . . . . . . . . 12
117 99 zcnd 10995 . . . . . . . . . . . . 13
118 23 , 102 pccld 14374 . . . . . . . . . . . . . . 15
119 25 , 118 nnexpcld 12331 . . . . . . . . . . . . . 14
120 119 nncnd 10577 . . . . . . . . . . . . 13
121 113 nnne0d 10605 . . . . . . . . . . . . 13
122 119 nnne0d 10605 . . . . . . . . . . . . 13
123 117 , 114 ,
103 , 120 , 121 , 122 , 104 divdivdivd 10392 . . . . . . . . . . . 12
124 100 oveq2d 6312 . . . . . . . . . . . . . . . . 17
125 pcdiv 14376 . . . . . . . . . . . . . . . . . 18
126 23 , 99 , 110 , 102 , 125 syl121anc 1233 . . . . . . . . . . . . . . . . 17
127 124 , 126 eqtrd 2498 . . . . . . . . . . . . . . . 16
128 127 oveq2d 6312 . . . . . . . . . . . . . . 15
129 118 nn0zd 10992 . . . . . . . . . . . . . . . 16
130 112 nn0zd 10992 . . . . . . . . . . . . . . . 16
131 79 , 80 , 129 , 130 expsubd 12321 . . . . . . . . . . . . . . 15
132 128 , 131 eqtrd 2498 . . . . . . . . . . . . . 14
133 132 oveq2d 6312 . . . . . . . . . . . . 13
134 100 oveq1d 6311 . . . . . . . . . . . . 13
