Metamath Proof Explorer

Theorem expubnd

Description: An upper bound on A ^ N when 2 <_ A . (Contributed by NM, 19-Dec-2005)

Ref Expression
Assertion expubnd 
|- ( ( A e. RR /\ N e. NN0 /\ 2 <_ A ) -> ( A ^ N ) <_ ( ( 2 ^ N ) x. ( ( A - 1 ) ^ N ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. RR /\ N e. NN0 /\ 2 <_ A ) -> A e. RR )
2 2re 
 |-  2 e. RR
3 peano2rem 
 |-  ( A e. RR -> ( A - 1 ) e. RR )
4 remulcl 
 |-  ( ( 2 e. RR /\ ( A - 1 ) e. RR ) -> ( 2 x. ( A - 1 ) ) e. RR )
5 2 3 4 sylancr 
 |-  ( A e. RR -> ( 2 x. ( A - 1 ) ) e. RR )
6 5 3ad2ant1 
 |-  ( ( A e. RR /\ N e. NN0 /\ 2 <_ A ) -> ( 2 x. ( A - 1 ) ) e. RR )
7 simp2 
 |-  ( ( A e. RR /\ N e. NN0 /\ 2 <_ A ) -> N e. NN0 )
8 0le2 
 |-  0 <_ 2
9 0re 
 |-  0 e. RR
10 letr 
 |-  ( ( 0 e. RR /\ 2 e. RR /\ A e. RR ) -> ( ( 0 <_ 2 /\ 2 <_ A ) -> 0 <_ A ) )
11 9 2 10 mp3an12 
 |-  ( A e. RR -> ( ( 0 <_ 2 /\ 2 <_ A ) -> 0 <_ A ) )
12 8 11 mpani 
 |-  ( A e. RR -> ( 2 <_ A -> 0 <_ A ) )
13 12 imp 
 |-  ( ( A e. RR /\ 2 <_ A ) -> 0 <_ A )
14 resubcl 
 |-  ( ( A e. RR /\ 2 e. RR ) -> ( A - 2 ) e. RR )
15 2 14 mpan2 
 |-  ( A e. RR -> ( A - 2 ) e. RR )
16 leadd2 
 |-  ( ( 2 e. RR /\ A e. RR /\ ( A - 2 ) e. RR ) -> ( 2 <_ A <-> ( ( A - 2 ) + 2 ) <_ ( ( A - 2 ) + A ) ) )
17 2 16 mp3an1 
 |-  ( ( A e. RR /\ ( A - 2 ) e. RR ) -> ( 2 <_ A <-> ( ( A - 2 ) + 2 ) <_ ( ( A - 2 ) + A ) ) )
18 15 17 mpdan 
 |-  ( A e. RR -> ( 2 <_ A <-> ( ( A - 2 ) + 2 ) <_ ( ( A - 2 ) + A ) ) )
19 18 biimpa 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( ( A - 2 ) + 2 ) <_ ( ( A - 2 ) + A ) )
20 recn 
 |-  ( A e. RR -> A e. CC )
21 2cn 
 |-  2 e. CC
22 npcan 
 |-  ( ( A e. CC /\ 2 e. CC ) -> ( ( A - 2 ) + 2 ) = A )
23 20 21 22 sylancl 
 |-  ( A e. RR -> ( ( A - 2 ) + 2 ) = A )
24 23 adantr 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( ( A - 2 ) + 2 ) = A )
25 ax-1cn 
 |-  1 e. CC
26 subdi 
 |-  ( ( 2 e. CC /\ A e. CC /\ 1 e. CC ) -> ( 2 x. ( A - 1 ) ) = ( ( 2 x. A ) - ( 2 x. 1 ) ) )
27 21 25 26 mp3an13 
 |-  ( A e. CC -> ( 2 x. ( A - 1 ) ) = ( ( 2 x. A ) - ( 2 x. 1 ) ) )
28 2times 
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )
29 2t1e2 
 |-  ( 2 x. 1 ) = 2
30 29 a1i 
 |-  ( A e. CC -> ( 2 x. 1 ) = 2 )
31 28 30 oveq12d 
 |-  ( A e. CC -> ( ( 2 x. A ) - ( 2 x. 1 ) ) = ( ( A + A ) - 2 ) )
32 addsub 
 |-  ( ( A e. CC /\ A e. CC /\ 2 e. CC ) -> ( ( A + A ) - 2 ) = ( ( A - 2 ) + A ) )
33 21 32 mp3an3 
 |-  ( ( A e. CC /\ A e. CC ) -> ( ( A + A ) - 2 ) = ( ( A - 2 ) + A ) )
34 33 anidms 
 |-  ( A e. CC -> ( ( A + A ) - 2 ) = ( ( A - 2 ) + A ) )
35 27 31 34 3eqtrrd 
 |-  ( A e. CC -> ( ( A - 2 ) + A ) = ( 2 x. ( A - 1 ) ) )
36 20 35 syl 
 |-  ( A e. RR -> ( ( A - 2 ) + A ) = ( 2 x. ( A - 1 ) ) )
37 36 adantr 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( ( A - 2 ) + A ) = ( 2 x. ( A - 1 ) ) )
38 19 24 37 3brtr3d 
 |-  ( ( A e. RR /\ 2 <_ A ) -> A <_ ( 2 x. ( A - 1 ) ) )
39 13 38 jca 
 |-  ( ( A e. RR /\ 2 <_ A ) -> ( 0 <_ A /\ A <_ ( 2 x. ( A - 1 ) ) ) )
40 39 3adant2 
 |-  ( ( A e. RR /\ N e. NN0 /\ 2 <_ A ) -> ( 0 <_ A /\ A <_ ( 2 x. ( A - 1 ) ) ) )
41 leexp1a 
 |-  ( ( ( A e. RR /\ ( 2 x. ( A - 1 ) ) e. RR /\ N e. NN0 ) /\ ( 0 <_ A /\ A <_ ( 2 x. ( A - 1 ) ) ) ) -> ( A ^ N ) <_ ( ( 2 x. ( A - 1 ) ) ^ N ) )
42 1 6 7 40 41 syl31anc 
 |-  ( ( A e. RR /\ N e. NN0 /\ 2 <_ A ) -> ( A ^ N ) <_ ( ( 2 x. ( A - 1 ) ) ^ N ) )
43 3 recnd 
 |-  ( A e. RR -> ( A - 1 ) e. CC )
44 mulexp 
 |-  ( ( 2 e. CC /\ ( A - 1 ) e. CC /\ N e. NN0 ) -> ( ( 2 x. ( A - 1 ) ) ^ N ) = ( ( 2 ^ N ) x. ( ( A - 1 ) ^ N ) ) )
45 21 44 mp3an1 
 |-  ( ( ( A - 1 ) e. CC /\ N e. NN0 ) -> ( ( 2 x. ( A - 1 ) ) ^ N ) = ( ( 2 ^ N ) x. ( ( A - 1 ) ^ N ) ) )
46 43 45 sylan 
 |-  ( ( A e. RR /\ N e. NN0 ) -> ( ( 2 x. ( A - 1 ) ) ^ N ) = ( ( 2 ^ N ) x. ( ( A - 1 ) ^ N ) ) )
47 46 3adant3 
 |-  ( ( A e. RR /\ N e. NN0 /\ 2 <_ A ) -> ( ( 2 x. ( A - 1 ) ) ^ N ) = ( ( 2 ^ N ) x. ( ( A - 1 ) ^ N ) ) )
48 42 47 breqtrd 
 |-  ( ( A e. RR /\ N e. NN0 /\ 2 <_ A ) -> ( A ^ N ) <_ ( ( 2 ^ N ) x. ( ( A - 1 ) ^ N ) ) )