prmdvdsfz

Description: Each integer greater than 1 and less then or equal to a fixed number is divisible by a prime less then or equal to this fixed number. (Contributed by AV, 15-Aug-2020)

		Ref	Expression
	Assertion	prmdvdsfz	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \exists p \in ℙ (p \leq N \land p ∥ I)$

Proof

Step	Hyp	Ref	Expression
1		elfzuz	$⊢ I \in (2 \dots N) \to I \in ℤ_{\geq 2}$
2	1	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I \in ℤ_{\geq 2}$
3		exprmfct	$⊢ I \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ I$
4	2 3	syl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \exists p \in ℙ p ∥ I$
5		prmz	$⊢ p \in ℙ \to p \in ℤ$
6		eluz2nn	$⊢ I \in ℤ_{\geq 2} \to I \in ℕ$
7	1 6	syl	$⊢ I \in (2 \dots N) \to I \in ℕ$
8	7	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I \in ℕ$
9		dvdsle	$⊢ (p \in ℤ \land I \in ℕ) \to (p ∥ I \to p \leq I)$
10	5 8 9	syl2anr	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to (p ∥ I \to p \leq I)$
11		elfzle2	$⊢ I \in (2 \dots N) \to I \leq N$
12	11	ad2antlr	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to I \leq N$
13	5	zred	$⊢ p \in ℙ \to p \in ℝ$
14	13	adantl	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to p \in ℝ$
15		elfzelz	$⊢ I \in (2 \dots N) \to I \in ℤ$
16	15	zred	$⊢ I \in (2 \dots N) \to I \in ℝ$
17	16	ad2antlr	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to I \in ℝ$
18		nnre	$⊢ N \in ℕ \to N \in ℝ$
19	18	ad2antrr	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to N \in ℝ$
20		letr	$⊢ (p \in ℝ \land I \in ℝ \land N \in ℝ) \to ((p \leq I \land I \leq N) \to p \leq N)$
21	14 17 19 20	syl3anc	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to ((p \leq I \land I \leq N) \to p \leq N)$
22	12 21	mpan2d	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to (p \leq I \to p \leq N)$
23	10 22	syld	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to (p ∥ I \to p \leq N)$
24	23	ancrd	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to (p ∥ I \to (p \leq N \land p ∥ I))$
25	24	reximdva	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to (\exists p \in ℙ p ∥ I \to \exists p \in ℙ (p \leq N \land p ∥ I))$
26	4 25	mpd	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \exists p \in ℙ (p \leq N \land p ∥ I)$

Metamath Proof Explorer

Theorem prmdvdsfz

Proof