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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prmdvdsfz | |
|
2 | simprl | |
|
3 | simprr | |
|
4 | prmz | |
|
5 | 4 | ad2antlr | |
6 | nnnn0 | |
|
7 | prmocl | |
|
8 | 6 7 | syl | |
9 | 8 | nnzd | |
10 | 9 | adantr | |
11 | 10 | adantr | |
12 | 11 | adantr | |
13 | elfzelz | |
|
14 | 13 | ad2antlr | |
15 | 14 | adantr | |
16 | prmdvdsprmo | |
|
17 | breq1 | |
|
18 | breq1 | |
|
19 | 17 18 | imbi12d | |
20 | 19 | rspcv | |
21 | 16 20 | syl5com | |
22 | 21 | adantr | |
23 | 22 | imp | |
24 | 23 | adantrd | |
25 | 24 | imp | |
26 | 5 12 15 25 3 | dvds2addd | |
27 | 2 3 26 | 3jca | |
28 | 27 | ex | |
29 | 28 | reximdva | |
30 | 1 29 | mpd | |