# 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 ${⊢}\left({N}\in ℕ\wedge {I}\in \left(2\dots {N}\right)\right)\to 1<\left(\underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)+{I}\right)\mathrm{gcd}{I}$

### Proof

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