Theorem prmgaplcmlem2

Description: Lemma for prmgaplcm : The least common multiple of all positive integers less than or equal to a number plus an integer greater than 1 and less then or equal to the number are not coprime. (Contributed by AV, 14-Aug-2020) (Revised by AV, 27-Aug-2020)

	Ref	Expression
Assertion	prmgaplcmlem2	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( ( _lcm ` ( 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 || ( ( _lcm ` ( 1 ... N ) ) + I ) <-> I || ( ( _lcm ` ( 1 ... N ) ) + I ) ) )
4		breq1	|- ( i = I -> ( i || I <-> I || I ) )
5	3 4	anbi12d	|- ( i = I -> ( ( i || ( ( _lcm ` ( 1 ... N ) ) + I ) /\ i || I ) <-> ( I || ( ( _lcm ` ( 1 ... N ) ) + I ) /\ I || I ) ) )
6	5	adantl	|- ( ( ( N e. NN /\ I e. ( 2 ... N ) ) /\ i = I ) -> ( ( i || ( ( _lcm ` ( 1 ... N ) ) + I ) /\ i || I ) <-> ( I || ( ( _lcm ` ( 1 ... N ) ) + I ) /\ I || I ) ) )
7		prmgaplcmlem1	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( ( _lcm ` ( 1 ... 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 || ( ( _lcm ` ( 1 ... N ) ) + I ) /\ I || I ) )
13	2 6 12	rspcedvd	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. i e. ( ZZ>= ` 2 ) ( i || ( ( _lcm ` ( 1 ... N ) ) + I ) /\ i || I ) )
14		fzssz	|- ( 1 ... N ) C_ ZZ
15		fzfid	|- ( N e. NN -> ( 1 ... N ) e. Fin )
16		0nelfz1	|- 0 e/ ( 1 ... N )
17	16	a1i	|- ( N e. NN -> 0 e/ ( 1 ... N ) )
18		lcmfn0cl	|- ( ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin /\ 0 e/ ( 1 ... N ) ) -> ( _lcm ` ( 1 ... N ) ) e. NN )
19	14 15 17 18	mp3an2i	|- ( N e. NN -> ( _lcm ` ( 1 ... N ) ) e. NN )
20	19	adantr	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( _lcm ` ( 1 ... N ) ) e. NN )
21		eluz2nn	|- ( I e. ( ZZ>= ` 2 ) -> I e. NN )
22	1 21	syl	|- ( I e. ( 2 ... N ) -> I e. NN )
23	22	adantl	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I e. NN )
24	20 23	nnaddcld	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( ( _lcm ` ( 1 ... N ) ) + I ) e. NN )
25		ncoprmgcdgt1b	|- ( ( ( ( _lcm ` ( 1 ... N ) ) + I ) e. NN /\ I e. NN ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || ( ( _lcm ` ( 1 ... N ) ) + I ) /\ i || I ) <-> 1 < ( ( ( _lcm ` ( 1 ... N ) ) + I ) gcd I ) ) )
26	24 23 25	syl2anc	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || ( ( _lcm ` ( 1 ... N ) ) + I ) /\ i || I ) <-> 1 < ( ( ( _lcm ` ( 1 ... N ) ) + I ) gcd I ) ) )
27	13 26	mpbid	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( ( _lcm ` ( 1 ... N ) ) + I ) gcd I ) )