Theorem prmgaplem2

Description: Lemma for prmgap : The factorial of a number plus an integer greater than 1 and less then or equal to the number are not coprime. (Contributed by AV, 13-Aug-2020)

	Ref	Expression
Assertion	prmgaplem2	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( ( ! ` N ) + I ) gcd I ) )

Proof

Step	Hyp	Ref	Expression
1		elfzuz	|- ( I e. ( 2 ... N ) -> I e. ( ZZ>= ` 2 ) )
2	1	adantl	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I e. ( ZZ>= ` 2 ) )
3		breq1	|- ( i = I -> ( i || ( ( ! ` N ) + I ) <-> I || ( ( ! ` N ) + I ) ) )
4		breq1	|- ( i = I -> ( i || I <-> I || I ) )
5	3 4	anbi12d	|- ( i = I -> ( ( i || ( ( ! ` N ) + I ) /\ i || I ) <-> ( I || ( ( ! ` N ) + I ) /\ I || I ) ) )
6	5	adantl	|- ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ i = I ) -> ( ( i || ( ( ! ` N ) + I ) /\ i || I ) <-> ( I || ( ( ! ` N ) + I ) /\ I || I ) ) )
7		prmgaplem1	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( ( ! ` N ) + I ) )
8		elfzelz	|- ( I e. ( 2 ... N ) -> I e. ZZ )
9		iddvds	|- ( I e. ZZ -> I || I )
10	8 9	syl	|- ( I e. ( 2 ... N ) -> I || I )
11	10	adantl	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || I )
12	7 11	jca	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( I || ( ( ! ` N ) + I ) /\ I || I ) )
13	2 6 12	rspcedvd	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. i e. ( ZZ>= ` 2 ) ( i || ( ( ! ` N ) + I ) /\ i || I ) )
14		nnnn0	|- ( N e. NN -> N e. NN0 )
15	14	faccld	|- ( N e. NN -> ( ! ` N ) e. NN )
16	15	adantr	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( ! ` N ) e. NN )
17		eluz2nn	|- ( I e. ( ZZ>= ` 2 ) -> I e. NN )
18	1 17	syl	|- ( I e. ( 2 ... N ) -> I e. NN )
19	18	adantl	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I e. NN )
20	16 19	nnaddcld	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( ( ! ` N ) + I ) e. NN )
21		ncoprmgcdgt1b	|- ( ( ( ( ! ` N ) + I ) e. NN /\ I e. NN ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || ( ( ! ` N ) + I ) /\ i || I ) <-> 1 < ( ( ( ! ` N ) + I ) gcd I ) ) )
22	20 19 21	syl2anc	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || ( ( ! ` N ) + I ) /\ i || I ) <-> 1 < ( ( ( ! ` N ) + I ) gcd I ) ) )
23	13 22	mpbid	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( ( ! ` N ) + I ) gcd I ) )