This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
pclem.2 ⊢ 𝑆 = sup ( 𝐴 , ℝ , < )
Assertion pcpre1 ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 = 1 ) → 𝑆 = 0 )

Proof

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