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 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑁 ) )