Theorem pcqdiv

Description: Division property of the prime power function. (Contributed by Mario Carneiro, 10-Aug-2015)

	Ref	Expression
Assertion	pcqdiv	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp2l	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℚ )
2		qcn	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℂ )
3	1 2	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℂ )
4		simp3l	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℚ )
5		qcn	⊢ ( 𝐵 ∈ ℚ → 𝐵 ∈ ℂ )
6	4 5	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℂ )
7		simp3r	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
8	3 6 7	divcan1d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) · 𝐵 ) = 𝐴 )
9	8	oveq2d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( 𝑃 pCnt 𝐴 ) )
10		simp1	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝑃 ∈ ℙ )
11		qdivcl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℚ )
12	1 4 7 11	syl3anc	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ ℚ )
13		simp2r	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → 𝐴 ≠ 0 )
14	3 6 13 7	divne0d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ≠ 0 )
15		pcqmul	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐴 / 𝐵 ) ∈ ℚ ∧ ( 𝐴 / 𝐵 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) + ( 𝑃 pCnt 𝐵 ) ) )
16	10 12 14 4 7 15	syl122anc	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) + ( 𝑃 pCnt 𝐵 ) ) )
17	9 16	eqtr3d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) = ( ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) + ( 𝑃 pCnt 𝐵 ) ) )
18	17	oveq1d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) = ( ( ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) + ( 𝑃 pCnt 𝐵 ) ) − ( 𝑃 pCnt 𝐵 ) ) )
19		pcqcl	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐴 / 𝐵 ) ∈ ℚ ∧ ( 𝐴 / 𝐵 ) ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) ∈ ℤ )
20	10 12 14 19	syl12anc	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) ∈ ℤ )
21	20	zcnd	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) ∈ ℂ )
22		pcqcl	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐵 ) ∈ ℤ )
23	22	3adant2	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐵 ) ∈ ℤ )
24	23	zcnd	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐵 ) ∈ ℂ )
25	21 24	pncand	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) + ( 𝑃 pCnt 𝐵 ) ) − ( 𝑃 pCnt 𝐵 ) ) = ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) )
26	18 25	eqtr2d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 / 𝐵 ) ) = ( ( 𝑃 pCnt 𝐴 ) − ( 𝑃 pCnt 𝐵 ) ) )