Metamath Proof Explorer

Theorem pcqdiv

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

Ref Expression
Assertion pcqdiv ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntAB=PpCntA−PpCntB

Proof

Step Hyp Ref Expression
1 simp2l ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→A∈ℚ
2 qcn ⊢A∈ℚ→A∈ℂ
3 1 2 syl ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→A∈ℂ
4 simp3l ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→B∈ℚ
5 qcn ⊢B∈ℚ→B∈ℂ
6 4 5 syl ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→B∈ℂ
7 simp3r ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→B≠0
8 3 6 7 divcan1d ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→AB⁢B=A
9 8 oveq2d ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntAB⁢B=PpCntA
10 simp1 ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→P∈ℙ
11 qdivcl ⊢A∈ℚ∧B∈ℚ∧B≠0→AB∈ℚ
12 1 4 7 11 syl3anc ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→AB∈ℚ
13 simp2r ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→A≠0
14 3 6 13 7 divne0d ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→AB≠0
15 pcqmul ⊢P∈ℙ∧AB∈ℚ∧AB≠0∧B∈ℚ∧B≠0→PpCntAB⁢B=PpCntAB+PpCntB
16 10 12 14 4 7 15 syl122anc ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntAB⁢B=PpCntAB+PpCntB
17 9 16 eqtr3d ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntA=PpCntAB+PpCntB
18 17 oveq1d ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntA−PpCntB=PpCntAB+PpCntB-PpCntB
19 pcqcl ⊢P∈ℙ∧AB∈ℚ∧AB≠0→PpCntAB∈ℤ
20 10 12 14 19 syl12anc ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntAB∈ℤ
21 20 zcnd ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntAB∈ℂ
22 pcqcl ⊢P∈ℙ∧B∈ℚ∧B≠0→PpCntB∈ℤ
23 22 3adant2 ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntB∈ℤ
24 23 zcnd ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntB∈ℂ
25 21 24 pncand ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntAB+PpCntB-PpCntB=PpCntAB
26 18 25 eqtr2d ⊢P∈ℙ∧A∈ℚ∧A≠0∧B∈ℚ∧B≠0→PpCntAB=PpCntA−PpCntB