pcprecl

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

	Ref	Expression
Hypotheses	pclem.1	$⊢ A = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
	pclem.2	$⊢ S = sup (A ℝ <)$
Assertion	pcprecl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (S \in ℕ_{0} \land P^{S} ∥ N)$

Step	Hyp	Ref	Expression
1		pclem.1	$⊢ A = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
2		pclem.2	$⊢ S = sup (A ℝ <)$
3	1	pclem	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (A \subseteq ℤ \land A \neq \emptyset \land \exists y \in ℤ \forall z \in A z \leq y)$
4		suprzcl2	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists y \in ℤ \forall z \in A z \leq y) \to sup (A ℝ <) \in A$
5	3 4	syl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to sup (A ℝ <) \in A$
6	2 5	eqeltrid	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to S \in A$
7		oveq2	$⊢ x = S \to P^{x} = P^{S}$
8	7	breq1d	$⊢ x = S \to (P^{x} ∥ N \leftrightarrow P^{S} ∥ N)$
9		oveq2	$⊢ n = x \to P^{n} = P^{x}$
10	9	breq1d	$⊢ n = x \to (P^{n} ∥ N \leftrightarrow P^{x} ∥ N)$
11	10	cbvrabv	$⊢ \{n \in ℕ_{0} \| P^{n} ∥ N\} = \{x \in ℕ_{0} \| P^{x} ∥ N\}$
12	1 11	eqtri	$⊢ A = \{x \in ℕ_{0} \| P^{x} ∥ N\}$
13	8 12	elrab2	$⊢ S \in A \leftrightarrow (S \in ℕ_{0} \land P^{S} ∥ N)$
14	6 13	sylib	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (S \in ℕ_{0} \land P^{S} ∥ N)$

Metamath Proof Explorer