leexp1a

Description: Weak base ordering relationship for exponentiation of real bases to a fixed nonnegative integer exponent. (Contributed by NM, 18-Dec-2005)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ j = 0 \to A^{j} = A^{0}$
2		oveq2	$⊢ j = 0 \to B^{j} = B^{0}$
3	1 2	breq12d	$⊢ j = 0 \to (A^{j} \leq B^{j} \leftrightarrow A^{0} \leq B^{0})$
4	3	imbi2d	$⊢ j = 0 \to ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{j} \leq B^{j}) \leftrightarrow (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{0} \leq B^{0}))$
5		oveq2	$⊢ j = k \to A^{j} = A^{k}$
6		oveq2	$⊢ j = k \to B^{j} = B^{k}$
7	5 6	breq12d	$⊢ j = k \to (A^{j} \leq B^{j} \leftrightarrow A^{k} \leq B^{k})$
8	7	imbi2d	$⊢ j = k \to ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{j} \leq B^{j}) \leftrightarrow (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{k} \leq B^{k}))$
9		oveq2	$⊢ j = k + 1 \to A^{j} = A^{k + 1}$
10		oveq2	$⊢ j = k + 1 \to B^{j} = B^{k + 1}$
11	9 10	breq12d	$⊢ j = k + 1 \to (A^{j} \leq B^{j} \leftrightarrow A^{k + 1} \leq B^{k + 1})$
12	11	imbi2d	$⊢ j = k + 1 \to ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{j} \leq B^{j}) \leftrightarrow (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{k + 1} \leq B^{k + 1}))$
13		oveq2	$⊢ j = N \to A^{j} = A^{N}$
14		oveq2	$⊢ j = N \to B^{j} = B^{N}$
15	13 14	breq12d	$⊢ j = N \to (A^{j} \leq B^{j} \leftrightarrow A^{N} \leq B^{N})$
16	15	imbi2d	$⊢ j = N \to ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{j} \leq B^{j}) \leftrightarrow (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{N} \leq B^{N}))$
17		recn	$⊢ A \in ℝ \to A \in ℂ$
18		recn	$⊢ B \in ℝ \to B \in ℂ$
19		exp0	$⊢ A \in ℂ \to A^{0} = 1$
20	19	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to A^{0} = 1$
21		1le1	$⊢ 1 \leq 1$
22	20 21	eqbrtrdi	$⊢ (A \in ℂ \land B \in ℂ) \to A^{0} \leq 1$
23		exp0	$⊢ B \in ℂ \to B^{0} = 1$
24	23	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to B^{0} = 1$
25	22 24	breqtrrd	$⊢ (A \in ℂ \land B \in ℂ) \to A^{0} \leq B^{0}$
26	17 18 25	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to A^{0} \leq B^{0}$
27	26	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{0} \leq B^{0}$
28		reexpcl	$⊢ (A \in ℝ \land k \in ℕ_{0}) \to A^{k} \in ℝ$
29	28	ad4ant14	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to A^{k} \in ℝ$
30		simplll	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to A \in ℝ$
31		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
32		simplrl	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to 0 \leq A$
33		expge0	$⊢ (A \in ℝ \land k \in ℕ_{0} \land 0 \leq A) \to 0 \leq A^{k}$
34	30 31 32 33	syl3anc	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to 0 \leq A^{k}$
35		reexpcl	$⊢ (B \in ℝ \land k \in ℕ_{0}) \to B^{k} \in ℝ$
36	35	ad4ant24	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to B^{k} \in ℝ$
37	29 34 36	jca31	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to ((A^{k} \in ℝ \land 0 \leq A^{k}) \land B^{k} \in ℝ)$
38		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
39		simpl	$⊢ (0 \leq A \land A \leq B) \to 0 \leq A$
40	38 39	anim12i	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to (A \in ℝ \land 0 \leq A)$
41	40	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to (A \in ℝ \land 0 \leq A)$
42		simpllr	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to B \in ℝ$
43	37 41 42	jca32	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to (((A^{k} \in ℝ \land 0 \leq A^{k}) \land B^{k} \in ℝ) \land ((A \in ℝ \land 0 \leq A) \land B \in ℝ))$
44	43	adantr	$⊢ ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \land A^{k} \leq B^{k}) \to (((A^{k} \in ℝ \land 0 \leq A^{k}) \land B^{k} \in ℝ) \land ((A \in ℝ \land 0 \leq A) \land B \in ℝ))$
45		simplrr	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to A \leq B$
46	45	anim1ci	$⊢ ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \land A^{k} \leq B^{k}) \to (A^{k} \leq B^{k} \land A \leq B)$
47		lemul12a	$⊢ (((A^{k} \in ℝ \land 0 \leq A^{k}) \land B^{k} \in ℝ) \land ((A \in ℝ \land 0 \leq A) \land B \in ℝ)) \to ((A^{k} \leq B^{k} \land A \leq B) \to A^{k} A \leq B^{k} B)$
48	44 46 47	sylc	$⊢ ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \land A^{k} \leq B^{k}) \to A^{k} A \leq B^{k} B$
49		expp1	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k + 1} = A^{k} A$
50	17 49	sylan	$⊢ (A \in ℝ \land k \in ℕ_{0}) \to A^{k + 1} = A^{k} A$
51	50	ad5ant14	$⊢ ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \land A^{k} \leq B^{k}) \to A^{k + 1} = A^{k} A$
52		expp1	$⊢ (B \in ℂ \land k \in ℕ_{0}) \to B^{k + 1} = B^{k} B$
53	18 52	sylan	$⊢ (B \in ℝ \land k \in ℕ_{0}) \to B^{k + 1} = B^{k} B$
54	53	ad5ant24	$⊢ ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \land A^{k} \leq B^{k}) \to B^{k + 1} = B^{k} B$
55	48 51 54	3brtr4d	$⊢ ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \land A^{k} \leq B^{k}) \to A^{k + 1} \leq B^{k + 1}$
56	55	ex	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \land k \in ℕ_{0}) \to (A^{k} \leq B^{k} \to A^{k + 1} \leq B^{k + 1})$
57	56	expcom	$⊢ k \in ℕ_{0} \to (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to (A^{k} \leq B^{k} \to A^{k + 1} \leq B^{k + 1}))$
58	57	a2d	$⊢ k \in ℕ_{0} \to ((((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{k} \leq B^{k}) \to (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{k + 1} \leq B^{k + 1}))$
59	4 8 12 16 27 58	nn0ind	$⊢ N \in ℕ_{0} \to (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A^{N} \leq B^{N})$
60	59	exp4c	$⊢ N \in ℕ_{0} \to (A \in ℝ \to (B \in ℝ \to ((0 \leq A \land A \leq B) \to A^{N} \leq B^{N})))$
61	60	com3l	$⊢ A \in ℝ \to (B \in ℝ \to (N \in ℕ_{0} \to ((0 \leq A \land A \leq B) \to A^{N} \leq B^{N})))$
62	61	3imp1	$⊢ ((A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \land (0 \leq A \land A \leq B)) \to A^{N} \leq B^{N}$

Metamath Proof Explorer

Theorem leexp1a

Proof