Metamath Proof Explorer

Theorem pcaddlem

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 
|- ( ph -> P e. Prime )
pcaddlem.2 
|- ( ph -> A = ( ( P ^ M ) x. ( R / S ) ) )
pcaddlem.3 
|- ( ph -> B = ( ( P ^ N ) x. ( T / U ) ) )
pcaddlem.4 
|- ( ph -> N e. ( ZZ>= ` M ) )
pcaddlem.5 
|- ( ph -> ( R e. ZZ /\ -. P || R ) )
pcaddlem.6 
|- ( ph -> ( S e. NN /\ -. P || S ) )
pcaddlem.7 
|- ( ph -> ( T e. ZZ /\ -. P || T ) )
pcaddlem.8 
|- ( ph -> ( U e. NN /\ -. P || U ) )
Assertion pcaddlem 
|- ( ph -> M <_ ( P pCnt ( A + B ) ) )

Proof

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