pcdiv

Description: Division property of the prime power function. (Contributed by Mario Carneiro, 1-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to P \in ℙ$
2		simp2l	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to A \in ℤ$
3		simp3	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to B \in ℕ$
4		znq	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{A}{B} \in ℚ$
5	2 3 4	syl2anc	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to \frac{A}{B} \in ℚ$
6	2	zcnd	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to A \in ℂ$
7	3	nncnd	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to B \in ℂ$
8		simp2r	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to A \neq 0$
9	3	nnne0d	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to B \neq 0$
10	6 7 8 9	divne0d	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to \frac{A}{B} \neq 0$
11		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <)$
12		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)$
13	11 12	pcval	$⊢ (P \in ℙ \land (\frac{A}{B} \in ℚ \land \frac{A}{B} \neq 0)) \to P pCnt (\frac{A}{B}) = (ι z \| \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)))$
14	1 5 10 13	syl12anc	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to P pCnt (\frac{A}{B}) = (ι z \| \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)))$
15		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <)$
16	15	pczpre	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0)) \to P pCnt A = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <)$
17	16	3adant3	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to P pCnt A = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <)$
18		nnz	$⊢ B \in ℕ \to B \in ℤ$
19		nnne0	$⊢ B \in ℕ \to B \neq 0$
20	18 19	jca	$⊢ B \in ℕ \to (B \in ℤ \land B \neq 0)$
21		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
22	21	pczpre	$⊢ (P \in ℙ \land (B \in ℤ \land B \neq 0)) \to P pCnt B = sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
23	20 22	sylan2	$⊢ (P \in ℙ \land B \in ℕ) \to P pCnt B = sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
24	23	3adant2	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to P pCnt B = sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
25	17 24	oveq12d	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
26		eqid	$⊢ \frac{A}{B} = \frac{A}{B}$
27	25 26	jctil	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to (\frac{A}{B} = \frac{A}{B} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <))$
28		oveq1	$⊢ x = A \to \frac{x}{y} = \frac{A}{y}$
29	28	eqeq2d	$⊢ x = A \to (\frac{A}{B} = \frac{x}{y} \leftrightarrow \frac{A}{B} = \frac{A}{y})$
30		breq2	$⊢ x = A \to (P^{n} ∥ x \leftrightarrow P^{n} ∥ A)$
31	30	rabbidv	$⊢ x = A \to \{n \in ℕ_{0} \| P^{n} ∥ x\} = \{n \in ℕ_{0} \| P^{n} ∥ A\}$
32	31	supeq1d	$⊢ x = A \to sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <)$
33	32	oveq1d	$⊢ x = A \to sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)$
34	33	eqeq2d	$⊢ x = A \to ((P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) \leftrightarrow (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
35	29 34	anbi12d	$⊢ x = A \to ((\frac{A}{B} = \frac{x}{y} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow (\frac{A}{B} = \frac{A}{y} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)))$
36		oveq2	$⊢ y = B \to \frac{A}{y} = \frac{A}{B}$
37	36	eqeq2d	$⊢ y = B \to (\frac{A}{B} = \frac{A}{y} \leftrightarrow \frac{A}{B} = \frac{A}{B})$
38		breq2	$⊢ y = B \to (P^{n} ∥ y \leftrightarrow P^{n} ∥ B)$
39	38	rabbidv	$⊢ y = B \to \{n \in ℕ_{0} \| P^{n} ∥ y\} = \{n \in ℕ_{0} \| P^{n} ∥ B\}$
40	39	supeq1d	$⊢ y = B \to sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
41	40	oveq2d	$⊢ y = B \to sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)$
42	41	eqeq2d	$⊢ y = B \to ((P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) \leftrightarrow (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <))$
43	37 42	anbi12d	$⊢ y = B \to ((\frac{A}{B} = \frac{A}{y} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow (\frac{A}{B} = \frac{A}{B} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <)))$
44	35 43	rspc2ev	$⊢ (A \in ℤ \land B \in ℕ \land (\frac{A}{B} = \frac{A}{B} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ A\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ B\} ℝ <))) \to \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
45	2 3 27 44	syl3anc	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
46		ovex	$⊢ (P pCnt A) - (P pCnt B) \in V$
47	11 12	pceu	$⊢ (P \in ℙ \land (\frac{A}{B} \in ℚ \land \frac{A}{B} \neq 0)) \to \exists! z \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
48	1 5 10 47	syl12anc	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to \exists! z \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
49		eqeq1	$⊢ z = (P pCnt A) - (P pCnt B) \to (z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) \leftrightarrow (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
50	49	anbi2d	$⊢ z = (P pCnt A) - (P pCnt B) \to ((\frac{A}{B} = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow (\frac{A}{B} = \frac{x}{y} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)))$
51	50	2rexbidv	$⊢ z = (P pCnt A) - (P pCnt B) \to (\exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)))$
52	51	iota2	$⊢ ((P pCnt A) - (P pCnt B) \in V \land \exists! z \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))) \to (\exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow (ι z \| \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))) = (P pCnt A) - (P pCnt B))$
53	46 48 52	sylancr	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to (\exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land (P pCnt A) - (P pCnt B) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow (ι z \| \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))) = (P pCnt A) - (P pCnt B))$
54	45 53	mpbid	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to (ι z \| \exists x \in ℤ \exists y \in ℕ (\frac{A}{B} = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))) = (P pCnt A) - (P pCnt B)$
55	14 54	eqtrd	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0) \land B \in ℕ) \to P pCnt (\frac{A}{B}) = (P pCnt A) - (P pCnt B)$

Metamath Proof Explorer

Theorem pcdiv

Proof