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 ( 𝐴 + 𝐵 ) ) )