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 ( 𝜑𝑃 ∈ ℙ )
pcaddlem.2 ( 𝜑𝐴 = ( ( 𝑃𝑀 ) · ( 𝑅 / 𝑆 ) ) )
pcaddlem.3 ( 𝜑𝐵 = ( ( 𝑃𝑁 ) · ( 𝑇 / 𝑈 ) ) )
pcaddlem.4 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
pcaddlem.5 ( 𝜑 → ( 𝑅 ∈ ℤ ∧ ¬ 𝑃𝑅 ) )
pcaddlem.6 ( 𝜑 → ( 𝑆 ∈ ℕ ∧ ¬ 𝑃𝑆 ) )
pcaddlem.7 ( 𝜑 → ( 𝑇 ∈ ℤ ∧ ¬ 𝑃𝑇 ) )
pcaddlem.8 ( 𝜑 → ( 𝑈 ∈ ℕ ∧ ¬ 𝑃𝑈 ) )
Assertion pcaddlem ( 𝜑𝑀 ≤ ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) )

Proof

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