Theorem expgt1

Description: Positive integer exponentiation with a mantissa greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005) (Revised by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	expgt1	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 1 < ( A ^ N ) )

Proof

Step	Hyp	Ref	Expression
1		1re	|- 1 e. RR
2	1	a1i	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 1 e. RR )
3		simp1	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> A e. RR )
4		simp2	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> N e. NN )
5	4	nnnn0d	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> N e. NN0 )
6		reexpcl	|- ( ( A e. RR /\ N e. NN0 ) -> ( A ^ N ) e. RR )
7	3 5 6	syl2anc	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> ( A ^ N ) e. RR )
8		simp3	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 1 < A )
9		nnm1nn0	|- ( N e. NN -> ( N - 1 ) e. NN0 )
10	4 9	syl	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> ( N - 1 ) e. NN0 )
11		ltle	|- ( ( 1 e. RR /\ A e. RR ) -> ( 1 < A -> 1 <_ A ) )
12	1 3 11	sylancr	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> ( 1 < A -> 1 <_ A ) )
13	8 12	mpd	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 1 <_ A )
14		expge1	|- ( ( A e. RR /\ ( N - 1 ) e. NN0 /\ 1 <_ A ) -> 1 <_ ( A ^ ( N - 1 ) ) )
15	3 10 13 14	syl3anc	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 1 <_ ( A ^ ( N - 1 ) ) )
16		reexpcl	|- ( ( A e. RR /\ ( N - 1 ) e. NN0 ) -> ( A ^ ( N - 1 ) ) e. RR )
17	3 10 16	syl2anc	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> ( A ^ ( N - 1 ) ) e. RR )
18		0red	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 0 e. RR )
19		0lt1	|- 0 < 1
20	19	a1i	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 0 < 1 )
21	18 2 3 20 8	lttrd	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 0 < A )
22		lemul1	|- ( ( 1 e. RR /\ ( A ^ ( N - 1 ) ) e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( 1 <_ ( A ^ ( N - 1 ) ) <-> ( 1 x. A ) <_ ( ( A ^ ( N - 1 ) ) x. A ) ) )
23	2 17 3 21 22	syl112anc	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> ( 1 <_ ( A ^ ( N - 1 ) ) <-> ( 1 x. A ) <_ ( ( A ^ ( N - 1 ) ) x. A ) ) )
24	15 23	mpbid	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> ( 1 x. A ) <_ ( ( A ^ ( N - 1 ) ) x. A ) )
25		recn	|- ( A e. RR -> A e. CC )
26	25	3ad2ant1	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> A e. CC )
27	26	mulid2d	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> ( 1 x. A ) = A )
28	27	eqcomd	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> A = ( 1 x. A ) )
29		expm1t	|- ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = ( ( A ^ ( N - 1 ) ) x. A ) )
30	26 4 29	syl2anc	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> ( A ^ N ) = ( ( A ^ ( N - 1 ) ) x. A ) )
31	24 28 30	3brtr4d	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> A <_ ( A ^ N ) )
32	2 3 7 8 31	ltletrd	|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 1 < ( A ^ N ) )