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	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( ( #p ` N ) + I ) gcd I ) )

Proof

Step	Hyp	Ref	Expression
1		prmuz2	|- ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
2	1	ad2antlr	|- ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) ) -> p e. ( ZZ>= ` 2 ) )
3		breq1	|- ( q = p -> ( q || ( ( #p ` N ) + I ) <-> p || ( ( #p ` N ) + I ) ) )
4		breq1	|- ( q = p -> ( q || I <-> p || I ) )
5	3 4	anbi12d	|- ( q = p -> ( ( q || ( ( #p ` N ) + I ) /\ q || I ) <-> ( p || ( ( #p ` N ) + I ) /\ p || I ) ) )
6	5	adantl	|- ( ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) ) /\ q = p ) -> ( ( q || ( ( #p ` N ) + I ) /\ q || I ) <-> ( p || ( ( #p ` N ) + I ) /\ p || I ) ) )
7		pm3.22	|- ( ( p || I /\ p || ( ( #p ` N ) + I ) ) -> ( p || ( ( #p ` N ) + I ) /\ p || I ) )
8	7	3adant1	|- ( ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) -> ( p || ( ( #p ` N ) + I ) /\ p || I ) )
9	8	adantl	|- ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) ) -> ( p || ( ( #p ` N ) + I ) /\ p || I ) )
10	2 6 9	rspcedvd	|- ( ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ p e. Prime ) /\ ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) ) -> E. q e. ( ZZ>= ` 2 ) ( q || ( ( #p ` N ) + I ) /\ q || I ) )
11		prmdvdsprmop	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. p e. Prime ( p <_ N /\ p || I /\ p || ( ( #p ` N ) + I ) ) )
12	10 11	r19.29a	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. q e. ( ZZ>= ` 2 ) ( q || ( ( #p ` N ) + I ) /\ q || I ) )
13		nnnn0	|- ( N e. NN -> N e. NN0 )
14		prmocl	|- ( N e. NN0 -> ( #p ` N ) e. NN )
15	13 14	syl	|- ( N e. NN -> ( #p ` N ) e. NN )
16		elfzuz	|- ( I e. ( 2 ... N ) -> I e. ( ZZ>= ` 2 ) )
17		eluz2nn	|- ( I e. ( ZZ>= ` 2 ) -> I e. NN )
18	16 17	syl	|- ( I e. ( 2 ... N ) -> I e. NN )
19		nnaddcl	|- ( ( ( #p ` N ) e. NN /\ I e. NN ) -> ( ( #p ` N ) + I ) e. NN )
20	15 18 19	syl2an	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( ( #p ` N ) + I ) e. NN )
21	18	adantl	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I e. NN )
22		ncoprmgcdgt1b	|- ( ( ( ( #p ` N ) + I ) e. NN /\ I e. NN ) -> ( E. q e. ( ZZ>= ` 2 ) ( q || ( ( #p ` N ) + I ) /\ q || I ) <-> 1 < ( ( ( #p ` N ) + I ) gcd I ) ) )
23	20 21 22	syl2anc	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( E. q e. ( ZZ>= ` 2 ) ( q || ( ( #p ` N ) + I ) /\ q || I ) <-> 1 < ( ( ( #p ` N ) + I ) gcd I ) ) )
24	12 23	mpbid	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( ( #p ` N ) + I ) gcd I ) )