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

Metamath Proof Explorer

Theorem pcprecl

Description: Closure of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Hypotheses pclem.1 ⊢ 𝐴 = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
pclem.2 ⊢ 𝑆 = sup ( 𝐴 , ℝ , < )
Assertion pcprecl ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 pclem.1 ⊢ 𝐴 = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
2 pclem.2 ⊢ 𝑆 = sup ( 𝐴 , ℝ , < )
3 1 pclem ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) )
4 suprzcl2 ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℤ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
5 3 4 syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
6 2 5 eqeltrid ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑆 ∈ 𝐴 )
7 oveq2 ⊢ ( 𝑥 = 𝑆 → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ 𝑆 ) )
8 7 breq1d ⊢ ( 𝑥 = 𝑆 → ( ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 ↔ ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ) )
9 oveq2 ⊢ ( 𝑛 = 𝑥 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑥 ) )
10 9 breq1d ⊢ ( 𝑛 = 𝑥 → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 ↔ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 ) )
11 10 cbvrabv ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 } = { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 }
12 1 11 eqtri ⊢ 𝐴 = { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 }
13 8 12 elrab2 ⊢ ( 𝑆 ∈ 𝐴 ↔ ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ) )
14 6 13 sylib ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ) )