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	⊢ ( 𝐼 ∈ ℕ → ( 2 ↑ ( 𝐼 − 1 ) ) ≤ ( ( 2 ↑ 𝐼 ) − 1 ) )

Proof

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