prmgaplcm

Description: Alternate proof of prmgap : in contrast to prmgap , where the gap starts at n! , the factorial of n, the gap starts at the least common multiple of all positive integers less than or equal to n. (Contributed by AV, 13-Aug-2020) (Revised by AV, 27-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	prmgaplcm	$⊢ \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		fzssz	$⊢ (1 \dots x) \subseteq ℤ$
3	2	a1i	$⊢ x \in ℕ \to (1 \dots x) \subseteq ℤ$
4		fzfi	$⊢ (1 \dots x) \in Fin$
5	4	a1i	$⊢ x \in ℕ \to (1 \dots x) \in Fin$
6		0nelfz1	$⊢ 0 \notin (1 \dots x)$
7	6	a1i	$⊢ x \in ℕ \to 0 \notin (1 \dots x)$
8		lcmfn0cl	$⊢ ((1 \dots x) \subseteq ℤ \land (1 \dots x) \in Fin \land 0 \notin (1 \dots x)) \to \underline{lcm} ((1 \dots x)) \in ℕ$
9	3 5 7 8	syl3anc	$⊢ x \in ℕ \to \underline{lcm} ((1 \dots x)) \in ℕ$
10	9	adantl	$⊢ (n \in ℕ \land x \in ℕ) \to \underline{lcm} ((1 \dots x)) \in ℕ$
11		eqid	$⊢ (x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) = (x \in ℕ ⟼ \underline{lcm} ((1 \dots x)))$
12	10 11	fmptd	$⊢ n \in ℕ \to (x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) : ℕ ⟶ ℕ$
13		nnex	$⊢ ℕ \in V$
14	13 13	pm3.2i	$⊢ (ℕ \in V \land ℕ \in V)$
15		elmapg	$⊢ (ℕ \in V \land ℕ \in V) \to ((x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) \in (ℕ^{ℕ}) \leftrightarrow (x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) : ℕ ⟶ ℕ)$
16	14 15	mp1i	$⊢ n \in ℕ \to ((x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) \in (ℕ^{ℕ}) \leftrightarrow (x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) : ℕ ⟶ ℕ)$
17	12 16	mpbird	$⊢ n \in ℕ \to (x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) \in (ℕ^{ℕ})$
18		prmgaplcmlem2	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to 1 < (\underline{lcm} ((1 \dots n)) + i) \gcd i$
19		eqidd	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) = (x \in ℕ ⟼ \underline{lcm} ((1 \dots x)))$
20		oveq2	$⊢ x = n \to (1 \dots x) = (1 \dots n)$
21	20	fveq2d	$⊢ x = n \to \underline{lcm} ((1 \dots x)) = \underline{lcm} ((1 \dots n))$
22	21	adantl	$⊢ ((n \in ℕ \land i \in (2 \dots n)) \land x = n) \to \underline{lcm} ((1 \dots x)) = \underline{lcm} ((1 \dots n))$
23		simpl	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to n \in ℕ$
24		fzssz	$⊢ (1 \dots n) \subseteq ℤ$
25		fzfi	$⊢ (1 \dots n) \in Fin$
26	24 25	pm3.2i	$⊢ ((1 \dots n) \subseteq ℤ \land (1 \dots n) \in Fin)$
27		lcmfcl	$⊢ ((1 \dots n) \subseteq ℤ \land (1 \dots n) \in Fin) \to \underline{lcm} ((1 \dots n)) \in ℕ_{0}$
28	26 27	mp1i	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to \underline{lcm} ((1 \dots n)) \in ℕ_{0}$
29	19 22 23 28	fvmptd	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) (n) = \underline{lcm} ((1 \dots n))$
30	29	oveq1d	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) (n) + i = \underline{lcm} ((1 \dots n)) + i$
31	30	oveq1d	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to ((x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) (n) + i) \gcd i = (\underline{lcm} ((1 \dots n)) + i) \gcd i$
32	18 31	breqtrrd	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to 1 < ((x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) (n) + i) \gcd i$
33	32	ralrimiva	$⊢ n \in ℕ \to \forall i \in (2 \dots n) 1 < ((x \in ℕ ⟼ \underline{lcm} ((1 \dots x))) (n) + i) \gcd i$
34	1 17 33	prmgaplem8	$⊢ n \in ℕ \to \exists p \in ℙ \exists q \in ℙ (n \leq q - p \land \forall z \in (p + 1 ..^q) z \notin ℙ)$
35	34	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 prmgaplcm

Proof