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 ) ) → ( 𝑆 + 𝑇 ) = 𝑈 )