explt1d

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

Step	Hyp	Ref	Expression
1		explt1d.a	$⊢ φ \to A \in ℝ$
2		explt1d.n	$⊢ φ \to N \in ℕ$
3		explt1d.0	$⊢ φ \to 0 \leq A$
4		explt1d.1	$⊢ φ \to A < 1$
5		oveq1	$⊢ A = 0 \to A^{N} = 0^{N}$
6	5	breq1d	$⊢ A = 0 \to (A^{N} < 1^{N} \leftrightarrow 0^{N} < 1^{N})$
7	1	adantr	$⊢ (φ \land A \neq 0) \to A \in ℝ$
8	3	adantr	$⊢ (φ \land A \neq 0) \to 0 \leq A$
9		simpr	$⊢ (φ \land A \neq 0) \to A \neq 0$
10	7 8 9	ne0gt0d	$⊢ (φ \land A \neq 0) \to 0 < A$
11	7 10	elrpd	$⊢ (φ \land A \neq 0) \to A \in ℝ^{+}$
12		simpr	$⊢ (φ \land A \in ℝ^{+}) \to A \in ℝ^{+}$
13		1rp	$⊢ 1 \in ℝ^{+}$
14	13	a1i	$⊢ (φ \land A \in ℝ^{+}) \to 1 \in ℝ^{+}$
15	2	adantr	$⊢ (φ \land A \in ℝ^{+}) \to N \in ℕ$
16	4	adantr	$⊢ (φ \land A \in ℝ^{+}) \to A < 1$
17	12 14 15 16	ltexp1dd	$⊢ (φ \land A \in ℝ^{+}) \to A^{N} < 1^{N}$
18	11 17	syldan	$⊢ (φ \land A \neq 0) \to A^{N} < 1^{N}$
19		0lt1	$⊢ 0 < 1$
20	19	a1i	$⊢ φ \to 0 < 1$
21	2	0expd	$⊢ φ \to 0^{N} = 0$
22	2	nnzd	$⊢ φ \to N \in ℤ$
23		1exp	$⊢ N \in ℤ \to 1^{N} = 1$
24	22 23	syl	$⊢ φ \to 1^{N} = 1$
25	20 21 24	3brtr4d	$⊢ φ \to 0^{N} < 1^{N}$
26	6 18 25	pm2.61ne	$⊢ φ \to A^{N} < 1^{N}$
27	26 24	breqtrd	$⊢ φ \to A^{N} < 1$

Metamath Proof Explorer