Metamath Proof Explorer

Theorem prmgapprmolem

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

Ref Expression
Assertion prmgapprmolem ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 1 < ( ( ( #p ‘ 𝑁 ) + 𝐼 ) gcd 𝐼 ) )

Proof

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