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 
|- A = { n e. NN0 | ( P ^ n ) || N }
pclem.2 
|- S = sup ( A , RR , < )
Assertion pcprecl 
|- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || N ) )

Proof

Step Hyp Ref Expression
1 pclem.1 
 |-  A = { n e. NN0 | ( P ^ n ) || N }
2 pclem.2 
 |-  S = sup ( A , RR , < )
3 1 pclem 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( A C_ ZZ /\ A =/= (/) /\ E. y e. ZZ A. z e. A z <_ y ) )
4 suprzcl2 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. y e. ZZ A. z e. A z <_ y ) -> sup ( A , RR , < ) e. A )
5 3 4 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> sup ( A , RR , < ) e. A )
6 2 5 eqeltrid 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> S e. A )
7 oveq2 
 |-  ( x = S -> ( P ^ x ) = ( P ^ S ) )
8 7 breq1d 
 |-  ( x = S -> ( ( P ^ x ) || N <-> ( P ^ S ) || N ) )
9 oveq2 
 |-  ( n = x -> ( P ^ n ) = ( P ^ x ) )
10 9 breq1d 
 |-  ( n = x -> ( ( P ^ n ) || N <-> ( P ^ x ) || N ) )
11 10 cbvrabv 
 |-  { n e. NN0 | ( P ^ n ) || N } = { x e. NN0 | ( P ^ x ) || N }
12 1 11 eqtri 
 |-  A = { x e. NN0 | ( P ^ x ) || N }
13 8 12 elrab2 
 |-  ( S e. A <-> ( S e. NN0 /\ ( P ^ S ) || N ) )
14 6 13 sylib 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || N ) )