pcmul

Description: Multiplication property of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014)

		Ref	Expression
	Assertion	pcmul	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to P pCnt A B = (P pCnt A) + (P pCnt B)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <)$
2		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
3		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ A B\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A B\} ℝ <)$
4	1 2 3	pcpremul	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) + sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A B\} ℝ <)$
5	1	pczpre	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0)) \to P pCnt A = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <)$
6	5	3adant3	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to P pCnt A = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <)$
7	2	pczpre	$⊢ (P \in ℙ \land (B \in ℤ \land B \neq 0)) \to P pCnt B = sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
8	7	3adant2	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to P pCnt B = sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
9	6 8	oveq12d	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to (P pCnt A) + (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) + sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
10		zmulcl	$⊢ (A \in ℤ \land B \in ℤ) \to A B \in ℤ$
11	10	ad2ant2r	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to A B \in ℤ$
12		zcn	$⊢ A \in ℤ \to A \in ℂ$
13	12	anim1i	$⊢ (A \in ℤ \land A \neq 0) \to (A \in ℂ \land A \neq 0)$
14		zcn	$⊢ B \in ℤ \to B \in ℂ$
15	14	anim1i	$⊢ (B \in ℤ \land B \neq 0) \to (B \in ℂ \land B \neq 0)$
16		mulne0	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to A B \neq 0$
17	13 15 16	syl2an	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to A B \neq 0$
18	11 17	jca	$⊢ ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to (A B \in ℤ \land A B \neq 0)$
19	3	pczpre	$⊢ (P \in ℙ \land (A B \in ℤ \land A B \neq 0)) \to P pCnt A B = sup (\{n \in ℕ_{0} \| P^{n} ∥ A B\} ℝ <)$
20	18 19	sylan2	$⊢ (P \in ℙ \land ((A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0))) \to P pCnt A B = sup (\{n \in ℕ_{0} \| P^{n} ∥ A B\} ℝ <)$
21	20	3impb	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to P pCnt A B = sup (\{n \in ℕ_{0} \| P^{n} ∥ A B\} ℝ <)$
22	4 9 21	3eqtr4rd	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land (B \in ℤ \land B \neq 0)) \to P pCnt A B = (P pCnt A) + (P pCnt B)$

Metamath Proof Explorer

Theorem pcmul

Proof