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 ⊢ N ∈ ℕ ∧ I ∈ 2 … N → ∃ p ∈ ℙ p ≤ N ∧ p ∥ I

Proof

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