Metamath Proof Explorer

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 𝐵 ) ) )