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	$$⊢\phi \to A\in ℝ$$
	explt1d.n	$$⊢\phi \to N\in \mathbb{N}$$
	explt1d.0	$$⊢\phi \to 0\le A$$
	explt1d.1	$$⊢\phi \to A<1$$
Assertion	explt1d	$$⊢\phi \to A^N<1$$

Proof

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