pcqmul

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

		Ref	Expression
	Assertion	pcqmul	$⊢ (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		simp2l	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to A \in ℚ$
2		elq	$⊢ A \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y}$
3	1 2	sylib	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y}$
4		simp3l	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to B \in ℚ$
5		elq	$⊢ B \in ℚ \leftrightarrow \exists z \in ℤ \exists w \in ℕ B = \frac{z}{w}$
6	4 5	sylib	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to \exists z \in ℤ \exists w \in ℕ B = \frac{z}{w}$
7		reeanv	$⊢ \exists x \in ℤ \exists z \in ℤ (\exists y \in ℕ A = \frac{x}{y} \land \exists w \in ℕ B = \frac{z}{w}) \leftrightarrow (\exists x \in ℤ \exists y \in ℕ A = \frac{x}{y} \land \exists z \in ℤ \exists w \in ℕ B = \frac{z}{w})$
8		reeanv	$⊢ \exists y \in ℕ \exists w \in ℕ (A = \frac{x}{y} \land B = \frac{z}{w}) \leftrightarrow (\exists y \in ℕ A = \frac{x}{y} \land \exists w \in ℕ B = \frac{z}{w})$
9		simp2r	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to A \neq 0$
10		simp3r	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to B \neq 0$
11	9 10	jca	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to (A \neq 0 \land B \neq 0)$
12	11	ad2antrr	$⊢ (((P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to (A \neq 0 \land B \neq 0)$
13		simp1	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to P \in ℙ$
14		simprl	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to y \in ℕ$
15	14	nncnd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to y \in ℂ$
16	14	nnne0d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to y \neq 0$
17	15 16	div0d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to \frac{0}{y} = 0$
18		oveq1	$⊢ x = 0 \to \frac{x}{y} = \frac{0}{y}$
19	18	eqeq1d	$⊢ x = 0 \to (\frac{x}{y} = 0 \leftrightarrow \frac{0}{y} = 0)$
20	17 19	syl5ibrcom	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to (x = 0 \to \frac{x}{y} = 0)$
21	20	necon3d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to (\frac{x}{y} \neq 0 \to x \neq 0)$
22		simprr	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to w \in ℕ$
23	22	nncnd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to w \in ℂ$
24	22	nnne0d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to w \neq 0$
25	23 24	div0d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to \frac{0}{w} = 0$
26		oveq1	$⊢ z = 0 \to \frac{z}{w} = \frac{0}{w}$
27	26	eqeq1d	$⊢ z = 0 \to (\frac{z}{w} = 0 \leftrightarrow \frac{0}{w} = 0)$
28	25 27	syl5ibrcom	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to (z = 0 \to \frac{z}{w} = 0)$
29	28	necon3d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to (\frac{z}{w} \neq 0 \to z \neq 0)$
30		simpll	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P \in ℙ$
31		simplrl	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to x \in ℤ$
32		simplrr	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to z \in ℤ$
33	31 32	zmulcld	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to x z \in ℤ$
34	31	zcnd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to x \in ℂ$
35	32	zcnd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to z \in ℂ$
36		simprrl	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to x \neq 0$
37		simprrr	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to z \neq 0$
38	34 35 36 37	mulne0d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to x z \neq 0$
39	14	adantrr	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to y \in ℕ$
40	22	adantrr	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to w \in ℕ$
41	39 40	nnmulcld	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to y w \in ℕ$
42		pcdiv	$⊢ (P \in ℙ \land (x z \in ℤ \land x z \neq 0) \land y w \in ℕ) \to P pCnt (\frac{x z}{y w}) = (P pCnt x z) - (P pCnt y w)$
43	30 33 38 41 42	syl121anc	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt (\frac{x z}{y w}) = (P pCnt x z) - (P pCnt y w)$
44		pcmul	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0) \land (z \in ℤ \land z \neq 0)) \to P pCnt x z = (P pCnt x) + (P pCnt z)$
45	30 31 36 32 37 44	syl122anc	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt x z = (P pCnt x) + (P pCnt z)$
46	39	nnzd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to y \in ℤ$
47	16	adantrr	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to y \neq 0$
48	40	nnzd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to w \in ℤ$
49	24	adantrr	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to w \neq 0$
50		pcmul	$⊢ (P \in ℙ \land (y \in ℤ \land y \neq 0) \land (w \in ℤ \land w \neq 0)) \to P pCnt y w = (P pCnt y) + (P pCnt w)$
51	30 46 47 48 49 50	syl122anc	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt y w = (P pCnt y) + (P pCnt w)$
52	45 51	oveq12d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to (P pCnt x z) - (P pCnt y w) = (P pCnt x) + (P pCnt z) - ((P pCnt y) + (P pCnt w))$
53		pczcl	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0)) \to P pCnt x \in ℕ_{0}$
54	30 31 36 53	syl12anc	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt x \in ℕ_{0}$
55	54	nn0cnd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt x \in ℂ$
56		pczcl	$⊢ (P \in ℙ \land (z \in ℤ \land z \neq 0)) \to P pCnt z \in ℕ_{0}$
57	30 32 37 56	syl12anc	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt z \in ℕ_{0}$
58	57	nn0cnd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt z \in ℂ$
59	30 39	pccld	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt y \in ℕ_{0}$
60	59	nn0cnd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt y \in ℂ$
61	30 40	pccld	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt w \in ℕ_{0}$
62	61	nn0cnd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt w \in ℂ$
63	55 58 60 62	addsub4d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to (P pCnt x) + (P pCnt z) - ((P pCnt y) + (P pCnt w)) = ((P pCnt x) - (P pCnt y)) + (P pCnt z) - (P pCnt w)$
64	43 52 63	3eqtrd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt (\frac{x z}{y w}) = ((P pCnt x) - (P pCnt y)) + (P pCnt z) - (P pCnt w)$
65	15	adantrr	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to y \in ℂ$
66	23	adantrr	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to w \in ℂ$
67	34 65 35 66 47 49	divmuldivd	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to (\frac{x}{y}) (\frac{z}{w}) = \frac{x z}{y w}$
68	67	oveq2d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt (\frac{x}{y}) (\frac{z}{w}) = P pCnt (\frac{x z}{y w})$
69		pcdiv	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0) \land y \in ℕ) \to P pCnt (\frac{x}{y}) = (P pCnt x) - (P pCnt y)$
70	30 31 36 39 69	syl121anc	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt (\frac{x}{y}) = (P pCnt x) - (P pCnt y)$
71		pcdiv	$⊢ (P \in ℙ \land (z \in ℤ \land z \neq 0) \land w \in ℕ) \to P pCnt (\frac{z}{w}) = (P pCnt z) - (P pCnt w)$
72	30 32 37 40 71	syl121anc	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt (\frac{z}{w}) = (P pCnt z) - (P pCnt w)$
73	70 72	oveq12d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to (P pCnt (\frac{x}{y})) + (P pCnt (\frac{z}{w})) = ((P pCnt x) - (P pCnt y)) + (P pCnt z) - (P pCnt w)$
74	64 68 73	3eqtr4d	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (x \neq 0 \land z \neq 0))) \to P pCnt (\frac{x}{y}) (\frac{z}{w}) = (P pCnt (\frac{x}{y})) + (P pCnt (\frac{z}{w}))$
75	74	expr	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to ((x \neq 0 \land z \neq 0) \to P pCnt (\frac{x}{y}) (\frac{z}{w}) = (P pCnt (\frac{x}{y})) + (P pCnt (\frac{z}{w})))$
76	21 29 75	syl2and	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to ((\frac{x}{y} \neq 0 \land \frac{z}{w} \neq 0) \to P pCnt (\frac{x}{y}) (\frac{z}{w}) = (P pCnt (\frac{x}{y})) + (P pCnt (\frac{z}{w})))$
77		neeq1	$⊢ A = \frac{x}{y} \to (A \neq 0 \leftrightarrow \frac{x}{y} \neq 0)$
78		neeq1	$⊢ B = \frac{z}{w} \to (B \neq 0 \leftrightarrow \frac{z}{w} \neq 0)$
79	77 78	bi2anan9	$⊢ (A = \frac{x}{y} \land B = \frac{z}{w}) \to ((A \neq 0 \land B \neq 0) \leftrightarrow (\frac{x}{y} \neq 0 \land \frac{z}{w} \neq 0))$
80		oveq12	$⊢ (A = \frac{x}{y} \land B = \frac{z}{w}) \to A B = (\frac{x}{y}) (\frac{z}{w})$
81	80	oveq2d	$⊢ (A = \frac{x}{y} \land B = \frac{z}{w}) \to P pCnt A B = P pCnt (\frac{x}{y}) (\frac{z}{w})$
82		oveq2	$⊢ A = \frac{x}{y} \to P pCnt A = P pCnt (\frac{x}{y})$
83		oveq2	$⊢ B = \frac{z}{w} \to P pCnt B = P pCnt (\frac{z}{w})$
84	82 83	oveqan12d	$⊢ (A = \frac{x}{y} \land B = \frac{z}{w}) \to (P pCnt A) + (P pCnt B) = (P pCnt (\frac{x}{y})) + (P pCnt (\frac{z}{w}))$
85	81 84	eqeq12d	$⊢ (A = \frac{x}{y} \land B = \frac{z}{w}) \to (P pCnt A B = (P pCnt A) + (P pCnt B) \leftrightarrow P pCnt (\frac{x}{y}) (\frac{z}{w}) = (P pCnt (\frac{x}{y})) + (P pCnt (\frac{z}{w})))$
86	79 85	imbi12d	$⊢ (A = \frac{x}{y} \land B = \frac{z}{w}) \to (((A \neq 0 \land B \neq 0) \to P pCnt A B = (P pCnt A) + (P pCnt B)) \leftrightarrow ((\frac{x}{y} \neq 0 \land \frac{z}{w} \neq 0) \to P pCnt (\frac{x}{y}) (\frac{z}{w}) = (P pCnt (\frac{x}{y})) + (P pCnt (\frac{z}{w}))))$
87	76 86	syl5ibrcom	$⊢ ((P \in ℙ \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to ((A = \frac{x}{y} \land B = \frac{z}{w}) \to ((A \neq 0 \land B \neq 0) \to P pCnt A B = (P pCnt A) + (P pCnt B)))$
88	13 87	sylanl1	$⊢ (((P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to ((A = \frac{x}{y} \land B = \frac{z}{w}) \to ((A \neq 0 \land B \neq 0) \to P pCnt A B = (P pCnt A) + (P pCnt B)))$
89	12 88	mpid	$⊢ (((P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to ((A = \frac{x}{y} \land B = \frac{z}{w}) \to P pCnt A B = (P pCnt A) + (P pCnt B))$
90	89	rexlimdvva	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \land (x \in ℤ \land z \in ℤ)) \to (\exists y \in ℕ \exists w \in ℕ (A = \frac{x}{y} \land B = \frac{z}{w}) \to P pCnt A B = (P pCnt A) + (P pCnt B))$
91	8 90	biimtrrid	$⊢ ((P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \land (x \in ℤ \land z \in ℤ)) \to ((\exists y \in ℕ A = \frac{x}{y} \land \exists w \in ℕ B = \frac{z}{w}) \to P pCnt A B = (P pCnt A) + (P pCnt B))$
92	91	rexlimdvva	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to (\exists x \in ℤ \exists z \in ℤ (\exists y \in ℕ A = \frac{x}{y} \land \exists w \in ℕ B = \frac{z}{w}) \to P pCnt A B = (P pCnt A) + (P pCnt B))$
93	7 92	biimtrrid	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0) \land (B \in ℚ \land B \neq 0)) \to ((\exists x \in ℤ \exists y \in ℕ A = \frac{x}{y} \land \exists z \in ℤ \exists w \in ℕ B = \frac{z}{w}) \to P pCnt A B = (P pCnt A) + (P pCnt B))$
94	3 6 93	mp2and	$⊢ (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 pcqmul

Proof