Metamath Proof Explorer

Theorem prmgaplem2

Description: Lemma for prmgap : The factorial of a number plus an integer greater than 1 and less then or equal to the number are not coprime. (Contributed by AV, 13-Aug-2020)

Ref Expression
Assertion prmgaplem2 ⊢ N ∈ ℕ ∧ I ∈ 2 … N → 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 ∥ N ! + I ↔ I ∥ N ! + I
4 breq1 ⊢ i = I → i ∥ I ↔ I ∥ I
5 3 4 anbi12d ⊢ i = I → i ∥ N ! + I ∧ i ∥ I ↔ I ∥ N ! + I ∧ I ∥ I
6 5 adantl ⊢ N ∈ ℕ ∧ I ∈ 2 … N ∧ i = I → i ∥ N ! + I ∧ i ∥ I ↔ I ∥ N ! + I ∧ I ∥ I
7 prmgaplem1 ⊢ N ∈ ℕ ∧ I ∈ 2 … N → I ∥ 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 ∥ N ! + I ∧ I ∥ I
13 2 6 12 rspcedvd ⊢ N ∈ ℕ ∧ I ∈ 2 … N → ∃ i ∈ ℤ ≥ 2 i ∥ N ! + I ∧ i ∥ I
14 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
15 14 faccld ⊢ N ∈ ℕ → N ! ∈ ℕ
16 15 adantr ⊢ N ∈ ℕ ∧ I ∈ 2 … N → N ! ∈ ℕ
17 eluz2nn ⊢ I ∈ ℤ ≥ 2 → I ∈ ℕ
18 1 17 syl ⊢ I ∈ 2 … N → I ∈ ℕ
19 18 adantl ⊢ N ∈ ℕ ∧ I ∈ 2 … N → I ∈ ℕ
20 16 19 nnaddcld ⊢ N ∈ ℕ ∧ I ∈ 2 … N → N ! + I ∈ ℕ
21 ncoprmgcdgt1b ⊢ N ! + I ∈ ℕ ∧ I ∈ ℕ → ∃ i ∈ ℤ ≥ 2 i ∥ N ! + I ∧ i ∥ I ↔ 1 < N ! + I gcd I
22 20 19 21 syl2anc ⊢ N ∈ ℕ ∧ I ∈ 2 … N → ∃ i ∈ ℤ ≥ 2 i ∥ N ! + I ∧ i ∥ I ↔ 1 < N ! + I gcd I
23 13 22 mpbid ⊢ N ∈ ℕ ∧ I ∈ 2 … N → 1 < N ! + I gcd I