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 2 I 1 2 I 1

Proof

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