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

Proof

Step Hyp Ref Expression
1 elfzuz ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ( ℤ≥ ‘ 2 ) )
2 1 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∈ ( ℤ≥ ‘ 2 ) )
3 breq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ↔ 𝐼 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ) )
4 breq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∥ 𝐼 ↔ 𝐼 ∥ 𝐼 ) )
5 3 4 anbi12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ∧ 𝑖 ∥ 𝐼 ) ↔ ( 𝐼 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ∧ 𝐼 ∥ 𝐼 ) ) )
6 5 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑖 = 𝐼 ) → ( ( 𝑖 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ∧ 𝑖 ∥ 𝐼 ) ↔ ( 𝐼 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ∧ 𝐼 ∥ 𝐼 ) ) )
7 prmgaplem1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) )
8 elfzelz ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℤ )
9 iddvds ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∥ 𝐼 )
10 8 9 syl ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∥ 𝐼 )
11 10 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ 𝐼 )
12 7 11 jca ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( 𝐼 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ∧ 𝐼 ∥ 𝐼 ) )
13 2 6 12 rspcedvd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ∧ 𝑖 ∥ 𝐼 ) )
14 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
15 14 faccld ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℕ )
16 15 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℕ )
17 eluz2nn ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 2 ) → 𝐼 ∈ ℕ )
18 1 17 syl ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℕ )
19 18 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∈ ℕ )
20 16 19 nnaddcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( ( ! ‘ 𝑁 ) + 𝐼 ) ∈ ℕ )
21 ncoprmgcdgt1b ⊢ ( ( ( ( ! ‘ 𝑁 ) + 𝐼 ) ∈ ℕ ∧ 𝐼 ∈ ℕ ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ∧ 𝑖 ∥ 𝐼 ) ↔ 1 < ( ( ( ! ‘ 𝑁 ) + 𝐼 ) gcd 𝐼 ) ) )
22 20 19 21 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) ∧ 𝑖 ∥ 𝐼 ) ↔ 1 < ( ( ( ! ‘ 𝑁 ) + 𝐼 ) gcd 𝐼 ) ) )
23 13 22 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 1 < ( ( ( ! ‘ 𝑁 ) + 𝐼 ) gcd 𝐼 ) )