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 e. NN /\ I e. ( 2 ... N ) ) -> E. p e. Prime ( p <_ N /\ p || I ) )

Proof

Step Hyp Ref Expression
1 elfzuz 
 |-  ( I e. ( 2 ... N ) -> I e. ( ZZ>= ` 2 ) )
2 1 adantl 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I e. ( ZZ>= ` 2 ) )
3 exprmfct 
 |-  ( I e. ( ZZ>= ` 2 ) -> E. p e. Prime p || I )
4 2 3 syl 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. p e. Prime p || I )
5 prmz 
 |-  ( p e. Prime -> p e. ZZ )
6 eluz2nn 
 |-  ( I e. ( ZZ>= ` 2 ) -> I e. NN )
7 1 6 syl 
 |-  ( I e. ( 2 ... N ) -> I e. NN )
8 7 adantl 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I e. NN )
9 dvdsle 
 |-  ( ( p e. ZZ /\ I e. NN ) -> ( p || I -> p <_ I ) )
10 5 8 9 syl2anr 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> ( p || I -> p <_ I ) )
11 elfzle2 
 |-  ( I e. ( 2 ... N ) -> I <_ N )
12 11 ad2antlr 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> I <_ N )
13 5 zred 
 |-  ( p e. Prime -> p e. RR )
14 13 adantl 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> p e. RR )
15 elfzelz 
 |-  ( I e. ( 2 ... N ) -> I e. ZZ )
16 15 zred 
 |-  ( I e. ( 2 ... N ) -> I e. RR )
17 16 ad2antlr 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> I e. RR )
18 nnre 
 |-  ( N e. NN -> N e. RR )
19 18 ad2antrr 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> N e. RR )
20 letr 
 |-  ( ( p e. RR /\ I e. RR /\ N e. RR ) -> ( ( p <_ I /\ I <_ N ) -> p <_ N ) )
21 14 17 19 20 syl3anc 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> ( ( p <_ I /\ I <_ N ) -> p <_ N ) )
22 12 21 mpan2d 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> ( p <_ I -> p <_ N ) )
23 10 22 syld 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> ( p || I -> p <_ N ) )
24 23 ancrd 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> ( p || I -> ( p <_ N /\ p || I ) ) )
25 24 reximdva 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( E. p e. Prime p || I -> E. p e. Prime ( p <_ N /\ p || I ) ) )
26 4 25 mpd 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. p e. Prime ( p <_ N /\ p || I ) )