# Metamath Proof Explorer

Description: Lemma for pcadd . The original numbers A and B have been decomposed using the prime count function as ( P ^ M ) x. ( R / S ) where R , S are both not divisible by P and M = ( P pCnt A ) , and similarly for B . (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Hypotheses pcaddlem.1 ${⊢}{\phi }\to {P}\in ℙ$
pcaddlem.2 ${⊢}{\phi }\to {A}={{P}}^{{M}}\left(\frac{{R}}{{S}}\right)$
pcaddlem.3 ${⊢}{\phi }\to {B}={{P}}^{{N}}\left(\frac{{T}}{{U}}\right)$
pcaddlem.4 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
pcaddlem.5 ${⊢}{\phi }\to \left({R}\in ℤ\wedge ¬{P}\parallel {R}\right)$
pcaddlem.6 ${⊢}{\phi }\to \left({S}\in ℕ\wedge ¬{P}\parallel {S}\right)$
pcaddlem.7 ${⊢}{\phi }\to \left({T}\in ℤ\wedge ¬{P}\parallel {T}\right)$
pcaddlem.8 ${⊢}{\phi }\to \left({U}\in ℕ\wedge ¬{P}\parallel {U}\right)$
Assertion pcaddlem ${⊢}{\phi }\to {M}\le {P}\mathrm{pCnt}\left({A}+{B}\right)$

### Proof

Step Hyp Ref Expression
1 pcaddlem.1 ${⊢}{\phi }\to {P}\in ℙ$
2 pcaddlem.2 ${⊢}{\phi }\to {A}={{P}}^{{M}}\left(\frac{{R}}{{S}}\right)$
3 pcaddlem.3 ${⊢}{\phi }\to {B}={{P}}^{{N}}\left(\frac{{T}}{{U}}\right)$
4 pcaddlem.4 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
5 pcaddlem.5 ${⊢}{\phi }\to \left({R}\in ℤ\wedge ¬{P}\parallel {R}\right)$
6 pcaddlem.6 ${⊢}{\phi }\to \left({S}\in ℕ\wedge ¬{P}\parallel {S}\right)$
7 pcaddlem.7 ${⊢}{\phi }\to \left({T}\in ℤ\wedge ¬{P}\parallel {T}\right)$
8 pcaddlem.8 ${⊢}{\phi }\to \left({U}\in ℕ\wedge ¬{P}\parallel {U}\right)$
9 oveq2 ${⊢}{A}+{B}=0\to {P}\mathrm{pCnt}\left({A}+{B}\right)={P}\mathrm{pCnt}0$
10 9 breq2d ${⊢}{A}+{B}=0\to \left({M}\le {P}\mathrm{pCnt}\left({A}+{B}\right)↔{M}\le {P}\mathrm{pCnt}0\right)$
11 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
12 4 11 syl ${⊢}{\phi }\to {M}\in ℤ$
13 12 zred ${⊢}{\phi }\to {M}\in ℝ$
14 13 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {M}\in ℝ$
15 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
16 1 15 syl ${⊢}{\phi }\to {P}\in ℕ$
17 16 nncnd ${⊢}{\phi }\to {P}\in ℂ$
18 16 nnne0d ${⊢}{\phi }\to {P}\ne 0$
19 eluzelz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in ℤ$
20 4 19 syl ${⊢}{\phi }\to {N}\in ℤ$
21 20 12 zsubcld ${⊢}{\phi }\to {N}-{M}\in ℤ$
22 17 18 21 expclzd ${⊢}{\phi }\to {{P}}^{{N}-{M}}\in ℂ$
23 7 simpld ${⊢}{\phi }\to {T}\in ℤ$
24 23 zcnd ${⊢}{\phi }\to {T}\in ℂ$
25 8 simpld ${⊢}{\phi }\to {U}\in ℕ$
26 25 nncnd ${⊢}{\phi }\to {U}\in ℂ$
27 25 nnne0d ${⊢}{\phi }\to {U}\ne 0$
28 22 24 26 27 divassd ${⊢}{\phi }\to \frac{{{P}}^{{N}-{M}}{T}}{{U}}={{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)$
29 28 oveq2d ${⊢}{\phi }\to \left(\frac{{R}}{{S}}\right)+\left(\frac{{{P}}^{{N}-{M}}{T}}{{U}}\right)=\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)$
30 5 simpld ${⊢}{\phi }\to {R}\in ℤ$
31 30 zcnd ${⊢}{\phi }\to {R}\in ℂ$
32 6 simpld ${⊢}{\phi }\to {S}\in ℕ$
33 32 nncnd ${⊢}{\phi }\to {S}\in ℂ$
34 22 24 mulcld ${⊢}{\phi }\to {{P}}^{{N}-{M}}{T}\in ℂ$
35 32 nnne0d ${⊢}{\phi }\to {S}\ne 0$
36 31 33 34 26 35 27 divadddivd ${⊢}{\phi }\to \left(\frac{{R}}{{S}}\right)+\left(\frac{{{P}}^{{N}-{M}}{T}}{{U}}\right)=\frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}$
37 29 36 eqtr3d ${⊢}{\phi }\to \left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)=\frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}$
38 37 oveq2d ${⊢}{\phi }\to {P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)={P}\mathrm{pCnt}\left(\frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}\right)$
39 38 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)={P}\mathrm{pCnt}\left(\frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}\right)$
40 1 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {P}\in ℙ$
41 25 nnzd ${⊢}{\phi }\to {U}\in ℤ$
42 30 41 zmulcld ${⊢}{\phi }\to {R}{U}\in ℤ$
43 uznn0sub ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}-{M}\in {ℕ}_{0}$
44 4 43 syl ${⊢}{\phi }\to {N}-{M}\in {ℕ}_{0}$
45 16 44 nnexpcld ${⊢}{\phi }\to {{P}}^{{N}-{M}}\in ℕ$
46 45 nnzd ${⊢}{\phi }\to {{P}}^{{N}-{M}}\in ℤ$
47 46 23 zmulcld ${⊢}{\phi }\to {{P}}^{{N}-{M}}{T}\in ℤ$
48 32 nnzd ${⊢}{\phi }\to {S}\in ℤ$
49 47 48 zmulcld ${⊢}{\phi }\to {{P}}^{{N}-{M}}{T}{S}\in ℤ$
50 42 49 zaddcld ${⊢}{\phi }\to {R}{U}+{{P}}^{{N}-{M}}{T}{S}\in ℤ$
51 50 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {R}{U}+{{P}}^{{N}-{M}}{T}{S}\in ℤ$
52 17 18 12 expclzd ${⊢}{\phi }\to {{P}}^{{M}}\in ℂ$
53 52 mul01d ${⊢}{\phi }\to {{P}}^{{M}}\cdot 0=0$
54 oveq2 ${⊢}\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)=0\to {{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)={{P}}^{{M}}\cdot 0$
55 54 eqeq1d ${⊢}\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)=0\to \left({{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)=0↔{{P}}^{{M}}\cdot 0=0\right)$
56 53 55 syl5ibrcom ${⊢}{\phi }\to \left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)=0\to {{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)=0\right)$
57 56 necon3d ${⊢}{\phi }\to \left({{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\ne 0\to \left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\ne 0\right)$
58 31 33 35 divcld ${⊢}{\phi }\to \frac{{R}}{{S}}\in ℂ$
59 24 26 27 divcld ${⊢}{\phi }\to \frac{{T}}{{U}}\in ℂ$
60 22 59 mulcld ${⊢}{\phi }\to {{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\in ℂ$
61 52 58 60 adddid ${⊢}{\phi }\to {{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)={{P}}^{{M}}\left(\frac{{R}}{{S}}\right)+{{P}}^{{M}}{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)$
62 12 zcnd ${⊢}{\phi }\to {M}\in ℂ$
63 20 zcnd ${⊢}{\phi }\to {N}\in ℂ$
64 62 63 pncan3d ${⊢}{\phi }\to {M}+{N}-{M}={N}$
65 64 oveq2d ${⊢}{\phi }\to {{P}}^{{M}+{N}-{M}}={{P}}^{{N}}$
66 expaddz ${⊢}\left(\left({P}\in ℂ\wedge {P}\ne 0\right)\wedge \left({M}\in ℤ\wedge {N}-{M}\in ℤ\right)\right)\to {{P}}^{{M}+{N}-{M}}={{P}}^{{M}}{{P}}^{{N}-{M}}$
67 17 18 12 21 66 syl22anc ${⊢}{\phi }\to {{P}}^{{M}+{N}-{M}}={{P}}^{{M}}{{P}}^{{N}-{M}}$
68 65 67 eqtr3d ${⊢}{\phi }\to {{P}}^{{N}}={{P}}^{{M}}{{P}}^{{N}-{M}}$
69 68 oveq1d ${⊢}{\phi }\to {{P}}^{{N}}\left(\frac{{T}}{{U}}\right)={{P}}^{{M}}{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)$
70 52 22 59 mulassd ${⊢}{\phi }\to {{P}}^{{M}}{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)={{P}}^{{M}}{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)$
71 3 69 70 3eqtrd ${⊢}{\phi }\to {B}={{P}}^{{M}}{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)$
72 2 71 oveq12d ${⊢}{\phi }\to {A}+{B}={{P}}^{{M}}\left(\frac{{R}}{{S}}\right)+{{P}}^{{M}}{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)$
73 61 72 eqtr4d ${⊢}{\phi }\to {{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)={A}+{B}$
74 73 neeq1d ${⊢}{\phi }\to \left({{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\ne 0↔{A}+{B}\ne 0\right)$
75 37 neeq1d ${⊢}{\phi }\to \left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\ne 0↔\frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}\ne 0\right)$
76 57 74 75 3imtr3d ${⊢}{\phi }\to \left({A}+{B}\ne 0\to \frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}\ne 0\right)$
77 32 25 nnmulcld ${⊢}{\phi }\to {S}{U}\in ℕ$
78 77 nncnd ${⊢}{\phi }\to {S}{U}\in ℂ$
79 77 nnne0d ${⊢}{\phi }\to {S}{U}\ne 0$
80 78 79 div0d ${⊢}{\phi }\to \frac{0}{{S}{U}}=0$
81 oveq1 ${⊢}{R}{U}+{{P}}^{{N}-{M}}{T}{S}=0\to \frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}=\frac{0}{{S}{U}}$
82 81 eqeq1d ${⊢}{R}{U}+{{P}}^{{N}-{M}}{T}{S}=0\to \left(\frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}=0↔\frac{0}{{S}{U}}=0\right)$
83 80 82 syl5ibrcom ${⊢}{\phi }\to \left({R}{U}+{{P}}^{{N}-{M}}{T}{S}=0\to \frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}=0\right)$
84 83 necon3d ${⊢}{\phi }\to \left(\frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}\ne 0\to {R}{U}+{{P}}^{{N}-{M}}{T}{S}\ne 0\right)$
85 76 84 syld ${⊢}{\phi }\to \left({A}+{B}\ne 0\to {R}{U}+{{P}}^{{N}-{M}}{T}{S}\ne 0\right)$
86 85 imp ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {R}{U}+{{P}}^{{N}-{M}}{T}{S}\ne 0$
87 77 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {S}{U}\in ℕ$
88 pcdiv ${⊢}\left({P}\in ℙ\wedge \left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\in ℤ\wedge {R}{U}+{{P}}^{{N}-{M}}{T}{S}\ne 0\right)\wedge {S}{U}\in ℕ\right)\to {P}\mathrm{pCnt}\left(\frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}\right)=\left({P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\right)-\left({P}\mathrm{pCnt}{S}{U}\right)$
89 40 51 86 87 88 syl121anc ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {P}\mathrm{pCnt}\left(\frac{{R}{U}+{{P}}^{{N}-{M}}{T}{S}}{{S}{U}}\right)=\left({P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\right)-\left({P}\mathrm{pCnt}{S}{U}\right)$
90 pcmul ${⊢}\left({P}\in ℙ\wedge \left({S}\in ℤ\wedge {S}\ne 0\right)\wedge \left({U}\in ℤ\wedge {U}\ne 0\right)\right)\to {P}\mathrm{pCnt}{S}{U}=\left({P}\mathrm{pCnt}{S}\right)+\left({P}\mathrm{pCnt}{U}\right)$
91 1 48 35 41 27 90 syl122anc ${⊢}{\phi }\to {P}\mathrm{pCnt}{S}{U}=\left({P}\mathrm{pCnt}{S}\right)+\left({P}\mathrm{pCnt}{U}\right)$
92 6 simprd ${⊢}{\phi }\to ¬{P}\parallel {S}$
93 pceq0 ${⊢}\left({P}\in ℙ\wedge {S}\in ℕ\right)\to \left({P}\mathrm{pCnt}{S}=0↔¬{P}\parallel {S}\right)$
94 1 32 93 syl2anc ${⊢}{\phi }\to \left({P}\mathrm{pCnt}{S}=0↔¬{P}\parallel {S}\right)$
95 92 94 mpbird ${⊢}{\phi }\to {P}\mathrm{pCnt}{S}=0$
96 8 simprd ${⊢}{\phi }\to ¬{P}\parallel {U}$
97 pceq0 ${⊢}\left({P}\in ℙ\wedge {U}\in ℕ\right)\to \left({P}\mathrm{pCnt}{U}=0↔¬{P}\parallel {U}\right)$
98 1 25 97 syl2anc ${⊢}{\phi }\to \left({P}\mathrm{pCnt}{U}=0↔¬{P}\parallel {U}\right)$
99 96 98 mpbird ${⊢}{\phi }\to {P}\mathrm{pCnt}{U}=0$
100 95 99 oveq12d ${⊢}{\phi }\to \left({P}\mathrm{pCnt}{S}\right)+\left({P}\mathrm{pCnt}{U}\right)=0+0$
101 00id ${⊢}0+0=0$
102 100 101 syl6eq ${⊢}{\phi }\to \left({P}\mathrm{pCnt}{S}\right)+\left({P}\mathrm{pCnt}{U}\right)=0$
103 91 102 eqtrd ${⊢}{\phi }\to {P}\mathrm{pCnt}{S}{U}=0$
104 103 oveq2d ${⊢}{\phi }\to \left({P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\right)-\left({P}\mathrm{pCnt}{S}{U}\right)=\left({P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\right)-0$
105 104 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to \left({P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\right)-\left({P}\mathrm{pCnt}{S}{U}\right)=\left({P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\right)-0$
106 pczcl ${⊢}\left({P}\in ℙ\wedge \left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\in ℤ\wedge {R}{U}+{{P}}^{{N}-{M}}{T}{S}\ne 0\right)\right)\to {P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\in {ℕ}_{0}$
107 40 51 86 106 syl12anc ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\in {ℕ}_{0}$
108 107 nn0cnd ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\in ℂ$
109 108 subid1d ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to \left({P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\right)-0={P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)$
110 105 109 eqtrd ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to \left({P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)\right)-\left({P}\mathrm{pCnt}{S}{U}\right)={P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)$
111 39 89 110 3eqtrd ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)={P}\mathrm{pCnt}\left({R}{U}+{{P}}^{{N}-{M}}{T}{S}\right)$
112 111 107 eqeltrd ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\in {ℕ}_{0}$
113 nn0addge1 ${⊢}\left({M}\in ℝ\wedge {P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\in {ℕ}_{0}\right)\to {M}\le {M}+\left({P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\right)$
114 14 112 113 syl2anc ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {M}\le {M}+\left({P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\right)$
115 nnq ${⊢}{P}\in ℕ\to {P}\in ℚ$
116 16 115 syl ${⊢}{\phi }\to {P}\in ℚ$
117 qexpclz ${⊢}\left({P}\in ℚ\wedge {P}\ne 0\wedge {M}\in ℤ\right)\to {{P}}^{{M}}\in ℚ$
118 116 18 12 117 syl3anc ${⊢}{\phi }\to {{P}}^{{M}}\in ℚ$
119 118 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {{P}}^{{M}}\in ℚ$
120 17 18 12 expne0d ${⊢}{\phi }\to {{P}}^{{M}}\ne 0$
121 120 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {{P}}^{{M}}\ne 0$
122 znq ${⊢}\left({R}\in ℤ\wedge {S}\in ℕ\right)\to \frac{{R}}{{S}}\in ℚ$
123 30 32 122 syl2anc ${⊢}{\phi }\to \frac{{R}}{{S}}\in ℚ$
124 qexpclz ${⊢}\left({P}\in ℚ\wedge {P}\ne 0\wedge {N}-{M}\in ℤ\right)\to {{P}}^{{N}-{M}}\in ℚ$
125 116 18 21 124 syl3anc ${⊢}{\phi }\to {{P}}^{{N}-{M}}\in ℚ$
126 znq ${⊢}\left({T}\in ℤ\wedge {U}\in ℕ\right)\to \frac{{T}}{{U}}\in ℚ$
127 23 25 126 syl2anc ${⊢}{\phi }\to \frac{{T}}{{U}}\in ℚ$
128 qmulcl ${⊢}\left({{P}}^{{N}-{M}}\in ℚ\wedge \frac{{T}}{{U}}\in ℚ\right)\to {{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\in ℚ$
129 125 127 128 syl2anc ${⊢}{\phi }\to {{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\in ℚ$
130 qaddcl ${⊢}\left(\frac{{R}}{{S}}\in ℚ\wedge {{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\in ℚ\right)\to \left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\in ℚ$
131 123 129 130 syl2anc ${⊢}{\phi }\to \left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\in ℚ$
132 131 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to \left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\in ℚ$
133 74 57 sylbird ${⊢}{\phi }\to \left({A}+{B}\ne 0\to \left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\ne 0\right)$
134 133 imp ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to \left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\ne 0$
135 pcqmul ${⊢}\left({P}\in ℙ\wedge \left({{P}}^{{M}}\in ℚ\wedge {{P}}^{{M}}\ne 0\right)\wedge \left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\in ℚ\wedge \left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\ne 0\right)\right)\to {P}\mathrm{pCnt}{{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)=\left({P}\mathrm{pCnt}{{P}}^{{M}}\right)+\left({P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\right)$
136 40 119 121 132 134 135 syl122anc ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {P}\mathrm{pCnt}{{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)=\left({P}\mathrm{pCnt}{{P}}^{{M}}\right)+\left({P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\right)$
137 73 oveq2d ${⊢}{\phi }\to {P}\mathrm{pCnt}{{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)={P}\mathrm{pCnt}\left({A}+{B}\right)$
138 137 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {P}\mathrm{pCnt}{{P}}^{{M}}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)={P}\mathrm{pCnt}\left({A}+{B}\right)$
139 pcid ${⊢}\left({P}\in ℙ\wedge {M}\in ℤ\right)\to {P}\mathrm{pCnt}{{P}}^{{M}}={M}$
140 1 12 139 syl2anc ${⊢}{\phi }\to {P}\mathrm{pCnt}{{P}}^{{M}}={M}$
141 140 oveq1d ${⊢}{\phi }\to \left({P}\mathrm{pCnt}{{P}}^{{M}}\right)+\left({P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\right)={M}+\left({P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\right)$
142 141 adantr ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to \left({P}\mathrm{pCnt}{{P}}^{{M}}\right)+\left({P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\right)={M}+\left({P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\right)$
143 136 138 142 3eqtr3d ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {P}\mathrm{pCnt}\left({A}+{B}\right)={M}+\left({P}\mathrm{pCnt}\left(\left(\frac{{R}}{{S}}\right)+{{P}}^{{N}-{M}}\left(\frac{{T}}{{U}}\right)\right)\right)$
144 114 143 breqtrrd ${⊢}\left({\phi }\wedge {A}+{B}\ne 0\right)\to {M}\le {P}\mathrm{pCnt}\left({A}+{B}\right)$
145 13 rexrd ${⊢}{\phi }\to {M}\in {ℝ}^{*}$
146 pnfge ${⊢}{M}\in {ℝ}^{*}\to {M}\le \mathrm{+\infty }$
147 145 146 syl ${⊢}{\phi }\to {M}\le \mathrm{+\infty }$
148 pc0 ${⊢}{P}\in ℙ\to {P}\mathrm{pCnt}0=\mathrm{+\infty }$
149 1 148 syl ${⊢}{\phi }\to {P}\mathrm{pCnt}0=\mathrm{+\infty }$
150 147 149 breqtrrd ${⊢}{\phi }\to {M}\le {P}\mathrm{pCnt}0$
151 10 144 150 pm2.61ne ${⊢}{\phi }\to {M}\le {P}\mathrm{pCnt}\left({A}+{B}\right)$