Metamath Proof Explorer

Theorem pclem

Description: - Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Hypothesis pclem.1 
|- A = { n e. NN0 | ( P ^ n ) || N }
Assertion pclem 
|- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) )

Proof

Step Hyp Ref Expression
1 pclem.1 
 |-  A = { n e. NN0 | ( P ^ n ) || N }
2 1 ssrab3 
 |-  A C_ NN0
3 nn0ssz 
 |-  NN0 C_ ZZ
4 2 3 sstri 
 |-  A C_ ZZ
5 4 a1i 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> A C_ ZZ )
6 0nn0 
 |-  0 e. NN0
7 6 a1i 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> 0 e. NN0 )
8 eluzelcn 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. CC )
9 8 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> P e. CC )
10 9 exp0d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ 0 ) = 1 )
11 1dvds 
 |-  ( N e. ZZ -> 1 || N )
12 11 ad2antrl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> 1 || N )
13 10 12 eqbrtrd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ 0 ) || N )
14 oveq2 
 |-  ( n = 0 -> ( P ^ n ) = ( P ^ 0 ) )
15 14 breq1d 
 |-  ( n = 0 -> ( ( P ^ n ) || N <-> ( P ^ 0 ) || N ) )
16 15 1 elrab2 
 |-  ( 0 e. A <-> ( 0 e. NN0 /\ ( P ^ 0 ) || N ) )
17 7 13 16 sylanbrc 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> 0 e. A )
18 17 ne0d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> A =/= (/) )
19 nnssz 
 |-  NN C_ ZZ
20 zcn 
 |-  ( N e. ZZ -> N e. CC )
21 20 abscld 
 |-  ( N e. ZZ -> ( abs ` N ) e. RR )
22 21 ad2antrl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( abs ` N ) e. RR )
23 eluzelre 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. RR )
24 23 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> P e. RR )
25 eluz2gt1 
 |-  ( P e. ( ZZ>= ` 2 ) -> 1 < P )
26 25 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> 1 < P )
27 expnbnd 
 |-  ( ( ( abs ` N ) e. RR /\ P e. RR /\ 1 < P ) -> E. x e. NN ( abs ` N ) < ( P ^ x ) )
28 22 24 26 27 syl3anc 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> E. x e. NN ( abs ` N ) < ( P ^ x ) )
29 simprr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> y e. A )
30 oveq2 
 |-  ( n = y -> ( P ^ n ) = ( P ^ y ) )
31 30 breq1d 
 |-  ( n = y -> ( ( P ^ n ) || N <-> ( P ^ y ) || N ) )
32 31 1 elrab2 
 |-  ( y e. A <-> ( y e. NN0 /\ ( P ^ y ) || N ) )
33 29 32 sylib 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( y e. NN0 /\ ( P ^ y ) || N ) )
34 33 simprd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( P ^ y ) || N )
35 eluz2nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. NN )
36 35 ad2antrr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> P e. NN )
37 33 simpld 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> y e. NN0 )
38 36 37 nnexpcld 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( P ^ y ) e. NN )
39 38 nnzd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( P ^ y ) e. ZZ )
40 simplrl 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> N e. ZZ )
41 simplrr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> N =/= 0 )
42 dvdsleabs 
 |-  ( ( ( P ^ y ) e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( ( P ^ y ) || N -> ( P ^ y ) <_ ( abs ` N ) ) )
43 39 40 41 42 syl3anc 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( ( P ^ y ) || N -> ( P ^ y ) <_ ( abs ` N ) ) )
44 34 43 mpd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( P ^ y ) <_ ( abs ` N ) )
45 38 nnred 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( P ^ y ) e. RR )
46 22 adantr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( abs ` N ) e. RR )
47 23 ad2antrr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> P e. RR )
48 nnnn0 
 |-  ( x e. NN -> x e. NN0 )
49 48 ad2antrl 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> x e. NN0 )
50 47 49 reexpcld 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( P ^ x ) e. RR )
51 lelttr 
 |-  ( ( ( P ^ y ) e. RR /\ ( abs ` N ) e. RR /\ ( P ^ x ) e. RR ) -> ( ( ( P ^ y ) <_ ( abs ` N ) /\ ( abs ` N ) < ( P ^ x ) ) -> ( P ^ y ) < ( P ^ x ) ) )
52 45 46 50 51 syl3anc 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( ( ( P ^ y ) <_ ( abs ` N ) /\ ( abs ` N ) < ( P ^ x ) ) -> ( P ^ y ) < ( P ^ x ) ) )
53 44 52 mpand 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( ( abs ` N ) < ( P ^ x ) -> ( P ^ y ) < ( P ^ x ) ) )
54 37 nn0zd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> y e. ZZ )
55 nnz 
 |-  ( x e. NN -> x e. ZZ )
56 55 ad2antrl 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> x e. ZZ )
57 25 ad2antrr 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> 1 < P )
58 47 54 56 57 ltexp2d 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( y < x <-> ( P ^ y ) < ( P ^ x ) ) )
59 53 58 sylibrd 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( ( abs ` N ) < ( P ^ x ) -> y < x ) )
60 37 nn0red 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> y e. RR )
61 nnre 
 |-  ( x e. NN -> x e. RR )
62 61 ad2antrl 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> x e. RR )
63 ltle 
 |-  ( ( y e. RR /\ x e. RR ) -> ( y < x -> y <_ x ) )
64 60 62 63 syl2anc 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( y < x -> y <_ x ) )
65 59 64 syld 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( x e. NN /\ y e. A ) ) -> ( ( abs ` N ) < ( P ^ x ) -> y <_ x ) )
66 65 anassrs 
 |-  ( ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ x e. NN ) /\ y e. A ) -> ( ( abs ` N ) < ( P ^ x ) -> y <_ x ) )
67 66 ralrimdva 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ x e. NN ) -> ( ( abs ` N ) < ( P ^ x ) -> A. y e. A y <_ x ) )
68 67 reximdva 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( E. x e. NN ( abs ` N ) < ( P ^ x ) -> E. x e. NN A. y e. A y <_ x ) )
69 28 68 mpd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> E. x e. NN A. y e. A y <_ x )
70 ssrexv 
 |-  ( NN C_ ZZ -> ( E. x e. NN A. y e. A y <_ x -> E. x e. ZZ A. y e. A y <_ x ) )
71 19 69 70 mpsyl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> E. x e. ZZ A. y e. A y <_ x )
72 5 18 71 3jca 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) )