Metamath Proof Explorer

Theorem prmdvdsprmop

Description: The primorial of a number plus an integer greater than 1 and less then or equal to the number is divisible by a prime less then or equal to the number. (Contributed by AV, 15-Aug-2020) (Revised by AV, 28-Aug-2020)

Ref Expression
Assertion prmdvdsprmop 
|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. p e. Prime ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) )

Proof

Step Hyp Ref Expression
1 prmdvdsfz 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. p e. Prime ( p <_ N /\ p || I ) )
2 simprl 
 |-  ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I ) ) -> p <_ N )
3 simprr 
 |-  ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I ) ) -> p || I )
4 prmz 
 |-  ( p e. Prime -> p e. ZZ )
5 4 ad2antlr 
 |-  ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I ) ) -> p e. ZZ )
6 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
7 prmocl 
 |-  ( N e. NN0 -> ( #p ` N ) e. NN )
8 6 7 syl 
 |-  ( N e. NN -> ( #p ` N ) e. NN )
9 8 nnzd 
 |-  ( N e. NN -> ( #p ` N ) e. ZZ )
10 9 adantr 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( #p ` N ) e. ZZ )
11 10 adantr 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> ( #p ` N ) e. ZZ )
12 11 adantr 
 |-  ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I ) ) -> ( #p ` N ) e. ZZ )
13 elfzelz 
 |-  ( I e. ( 2 ... N ) -> I e. ZZ )
14 13 ad2antlr 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> I e. ZZ )
15 14 adantr 
 |-  ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I ) ) -> I e. ZZ )
16 prmdvdsprmo 
 |-  ( N e. NN -> A. q e. Prime ( q <_ N -> q || ( #p ` N ) ) )
17 breq1 
 |-  ( q = p -> ( q <_ N <-> p <_ N ) )
18 breq1 
 |-  ( q = p -> ( q || ( #p ` N ) <-> p || ( #p ` N ) ) )
19 17 18 imbi12d 
 |-  ( q = p -> ( ( q <_ N -> q || ( #p ` N ) ) <-> ( p <_ N -> p || ( #p ` N ) ) ) )
20 19 rspcv 
 |-  ( p e. Prime -> ( A. q e. Prime ( q <_ N -> q || ( #p ` N ) ) -> ( p <_ N -> p || ( #p ` N ) ) ) )
21 16 20 syl5com 
 |-  ( N e. NN -> ( p e. Prime -> ( p <_ N -> p || ( #p ` N ) ) ) )
22 21 adantr 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( p e. Prime -> ( p <_ N -> p || ( #p ` N ) ) ) )
23 22 imp 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> ( p <_ N -> p || ( #p ` N ) ) )
24 23 adantrd 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> ( ( p <_ N /\ p || I ) -> p || ( #p ` N ) ) )
25 24 imp 
 |-  ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I ) ) -> p || ( #p ` N ) )
26 5 12 15 25 3 dvds2addd 
 |-  ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I ) ) -> p || ( ( #p ` N ) + I ) )
27 2 3 26 3jca 
 |-  ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I ) ) -> ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) )
28 27 ex 
 |-  ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) -> ( ( p <_ N /\ p || I ) -> ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) ) )
29 28 reximdva 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( E. p e. Prime ( p <_ N /\ p || I ) -> E. p e. Prime ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) ) )
30 1 29 mpd 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. p e. Prime ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) )