| 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 ) ) |