Theorem 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 then 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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzelz	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℤ )
2	1	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∈ ℤ )
3		fzssz	⊢ ( 1 ... 𝑁 ) ⊆ ℤ
4		fzfi	⊢ ( 1 ... 𝑁 ) ∈ Fin
5	3 4	pm3.2i	⊢ ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin )
6		lcmfcl	⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ0 )
7	6	nn0zd	⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℤ )
8	5 7	mp1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℤ )
9		breq1	⊢ ( 𝑥 = 𝐼 → ( 𝑥 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ↔ 𝐼 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
10		dvdslcmf	⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ∀ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑥 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
11	5 10	mp1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ∀ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑥 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
12		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
13		fzss1	⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
14	12 13	mp1i	⊢ ( 𝑁 ∈ ℕ → ( 2 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
15	14	sselda	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∈ ( 1 ... 𝑁 ) )
16	9 11 15	rspcdva	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
17		iddvds	⊢ ( 𝐼 ∈ ℤ → 𝐼 ∥ 𝐼 )
18	1 17	syl	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∥ 𝐼 )
19	18	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ 𝐼 )
20	2 8 2 16 19	dvds2addd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) )