Metamath Proof Explorer

Theorem pcprendvds

Description: Non-divisibility property 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 pcprendvds 
|- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( S + 1 ) ) || 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 2 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || N ) )
4 3 simpld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> S e. NN0 )
5 nn0re 
 |-  ( S e. NN0 -> S e. RR )
6 ltp1 
 |-  ( S e. RR -> S < ( S + 1 ) )
7 peano2re 
 |-  ( S e. RR -> ( S + 1 ) e. RR )
8 ltnle 
 |-  ( ( S e. RR /\ ( S + 1 ) e. RR ) -> ( S < ( S + 1 ) <-> -. ( S + 1 ) <_ S ) )
9 7 8 mpdan 
 |-  ( S e. RR -> ( S < ( S + 1 ) <-> -. ( S + 1 ) <_ S ) )
10 6 9 mpbid 
 |-  ( S e. RR -> -. ( S + 1 ) <_ S )
11 4 5 10 3syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( S + 1 ) <_ S )
12 1 pclem 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) )
13 peano2nn0 
 |-  ( S e. NN0 -> ( S + 1 ) e. NN0 )
14 oveq2 
 |-  ( x = ( S + 1 ) -> ( P ^ x ) = ( P ^ ( S + 1 ) ) )
15 14 breq1d 
 |-  ( x = ( S + 1 ) -> ( ( P ^ x ) || N <-> ( P ^ ( S + 1 ) ) || N ) )
16 oveq2 
 |-  ( n = x -> ( P ^ n ) = ( P ^ x ) )
17 16 breq1d 
 |-  ( n = x -> ( ( P ^ n ) || N <-> ( P ^ x ) || N ) )
18 17 cbvrabv 
 |-  { n e. NN0 | ( P ^ n ) || N } = { x e. NN0 | ( P ^ x ) || N }
19 1 18 eqtri 
 |-  A = { x e. NN0 | ( P ^ x ) || N }
20 15 19 elrab2 
 |-  ( ( S + 1 ) e. A <-> ( ( S + 1 ) e. NN0 /\ ( P ^ ( S + 1 ) ) || N ) )
21 20 simplbi2 
 |-  ( ( S + 1 ) e. NN0 -> ( ( P ^ ( S + 1 ) ) || N -> ( S + 1 ) e. A ) )
22 4 13 21 3syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( P ^ ( S + 1 ) ) || N -> ( S + 1 ) e. A ) )
23 suprzub 
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ ( S + 1 ) e. A ) -> ( S + 1 ) <_ sup ( A , RR , < ) )
24 23 2 breqtrrdi 
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ ( S + 1 ) e. A ) -> ( S + 1 ) <_ S )
25 24 3expia 
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x ) -> ( ( S + 1 ) e. A -> ( S + 1 ) <_ S ) )
26 25 3adant2 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) -> ( ( S + 1 ) e. A -> ( S + 1 ) <_ S ) )
27 12 22 26 sylsyld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( P ^ ( S + 1 ) ) || N -> ( S + 1 ) <_ S ) )
28 11 27 mtod 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P ^ ( S + 1 ) ) || N )