Metamath Proof Explorer

Theorem prmgapprmolem

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

Ref Expression
Assertion prmgapprmolem ⊢ N ∈ ℕ ∧ I ∈ 2 … N → 1 < # p ⁡ N + I gcd I

Proof

Step Hyp Ref Expression
1 prmuz2 ⊢ p ∈ ℙ → p ∈ ℤ ≥ 2
2 1 ad2antlr ⊢ N ∈ ℕ ∧ I ∈ 2 … N ∧ p ∈ ℙ ∧ p ≤ N ∧ p ∥ I ∧ p ∥ # p ⁡ N + I → p ∈ ℤ ≥ 2
3 breq1 ⊢ q = p → q ∥ # p ⁡ N + I ↔ p ∥ # p ⁡ N + I
4 breq1 ⊢ q = p → q ∥ I ↔ p ∥ I
5 3 4 anbi12d ⊢ q = p → q ∥ # p ⁡ N + I ∧ q ∥ I ↔ p ∥ # p ⁡ N + I ∧ p ∥ I
6 5 adantl ⊢ N ∈ ℕ ∧ I ∈ 2 … N ∧ p ∈ ℙ ∧ p ≤ N ∧ p ∥ I ∧ p ∥ # p ⁡ N + I ∧ q = p → q ∥ # p ⁡ N + I ∧ q ∥ I ↔ p ∥ # p ⁡ N + I ∧ p ∥ I
7 pm3.22 ⊢ p ∥ I ∧ p ∥ # p ⁡ N + I → p ∥ # p ⁡ N + I ∧ p ∥ I
8 7 3adant1 ⊢ p ≤ N ∧ p ∥ I ∧ p ∥ # p ⁡ N + I → p ∥ # p ⁡ N + I ∧ p ∥ I
9 8 adantl ⊢ N ∈ ℕ ∧ I ∈ 2 … N ∧ p ∈ ℙ ∧ p ≤ N ∧ p ∥ I ∧ p ∥ # p ⁡ N + I → p ∥ # p ⁡ N + I ∧ p ∥ I
10 2 6 9 rspcedvd ⊢ N ∈ ℕ ∧ I ∈ 2 … N ∧ p ∈ ℙ ∧ p ≤ N ∧ p ∥ I ∧ p ∥ # p ⁡ N + I → ∃ q ∈ ℤ ≥ 2 q ∥ # p ⁡ N + I ∧ q ∥ I
11 prmdvdsprmop ⊢ N ∈ ℕ ∧ I ∈ 2 … N → ∃ p ∈ ℙ p ≤ N ∧ p ∥ I ∧ p ∥ # p ⁡ N + I
12 10 11 r19.29a ⊢ N ∈ ℕ ∧ I ∈ 2 … N → ∃ q ∈ ℤ ≥ 2 q ∥ # p ⁡ N + I ∧ q ∥ I
13 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
14 prmocl ⊢ N ∈ ℕ 0 → # p ⁡ N ∈ ℕ
15 13 14 syl ⊢ N ∈ ℕ → # p ⁡ N ∈ ℕ
16 elfzuz ⊢ I ∈ 2 … N → I ∈ ℤ ≥ 2
17 eluz2nn ⊢ I ∈ ℤ ≥ 2 → I ∈ ℕ
18 16 17 syl ⊢ I ∈ 2 … N → I ∈ ℕ
19 nnaddcl ⊢ # p ⁡ N ∈ ℕ ∧ I ∈ ℕ → # p ⁡ N + I ∈ ℕ
20 15 18 19 syl2an ⊢ N ∈ ℕ ∧ I ∈ 2 … N → # p ⁡ N + I ∈ ℕ
21 18 adantl ⊢ N ∈ ℕ ∧ I ∈ 2 … N → I ∈ ℕ
22 ncoprmgcdgt1b ⊢ # p ⁡ N + I ∈ ℕ ∧ I ∈ ℕ → ∃ q ∈ ℤ ≥ 2 q ∥ # p ⁡ N + I ∧ q ∥ I ↔ 1 < # p ⁡ N + I gcd I
23 20 21 22 syl2anc ⊢ N ∈ ℕ ∧ I ∈ 2 … N → ∃ q ∈ ℤ ≥ 2 q ∥ # p ⁡ N + I ∧ q ∥ I ↔ 1 < # p ⁡ N + I gcd I
24 12 23 mpbid ⊢ N ∈ ℕ ∧ I ∈ 2 … N → 1 < # p ⁡ N + I gcd I