expgt1

Description: A real greater than 1 raised to a positive integer is greater than 1. (Contributed by NM, 13-Feb-2005) (Revised by Mario Carneiro, 4-Jun-2014)

		Ref	Expression
	Assertion	expgt1	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 1 < A^{N}$

Proof

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2	1	a1i	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 1 \in ℝ$
3		simp1	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to A \in ℝ$
4		simp2	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to N \in ℕ$
5	4	nnnn0d	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to N \in ℕ_{0}$
6		reexpcl	$⊢ (A \in ℝ \land N \in ℕ_{0}) \to A^{N} \in ℝ$
7	3 5 6	syl2anc	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to A^{N} \in ℝ$
8		simp3	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 1 < A$
9		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
10	4 9	syl	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to N - 1 \in ℕ_{0}$
11		ltle	$⊢ (1 \in ℝ \land A \in ℝ) \to (1 < A \to 1 \leq A)$
12	1 3 11	sylancr	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to (1 < A \to 1 \leq A)$
13	8 12	mpd	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 1 \leq A$
14		expge1	$⊢ (A \in ℝ \land N - 1 \in ℕ_{0} \land 1 \leq A) \to 1 \leq A^{N - 1}$
15	3 10 13 14	syl3anc	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 1 \leq A^{N - 1}$
16		reexpcl	$⊢ (A \in ℝ \land N - 1 \in ℕ_{0}) \to A^{N - 1} \in ℝ$
17	3 10 16	syl2anc	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to A^{N - 1} \in ℝ$
18		0red	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 0 \in ℝ$
19		0lt1	$⊢ 0 < 1$
20	19	a1i	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 0 < 1$
21	18 2 3 20 8	lttrd	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 0 < A$
22		lemul1	$⊢ (1 \in ℝ \land A^{N - 1} \in ℝ \land (A \in ℝ \land 0 < A)) \to (1 \leq A^{N - 1} \leftrightarrow 1 A \leq A^{N - 1} A)$
23	2 17 3 21 22	syl112anc	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to (1 \leq A^{N - 1} \leftrightarrow 1 A \leq A^{N - 1} A)$
24	15 23	mpbid	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 1 A \leq A^{N - 1} A$
25		recn	$⊢ A \in ℝ \to A \in ℂ$
26	25	3ad2ant1	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to A \in ℂ$
27	26	mullidd	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 1 A = A$
28	27	eqcomd	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to A = 1 A$
29		expm1t	$⊢ (A \in ℂ \land N \in ℕ) \to A^{N} = A^{N - 1} A$
30	26 4 29	syl2anc	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to A^{N} = A^{N - 1} A$
31	24 28 30	3brtr4d	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to A \leq A^{N}$
32	2 3 7 8 31	ltletrd	$⊢ (A \in ℝ \land N \in ℕ \land 1 < A) \to 1 < A^{N}$

Metamath Proof Explorer

Theorem expgt1

Proof