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	|- ( ph -> A e. RR )
	explt1d.n	|- ( ph -> N e. NN )
	explt1d.0	|- ( ph -> 0 <_ A )
	explt1d.1	|- ( ph -> A < 1 )
Assertion	explt1d	|- ( ph -> ( A ^ N ) < 1 )

Proof

Step	Hyp	Ref	Expression
1		explt1d.a	|- ( ph -> A e. RR )
2		explt1d.n	|- ( ph -> N e. NN )
3		explt1d.0	|- ( ph -> 0 <_ A )
4		explt1d.1	|- ( ph -> A < 1 )
5		oveq1	|- ( A = 0 -> ( A ^ N ) = ( 0 ^ N ) )
6	5	breq1d	|- ( A = 0 -> ( ( A ^ N ) < ( 1 ^ N ) <-> ( 0 ^ N ) < ( 1 ^ N ) ) )
7	1	adantr	|- ( ( ph /\ A =/= 0 ) -> A e. RR )
8	3	adantr	|- ( ( ph /\ A =/= 0 ) -> 0 <_ A )
9		simpr	|- ( ( ph /\ A =/= 0 ) -> A =/= 0 )
10	7 8 9	ne0gt0d	|- ( ( ph /\ A =/= 0 ) -> 0 < A )
11	7 10	elrpd	|- ( ( ph /\ A =/= 0 ) -> A e. RR+ )
12		simpr	|- ( ( ph /\ A e. RR+ ) -> A e. RR+ )
13		1rp	|- 1 e. RR+
14	13	a1i	|- ( ( ph /\ A e. RR+ ) -> 1 e. RR+ )
15	2	adantr	|- ( ( ph /\ A e. RR+ ) -> N e. NN )
16	4	adantr	|- ( ( ph /\ A e. RR+ ) -> A < 1 )
17	12 14 15 16	ltexp1dd	|- ( ( ph /\ A e. RR+ ) -> ( A ^ N ) < ( 1 ^ N ) )
18	11 17	syldan	|- ( ( ph /\ A =/= 0 ) -> ( A ^ N ) < ( 1 ^ N ) )
19		0lt1	|- 0 < 1
20	19	a1i	|- ( ph -> 0 < 1 )
21	2	0expd	|- ( ph -> ( 0 ^ N ) = 0 )
22	2	nnzd	|- ( ph -> N e. ZZ )
23		1exp	|- ( N e. ZZ -> ( 1 ^ N ) = 1 )
24	22 23	syl	|- ( ph -> ( 1 ^ N ) = 1 )
25	20 21 24	3brtr4d	|- ( ph -> ( 0 ^ N ) < ( 1 ^ N ) )
26	6 18 25	pm2.61ne	|- ( ph -> ( A ^ N ) < ( 1 ^ N ) )
27	26 24	breqtrd	|- ( ph -> ( A ^ N ) < 1 )