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 \in ℕ \land I \in (2 \dots N)) \to 1 < (\underline{lcm} ((1 \dots N)) + I) \gcd I$

Proof

Step	Hyp	Ref	Expression
1		elfzuz	$⊢ I \in (2 \dots N) \to I \in ℤ_{\geq 2}$
2	1	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I \in ℤ_{\geq 2}$
3		breq1	$⊢ i = I \to (i ∥ (\underline{lcm} ((1 \dots N)) + I) \leftrightarrow I ∥ (\underline{lcm} ((1 \dots N)) + I))$
4		breq1	$⊢ i = I \to (i ∥ I \leftrightarrow I ∥ I)$
5	3 4	anbi12d	$⊢ i = I \to ((i ∥ (\underline{lcm} ((1 \dots N)) + I) \land i ∥ I) \leftrightarrow (I ∥ (\underline{lcm} ((1 \dots N)) + I) \land I ∥ I))$
6	5	adantl	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land i = I) \to ((i ∥ (\underline{lcm} ((1 \dots N)) + I) \land i ∥ I) \leftrightarrow (I ∥ (\underline{lcm} ((1 \dots N)) + I) \land I ∥ I))$
7		prmgaplcmlem1	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ (\underline{lcm} ((1 \dots N)) + I)$
8		elfzelz	$⊢ I \in (2 \dots N) \to I \in ℤ$
9		iddvds	$⊢ I \in ℤ \to I ∥ I$
10	8 9	syl	$⊢ I \in (2 \dots N) \to I ∥ I$
11	10	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ I$
12	7 11	jca	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to (I ∥ (\underline{lcm} ((1 \dots N)) + I) \land I ∥ I)$
13	2 6 12	rspcedvd	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \exists i \in ℤ_{\geq 2} (i ∥ (\underline{lcm} ((1 \dots N)) + I) \land i ∥ I)$
14		fzssz	$⊢ (1 \dots N) \subseteq ℤ$
15		fzfid	$⊢ N \in ℕ \to (1 \dots N) \in Fin$
16		0nelfz1	$⊢ 0 \notin (1 \dots N)$
17	16	a1i	$⊢ N \in ℕ \to 0 \notin (1 \dots N)$
18		lcmfn0cl	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin \land 0 \notin (1 \dots N)) \to \underline{lcm} ((1 \dots N)) \in ℕ$
19	14 15 17 18	mp3an2i	$⊢ N \in ℕ \to \underline{lcm} ((1 \dots N)) \in ℕ$
20	19	adantr	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \underline{lcm} ((1 \dots N)) \in ℕ$
21		eluz2nn	$⊢ I \in ℤ_{\geq 2} \to I \in ℕ$
22	1 21	syl	$⊢ I \in (2 \dots N) \to I \in ℕ$
23	22	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I \in ℕ$
24	20 23	nnaddcld	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \underline{lcm} ((1 \dots N)) + I \in ℕ$
25		ncoprmgcdgt1b	$⊢ (\underline{lcm} ((1 \dots N)) + I \in ℕ \land I \in ℕ) \to (\exists i \in ℤ_{\geq 2} (i ∥ (\underline{lcm} ((1 \dots N)) + I) \land i ∥ I) \leftrightarrow 1 < (\underline{lcm} ((1 \dots N)) + I) \gcd I)$
26	24 23 25	syl2anc	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to (\exists i \in ℤ_{\geq 2} (i ∥ (\underline{lcm} ((1 \dots N)) + I) \land i ∥ I) \leftrightarrow 1 < (\underline{lcm} ((1 \dots N)) + I) \gcd I)$
27	13 26	mpbid	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to 1 < (\underline{lcm} ((1 \dots N)) + I) \gcd I$

Metamath Proof Explorer

Theorem prmgaplcmlem2

Proof