ppinprm

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

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

Proof

Step	Hyp	Ref	Expression
1		simprr	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in ((2 \dots A + 1) \cap ℙ)$
2	1	elin2d	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in ℙ$
3		simprl	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to \neg A + 1 \in ℙ$
4		nelne2	$⊢ (x \in ℙ \land \neg A + 1 \in ℙ) \to x \neq A + 1$
5	2 3 4	syl2anc	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \neq A + 1$
6		velsn	$⊢ x \in \{A + 1\} \leftrightarrow x = A + 1$
7	6	necon3bbii	$⊢ \neg x \in \{A + 1\} \leftrightarrow x \neq A + 1$
8	5 7	sylibr	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to \neg x \in \{A + 1\}$
9	1	elin1d	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in (2 \dots A + 1)$
10		2z	$⊢ 2 \in ℤ$
11		zcn	$⊢ A \in ℤ \to A \in ℂ$
12	11	adantr	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to A \in ℂ$
13		ax-1cn	$⊢ 1 \in ℂ$
14		pncan	$⊢ (A \in ℂ \land 1 \in ℂ) \to A + 1 - 1 = A$
15	12 13 14	sylancl	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to A + 1 - 1 = A$
16		elfzuz2	$⊢ x \in (2 \dots A + 1) \to A + 1 \in ℤ_{\geq 2}$
17		uz2m1nn	$⊢ A + 1 \in ℤ_{\geq 2} \to A + 1 - 1 \in ℕ$
18	9 16 17	3syl	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to A + 1 - 1 \in ℕ$
19	15 18	eqeltrrd	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to A \in ℕ$
20		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
21		2m1e1	$⊢ 2 - 1 = 1$
22	21	fveq2i	$⊢ ℤ_{\geq (2 - 1)} = ℤ_{\geq 1}$
23	20 22	eqtr4i	$⊢ ℕ = ℤ_{\geq (2 - 1)}$
24	19 23	eleqtrdi	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to A \in ℤ_{\geq (2 - 1)}$
25		fzsuc2	$⊢ (2 \in ℤ \land A \in ℤ_{\geq (2 - 1)}) \to (2 \dots A + 1) = (2 \dots A) \cup \{A + 1\}$
26	10 24 25	sylancr	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to (2 \dots A + 1) = (2 \dots A) \cup \{A + 1\}$
27	9 26	eleqtrd	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in ((2 \dots A) \cup \{A + 1\})$
28		elun	$⊢ x \in ((2 \dots A) \cup \{A + 1\}) \leftrightarrow (x \in (2 \dots A) \lor x \in \{A + 1\})$
29	27 28	sylib	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to (x \in (2 \dots A) \lor x \in \{A + 1\})$
30	29	ord	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to (\neg x \in (2 \dots A) \to x \in \{A + 1\})$
31	8 30	mt3d	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in (2 \dots A)$
32	31 2	elind	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in ((2 \dots A) \cap ℙ)$
33	32	expr	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (x \in ((2 \dots A + 1) \cap ℙ) \to x \in ((2 \dots A) \cap ℙ))$
34	33	ssrdv	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ \subseteq (2 \dots A) \cap ℙ$
35		uzid	$⊢ A \in ℤ \to A \in ℤ_{\geq A}$
36	35	adantr	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to A \in ℤ_{\geq A}$
37		peano2uz	$⊢ A \in ℤ_{\geq A} \to A + 1 \in ℤ_{\geq A}$
38		fzss2	$⊢ A + 1 \in ℤ_{\geq A} \to (2 \dots A) \subseteq (2 \dots A + 1)$
39		ssrin	$⊢ (2 \dots A) \subseteq (2 \dots A + 1) \to (2 \dots A) \cap ℙ \subseteq (2 \dots A + 1) \cap ℙ$
40	36 37 38 39	4syl	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots A) \cap ℙ \subseteq (2 \dots A + 1) \cap ℙ$
41	34 40	eqssd	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ = (2 \dots A) \cap ℙ$
42	41	fveq2d	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to \|(2 \dots A + 1) \cap ℙ\| = \|(2 \dots A) \cap ℙ\|$
43		peano2z	$⊢ A \in ℤ \to A + 1 \in ℤ$
44	43	adantr	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to A + 1 \in ℤ$
45		ppival2	$⊢ A + 1 \in ℤ \to \underline{π} (A + 1) = \|(2 \dots A + 1) \cap ℙ\|$
46	44 45	syl	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to \underline{π} (A + 1) = \|(2 \dots A + 1) \cap ℙ\|$
47		ppival2	$⊢ A \in ℤ \to \underline{π} (A) = \|(2 \dots A) \cap ℙ\|$
48	47	adantr	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to \underline{π} (A) = \|(2 \dots A) \cap ℙ\|$
49	42 46 48	3eqtr4d	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to \underline{π} (A + 1) = \underline{π} (A)$

Metamath Proof Explorer

Theorem ppinprm

Proof