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

Proof

Step Hyp Ref Expression
1 elfzuz ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ( ℤ≥ ‘ 2 ) )
2 1 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∈ ( ℤ≥ ‘ 2 ) )
3 breq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ↔ 𝐼 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ) )
4 breq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∥ 𝐼 ↔ 𝐼 ∥ 𝐼 ) )
5 3 4 anbi12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ∧ 𝑖 ∥ 𝐼 ) ↔ ( 𝐼 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ∧ 𝐼 ∥ 𝐼 ) ) )
6 5 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑖 = 𝐼 ) → ( ( 𝑖 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ∧ 𝑖 ∥ 𝐼 ) ↔ ( 𝐼 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ∧ 𝐼 ∥ 𝐼 ) ) )
7 prmgaplcmlem1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) )
8 elfzelz ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℤ )
9 iddvds ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∥ 𝐼 )
10 8 9 syl ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∥ 𝐼 )
11 10 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ 𝐼 )
12 7 11 jca ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( 𝐼 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ∧ 𝐼 ∥ 𝐼 ) )
13 2 6 12 rspcedvd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ∧ 𝑖 ∥ 𝐼 ) )
14 fzssz ⊢ ( 1 ... 𝑁 ) ⊆ ℤ
15 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ∈ Fin )
16 0nelfz1 ⊢ 0 ∉ ( 1 ... 𝑁 )
17 16 a1i ⊢ ( 𝑁 ∈ ℕ → 0 ∉ ( 1 ... 𝑁 ) )
18 lcmfn0cl ⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ∧ 0 ∉ ( 1 ... 𝑁 ) ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
19 14 15 17 18 mp3an2i ⊢ ( 𝑁 ∈ ℕ → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
20 19 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
21 eluz2nn ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 2 ) → 𝐼 ∈ ℕ )
22 1 21 syl ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℕ )
23 22 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∈ ℕ )
24 20 23 nnaddcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ∈ ℕ )
25 ncoprmgcdgt1b ⊢ ( ( ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ∈ ℕ ∧ 𝐼 ∈ ℕ ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ∧ 𝑖 ∥ 𝐼 ) ↔ 1 < ( ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) gcd 𝐼 ) ) )
26 24 23 25 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) ∧ 𝑖 ∥ 𝐼 ) ↔ 1 < ( ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) gcd 𝐼 ) ) )
27 13 26 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 1 < ( ( ( lcm ‘ ( 1 ... 𝑁 ) ) + 𝐼 ) gcd 𝐼 ) )