Theorem leexp2r

Description: Weak ordering relationship for exponentiation of a fixed real base in [ 0 , 1 ] to integer exponents. (Contributed by Paul Chapman, 14-Jan-2008) (Revised by Mario Carneiro, 29-Apr-2014)

	Ref	Expression
Assertion	leexp2r	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑗 = 𝑀 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑀 ) )
2	1	breq1d	⊢ ( 𝑗 = 𝑀 → ( ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ↔ ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
3	2	imbi2d	⊢ ( 𝑗 = 𝑀 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
4		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑘 ) )
5	4	breq1d	⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ↔ ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
6	5	imbi2d	⊢ ( 𝑗 = 𝑘 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
7		oveq2	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
8	7	breq1d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ↔ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
9	8	imbi2d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
10		oveq2	⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑁 ) )
11	10	breq1d	⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ↔ ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
12	11	imbi2d	⊢ ( 𝑗 = 𝑁 → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑗 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
13		reexpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ )
14	13	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ )
15	14	leidd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑀 ) )
16		simprll	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝐴 ∈ ℝ )
17		1red	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 1 ∈ ℝ )
18		simprlr	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝑀 ∈ ℕ0 )
19		simpl	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
20		eluznn0	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
21	18 19 20	syl2anc	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝑘 ∈ ℕ0 )
22		reexpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ )
23	16 21 22	syl2anc	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ )
24		simprrl	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 0 ≤ 𝐴 )
25		expge0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → 0 ≤ ( 𝐴 ↑ 𝑘 ) )
26	16 21 24 25	syl3anc	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 0 ≤ ( 𝐴 ↑ 𝑘 ) )
27		simprrr	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝐴 ≤ 1 )
28	16 17 23 26 27	lemul2ad	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ≤ ( ( 𝐴 ↑ 𝑘 ) · 1 ) )
29	16	recnd	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → 𝐴 ∈ ℂ )
30		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
31	29 21 30	syl2anc	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
32	23	recnd	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
33	32	mulridd	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( ( 𝐴 ↑ 𝑘 ) · 1 ) = ( 𝐴 ↑ 𝑘 ) )
34	33	eqcomd	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) · 1 ) )
35	28 31 34	3brtr4d	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑘 ) )
36		peano2nn0	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
37	21 36	syl	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
38		reexpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ∈ ℝ )
39	16 37 38	syl2anc	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ∈ ℝ )
40	13	ad2antrl	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ )
41		letr	⊢ ( ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( 𝐴 ↑ 𝑘 ) ∈ ℝ ∧ ( 𝐴 ↑ 𝑀 ) ∈ ℝ ) → ( ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑘 ) ∧ ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
42	39 23 40 41	syl3anc	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑘 ) ∧ ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
43	35 42	mpand	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) ) → ( ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
44	43	ex	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
45	44	a2d	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑘 ) ≤ ( 𝐴 ↑ 𝑀 ) ) → ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
46	3 6 9 12 15 45	uzind4i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
47	46	expd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
48	47	com12	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) ) )
49	48	3impia	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) ) )
50	49	imp	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 𝑀 ) )