Theorem 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	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )

Proof

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