Metamath Proof Explorer

Theorem jm3.1lem1

Description: Lemma for jm3.1 . (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Hypotheses jm3.1.a 
|- ( ph -> A e. ( ZZ>= ` 2 ) )
jm3.1.b 
|- ( ph -> K e. ( ZZ>= ` 2 ) )
jm3.1.c 
|- ( ph -> N e. NN )
jm3.1.d 
|- ( ph -> ( K rmY ( N + 1 ) ) <_ A )
Assertion jm3.1lem1 
|- ( ph -> ( K ^ N ) < A )

Proof

Step Hyp Ref Expression
1 jm3.1.a 
 |-  ( ph -> A e. ( ZZ>= ` 2 ) )
2 jm3.1.b 
 |-  ( ph -> K e. ( ZZ>= ` 2 ) )
3 jm3.1.c 
 |-  ( ph -> N e. NN )
4 jm3.1.d 
 |-  ( ph -> ( K rmY ( N + 1 ) ) <_ A )
5 eluzelre 
 |-  ( K e. ( ZZ>= ` 2 ) -> K e. RR )
6 2 5 syl 
 |-  ( ph -> K e. RR )
7 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
8 6 7 reexpcld 
 |-  ( ph -> ( K ^ N ) e. RR )
9 2z 
 |-  2 e. ZZ
10 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
11 9 10 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
12 uz2mulcl 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) ) -> ( 2 x. K ) e. ( ZZ>= ` 2 ) )
13 11 2 12 sylancr 
 |-  ( ph -> ( 2 x. K ) e. ( ZZ>= ` 2 ) )
14 uz2m1nn 
 |-  ( ( 2 x. K ) e. ( ZZ>= ` 2 ) -> ( ( 2 x. K ) - 1 ) e. NN )
15 13 14 syl 
 |-  ( ph -> ( ( 2 x. K ) - 1 ) e. NN )
16 15 nnred 
 |-  ( ph -> ( ( 2 x. K ) - 1 ) e. RR )
17 16 7 reexpcld 
 |-  ( ph -> ( ( ( 2 x. K ) - 1 ) ^ N ) e. RR )
18 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
19 1 18 syl 
 |-  ( ph -> A e. RR )
20 uz2m1nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> ( K - 1 ) e. NN )
21 2 20 syl 
 |-  ( ph -> ( K - 1 ) e. NN )
22 21 nngt0d 
 |-  ( ph -> 0 < ( K - 1 ) )
23 2cn 
 |-  2 e. CC
24 6 recnd 
 |-  ( ph -> K e. CC )
25 mulcl 
 |-  ( ( 2 e. CC /\ K e. CC ) -> ( 2 x. K ) e. CC )
26 23 24 25 sylancr 
 |-  ( ph -> ( 2 x. K ) e. CC )
27 1cnd 
 |-  ( ph -> 1 e. CC )
28 26 27 24 sub32d 
 |-  ( ph -> ( ( ( 2 x. K ) - 1 ) - K ) = ( ( ( 2 x. K ) - K ) - 1 ) )
29 24 2timesd 
 |-  ( ph -> ( 2 x. K ) = ( K + K ) )
30 24 24 29 mvrladdd 
 |-  ( ph -> ( ( 2 x. K ) - K ) = K )
31 30 oveq1d 
 |-  ( ph -> ( ( ( 2 x. K ) - K ) - 1 ) = ( K - 1 ) )
32 28 31 eqtrd 
 |-  ( ph -> ( ( ( 2 x. K ) - 1 ) - K ) = ( K - 1 ) )
33 22 32 breqtrrd 
 |-  ( ph -> 0 < ( ( ( 2 x. K ) - 1 ) - K ) )
34 6 16 posdifd 
 |-  ( ph -> ( K < ( ( 2 x. K ) - 1 ) <-> 0 < ( ( ( 2 x. K ) - 1 ) - K ) ) )
35 33 34 mpbird 
 |-  ( ph -> K < ( ( 2 x. K ) - 1 ) )
36 eluz2nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> K e. NN )
37 2 36 syl 
 |-  ( ph -> K e. NN )
38 37 nnrpd 
 |-  ( ph -> K e. RR+ )
39 15 nnrpd 
 |-  ( ph -> ( ( 2 x. K ) - 1 ) e. RR+ )
40 rpexpmord 
 |-  ( ( N e. NN /\ K e. RR+ /\ ( ( 2 x. K ) - 1 ) e. RR+ ) -> ( K < ( ( 2 x. K ) - 1 ) <-> ( K ^ N ) < ( ( ( 2 x. K ) - 1 ) ^ N ) ) )
41 3 38 39 40 syl3anc 
 |-  ( ph -> ( K < ( ( 2 x. K ) - 1 ) <-> ( K ^ N ) < ( ( ( 2 x. K ) - 1 ) ^ N ) ) )
42 35 41 mpbid 
 |-  ( ph -> ( K ^ N ) < ( ( ( 2 x. K ) - 1 ) ^ N ) )
43 3 nnzd 
 |-  ( ph -> N e. ZZ )
44 43 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
45 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
46 45 fovcl 
 |-  ( ( K e. ( ZZ>= ` 2 ) /\ ( N + 1 ) e. ZZ ) -> ( K rmY ( N + 1 ) ) e. ZZ )
47 2 44 46 syl2anc 
 |-  ( ph -> ( K rmY ( N + 1 ) ) e. ZZ )
48 47 zred 
 |-  ( ph -> ( K rmY ( N + 1 ) ) e. RR )
49 jm2.17a 
 |-  ( ( K e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( ( ( 2 x. K ) - 1 ) ^ N ) <_ ( K rmY ( N + 1 ) ) )
50 2 7 49 syl2anc 
 |-  ( ph -> ( ( ( 2 x. K ) - 1 ) ^ N ) <_ ( K rmY ( N + 1 ) ) )
51 17 48 19 50 4 letrd 
 |-  ( ph -> ( ( ( 2 x. K ) - 1 ) ^ N ) <_ A )
52 8 17 19 42 51 ltletrd 
 |-  ( ph -> ( K ^ N ) < A )