Metamath Proof Explorer

Theorem pcpremul

Description: Multiplicative property of the prime count pre-function. Note that the primality of P is essential for this property; ( 4 pCnt 2 ) = 0 but ( 4 pCnt ( 2 x. 2 ) ) = 1 =/= 2 x. ( 4 pCnt 2 ) = 0 . Since this is needed to show uniqueness for the real prime count function (over QQ ), we don't bother to define it off the primes. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Hypotheses pcpremul.1 ⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑀 } , ℝ , < )
pcpremul.2 ⊢ 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < )
pcpremul.3 ⊢ 𝑈 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } , ℝ , < )
Assertion pcpremul ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 + 𝑇 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 pcpremul.1 ⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑀 } , ℝ , < )
2 pcpremul.2 ⊢ 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } , ℝ , < )
3 pcpremul.3 ⊢ 𝑈 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } , ℝ , < )
4 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
5 4 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
6 zmulcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
7 6 ad2ant2r ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
8 7 3adant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
9 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
10 9 anim1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) )
11 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
12 11 anim1i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
13 mulne0 ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) ≠ 0 )
14 10 12 13 syl2an ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) ≠ 0 )
15 14 3adant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) ≠ 0 )
16 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) }
17 16 pclem ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑀 · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ≠ 0 ) ) → ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } ⊆ ℤ ∧ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } 𝑦 ≤ 𝑥 ) )
18 5 8 15 17 syl12anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } ⊆ ℤ ∧ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } 𝑦 ≤ 𝑥 ) )
19 18 simp1d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } ⊆ ℤ )
20 18 simp3d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } 𝑦 ≤ 𝑥 )
21 oveq2 ⊢ ( 𝑥 = ( 𝑆 + 𝑇 ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) )
22 21 breq1d ⊢ ( 𝑥 = ( 𝑆 + 𝑇 ) → ( ( 𝑃 ↑ 𝑥 ) ∥ ( 𝑀 · 𝑁 ) ↔ ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
23 simp2l ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑀 ∈ ℤ )
24 simp2r ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑀 ≠ 0 )
25 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑀 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑀 }
26 25 1 pcprecl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑀 ) )
27 5 23 24 26 syl12anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑀 ) )
28 27 simpld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑆 ∈ ℕ0 )
29 simp3l ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑁 ∈ ℤ )
30 simp3r ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑁 ≠ 0 )
31 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
32 31 2 pcprecl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑇 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑇 ) ∥ 𝑁 ) )
33 5 29 30 32 syl12anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑇 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑇 ) ∥ 𝑁 ) )
34 33 simpld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑇 ∈ ℕ0 )
35 28 34 nn0addcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 + 𝑇 ) ∈ ℕ0 )
36 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
37 36 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑃 ∈ ℕ )
38 37 35 nnexpcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ∈ ℕ )
39 38 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ∈ ℤ )
40 37 34 nnexpcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑇 ) ∈ ℕ )
41 40 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑇 ) ∈ ℤ )
42 23 41 zmulcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · ( 𝑃 ↑ 𝑇 ) ) ∈ ℤ )
43 37 nncnd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑃 ∈ ℂ )
44 43 34 28 expaddd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) = ( ( 𝑃 ↑ 𝑆 ) · ( 𝑃 ↑ 𝑇 ) ) )
45 27 simprd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑆 ) ∥ 𝑀 )
46 37 28 nnexpcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑆 ) ∈ ℕ )
47 46 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑆 ) ∈ ℤ )
48 dvdsmulc ⊢ ( ( ( 𝑃 ↑ 𝑆 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑃 ↑ 𝑇 ) ∈ ℤ ) → ( ( 𝑃 ↑ 𝑆 ) ∥ 𝑀 → ( ( 𝑃 ↑ 𝑆 ) · ( 𝑃 ↑ 𝑇 ) ) ∥ ( 𝑀 · ( 𝑃 ↑ 𝑇 ) ) ) )
49 47 23 41 48 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ 𝑆 ) ∥ 𝑀 → ( ( 𝑃 ↑ 𝑆 ) · ( 𝑃 ↑ 𝑇 ) ) ∥ ( 𝑀 · ( 𝑃 ↑ 𝑇 ) ) ) )
50 45 49 mpd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ 𝑆 ) · ( 𝑃 ↑ 𝑇 ) ) ∥ ( 𝑀 · ( 𝑃 ↑ 𝑇 ) ) )
51 44 50 eqbrtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ∥ ( 𝑀 · ( 𝑃 ↑ 𝑇 ) ) )
52 33 simprd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑇 ) ∥ 𝑁 )
53 dvdscmul ⊢ ( ( ( 𝑃 ↑ 𝑇 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑃 ↑ 𝑇 ) ∥ 𝑁 → ( 𝑀 · ( 𝑃 ↑ 𝑇 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
54 41 29 23 53 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ 𝑇 ) ∥ 𝑁 → ( 𝑀 · ( 𝑃 ↑ 𝑇 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
55 52 54 mpd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · ( 𝑃 ↑ 𝑇 ) ) ∥ ( 𝑀 · 𝑁 ) )
56 39 42 8 51 55 dvdstrd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ∥ ( 𝑀 · 𝑁 ) )
57 22 35 56 elrabd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 + 𝑇 ) ∈ { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ ( 𝑀 · 𝑁 ) } )
58 oveq2 ⊢ ( 𝑥 = 𝑛 → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) )
59 58 breq1d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑃 ↑ 𝑥 ) ∥ ( 𝑀 · 𝑁 ) ↔ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) ) )
60 59 cbvrabv ⊢ { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ ( 𝑀 · 𝑁 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) }
61 57 60 eleqtrdi ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 + 𝑇 ) ∈ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } )
62 suprzub ⊢ ( ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } 𝑦 ≤ 𝑥 ∧ ( 𝑆 + 𝑇 ) ∈ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } ) → ( 𝑆 + 𝑇 ) ≤ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } , ℝ , < ) )
63 19 20 61 62 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 + 𝑇 ) ≤ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑀 · 𝑁 ) } , ℝ , < ) )
64 63 3 breqtrrdi ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 + 𝑇 ) ≤ 𝑈 )
65 25 1 pcprendvds2 ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) )
66 5 23 24 65 syl12anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) )
67 31 2 pcprendvds2 ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) )
68 5 29 30 67 syl12anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) )
69 ioran ⊢ ( ¬ ( 𝑃 ∥ ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) ∨ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ↔ ( ¬ 𝑃 ∥ ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) ∧ ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) )
70 66 68 69 sylanbrc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ ( 𝑃 ∥ ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) ∨ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) )
71 simp1 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑃 ∈ ℙ )
72 46 nnne0d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑆 ) ≠ 0 )
73 dvdsval2 ⊢ ( ( ( 𝑃 ↑ 𝑆 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑆 ) ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑃 ↑ 𝑆 ) ∥ 𝑀 ↔ ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) ∈ ℤ ) )
74 47 72 23 73 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ 𝑆 ) ∥ 𝑀 ↔ ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) ∈ ℤ ) )
75 45 74 mpbid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) ∈ ℤ )
76 40 nnne0d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑇 ) ≠ 0 )
77 dvdsval2 ⊢ ( ( ( 𝑃 ↑ 𝑇 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑇 ) ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ↑ 𝑇 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ∈ ℤ ) )
78 41 76 29 77 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ 𝑇 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ∈ ℤ ) )
79 52 78 mpbid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ∈ ℤ )
80 euclemma ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) ∈ ℤ ∧ ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ↔ ( 𝑃 ∥ ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) ∨ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) )
81 71 75 79 80 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ∥ ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ↔ ( 𝑃 ∥ ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) ∨ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) )
82 70 81 mtbird ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ 𝑃 ∥ ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) )
83 16 3 pcprecl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑀 · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ≠ 0 ) ) → ( 𝑈 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑈 ) ∥ ( 𝑀 · 𝑁 ) ) )
84 5 8 15 83 syl12anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑈 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑈 ) ∥ ( 𝑀 · 𝑁 ) ) )
85 84 simpld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑈 ∈ ℕ0 )
86 nn0ltp1le ⊢ ( ( ( 𝑆 + 𝑇 ) ∈ ℕ0 ∧ 𝑈 ∈ ℕ0 ) → ( ( 𝑆 + 𝑇 ) < 𝑈 ↔ ( ( 𝑆 + 𝑇 ) + 1 ) ≤ 𝑈 ) )
87 35 85 86 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑆 + 𝑇 ) < 𝑈 ↔ ( ( 𝑆 + 𝑇 ) + 1 ) ≤ 𝑈 ) )
88 37 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑃 ∈ ℤ )
89 peano2nn0 ⊢ ( ( 𝑆 + 𝑇 ) ∈ ℕ0 → ( ( 𝑆 + 𝑇 ) + 1 ) ∈ ℕ0 )
90 35 89 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑆 + 𝑇 ) + 1 ) ∈ ℕ0 )
91 dvdsexp ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝑆 + 𝑇 ) + 1 ) ∈ ℕ0 ∧ 𝑈 ∈ ( ℤ≥ ‘ ( ( 𝑆 + 𝑇 ) + 1 ) ) ) → ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝑈 ) )
92 91 3expia ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝑆 + 𝑇 ) + 1 ) ∈ ℕ0 ) → ( 𝑈 ∈ ( ℤ≥ ‘ ( ( 𝑆 + 𝑇 ) + 1 ) ) → ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝑈 ) ) )
93 88 90 92 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑈 ∈ ( ℤ≥ ‘ ( ( 𝑆 + 𝑇 ) + 1 ) ) → ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝑈 ) ) )
94 84 simprd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑈 ) ∥ ( 𝑀 · 𝑁 ) )
95 37 90 nnexpcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∈ ℕ )
96 95 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∈ ℤ )
97 37 85 nnexpcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑈 ) ∈ ℕ )
98 97 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑈 ) ∈ ℤ )
99 dvdstr ⊢ ( ( ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑈 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝑈 ) ∧ ( 𝑃 ↑ 𝑈 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
100 96 98 8 99 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝑈 ) ∧ ( 𝑃 ↑ 𝑈 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
101 94 100 mpan2d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑃 ↑ 𝑈 ) → ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
102 93 101 syld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑈 ∈ ( ℤ≥ ‘ ( ( 𝑆 + 𝑇 ) + 1 ) ) → ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
103 90 nn0zd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑆 + 𝑇 ) + 1 ) ∈ ℤ )
104 85 nn0zd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑈 ∈ ℤ )
105 eluz ⊢ ( ( ( ( 𝑆 + 𝑇 ) + 1 ) ∈ ℤ ∧ 𝑈 ∈ ℤ ) → ( 𝑈 ∈ ( ℤ≥ ‘ ( ( 𝑆 + 𝑇 ) + 1 ) ) ↔ ( ( 𝑆 + 𝑇 ) + 1 ) ≤ 𝑈 ) )
106 103 104 105 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑈 ∈ ( ℤ≥ ‘ ( ( 𝑆 + 𝑇 ) + 1 ) ) ↔ ( ( 𝑆 + 𝑇 ) + 1 ) ≤ 𝑈 ) )
107 43 35 expp1d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) = ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · 𝑃 ) )
108 23 zcnd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑀 ∈ ℂ )
109 29 zcnd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑁 ∈ ℂ )
110 108 109 mulcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) ∈ ℂ )
111 38 nncnd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ∈ ℂ )
112 38 nnne0d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ≠ 0 )
113 110 111 112 divcan2d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · ( ( 𝑀 · 𝑁 ) / ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ) ) = ( 𝑀 · 𝑁 ) )
114 44 oveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑀 · 𝑁 ) / ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ) = ( ( 𝑀 · 𝑁 ) / ( ( 𝑃 ↑ 𝑆 ) · ( 𝑃 ↑ 𝑇 ) ) ) )
115 46 nncnd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑆 ) ∈ ℂ )
116 40 nncnd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 𝑇 ) ∈ ℂ )
117 108 115 109 116 72 76 divmuldivd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) = ( ( 𝑀 · 𝑁 ) / ( ( 𝑃 ↑ 𝑆 ) · ( 𝑃 ↑ 𝑇 ) ) ) )
118 114 117 eqtr4d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑀 · 𝑁 ) / ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ) = ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) )
119 118 oveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · ( ( 𝑀 · 𝑁 ) / ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ) ) = ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) )
120 113 119 eqtr3d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) = ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) )
121 107 120 breq12d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑀 · 𝑁 ) ↔ ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · 𝑃 ) ∥ ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) ) )
122 75 79 zmulcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ∈ ℤ )
123 dvdscmulr ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ∈ ℤ ∧ ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) ≠ 0 ) ) → ( ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · 𝑃 ) ∥ ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) ↔ 𝑃 ∥ ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) )
124 88 122 39 112 123 syl112anc ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · 𝑃 ) ∥ ( ( 𝑃 ↑ ( 𝑆 + 𝑇 ) ) · ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) ↔ 𝑃 ∥ ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) )
125 121 124 bitrd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑃 ↑ ( ( 𝑆 + 𝑇 ) + 1 ) ) ∥ ( 𝑀 · 𝑁 ) ↔ 𝑃 ∥ ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) )
126 102 106 125 3imtr3d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( ( 𝑆 + 𝑇 ) + 1 ) ≤ 𝑈 → 𝑃 ∥ ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) )
127 87 126 sylbid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑆 + 𝑇 ) < 𝑈 → 𝑃 ∥ ( ( 𝑀 / ( 𝑃 ↑ 𝑆 ) ) · ( 𝑁 / ( 𝑃 ↑ 𝑇 ) ) ) ) )
128 82 127 mtod ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ¬ ( 𝑆 + 𝑇 ) < 𝑈 )
129 35 nn0red ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 + 𝑇 ) ∈ ℝ )
130 85 nn0red ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑈 ∈ ℝ )
131 129 130 eqleltd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑆 + 𝑇 ) = 𝑈 ↔ ( ( 𝑆 + 𝑇 ) ≤ 𝑈 ∧ ¬ ( 𝑆 + 𝑇 ) < 𝑈 ) ) )
132 64 128 131 mpbir2and ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 + 𝑇 ) = 𝑈 )