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 𝑥 ) ∈ ℕ₀ )
54	30 31 36 53	syl12anc	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℕ₀ )
55	54	nn0cnd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℂ )
56		pczcl	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℕ₀ )
57	30 32 37 56	syl12anc	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℕ₀ )
58	57	nn0cnd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℂ )
59	30 39	pccld	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℕ₀ )
60	59	nn0cnd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℂ )
61	30 40	pccld	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑧 ≠ 0 ) ) ) → ( 𝑃 pCnt 𝑤 ) ∈ ℕ₀ )
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 𝐵 ) ) )

Metamath Proof Explorer

Theorem pcqmul

Proof