Metamath Proof Explorer


Theorem prmgapprmolem

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 NI2N1<#pN+IgcdI

Proof

Step Hyp Ref Expression
1 prmuz2 pp2
2 1 ad2antlr NI2NppNpIp#pN+Ip2
3 breq1 q=pq#pN+Ip#pN+I
4 breq1 q=pqIpI
5 3 4 anbi12d q=pq#pN+IqIp#pN+IpI
6 5 adantl NI2NppNpIp#pN+Iq=pq#pN+IqIp#pN+IpI
7 pm3.22 pIp#pN+Ip#pN+IpI
8 7 3adant1 pNpIp#pN+Ip#pN+IpI
9 8 adantl NI2NppNpIp#pN+Ip#pN+IpI
10 2 6 9 rspcedvd NI2NppNpIp#pN+Iq2q#pN+IqI
11 prmdvdsprmop NI2NppNpIp#pN+I
12 10 11 r19.29a NI2Nq2q#pN+IqI
13 nnnn0 NN0
14 prmocl N0#pN
15 13 14 syl N#pN
16 elfzuz I2NI2
17 eluz2nn I2I
18 16 17 syl I2NI
19 nnaddcl #pNI#pN+I
20 15 18 19 syl2an NI2N#pN+I
21 18 adantl NI2NI
22 ncoprmgcdgt1b #pN+IIq2q#pN+IqI1<#pN+IgcdI
23 20 21 22 syl2anc NI2Nq2q#pN+IqI1<#pN+IgcdI
24 12 23 mpbid NI2N1<#pN+IgcdI