leexp2r

Description: Weak ordering relationship for exponentiation. (Contributed by Paul Chapman, 14-Jan-2008) (Revised by Mario Carneiro, 29-Apr-2014)

		Ref	Expression
	Assertion	leexp2r	$⊢ ((A \in ℝ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \land (0 \leq A \land A \leq 1)) \to A^{N} \leq A^{M}$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ j = M \to A^{j} = A^{M}$
2	1	breq1d	$⊢ j = M \to (A^{j} \leq A^{M} \leftrightarrow A^{M} \leq A^{M})$
3	2	imbi2d	$⊢ j = M \to ((((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{j} \leq A^{M}) \leftrightarrow (((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{M} \leq A^{M}))$
4		oveq2	$⊢ j = k \to A^{j} = A^{k}$
5	4	breq1d	$⊢ j = k \to (A^{j} \leq A^{M} \leftrightarrow A^{k} \leq A^{M})$
6	5	imbi2d	$⊢ j = k \to ((((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{j} \leq A^{M}) \leftrightarrow (((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{k} \leq A^{M}))$
7		oveq2	$⊢ j = k + 1 \to A^{j} = A^{k + 1}$
8	7	breq1d	$⊢ j = k + 1 \to (A^{j} \leq A^{M} \leftrightarrow A^{k + 1} \leq A^{M})$
9	8	imbi2d	$⊢ j = k + 1 \to ((((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{j} \leq A^{M}) \leftrightarrow (((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{k + 1} \leq A^{M}))$
10		oveq2	$⊢ j = N \to A^{j} = A^{N}$
11	10	breq1d	$⊢ j = N \to (A^{j} \leq A^{M} \leftrightarrow A^{N} \leq A^{M})$
12	11	imbi2d	$⊢ j = N \to ((((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{j} \leq A^{M}) \leftrightarrow (((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{N} \leq A^{M}))$
13		reexpcl	$⊢ (A \in ℝ \land M \in ℕ_{0}) \to A^{M} \in ℝ$
14	13	adantr	$⊢ ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{M} \in ℝ$
15	14	leidd	$⊢ ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{M} \leq A^{M}$
16		simprll	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A \in ℝ$
17		1red	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to 1 \in ℝ$
18		simprlr	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to M \in ℕ_{0}$
19		simpl	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to k \in ℤ_{\geq M}$
20		eluznn0	$⊢ (M \in ℕ_{0} \land k \in ℤ_{\geq M}) \to k \in ℕ_{0}$
21	18 19 20	syl2anc	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to k \in ℕ_{0}$
22		reexpcl	$⊢ (A \in ℝ \land k \in ℕ_{0}) \to A^{k} \in ℝ$
23	16 21 22	syl2anc	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A^{k} \in ℝ$
24		simprrl	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to 0 \leq A$
25		expge0	$⊢ (A \in ℝ \land k \in ℕ_{0} \land 0 \leq A) \to 0 \leq A^{k}$
26	16 21 24 25	syl3anc	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to 0 \leq A^{k}$
27		simprrr	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A \leq 1$
28	16 17 23 26 27	lemul2ad	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A^{k} A \leq A^{k} \cdot 1$
29	16	recnd	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A \in ℂ$
30		expp1	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k + 1} = A^{k} A$
31	29 21 30	syl2anc	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A^{k + 1} = A^{k} A$
32	23	recnd	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A^{k} \in ℂ$
33	32	mulid1d	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A^{k} \cdot 1 = A^{k}$
34	33	eqcomd	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A^{k} = A^{k} \cdot 1$
35	28 31 34	3brtr4d	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A^{k + 1} \leq A^{k}$
36		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
37	21 36	syl	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to k + 1 \in ℕ_{0}$
38		reexpcl	$⊢ (A \in ℝ \land k + 1 \in ℕ_{0}) \to A^{k + 1} \in ℝ$
39	16 37 38	syl2anc	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A^{k + 1} \in ℝ$
40	13	ad2antrl	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to A^{M} \in ℝ$
41		letr	$⊢ (A^{k + 1} \in ℝ \land A^{k} \in ℝ \land A^{M} \in ℝ) \to ((A^{k + 1} \leq A^{k} \land A^{k} \leq A^{M}) \to A^{k + 1} \leq A^{M})$
42	39 23 40 41	syl3anc	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to ((A^{k + 1} \leq A^{k} \land A^{k} \leq A^{M}) \to A^{k + 1} \leq A^{M})$
43	35 42	mpand	$⊢ (k \in ℤ_{\geq M} \land ((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1))) \to (A^{k} \leq A^{M} \to A^{k + 1} \leq A^{M})$
44	43	ex	$⊢ k \in ℤ_{\geq M} \to (((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to (A^{k} \leq A^{M} \to A^{k + 1} \leq A^{M}))$
45	44	a2d	$⊢ k \in ℤ_{\geq M} \to ((((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{k} \leq A^{M}) \to (((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{k + 1} \leq A^{M}))$
46	3 6 9 12 15 45	uzind4i	$⊢ N \in ℤ_{\geq M} \to (((A \in ℝ \land M \in ℕ_{0}) \land (0 \leq A \land A \leq 1)) \to A^{N} \leq A^{M})$
47	46	expd	$⊢ N \in ℤ_{\geq M} \to ((A \in ℝ \land M \in ℕ_{0}) \to ((0 \leq A \land A \leq 1) \to A^{N} \leq A^{M}))$
48	47	com12	$⊢ (A \in ℝ \land M \in ℕ_{0}) \to (N \in ℤ_{\geq M} \to ((0 \leq A \land A \leq 1) \to A^{N} \leq A^{M}))$
49	48	3impia	$⊢ (A \in ℝ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to ((0 \leq A \land A \leq 1) \to A^{N} \leq A^{M})$
50	49	imp	$⊢ ((A \in ℝ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \land (0 \leq A \land A \leq 1)) \to A^{N} \leq A^{M}$

Metamath Proof Explorer

Theorem leexp2r

Proof