Metamath Proof Explorer

Theorem prmdvdsprmop

Description: The primorial of a number plus an integer greater than 1 and less than or equal to the number is divisible by a prime less than or equal to the number. (Contributed by AV, 15-Aug-2020) (Revised by AV, 28-Aug-2020)

Ref Expression
Assertion prmdvdsprmop ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ∧ 𝑝 ∥ ( ( #p ‘ 𝑁 ) + 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 prmdvdsfz ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) )
2 simprl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) ) → 𝑝 ≤ 𝑁 )
3 simprr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) ) → 𝑝 ∥ 𝐼 )
4 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
5 4 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) ) → 𝑝 ∈ ℤ )
6 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
7 prmocl ⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ∈ ℕ )
8 6 7 syl ⊢ ( 𝑁 ∈ ℕ → ( #p ‘ 𝑁 ) ∈ ℕ )
9 8 nnzd ⊢ ( 𝑁 ∈ ℕ → ( #p ‘ 𝑁 ) ∈ ℤ )
10 9 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( #p ‘ 𝑁 ) ∈ ℤ )
11 10 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → ( #p ‘ 𝑁 ) ∈ ℤ )
12 11 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) ) → ( #p ‘ 𝑁 ) ∈ ℤ )
13 elfzelz ⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℤ )
14 13 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐼 ∈ ℤ )
15 14 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) ) → 𝐼 ∈ ℤ )
16 prmdvdsprmo ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑞 ∈ ℙ ( 𝑞 ≤ 𝑁 → 𝑞 ∥ ( #p ‘ 𝑁 ) ) )
17 breq1 ⊢ ( 𝑞 = 𝑝 → ( 𝑞 ≤ 𝑁 ↔ 𝑝 ≤ 𝑁 ) )
18 breq1 ⊢ ( 𝑞 = 𝑝 → ( 𝑞 ∥ ( #p ‘ 𝑁 ) ↔ 𝑝 ∥ ( #p ‘ 𝑁 ) ) )
19 17 18 imbi12d ⊢ ( 𝑞 = 𝑝 → ( ( 𝑞 ≤ 𝑁 → 𝑞 ∥ ( #p ‘ 𝑁 ) ) ↔ ( 𝑝 ≤ 𝑁 → 𝑝 ∥ ( #p ‘ 𝑁 ) ) ) )
20 19 rspcv ⊢ ( 𝑝 ∈ ℙ → ( ∀ 𝑞 ∈ ℙ ( 𝑞 ≤ 𝑁 → 𝑞 ∥ ( #p ‘ 𝑁 ) ) → ( 𝑝 ≤ 𝑁 → 𝑝 ∥ ( #p ‘ 𝑁 ) ) ) )
21 16 20 syl5com ⊢ ( 𝑁 ∈ ℕ → ( 𝑝 ∈ ℙ → ( 𝑝 ≤ 𝑁 → 𝑝 ∥ ( #p ‘ 𝑁 ) ) ) )
22 21 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( 𝑝 ∈ ℙ → ( 𝑝 ≤ 𝑁 → 𝑝 ∥ ( #p ‘ 𝑁 ) ) ) )
23 22 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ≤ 𝑁 → 𝑝 ∥ ( #p ‘ 𝑁 ) ) )
24 23 adantrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) → 𝑝 ∥ ( #p ‘ 𝑁 ) ) )
25 24 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) ) → 𝑝 ∥ ( #p ‘ 𝑁 ) )
26 5 12 15 25 3 dvds2addd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) ) → 𝑝 ∥ ( ( #p ‘ 𝑁 ) + 𝐼 ) )
27 2 3 26 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) ) → ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ∧ 𝑝 ∥ ( ( #p ‘ 𝑁 ) + 𝐼 ) ) )
28 27 ex ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) → ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ∧ 𝑝 ∥ ( ( #p ‘ 𝑁 ) + 𝐼 ) ) ) )
29 28 reximdva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ∧ 𝑝 ∥ ( ( #p ‘ 𝑁 ) + 𝐼 ) ) ) )
30 1 29 mpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ∧ 𝑝 ∥ ( ( #p ‘ 𝑁 ) + 𝐼 ) ) )