Metamath Proof Explorer

Theorem pw2m1lepw2m1

Description: 2 to the power of a positive integer decreased by 1 is less than or equal to 2 to the power of the integer minus 1. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion pw2m1lepw2m1 
|- ( I e. NN -> ( 2 ^ ( I - 1 ) ) <_ ( ( 2 ^ I ) - 1 ) )

Proof

Step Hyp Ref Expression
1 1lt2 
 |-  1 < 2
2 nncn 
 |-  ( I e. NN -> I e. CC )
3 1cnd 
 |-  ( I e. NN -> 1 e. CC )
4 2 3 nncand 
 |-  ( I e. NN -> ( I - ( I - 1 ) ) = 1 )
5 4 oveq2d 
 |-  ( I e. NN -> ( 2 ^ ( I - ( I - 1 ) ) ) = ( 2 ^ 1 ) )
6 2cn 
 |-  2 e. CC
7 6 a1i 
 |-  ( I e. NN -> 2 e. CC )
8 2ne0 
 |-  2 =/= 0
9 8 a1i 
 |-  ( I e. NN -> 2 =/= 0 )
10 nnz 
 |-  ( I e. NN -> I e. ZZ )
11 peano2zm 
 |-  ( I e. ZZ -> ( I - 1 ) e. ZZ )
12 10 11 syl 
 |-  ( I e. NN -> ( I - 1 ) e. ZZ )
13 7 9 12 10 expsubd 
 |-  ( I e. NN -> ( 2 ^ ( I - ( I - 1 ) ) ) = ( ( 2 ^ I ) / ( 2 ^ ( I - 1 ) ) ) )
14 exp1 
 |-  ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
15 6 14 mp1i 
 |-  ( I e. NN -> ( 2 ^ 1 ) = 2 )
16 5 13 15 3eqtr3d 
 |-  ( I e. NN -> ( ( 2 ^ I ) / ( 2 ^ ( I - 1 ) ) ) = 2 )
17 1 16 breqtrrid 
 |-  ( I e. NN -> 1 < ( ( 2 ^ I ) / ( 2 ^ ( I - 1 ) ) ) )
18 2nn 
 |-  2 e. NN
19 18 a1i 
 |-  ( I e. NN -> 2 e. NN )
20 nnm1nn0 
 |-  ( I e. NN -> ( I - 1 ) e. NN0 )
21 19 20 nnexpcld 
 |-  ( I e. NN -> ( 2 ^ ( I - 1 ) ) e. NN )
22 21 nnrpd 
 |-  ( I e. NN -> ( 2 ^ ( I - 1 ) ) e. RR+ )
23 2z 
 |-  2 e. ZZ
24 nnnn0 
 |-  ( I e. NN -> I e. NN0 )
25 zexpcl 
 |-  ( ( 2 e. ZZ /\ I e. NN0 ) -> ( 2 ^ I ) e. ZZ )
26 23 24 25 sylancr 
 |-  ( I e. NN -> ( 2 ^ I ) e. ZZ )
27 26 zred 
 |-  ( I e. NN -> ( 2 ^ I ) e. RR )
28 divgt1b 
 |-  ( ( ( 2 ^ ( I - 1 ) ) e. RR+ /\ ( 2 ^ I ) e. RR ) -> ( ( 2 ^ ( I - 1 ) ) < ( 2 ^ I ) <-> 1 < ( ( 2 ^ I ) / ( 2 ^ ( I - 1 ) ) ) ) )
29 22 27 28 syl2anc 
 |-  ( I e. NN -> ( ( 2 ^ ( I - 1 ) ) < ( 2 ^ I ) <-> 1 < ( ( 2 ^ I ) / ( 2 ^ ( I - 1 ) ) ) ) )
30 17 29 mpbird 
 |-  ( I e. NN -> ( 2 ^ ( I - 1 ) ) < ( 2 ^ I ) )
31 21 nnzd 
 |-  ( I e. NN -> ( 2 ^ ( I - 1 ) ) e. ZZ )
32 zltlem1 
 |-  ( ( ( 2 ^ ( I - 1 ) ) e. ZZ /\ ( 2 ^ I ) e. ZZ ) -> ( ( 2 ^ ( I - 1 ) ) < ( 2 ^ I ) <-> ( 2 ^ ( I - 1 ) ) <_ ( ( 2 ^ I ) - 1 ) ) )
33 31 26 32 syl2anc 
 |-  ( I e. NN -> ( ( 2 ^ ( I - 1 ) ) < ( 2 ^ I ) <-> ( 2 ^ ( I - 1 ) ) <_ ( ( 2 ^ I ) - 1 ) ) )
34 30 33 mpbid 
 |-  ( I e. NN -> ( 2 ^ ( I - 1 ) ) <_ ( ( 2 ^ I ) - 1 ) )