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

Metamath Proof Explorer

Theorem ppinprm

Proof