expmordi

Description: Base ordering relationship for exponentiation of nonnegative reals to a fixed positive integer power. (Contributed by Stefan O'Rear, 16-Oct-2014)

		Ref	Expression
	Assertion	expmordi	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B) \land N \in ℕ) \to A^{N} < B^{N}$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ a = 1 \to A^{a} = A^{1}$
2		oveq2	$⊢ a = 1 \to B^{a} = B^{1}$
3	1 2	breq12d	$⊢ a = 1 \to (A^{a} < B^{a} \leftrightarrow A^{1} < B^{1})$
4	3	imbi2d	$⊢ a = 1 \to ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{a} < B^{a}) \leftrightarrow (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{1} < B^{1}))$
5		oveq2	$⊢ a = b \to A^{a} = A^{b}$
6		oveq2	$⊢ a = b \to B^{a} = B^{b}$
7	5 6	breq12d	$⊢ a = b \to (A^{a} < B^{a} \leftrightarrow A^{b} < B^{b})$
8	7	imbi2d	$⊢ a = b \to ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{a} < B^{a}) \leftrightarrow (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{b} < B^{b}))$
9		oveq2	$⊢ a = b + 1 \to A^{a} = A^{b + 1}$
10		oveq2	$⊢ a = b + 1 \to B^{a} = B^{b + 1}$
11	9 10	breq12d	$⊢ a = b + 1 \to (A^{a} < B^{a} \leftrightarrow A^{b + 1} < B^{b + 1})$
12	11	imbi2d	$⊢ a = b + 1 \to ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{a} < B^{a}) \leftrightarrow (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{b + 1} < B^{b + 1}))$
13		oveq2	$⊢ a = N \to A^{a} = A^{N}$
14		oveq2	$⊢ a = N \to B^{a} = B^{N}$
15	13 14	breq12d	$⊢ a = N \to (A^{a} < B^{a} \leftrightarrow A^{N} < B^{N})$
16	15	imbi2d	$⊢ a = N \to ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{a} < B^{a}) \leftrightarrow (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{N} < B^{N}))$
17		recn	$⊢ A \in ℝ \to A \in ℂ$
18		recn	$⊢ B \in ℝ \to B \in ℂ$
19		exp1	$⊢ A \in ℂ \to A^{1} = A$
20		exp1	$⊢ B \in ℂ \to B^{1} = B$
21	19 20	breqan12d	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{1} < B^{1} \leftrightarrow A < B)$
22	17 18 21	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to (A^{1} < B^{1} \leftrightarrow A < B)$
23	22	biimpar	$⊢ ((A \in ℝ \land B \in ℝ) \land A < B) \to A^{1} < B^{1}$
24	23	adantrl	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{1} < B^{1}$
25		simp2ll	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to A \in ℝ$
26		nnnn0	$⊢ b \in ℕ \to b \in ℕ_{0}$
27	26	3ad2ant1	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to b \in ℕ_{0}$
28	25 27	reexpcld	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to A^{b} \in ℝ$
29		simp2lr	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to B \in ℝ$
30	29 27	reexpcld	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to B^{b} \in ℝ$
31	28 30	jca	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to (A^{b} \in ℝ \land B^{b} \in ℝ)$
32		simp2rl	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to 0 \leq A$
33	25 27 32	expge0d	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to 0 \leq A^{b}$
34		simp3	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to A^{b} < B^{b}$
35	33 34	jca	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to (0 \leq A^{b} \land A^{b} < B^{b})$
36		simp2l	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to (A \in ℝ \land B \in ℝ)$
37		simp2r	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to (0 \leq A \land A < B)$
38		ltmul12a	$⊢ (((A^{b} \in ℝ \land B^{b} \in ℝ) \land (0 \leq A^{b} \land A^{b} < B^{b})) \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B))) \to A^{b} A < B^{b} B$
39	31 35 36 37 38	syl22anc	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to A^{b} A < B^{b} B$
40	25	recnd	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to A \in ℂ$
41	40 27	expp1d	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to A^{b + 1} = A^{b} A$
42	29	recnd	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to B \in ℂ$
43	42 27	expp1d	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to B^{b + 1} = B^{b} B$
44	39 41 43	3brtr4d	$⊢ (b \in ℕ \land ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land A^{b} < B^{b}) \to A^{b + 1} < B^{b + 1}$
45	44	3exp	$⊢ b \in ℕ \to (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to (A^{b} < B^{b} \to A^{b + 1} < B^{b + 1}))$
46	45	a2d	$⊢ b \in ℕ \to ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{b} < B^{b}) \to (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{b + 1} < B^{b + 1}))$
47	4 8 12 16 24 46	nnind	$⊢ N \in ℕ \to (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A^{N} < B^{N})$
48	47	impcom	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land N \in ℕ) \to A^{N} < B^{N}$
49	48	3impa	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B) \land N \in ℕ) \to A^{N} < B^{N}$

Metamath Proof Explorer

Theorem expmordi

Proof