ppiprm

Description: The prime-counting function ppi at a prime. (Contributed by Mario Carneiro, 19-Sep-2014)

		Ref	Expression
	Assertion	ppiprm	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \underline{π} (A + 1) = \underline{π} (A) + 1$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A) \in Fin$
2		inss1	$⊢ (2 \dots A) \cap ℙ \subseteq (2 \dots A)$
3		ssfi	$⊢ ((2 \dots A) \in Fin \land (2 \dots A) \cap ℙ \subseteq (2 \dots A)) \to (2 \dots A) \cap ℙ \in Fin$
4	1 2 3	sylancl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A) \cap ℙ \in Fin$
5		zre	$⊢ A \in ℤ \to A \in ℝ$
6	5	adantr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A \in ℝ$
7	6	ltp1d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A < A + 1$
8		peano2z	$⊢ A \in ℤ \to A + 1 \in ℤ$
9	8	adantr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 \in ℤ$
10	9	zred	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 \in ℝ$
11	6 10	ltnled	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (A < A + 1 \leftrightarrow \neg A + 1 \leq A)$
12	7 11	mpbid	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \neg A + 1 \leq A$
13		elinel1	$⊢ A + 1 \in ((2 \dots A) \cap ℙ) \to A + 1 \in (2 \dots A)$
14		elfzle2	$⊢ A + 1 \in (2 \dots A) \to A + 1 \leq A$
15	13 14	syl	$⊢ A + 1 \in ((2 \dots A) \cap ℙ) \to A + 1 \leq A$
16	12 15	nsyl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \neg A + 1 \in ((2 \dots A) \cap ℙ)$
17		ovex	$⊢ A + 1 \in V$
18		hashunsng	$⊢ A + 1 \in V \to (((2 \dots A) \cap ℙ \in Fin \land \neg A + 1 \in ((2 \dots A) \cap ℙ)) \to \|((2 \dots A) \cap ℙ) \cup \{A + 1\}\| = \|(2 \dots A) \cap ℙ\| + 1)$
19	17 18	ax-mp	$⊢ ((2 \dots A) \cap ℙ \in Fin \land \neg A + 1 \in ((2 \dots A) \cap ℙ)) \to \|((2 \dots A) \cap ℙ) \cup \{A + 1\}\| = \|(2 \dots A) \cap ℙ\| + 1$
20	4 16 19	syl2anc	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \|((2 \dots A) \cap ℙ) \cup \{A + 1\}\| = \|(2 \dots A) \cap ℙ\| + 1$
21		ppival2	$⊢ A + 1 \in ℤ \to \underline{π} (A + 1) = \|(2 \dots A + 1) \cap ℙ\|$
22	9 21	syl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \underline{π} (A + 1) = \|(2 \dots A + 1) \cap ℙ\|$
23		2z	$⊢ 2 \in ℤ$
24		zcn	$⊢ A \in ℤ \to A \in ℂ$
25	24	adantr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A \in ℂ$
26		ax-1cn	$⊢ 1 \in ℂ$
27		pncan	$⊢ (A \in ℂ \land 1 \in ℂ) \to A + 1 - 1 = A$
28	25 26 27	sylancl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 - 1 = A$
29		prmuz2	$⊢ A + 1 \in ℙ \to A + 1 \in ℤ_{\geq 2}$
30	29	adantl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 \in ℤ_{\geq 2}$
31		uz2m1nn	$⊢ A + 1 \in ℤ_{\geq 2} \to A + 1 - 1 \in ℕ$
32	30 31	syl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 - 1 \in ℕ$
33	28 32	eqeltrrd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A \in ℕ$
34		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
35		2m1e1	$⊢ 2 - 1 = 1$
36	35	fveq2i	$⊢ ℤ_{\geq (2 - 1)} = ℤ_{\geq 1}$
37	34 36	eqtr4i	$⊢ ℕ = ℤ_{\geq (2 - 1)}$
38	33 37	eleqtrdi	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A \in ℤ_{\geq (2 - 1)}$
39		fzsuc2	$⊢ (2 \in ℤ \land A \in ℤ_{\geq (2 - 1)}) \to (2 \dots A + 1) = (2 \dots A) \cup \{A + 1\}$
40	23 38 39	sylancr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A + 1) = (2 \dots A) \cup \{A + 1\}$
41	40	ineq1d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ = ((2 \dots A) \cup \{A + 1\}) \cap ℙ$
42		indir	$⊢ ((2 \dots A) \cup \{A + 1\}) \cap ℙ = ((2 \dots A) \cap ℙ) \cup (\{A + 1\} \cap ℙ)$
43	41 42	eqtrdi	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ = ((2 \dots A) \cap ℙ) \cup (\{A + 1\} \cap ℙ)$
44		simpr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 \in ℙ$
45	44	snssd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \{A + 1\} \subseteq ℙ$
46		dfss2	$⊢ \{A + 1\} \subseteq ℙ \leftrightarrow \{A + 1\} \cap ℙ = \{A + 1\}$
47	45 46	sylib	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \{A + 1\} \cap ℙ = \{A + 1\}$
48	47	uneq2d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to ((2 \dots A) \cap ℙ) \cup (\{A + 1\} \cap ℙ) = ((2 \dots A) \cap ℙ) \cup \{A + 1\}$
49	43 48	eqtrd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ = ((2 \dots A) \cap ℙ) \cup \{A + 1\}$
50	49	fveq2d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \|(2 \dots A + 1) \cap ℙ\| = \|((2 \dots A) \cap ℙ) \cup \{A + 1\}\|$
51	22 50	eqtrd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \underline{π} (A + 1) = \|((2 \dots A) \cap ℙ) \cup \{A + 1\}\|$
52		ppival2	$⊢ A \in ℤ \to \underline{π} (A) = \|(2 \dots A) \cap ℙ\|$
53	52	adantr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \underline{π} (A) = \|(2 \dots A) \cap ℙ\|$
54	53	oveq1d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \underline{π} (A) + 1 = \|(2 \dots A) \cap ℙ\| + 1$
55	20 51 54	3eqtr4d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \underline{π} (A + 1) = \underline{π} (A) + 1$

Metamath Proof Explorer

Theorem ppiprm

Proof