This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem explt1d

Description: A nonnegative real number less than one raised to a positive integer is less than one. (Contributed by SN, 3-Jul-2025)

Ref Expression
Hypotheses explt1d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
explt1d.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
explt1d.0 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
explt1d.1 ⊢ ( 𝜑 → 𝐴 < 1 )
Assertion explt1d ( 𝜑 → ( 𝐴 ↑ 𝑁 ) < 1 )

Proof

Step Hyp Ref Expression
1 explt1d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 explt1d.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 explt1d.0 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
4 explt1d.1 ⊢ ( 𝜑 → 𝐴 < 1 )
5 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
6 5 breq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑ 𝑁 ) < ( 1 ↑ 𝑁 ) ↔ ( 0 ↑ 𝑁 ) < ( 1 ↑ 𝑁 ) ) )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ )
8 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 0 ≤ 𝐴 )
9 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
10 7 8 9 ne0gt0d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 0 < 𝐴 )
11 7 10 elrpd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ+ )
12 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℝ+ )
13 1rp ⊢ 1 ∈ ℝ+
14 13 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ+ ) → 1 ∈ ℝ+ )
15 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ+ ) → 𝑁 ∈ ℕ )
16 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ+ ) → 𝐴 < 1 )
17 12 14 15 16 ltexp1dd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ+ ) → ( 𝐴 ↑ 𝑁 ) < ( 1 ↑ 𝑁 ) )
18 11 17 syldan ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑ 𝑁 ) < ( 1 ↑ 𝑁 ) )
19 0lt1 ⊢ 0 < 1
20 19 a1i ⊢ ( 𝜑 → 0 < 1 )
21 2 0expd ⊢ ( 𝜑 → ( 0 ↑ 𝑁 ) = 0 )
22 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
23 1exp ⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
24 22 23 syl ⊢ ( 𝜑 → ( 1 ↑ 𝑁 ) = 1 )
25 20 21 24 3brtr4d ⊢ ( 𝜑 → ( 0 ↑ 𝑁 ) < ( 1 ↑ 𝑁 ) )
26 6 18 25 pm2.61ne ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) < ( 1 ↑ 𝑁 ) )
27 26 24 breqtrd ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) < 1 )