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∈ℕ→2I−1≤2I−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∈ℕ→2I−I−1=21
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∈ℕ→2I−I−1=2I2I−1
14 exp1 ⊢2∈ℂ→21=2
15 6 14 mp1i ⊢I∈ℕ→21=2
16 5 13 15 3eqtr3d ⊢I∈ℕ→2I2I−1=2
17 1 16 breqtrrid ⊢I∈ℕ→1<2I2I−1
18 2nn ⊢2∈ℕ
19 18 a1i ⊢I∈ℕ→2∈ℕ
20 nnm1nn0 ⊢I∈ℕ→I−1∈ℕ0
21 19 20 nnexpcld ⊢I∈ℕ→2I−1∈ℕ
22 21 nnrpd ⊢I∈ℕ→2I−1∈ℝ+
23 2z ⊢2∈ℤ
24 nnnn0 ⊢I∈ℕ→I∈ℕ0
25 zexpcl ⊢2∈ℤ∧I∈ℕ0→2I∈ℤ
26 23 24 25 sylancr ⊢I∈ℕ→2I∈ℤ
27 26 zred ⊢I∈ℕ→2I∈ℝ
28 divgt1b ⊢2I−1∈ℝ+∧2I∈ℝ→2I−1<2I↔1<2I2I−1
29 22 27 28 syl2anc ⊢I∈ℕ→2I−1<2I↔1<2I2I−1
30 17 29 mpbird ⊢I∈ℕ→2I−1<2I
31 21 nnzd ⊢I∈ℕ→2I−1∈ℤ
32 zltlem1 ⊢2I−1∈ℤ∧2I∈ℤ→2I−1<2I↔2I−1≤2I−1
33 31 26 32 syl2anc ⊢I∈ℕ→2I−1<2I↔2I−1≤2I−1
34 30 33 mpbid ⊢I∈ℕ→2I−1≤2I−1