Description: Lemma for prmgapprmo : The primorial of a number plus an integer greater than 1 and less then or equal to the number are not coprime. (Contributed by AV, 15-Aug-2020) (Revised by AV, 29-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | prmgapprmolem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prmuz2 | |
|
2 | 1 | ad2antlr | |
3 | breq1 | |
|
4 | breq1 | |
|
5 | 3 4 | anbi12d | |
6 | 5 | adantl | |
7 | pm3.22 | |
|
8 | 7 | 3adant1 | |
9 | 8 | adantl | |
10 | 2 6 9 | rspcedvd | |
11 | prmdvdsprmop | |
|
12 | 10 11 | r19.29a | |
13 | nnnn0 | |
|
14 | prmocl | |
|
15 | 13 14 | syl | |
16 | elfzuz | |
|
17 | eluz2nn | |
|
18 | 16 17 | syl | |
19 | nnaddcl | |
|
20 | 15 18 19 | syl2an | |
21 | 18 | adantl | |
22 | ncoprmgcdgt1b | |
|
23 | 20 21 22 | syl2anc | |
24 | 12 23 | mpbid | |