Metamath Proof Explorer

Theorem pcpre1

Description: Value of the prime power pre-function at 1. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses pclem.1 ⊢ A = n ∈ ℕ 0 | P n ∥ N
pclem.2 ⊢ S = sup A ℝ <
Assertion pcpre1 ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → S = 0

Proof

Step Hyp Ref Expression
1 pclem.1 ⊢ A = n ∈ ℕ 0 | P n ∥ N
2 pclem.2 ⊢ S = sup A ℝ <
3 1z ⊢ 1 ∈ ℤ
4 eleq1 ⊢ N = 1 → N ∈ ℤ ↔ 1 ∈ ℤ
5 3 4 mpbiri ⊢ N = 1 → N ∈ ℤ
6 ax-1ne0 ⊢ 1 ≠ 0
7 neeq1 ⊢ N = 1 → N ≠ 0 ↔ 1 ≠ 0
8 6 7 mpbiri ⊢ N = 1 → N ≠ 0
9 5 8 jca ⊢ N = 1 → N ∈ ℤ ∧ N ≠ 0
10 1 2 pcprecl ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → S ∈ ℕ 0 ∧ P S ∥ N
11 9 10 sylan2 ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → S ∈ ℕ 0 ∧ P S ∥ N
12 11 simprd ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P S ∥ N
13 simpr ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → N = 1
14 12 13 breqtrd ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P S ∥ 1
15 eluz2nn ⊢ P ∈ ℤ ≥ 2 → P ∈ ℕ
16 15 adantr ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P ∈ ℕ
17 11 simpld ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → S ∈ ℕ 0
18 16 17 nnexpcld ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P S ∈ ℕ
19 18 nnzd ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P S ∈ ℤ
20 1nn ⊢ 1 ∈ ℕ
21 dvdsle ⊢ P S ∈ ℤ ∧ 1 ∈ ℕ → P S ∥ 1 → P S ≤ 1
22 19 20 21 sylancl ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P S ∥ 1 → P S ≤ 1
23 14 22 mpd ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P S ≤ 1
24 16 nncnd ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P ∈ ℂ
25 24 exp0d ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P 0 = 1
26 23 25 breqtrrd ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P S ≤ P 0
27 16 nnred ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → P ∈ ℝ
28 17 nn0zd ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → S ∈ ℤ
29 0zd ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → 0 ∈ ℤ
30 eluz2gt1 ⊢ P ∈ ℤ ≥ 2 → 1 < P
31 30 adantr ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → 1 < P
32 27 28 29 31 leexp2d ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → S ≤ 0 ↔ P S ≤ P 0
33 26 32 mpbird ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → S ≤ 0
34 10 simpld ⊢ P ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ N ≠ 0 → S ∈ ℕ 0
35 9 34 sylan2 ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → S ∈ ℕ 0
36 nn0le0eq0 ⊢ S ∈ ℕ 0 → S ≤ 0 ↔ S = 0
37 35 36 syl ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → S ≤ 0 ↔ S = 0
38 33 37 mpbid ⊢ P ∈ ℤ ≥ 2 ∧ N = 1 → S = 0