prmgapprmo

Description: Alternate proof of prmgap : in contrast to prmgap , where the gap starts at n! , the factorial of n, the gap starts at n#, the primorial of n. (Contributed by AV, 15-Aug-2020) (Revised by AV, 29-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	prmgapprmo	$⊢ \forall n \in ℕ \exists p \in ℙ \exists q \in ℙ (n \leq q - p \land \forall z \in (p + 1 ..^q) z \notin ℙ)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ n \in ℕ \to n \in ℕ$
2		eqid	$⊢ (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) = (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k))$
3		fzfid	$⊢ j \in ℕ \to (1 \dots j) \in Fin$
4		eqidd	$⊢ (j \in ℕ \land k \in (1 \dots j)) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) = (m \in ℕ ⟼ if (m \in ℙ, m, 1))$
5		eleq1	$⊢ m = k \to (m \in ℙ \leftrightarrow k \in ℙ)$
6		id	$⊢ m = k \to m = k$
7	5 6	ifbieq1d	$⊢ m = k \to if (m \in ℙ, m, 1) = if (k \in ℙ, k, 1)$
8	7	adantl	$⊢ ((j \in ℕ \land k \in (1 \dots j)) \land m = k) \to if (m \in ℙ, m, 1) = if (k \in ℙ, k, 1)$
9		elfznn	$⊢ k \in (1 \dots j) \to k \in ℕ$
10	9	adantl	$⊢ (j \in ℕ \land k \in (1 \dots j)) \to k \in ℕ$
11		1nn	$⊢ 1 \in ℕ$
12	11	a1i	$⊢ k \in (1 \dots j) \to 1 \in ℕ$
13	9 12	ifcld	$⊢ k \in (1 \dots j) \to if (k \in ℙ, k, 1) \in ℕ$
14	13	adantl	$⊢ (j \in ℕ \land k \in (1 \dots j)) \to if (k \in ℙ, k, 1) \in ℕ$
15	4 8 10 14	fvmptd	$⊢ (j \in ℕ \land k \in (1 \dots j)) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) = if (k \in ℙ, k, 1)$
16	15 14	eqeltrd	$⊢ (j \in ℕ \land k \in (1 \dots j)) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) \in ℕ$
17	3 16	fprodnncl	$⊢ j \in ℕ \to \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) \in ℕ$
18	2 17	fmpti	$⊢ (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) : ℕ ⟶ ℕ$
19		nnex	$⊢ ℕ \in V$
20	19 19	elmap	$⊢ (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) \in (ℕ^{ℕ}) \leftrightarrow (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) : ℕ ⟶ ℕ$
21	18 20	mpbir	$⊢ (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) \in (ℕ^{ℕ})$
22	21	a1i	$⊢ n \in ℕ \to (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) \in (ℕ^{ℕ})$
23		prmgapprmolem	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to 1 < (#_{p} (n) + i) \gcd i$
24		eqidd	$⊢ (((n \in ℕ \land i \in (2 \dots n)) \land j \in ℕ) \land k \in (1 \dots j)) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) = (m \in ℕ ⟼ if (m \in ℙ, m, 1))$
25	7	adantl	$⊢ ((((n \in ℕ \land i \in (2 \dots n)) \land j \in ℕ) \land k \in (1 \dots j)) \land m = k) \to if (m \in ℙ, m, 1) = if (k \in ℙ, k, 1)$
26	9	adantl	$⊢ (((n \in ℕ \land i \in (2 \dots n)) \land j \in ℕ) \land k \in (1 \dots j)) \to k \in ℕ$
27		elfzelz	$⊢ k \in (1 \dots j) \to k \in ℤ$
28		1zzd	$⊢ k \in (1 \dots j) \to 1 \in ℤ$
29	27 28	ifcld	$⊢ k \in (1 \dots j) \to if (k \in ℙ, k, 1) \in ℤ$
30	29	adantl	$⊢ (((n \in ℕ \land i \in (2 \dots n)) \land j \in ℕ) \land k \in (1 \dots j)) \to if (k \in ℙ, k, 1) \in ℤ$
31	24 25 26 30	fvmptd	$⊢ (((n \in ℕ \land i \in (2 \dots n)) \land j \in ℕ) \land k \in (1 \dots j)) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) = if (k \in ℙ, k, 1)$
32	31	prodeq2dv	$⊢ ((n \in ℕ \land i \in (2 \dots n)) \land j \in ℕ) \to \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) = \prod_{k = 1}^{j} if (k \in ℙ, k, 1)$
33	32	mpteq2dva	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) = (j \in ℕ ⟼ \prod_{k = 1}^{j} if (k \in ℙ, k, 1))$
34		oveq2	$⊢ j = n \to (1 \dots j) = (1 \dots n)$
35	34	prodeq1d	$⊢ j = n \to \prod_{k = 1}^{j} if (k \in ℙ, k, 1) = \prod_{k = 1}^{n} if (k \in ℙ, k, 1)$
36	35	adantl	$⊢ ((n \in ℕ \land i \in (2 \dots n)) \land j = n) \to \prod_{k = 1}^{j} if (k \in ℙ, k, 1) = \prod_{k = 1}^{n} if (k \in ℙ, k, 1)$
37		simpl	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to n \in ℕ$
38		fzfid	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (1 \dots n) \in Fin$
39		elfznn	$⊢ k \in (1 \dots n) \to k \in ℕ$
40	11	a1i	$⊢ k \in (1 \dots n) \to 1 \in ℕ$
41	39 40	ifcld	$⊢ k \in (1 \dots n) \to if (k \in ℙ, k, 1) \in ℕ$
42	41	adantl	$⊢ ((n \in ℕ \land i \in (2 \dots n)) \land k \in (1 \dots n)) \to if (k \in ℙ, k, 1) \in ℕ$
43	38 42	fprodnncl	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to \prod_{k = 1}^{n} if (k \in ℙ, k, 1) \in ℕ$
44	33 36 37 43	fvmptd	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) (n) = \prod_{k = 1}^{n} if (k \in ℙ, k, 1)$
45		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
46		prmoval	$⊢ n \in ℕ_{0} \to #_{p} (n) = \prod_{k = 1}^{n} if (k \in ℙ, k, 1)$
47	45 46	syl	$⊢ n \in ℕ \to #_{p} (n) = \prod_{k = 1}^{n} if (k \in ℙ, k, 1)$
48	47	eqcomd	$⊢ n \in ℕ \to \prod_{k = 1}^{n} if (k \in ℙ, k, 1) = #_{p} (n)$
49	48	adantr	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to \prod_{k = 1}^{n} if (k \in ℙ, k, 1) = #_{p} (n)$
50	44 49	eqtrd	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) (n) = #_{p} (n)$
51	50	oveq1d	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) (n) + i = #_{p} (n) + i$
52	51	oveq1d	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to ((j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) (n) + i) \gcd i = (#_{p} (n) + i) \gcd i$
53	23 52	breqtrrd	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to 1 < ((j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) (n) + i) \gcd i$
54	53	ralrimiva	$⊢ n \in ℕ \to \forall i \in (2 \dots n) 1 < ((j \in ℕ ⟼ \prod_{k = 1}^{j} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)) (n) + i) \gcd i$
55	1 22 54	prmgaplem8	$⊢ n \in ℕ \to \exists p \in ℙ \exists q \in ℙ (n \leq q - p \land \forall z \in (p + 1 ..^q) z \notin ℙ)$
56	55	rgen	$⊢ \forall n \in ℕ \exists p \in ℙ \exists q \in ℙ (n \leq q - p \land \forall z \in (p + 1 ..^q) z \notin ℙ)$

Metamath Proof Explorer

Theorem prmgapprmo

Proof