pcqdiv

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

		Ref	Expression
	Assertion	pcqdiv	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P pCnt (\frac{A}{B}) = (P pCnt A) - (P pCnt B)$

Proof

Step	Hyp	Ref	Expression
1		simp2l	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to A \in ℚ$
2		qcn	$⊢ A \in ℚ \to A \in ℂ$
3	1 2	syl	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to A \in ℂ$
4		simp3l	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to B \in ℚ$
5		qcn	$⊢ B \in ℚ \to B \in ℂ$
6	4 5	syl	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to B \in ℂ$
7		simp3r	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to B \neq 0$
8	3 6 7	divcan1d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to (\frac{A}{B}) B = A$
9	8	oveq2d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P pCnt (\frac{A}{B}) B = P pCnt A$
10		simp1	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P \in ℙ$
11		qdivcl	$⊢ (A \in ℚ \land B \in ℚ \land B \neq 0) \to \frac{A}{B} \in ℚ$
12	1 4 7 11	syl3anc	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to \frac{A}{B} \in ℚ$
13		simp2r	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to A \neq 0$
14	3 6 13 7	divne0d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to \frac{A}{B} \neq 0$
15		pcqmul	$⊢ (P \in ℙ \land (\frac{A}{B} \in ℚ \land \frac{A}{B} \neq 0) \land (B \in ℚ \land B \neq 0)) \to P pCnt (\frac{A}{B}) B = (P pCnt (\frac{A}{B})) + (P pCnt B)$
16	10 12 14 4 7 15	syl122anc	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P pCnt (\frac{A}{B}) B = (P pCnt (\frac{A}{B})) + (P pCnt B)$
17	9 16	eqtr3d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P pCnt A = (P pCnt (\frac{A}{B})) + (P pCnt B)$
18	17	oveq1d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to (P pCnt A) - (P pCnt B) = (P pCnt (\frac{A}{B})) + (P pCnt B) - (P pCnt B)$
19		pcqcl	$⊢ (P \in ℙ \land (\frac{A}{B} \in ℚ \land \frac{A}{B} \neq 0)) \to P pCnt (\frac{A}{B}) \in ℤ$
20	10 12 14 19	syl12anc	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P pCnt (\frac{A}{B}) \in ℤ$
21	20	zcnd	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P pCnt (\frac{A}{B}) \in ℂ$
22		pcqcl	$⊢ (P \in ℙ \land (B \in ℚ \land B \neq 0)) \to P pCnt B \in ℤ$
23	22	3adant2	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P pCnt B \in ℤ$
24	23	zcnd	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P pCnt B \in ℂ$
25	21 24	pncand	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to (P pCnt (\frac{A}{B})) + (P pCnt B) - (P pCnt B) = P pCnt (\frac{A}{B})$
26	18 25	eqtr2d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P pCnt (\frac{A}{B}) = (P pCnt A) - (P pCnt B)$

Metamath Proof Explorer

Theorem pcqdiv

Proof