Metamath Proof Explorer

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 ${⊢}\left({N}\in ℕ\wedge {I}\in \left(2\dots {N}\right)\right)\to \exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\left({p}\le {N}\wedge {p}\parallel {I}\right)$

Proof

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