Theorem 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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzuz	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ( ℤ≥ ‘ 2 ) )
2	1	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∈ ( ℤ≥ ‘ 2 ) )
3		exprmfct	⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝐼 )
4	2 3	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝐼 )
5		prmz	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
6		eluz2nn	⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 2 ) → 𝐼 ∈ ℕ )
7	1 6	syl	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℕ )
8	7	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∈ ℕ )
9		dvdsle	⊢ ( ( 𝑝 ∈ ℤ ∧ 𝐼 ∈ ℕ ) → ( 𝑝 ∥ 𝐼 → 𝑝 ≤ 𝐼 ) )
10	5 8 9	syl2anr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝐼 → 𝑝 ≤ 𝐼 ) )
11		elfzle2	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ≤ 𝑁 )
12	11	ad2antlr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐼 ≤ 𝑁 )
13	5	zred	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ )
14	13	adantl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℝ )
15		elfzelz	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℤ )
16	15	zred	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℝ )
17	16	ad2antlr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐼 ∈ ℝ )
18		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
19	18	ad2antrr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℝ )
20		letr	⊢ ( ( 𝑝 ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑝 ≤ 𝐼 ∧ 𝐼 ≤ 𝑁 ) → 𝑝 ≤ 𝑁 ) )
21	14 17 19 20	syl3anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ≤ 𝐼 ∧ 𝐼 ≤ 𝑁 ) → 𝑝 ≤ 𝑁 ) )
22	12 21	mpan2d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ≤ 𝐼 → 𝑝 ≤ 𝑁 ) )
23	10 22	syld	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝐼 → 𝑝 ≤ 𝑁 ) )
24	23	ancrd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝐼 → ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) ) )
25	24	reximdva	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝐼 → ∃ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) ) )
26	4 25	mpd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) )