pczpre

Description: Connect the prime count pre-function to the actual prime count function, when restricted to the integers. (Contributed by Mario Carneiro, 23-Feb-2014) (Proof shortened by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Hypothesis	pczpre.1	$⊢ S = sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)$
	Assertion	pczpre	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P pCnt N = S$

Proof

Step	Hyp	Ref	Expression
1		pczpre.1	$⊢ S = sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)$
2		zq	$⊢ N \in ℤ \to N \in ℚ$
3		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <)$
4		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)$
5	3 4	pcval	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to P pCnt N = (ι z \| \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)))$
6	2 5	sylanr1	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P pCnt N = (ι z \| \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)))$
7		simprl	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to N \in ℤ$
8	7	zcnd	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to N \in ℂ$
9	8	div1d	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to \frac{N}{1} = N$
10	9	eqcomd	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to N = \frac{N}{1}$
11		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
12		eqid	$⊢ 1 = 1$
13		eqid	$⊢ \{n \in ℕ_{0} \| P^{n} ∥ 1\} = \{n \in ℕ_{0} \| P^{n} ∥ 1\}$
14		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <)$
15	13 14	pcpre1	$⊢ (P \in ℤ_{\geq 2} \land 1 = 1) \to sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <) = 0$
16	11 12 15	sylancl	$⊢ P \in ℙ \to sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <) = 0$
17	16	adantr	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <) = 0$
18	17	oveq2d	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to S - sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <) = S - 0$
19		eqid	$⊢ \{n \in ℕ_{0} \| P^{n} ∥ N\} = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
20	19 1	pcprecl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (S \in ℕ_{0} \land P^{S} ∥ N)$
21	11 20	sylan	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to (S \in ℕ_{0} \land P^{S} ∥ N)$
22	21	simpld	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to S \in ℕ_{0}$
23	22	nn0cnd	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to S \in ℂ$
24	23	subid1d	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to S - 0 = S$
25	18 24	eqtr2d	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to S = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <)$
26		1nn	$⊢ 1 \in ℕ$
27		oveq1	$⊢ x = N \to \frac{x}{y} = \frac{N}{y}$
28	27	eqeq2d	$⊢ x = N \to (N = \frac{x}{y} \leftrightarrow N = \frac{N}{y})$
29		breq2	$⊢ x = N \to (P^{n} ∥ x \leftrightarrow P^{n} ∥ N)$
30	29	rabbidv	$⊢ x = N \to \{n \in ℕ_{0} \| P^{n} ∥ x\} = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
31	30	supeq1d	$⊢ x = N \to sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)$
32	31 1	eqtr4di	$⊢ x = N \to sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) = S$
33	32	oveq1d	$⊢ x = N \to sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)$
34	33	eqeq2d	$⊢ x = N \to (S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) \leftrightarrow S = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
35	28 34	anbi12d	$⊢ x = N \to ((N = \frac{x}{y} \land S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow (N = \frac{N}{y} \land S = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)))$
36		oveq2	$⊢ y = 1 \to \frac{N}{y} = \frac{N}{1}$
37	36	eqeq2d	$⊢ y = 1 \to (N = \frac{N}{y} \leftrightarrow N = \frac{N}{1})$
38		breq2	$⊢ y = 1 \to (P^{n} ∥ y \leftrightarrow P^{n} ∥ 1)$
39	38	rabbidv	$⊢ y = 1 \to \{n \in ℕ_{0} \| P^{n} ∥ y\} = \{n \in ℕ_{0} \| P^{n} ∥ 1\}$
40	39	supeq1d	$⊢ y = 1 \to sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <)$
41	40	oveq2d	$⊢ y = 1 \to S - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <)$
42	41	eqeq2d	$⊢ y = 1 \to (S = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) \leftrightarrow S = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <))$
43	37 42	anbi12d	$⊢ y = 1 \to ((N = \frac{N}{y} \land S = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow (N = \frac{N}{1} \land S = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <)))$
44	35 43	rspc2ev	$⊢ (N \in ℤ \land 1 \in ℕ \land (N = \frac{N}{1} \land S = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <))) \to \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
45	26 44	mp3an2	$⊢ (N \in ℤ \land (N = \frac{N}{1} \land S = S - sup (\{n \in ℕ_{0} \| P^{n} ∥ 1\} ℝ <))) \to \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
46	7 10 25 45	syl12anc	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
47		ltso	$⊢ < Or ℝ$
48	47	supex	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <) \in V$
49	1 48	eqeltri	$⊢ S \in V$
50	3 4	pceu	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to \exists! z \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
51	2 50	sylanr1	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to \exists! z \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
52		eqeq1	$⊢ z = S \to (z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) \leftrightarrow S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))$
53	52	anbi2d	$⊢ z = S \to ((N = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow (N = \frac{x}{y} \land S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)))$
54	53	2rexbidv	$⊢ z = S \to (\exists x \in ℤ \exists y \in ℕ (N = \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 ℕ (N = \frac{x}{y} \land S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)))$
55	54	iota2	$⊢ (S \in V \land \exists! z \exists x \in ℤ \exists y \in ℕ (N = \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 ℕ (N = \frac{x}{y} \land S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow (ι z \| \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))) = S)$
56	49 51 55	sylancr	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to (\exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)) \leftrightarrow (ι z \| \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))) = S)$
57	46 56	mpbid	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to (ι z \| \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <))) = S$
58	6 57	eqtrd	$⊢ (P \in ℙ \land (N \in ℤ \land N \neq 0)) \to P pCnt N = S$

Metamath Proof Explorer

Theorem pczpre

Proof