Metamath Proof Explorer

Theorem jm2.17c

Description: Second half of lemma 2.17 of JonesMatijasevic p. 696. (Contributed by Stefan O'Rear, 15-Oct-2014)

Ref Expression
Assertion jm2.17c 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( ( N + 1 ) + 1 ) ) < ( ( 2 x. A ) ^ ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
3 2 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> A e. RR )
4 remulcl 
 |-  ( ( 2 e. RR /\ A e. RR ) -> ( 2 x. A ) e. RR )
5 1 3 4 sylancr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 2 x. A ) e. RR )
6 nnz 
 |-  ( N e. NN -> N e. ZZ )
7 6 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. ZZ )
8 7 peano2zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( N + 1 ) e. ZZ )
9 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
10 9 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N + 1 ) e. ZZ ) -> ( A rmY ( N + 1 ) ) e. ZZ )
11 10 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N + 1 ) e. ZZ ) -> ( A rmY ( N + 1 ) ) e. RR )
12 8 11 syldan 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( N + 1 ) ) e. RR )
13 5 12 remulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) e. RR )
14 nncn 
 |-  ( N e. NN -> N e. CC )
15 14 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. CC )
16 ax-1cn 
 |-  1 e. CC
17 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
18 15 16 17 sylancl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( N + 1 ) - 1 ) = N )
19 18 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( ( N + 1 ) - 1 ) ) = ( A rmY N ) )
20 9 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
21 20 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. RR )
22 6 21 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY N ) e. RR )
23 19 22 eqeltrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( ( N + 1 ) - 1 ) ) e. RR )
24 13 23 resubcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) - ( A rmY ( ( N + 1 ) - 1 ) ) ) e. RR )
25 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
26 25 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. NN0 )
27 5 26 reexpcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. A ) ^ N ) e. RR )
28 5 27 remulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. A ) x. ( ( 2 x. A ) ^ N ) ) e. RR )
29 rmy0 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )
30 29 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY 0 ) = 0 )
31 nngt0 
 |-  ( N e. NN -> 0 < N )
32 31 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 < N )
33 simpl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> A e. ( ZZ>= ` 2 ) )
34 0zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 e. ZZ )
35 ltrmy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ /\ N e. ZZ ) -> ( 0 < N <-> ( A rmY 0 ) < ( A rmY N ) ) )
36 33 34 7 35 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 0 < N <-> ( A rmY 0 ) < ( A rmY N ) ) )
37 32 36 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY 0 ) < ( A rmY N ) )
38 30 37 eqbrtrrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 < ( A rmY N ) )
39 38 19 breqtrrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 < ( A rmY ( ( N + 1 ) - 1 ) ) )
40 23 13 ltsubposd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 0 < ( A rmY ( ( N + 1 ) - 1 ) ) <-> ( ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) - ( A rmY ( ( N + 1 ) - 1 ) ) ) < ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) ) )
41 39 40 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) - ( A rmY ( ( N + 1 ) - 1 ) ) ) < ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) )
42 jm2.17b 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A rmY ( N + 1 ) ) <_ ( ( 2 x. A ) ^ N ) )
43 25 42 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( N + 1 ) ) <_ ( ( 2 x. A ) ^ N ) )
44 2nn 
 |-  2 e. NN
45 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
46 nnmulcl 
 |-  ( ( 2 e. NN /\ A e. NN ) -> ( 2 x. A ) e. NN )
47 44 45 46 sylancr 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 2 x. A ) e. NN )
48 47 nngt0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 < ( 2 x. A ) )
49 48 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 < ( 2 x. A ) )
50 lemul2 
 |-  ( ( ( A rmY ( N + 1 ) ) e. RR /\ ( ( 2 x. A ) ^ N ) e. RR /\ ( ( 2 x. A ) e. RR /\ 0 < ( 2 x. A ) ) ) -> ( ( A rmY ( N + 1 ) ) <_ ( ( 2 x. A ) ^ N ) <-> ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) <_ ( ( 2 x. A ) x. ( ( 2 x. A ) ^ N ) ) ) )
51 12 27 5 49 50 syl112anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY ( N + 1 ) ) <_ ( ( 2 x. A ) ^ N ) <-> ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) <_ ( ( 2 x. A ) x. ( ( 2 x. A ) ^ N ) ) ) )
52 43 51 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) <_ ( ( 2 x. A ) x. ( ( 2 x. A ) ^ N ) ) )
53 24 13 28 41 52 ltletrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) - ( A rmY ( ( N + 1 ) - 1 ) ) ) < ( ( 2 x. A ) x. ( ( 2 x. A ) ^ N ) ) )
54 rmyluc2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N + 1 ) e. ZZ ) -> ( A rmY ( ( N + 1 ) + 1 ) ) = ( ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) - ( A rmY ( ( N + 1 ) - 1 ) ) ) )
55 8 54 syldan 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( ( N + 1 ) + 1 ) ) = ( ( ( 2 x. A ) x. ( A rmY ( N + 1 ) ) ) - ( A rmY ( ( N + 1 ) - 1 ) ) ) )
56 5 recnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 2 x. A ) e. CC )
57 56 26 expp1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. A ) ^ ( N + 1 ) ) = ( ( ( 2 x. A ) ^ N ) x. ( 2 x. A ) ) )
58 27 recnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. A ) ^ N ) e. CC )
59 58 56 mulcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( 2 x. A ) ^ N ) x. ( 2 x. A ) ) = ( ( 2 x. A ) x. ( ( 2 x. A ) ^ N ) ) )
60 57 59 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. A ) ^ ( N + 1 ) ) = ( ( 2 x. A ) x. ( ( 2 x. A ) ^ N ) ) )
61 53 55 60 3brtr4d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( ( N + 1 ) + 1 ) ) < ( ( 2 x. A ) ^ ( N + 1 ) ) )