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

Metamath Proof Explorer

Theorem pcqmul

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

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

Proof

Step Hyp Ref Expression
1 simp2l ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℚ )
2 elq ⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
3 1 2 sylib ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
4 simp3l ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℚ )
5 elq ⊢ ( 𝐵 ∈ ℚ ↔ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) )
6 4 5 sylib ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) )
7 reeanv ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑧 ∈ ℤ ( ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) ↔ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) )
8 reeanv ⊢ ( ∃ 𝑦 ∈ ℕ ∃ 𝑤 ∈ ℕ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) )
9 simp2r ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝐴 ≠ 0 )
10 simp3r ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
11 9 10 jca ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) )
12 11 ad2antrr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) )
13 simp1 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝑃 ∈ ℙ )
14 simprl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → 𝑦 ∈ ℕ )
15 14 nncnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → 𝑦 ∈ ℂ )
16 14 nnne0d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → 𝑦 ≠ 0 )
17 15 16 div0d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( 0 / 𝑦 ) = 0 )
18 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 / 𝑦 ) = ( 0 / 𝑦 ) )
19 18 eqeq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 / 𝑦 ) = 0 ↔ ( 0 / 𝑦 ) = 0 ) )
20 17 19 syl5ibrcom ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( 𝑥 = 0 → ( 𝑥 / 𝑦 ) = 0 ) )
21 20 necon3d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 / 𝑦 ) ≠ 0 → 𝑥 ≠ 0 ) )
22 simprr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → 𝑤 ∈ ℕ )
23 22 nncnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → 𝑤 ∈ ℂ )
24 22 nnne0d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → 𝑤 ≠ 0 )
25 23 24 div0d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( 0 / 𝑤 ) = 0 )
26 oveq1 ⊢ ( 𝑧 = 0 → ( 𝑧 / 𝑤 ) = ( 0 / 𝑤 ) )
27 26 eqeq1d ⊢ ( 𝑧 = 0 → ( ( 𝑧 / 𝑤 ) = 0 ↔ ( 0 / 𝑤 ) = 0 ) )
28 25 27 syl5ibrcom ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( 𝑧 = 0 → ( 𝑧 / 𝑤 ) = 0 ) )
29 28 necon3d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑧 / 𝑤 ) ≠ 0 → 𝑧 ≠ 0 ) )
30 simpll ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑃 ∈ ℙ )
31 simplrl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑥 ∈ ℤ )
32 simplrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑧 ∈ ℤ )
33 31 32 zmulcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑥 · 𝑧 ) ∈ ℤ )
34 31 zcnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑥 ∈ ℂ )
35 32 zcnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑧 ∈ ℂ )
36 simprrl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑥 ≠ 0 )
37 simprrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑧 ≠ 0 )
38 34 35 36 37 mulne0d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑥 · 𝑧 ) ≠ 0 )
39 14 adantrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑦 ∈ ℕ )
40 22 adantrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑤 ∈ ℕ )
41 39 40 nnmulcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑦 · 𝑤 ) ∈ ℕ )
42 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝑥 · 𝑧 ) ∈ ℤ ∧ ( 𝑥 · 𝑧 ) ≠ 0 ) ∧ ( 𝑦 · 𝑤 ) ∈ ℕ ) → ( 𝑃 pCnt ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) ) = ( ( 𝑃 pCnt ( 𝑥 · 𝑧 ) ) − ( 𝑃 pCnt ( 𝑦 · 𝑤 ) ) ) )
43 30 33 38 41 42 syl121anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) ) = ( ( 𝑃 pCnt ( 𝑥 · 𝑧 ) ) − ( 𝑃 pCnt ( 𝑦 · 𝑤 ) ) ) )
44 pcmul ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝑥 · 𝑧 ) ) = ( ( 𝑃 pCnt 𝑥 ) + ( 𝑃 pCnt 𝑧 ) ) )
45 30 31 36 32 37 44 syl122anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt ( 𝑥 · 𝑧 ) ) = ( ( 𝑃 pCnt 𝑥 ) + ( 𝑃 pCnt 𝑧 ) ) )
46 39 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑦 ∈ ℤ )
47 16 adantrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑦 ≠ 0 )
48 40 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑤 ∈ ℤ )
49 24 adantrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑤 ≠ 0 )
50 pcmul ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑤 ∈ ℤ ∧ 𝑤 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝑦 · 𝑤 ) ) = ( ( 𝑃 pCnt 𝑦 ) + ( 𝑃 pCnt 𝑤 ) ) )
51 30 46 47 48 49 50 syl122anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt ( 𝑦 · 𝑤 ) ) = ( ( 𝑃 pCnt 𝑦 ) + ( 𝑃 pCnt 𝑤 ) ) )
52 45 51 oveq12d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( ( 𝑃 pCnt ( 𝑥 · 𝑧 ) ) − ( 𝑃 pCnt ( 𝑦 · 𝑤 ) ) ) = ( ( ( 𝑃 pCnt 𝑥 ) + ( 𝑃 pCnt 𝑧 ) ) − ( ( 𝑃 pCnt 𝑦 ) + ( 𝑃 pCnt 𝑤 ) ) ) )
53 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℕ0 )
54 30 31 36 53 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℕ0 )
55 54 nn0cnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℂ )
56 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℕ0 )
57 30 32 37 56 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℕ0 )
58 57 nn0cnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℂ )
59 30 39 pccld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℕ0 )
60 59 nn0cnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℂ )
61 30 40 pccld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑤 ) ∈ ℕ0 )
62 61 nn0cnd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑤 ) ∈ ℂ )
63 55 58 60 62 addsub4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( ( ( 𝑃 pCnt 𝑥 ) + ( 𝑃 pCnt 𝑧 ) ) − ( ( 𝑃 pCnt 𝑦 ) + ( 𝑃 pCnt 𝑤 ) ) ) = ( ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) + ( ( 𝑃 pCnt 𝑧 ) − ( 𝑃 pCnt 𝑤 ) ) ) )
64 43 52 63 3eqtrd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) ) = ( ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) + ( ( 𝑃 pCnt 𝑧 ) − ( 𝑃 pCnt 𝑤 ) ) ) )
65 15 adantrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑦 ∈ ℂ )
66 23 adantrr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → 𝑤 ∈ ℂ )
67 34 65 35 66 47 49 divmuldivd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) = ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) )
68 67 oveq2d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) ) = ( 𝑃 pCnt ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) ) )
69 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) = ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
70 30 31 36 39 69 syl121anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) = ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) )
71 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ) ∧ 𝑤 ∈ ℕ ) → ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) = ( ( 𝑃 pCnt 𝑧 ) − ( 𝑃 pCnt 𝑤 ) ) )
72 30 32 37 40 71 syl121anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) = ( ( 𝑃 pCnt 𝑧 ) − ( 𝑃 pCnt 𝑤 ) ) )
73 70 72 oveq12d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) + ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) ) = ( ( ( 𝑃 pCnt 𝑥 ) − ( 𝑃 pCnt 𝑦 ) ) + ( ( 𝑃 pCnt 𝑧 ) − ( 𝑃 pCnt 𝑤 ) ) ) )
74 64 68 73 3eqtr4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) ) = ( ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) + ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) ) )
75 74 expr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) → ( 𝑃 pCnt ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) ) = ( ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) + ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) ) ) )
76 21 29 75 syl2and ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( ( 𝑥 / 𝑦 ) ≠ 0 ∧ ( 𝑧 / 𝑤 ) ≠ 0 ) → ( 𝑃 pCnt ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) ) = ( ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) + ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) ) ) )
77 neeq1 ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ≠ 0 ↔ ( 𝑥 / 𝑦 ) ≠ 0 ) )
78 neeq1 ⊢ ( 𝐵 = ( 𝑧 / 𝑤 ) → ( 𝐵 ≠ 0 ↔ ( 𝑧 / 𝑤 ) ≠ 0 ) )
79 77 78 bi2anan9 ⊢ ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ↔ ( ( 𝑥 / 𝑦 ) ≠ 0 ∧ ( 𝑧 / 𝑤 ) ≠ 0 ) ) )
80 oveq12 ⊢ ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝐴 · 𝐵 ) = ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) )
81 80 oveq2d ⊢ ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( 𝑃 pCnt ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) ) )
82 oveq2 ⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝑃 pCnt 𝐴 ) = ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) )
83 oveq2 ⊢ ( 𝐵 = ( 𝑧 / 𝑤 ) → ( 𝑃 pCnt 𝐵 ) = ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) )
84 82 83 oveqan12d ⊢ ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) = ( ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) + ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) ) )
85 81 84 eqeq12d ⊢ ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) ↔ ( 𝑃 pCnt ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) ) = ( ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) + ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) ) ) )
86 79 85 imbi12d ⊢ ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( ( ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) ) ↔ ( ( ( 𝑥 / 𝑦 ) ≠ 0 ∧ ( 𝑧 / 𝑤 ) ≠ 0 ) → ( 𝑃 pCnt ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) ) = ( ( 𝑃 pCnt ( 𝑥 / 𝑦 ) ) + ( 𝑃 pCnt ( 𝑧 / 𝑤 ) ) ) ) ) )
87 76 86 syl5ibrcom ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) ) ) )
88 13 87 sylanl1 ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) ) ) )
89 12 88 mpid ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) ) )
90 89 rexlimdvva ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ∃ 𝑦 ∈ ℕ ∃ 𝑤 ∈ ℕ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) ) )
91 8 90 biimtrrid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) ) )
92 91 rexlimdvva ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑧 ∈ ℤ ( ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) ) )
93 7 92 biimtrrid ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) ) )
94 3 6 93 mp2and ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) + ( 𝑃 pCnt 𝐵 ) ) )