prmgaplcmlem1

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 than or equal to the number is divisible by that integer. (Contributed by AV, 14-Aug-2020) (Revised by AV, 27-Aug-2020)

		Ref	Expression
	Assertion	prmgaplcmlem1	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ (\underline{lcm} ((1 \dots N)) + I)$

Proof

Step	Hyp	Ref	Expression
1		elfzelz	$⊢ I \in (2 \dots N) \to I \in ℤ$
2	1	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I \in ℤ$
3		fzssz	$⊢ (1 \dots N) \subseteq ℤ$
4		fzfi	$⊢ (1 \dots N) \in Fin$
5	3 4	pm3.2i	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin)$
6		lcmfcl	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin) \to \underline{lcm} ((1 \dots N)) \in ℕ_{0}$
7	6	nn0zd	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin) \to \underline{lcm} ((1 \dots N)) \in ℤ$
8	5 7	mp1i	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \underline{lcm} ((1 \dots N)) \in ℤ$
9		breq1	$⊢ x = I \to (x ∥ \underline{lcm} ((1 \dots N)) \leftrightarrow I ∥ \underline{lcm} ((1 \dots N)))$
10		dvdslcmf	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin) \to \forall x \in (1 \dots N) x ∥ \underline{lcm} ((1 \dots N))$
11	5 10	mp1i	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \forall x \in (1 \dots N) x ∥ \underline{lcm} ((1 \dots N))$
12		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
13		fzss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 \dots N) \subseteq (1 \dots N)$
14	12 13	mp1i	$⊢ N \in ℕ \to (2 \dots N) \subseteq (1 \dots N)$
15	14	sselda	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I \in (1 \dots N)$
16	9 11 15	rspcdva	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ \underline{lcm} ((1 \dots N))$
17		iddvds	$⊢ I \in ℤ \to I ∥ I$
18	1 17	syl	$⊢ I \in (2 \dots N) \to I ∥ I$
19	18	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ I$
20	2 8 2 16 19	dvds2addd	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ (\underline{lcm} ((1 \dots N)) + I)$

Metamath Proof Explorer

Theorem prmgaplcmlem1

Proof