Metamath Proof Explorer

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 ∈ ℕ ∧ I ∈ 2 … N → 1 < lcm _ ⁡ 1 … N + I gcd I

Proof

Step Hyp Ref Expression
1 elfzuz ⊢ I ∈ 2 … N → I ∈ ℤ ≥ 2
2 1 adantl ⊢ N ∈ ℕ ∧ I ∈ 2 … N → I ∈ ℤ ≥ 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 ∈ ℕ ∧ I ∈ 2 … N ∧ i = I → i ∥ lcm _ ⁡ 1 … N + I ∧ i ∥ I ↔ I ∥ lcm _ ⁡ 1 … N + I ∧ I ∥ I
7 prmgaplcmlem1 ⊢ N ∈ ℕ ∧ I ∈ 2 … N → I ∥ lcm _ ⁡ 1 … N + I
8 elfzelz ⊢ I ∈ 2 … N → I ∈ ℤ
9 iddvds ⊢ I ∈ ℤ → I ∥ I
10 8 9 syl ⊢ I ∈ 2 … N → I ∥ I
11 10 adantl ⊢ N ∈ ℕ ∧ I ∈ 2 … N → I ∥ I
12 7 11 jca ⊢ N ∈ ℕ ∧ I ∈ 2 … N → I ∥ lcm _ ⁡ 1 … N + I ∧ I ∥ I
13 2 6 12 rspcedvd ⊢ N ∈ ℕ ∧ I ∈ 2 … N → ∃ i ∈ ℤ ≥ 2 i ∥ lcm _ ⁡ 1 … N + I ∧ i ∥ I
14 fzssz ⊢ 1 … N ⊆ ℤ
15 fzfid ⊢ N ∈ ℕ → 1 … N ∈ Fin
16 0nelfz1 ⊢ 0 ∉ 1 … N
17 16 a1i ⊢ N ∈ ℕ → 0 ∉ 1 … N
18 lcmfn0cl ⊢ 1 … N ⊆ ℤ ∧ 1 … N ∈ Fin ∧ 0 ∉ 1 … N → lcm _ ⁡ 1 … N ∈ ℕ
19 14 15 17 18 mp3an2i ⊢ N ∈ ℕ → lcm _ ⁡ 1 … N ∈ ℕ
20 19 adantr ⊢ N ∈ ℕ ∧ I ∈ 2 … N → lcm _ ⁡ 1 … N ∈ ℕ
21 eluz2nn ⊢ I ∈ ℤ ≥ 2 → I ∈ ℕ
22 1 21 syl ⊢ I ∈ 2 … N → I ∈ ℕ
23 22 adantl ⊢ N ∈ ℕ ∧ I ∈ 2 … N → I ∈ ℕ
24 20 23 nnaddcld ⊢ N ∈ ℕ ∧ I ∈ 2 … N → lcm _ ⁡ 1 … N + I ∈ ℕ
25 ncoprmgcdgt1b ⊢ lcm _ ⁡ 1 … N + I ∈ ℕ ∧ I ∈ ℕ → ∃ i ∈ ℤ ≥ 2 i ∥ lcm _ ⁡ 1 … N + I ∧ i ∥ I ↔ 1 < lcm _ ⁡ 1 … N + I gcd I
26 24 23 25 syl2anc ⊢ N ∈ ℕ ∧ I ∈ 2 … N → ∃ i ∈ ℤ ≥ 2 i ∥ lcm _ ⁡ 1 … N + I ∧ i ∥ I ↔ 1 < lcm _ ⁡ 1 … N + I gcd I
27 13 26 mpbid ⊢ N ∈ ℕ ∧ I ∈ 2 … N → 1 < lcm _ ⁡ 1 … N + I gcd I