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