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 NI2NppNpIp#pN+I

Proof

Step Hyp Ref Expression
1 prmdvdsfz NI2NppNpI
2 simprl NI2NppNpIpN
3 simprr NI2NppNpIpI
4 prmz pp
5 4 ad2antlr NI2NppNpIp
6 nnnn0 NN0
7 prmocl N0#pN
8 6 7 syl N#pN
9 8 nnzd N#pN
10 9 adantr NI2N#pN
11 10 adantr NI2Np#pN
12 11 adantr NI2NppNpI#pN
13 elfzelz I2NI
14 13 ad2antlr NI2NpI
15 14 adantr NI2NppNpII
16 prmdvdsprmo NqqNq#pN
17 breq1 q=pqNpN
18 breq1 q=pq#pNp#pN
19 17 18 imbi12d q=pqNq#pNpNp#pN
20 19 rspcv pqqNq#pNpNp#pN
21 16 20 syl5com NppNp#pN
22 21 adantr NI2NppNp#pN
23 22 imp NI2NppNp#pN
24 23 adantrd NI2NppNpIp#pN
25 24 imp NI2NppNpIp#pN
26 5 12 15 25 3 dvds2addd NI2NppNpIp#pN+I
27 2 3 26 3jca NI2NppNpIpNpIp#pN+I
28 27 ex NI2NppNpIpNpIp#pN+I
29 28 reximdva NI2NppNpIppNpIp#pN+I
30 1 29 mpd NI2NppNpIp#pN+I