This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pcmul

Description: Multiplication property of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pcmul ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < )
2 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < )
3 eqid ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝐴 · 𝐵 ) } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝐴 · 𝐵 ) } , ℝ , < )
4 1 2 3 pcpremul ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) + sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝐴 · 𝐵 ) } , ℝ , < ) )
5 1 pczpre ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) )
6 5 3adant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) )
7 2 pczpre ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐵 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) )
8 7 3adant2 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐵 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) )
9 6 8 oveq12d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐴 } , ℝ , < ) + sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝐵 } , ℝ , < ) ) )
10 zmulcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 · 𝐵 ) ∈ ℤ )
11 10 ad2ant2r ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · 𝐵 ) ∈ ℤ )
12 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
13 12 anim1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
14 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
15 14 anim1i ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
16 mulne0 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · 𝐵 ) ≠ 0 )
17 13 15 16 syl2an ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · 𝐵 ) ≠ 0 )
18 11 17 jca ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) ∈ ℤ ∧ ( 𝐴 · 𝐵 ) ≠ 0 ) )
19 3 pczpre ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐴 · 𝐵 ) ∈ ℤ ∧ ( 𝐴 · 𝐵 ) ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝐴 · 𝐵 ) } , ℝ , < ) )
20 18 19 sylan2 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝐴 · 𝐵 ) } , ℝ , < ) )
21 20 3impb ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝐴 · 𝐵 ) } , ℝ , < ) )
22 4 9 21 3eqtr4rd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) )