This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prmdvdsfz

Description: Each integer greater than 1 and less than or equal to a fixed number is divisible by a prime less than 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 ... 𝑁 ) ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) )