Theorem expubnd

Description: An upper bound on A ^ N when 2 <_ A . (Contributed by NM, 19-Dec-2005)

	Ref	Expression
Assertion	expubnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( ( 2 ↑ 𝑁 ) · ( ( 𝐴 − 1 ) ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
2		2re	⊢ 2 ∈ ℝ
3		peano2rem	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℝ )
4		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( 𝐴 − 1 ) ∈ ℝ ) → ( 2 · ( 𝐴 − 1 ) ) ∈ ℝ )
5	2 3 4	sylancr	⊢ ( 𝐴 ∈ ℝ → ( 2 · ( 𝐴 − 1 ) ) ∈ ℝ )
6	5	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴 ) → ( 2 · ( 𝐴 − 1 ) ) ∈ ℝ )
7		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴 ) → 𝑁 ∈ ℕ0 )
8		0le2	⊢ 0 ≤ 2
9		0re	⊢ 0 ∈ ℝ
10		letr	⊢ ( ( 0 ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 ≤ 2 ∧ 2 ≤ 𝐴 ) → 0 ≤ 𝐴 ) )
11	9 2 10	mp3an12	⊢ ( 𝐴 ∈ ℝ → ( ( 0 ≤ 2 ∧ 2 ≤ 𝐴 ) → 0 ≤ 𝐴 ) )
12	8 11	mpani	⊢ ( 𝐴 ∈ ℝ → ( 2 ≤ 𝐴 → 0 ≤ 𝐴 ) )
13	12	imp	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → 0 ≤ 𝐴 )
14		resubcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ℝ ) → ( 𝐴 − 2 ) ∈ ℝ )
15	2 14	mpan2	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 2 ) ∈ ℝ )
16		leadd2	⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝐴 − 2 ) ∈ ℝ ) → ( 2 ≤ 𝐴 ↔ ( ( 𝐴 − 2 ) + 2 ) ≤ ( ( 𝐴 − 2 ) + 𝐴 ) ) )
17	2 16	mp3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 − 2 ) ∈ ℝ ) → ( 2 ≤ 𝐴 ↔ ( ( 𝐴 − 2 ) + 2 ) ≤ ( ( 𝐴 − 2 ) + 𝐴 ) ) )
18	15 17	mpdan	⊢ ( 𝐴 ∈ ℝ → ( 2 ≤ 𝐴 ↔ ( ( 𝐴 − 2 ) + 2 ) ≤ ( ( 𝐴 − 2 ) + 𝐴 ) ) )
19	18	biimpa	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( ( 𝐴 − 2 ) + 2 ) ≤ ( ( 𝐴 − 2 ) + 𝐴 ) )
20		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
21		2cn	⊢ 2 ∈ ℂ
22		npcan	⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 𝐴 − 2 ) + 2 ) = 𝐴 )
23	20 21 22	sylancl	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 − 2 ) + 2 ) = 𝐴 )
24	23	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( ( 𝐴 − 2 ) + 2 ) = 𝐴 )
25		ax-1cn	⊢ 1 ∈ ℂ
26		subdi	⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 2 · ( 𝐴 − 1 ) ) = ( ( 2 · 𝐴 ) − ( 2 · 1 ) ) )
27	21 25 26	mp3an13	⊢ ( 𝐴 ∈ ℂ → ( 2 · ( 𝐴 − 1 ) ) = ( ( 2 · 𝐴 ) − ( 2 · 1 ) ) )
28		2times	⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
29		2t1e2	⊢ ( 2 · 1 ) = 2
30	29	a1i	⊢ ( 𝐴 ∈ ℂ → ( 2 · 1 ) = 2 )
31	28 30	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( 2 · 𝐴 ) − ( 2 · 1 ) ) = ( ( 𝐴 + 𝐴 ) − 2 ) )
32		addsub	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 𝐴 + 𝐴 ) − 2 ) = ( ( 𝐴 − 2 ) + 𝐴 ) )
33	21 32	mp3an3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 + 𝐴 ) − 2 ) = ( ( 𝐴 − 2 ) + 𝐴 ) )
34	33	anidms	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + 𝐴 ) − 2 ) = ( ( 𝐴 − 2 ) + 𝐴 ) )
35	27 31 34	3eqtrrd	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 − 2 ) + 𝐴 ) = ( 2 · ( 𝐴 − 1 ) ) )
36	20 35	syl	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 − 2 ) + 𝐴 ) = ( 2 · ( 𝐴 − 1 ) ) )
37	36	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( ( 𝐴 − 2 ) + 𝐴 ) = ( 2 · ( 𝐴 − 1 ) ) )
38	19 24 37	3brtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → 𝐴 ≤ ( 2 · ( 𝐴 − 1 ) ) )
39	13 38	jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( 0 ≤ 𝐴 ∧ 𝐴 ≤ ( 2 · ( 𝐴 − 1 ) ) ) )
40	39	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴 ) → ( 0 ≤ 𝐴 ∧ 𝐴 ≤ ( 2 · ( 𝐴 − 1 ) ) ) )
41		leexp1a	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 2 · ( 𝐴 − 1 ) ) ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ ( 2 · ( 𝐴 − 1 ) ) ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( ( 2 · ( 𝐴 − 1 ) ) ↑ 𝑁 ) )
42	1 6 7 40 41	syl31anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( ( 2 · ( 𝐴 − 1 ) ) ↑ 𝑁 ) )
43	3	recnd	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℂ )
44		mulexp	⊢ ( ( 2 ∈ ℂ ∧ ( 𝐴 − 1 ) ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 · ( 𝐴 − 1 ) ) ↑ 𝑁 ) = ( ( 2 ↑ 𝑁 ) · ( ( 𝐴 − 1 ) ↑ 𝑁 ) ) )
45	21 44	mp3an1	⊢ ( ( ( 𝐴 − 1 ) ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 · ( 𝐴 − 1 ) ) ↑ 𝑁 ) = ( ( 2 ↑ 𝑁 ) · ( ( 𝐴 − 1 ) ↑ 𝑁 ) ) )
46	43 45	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 · ( 𝐴 − 1 ) ) ↑ 𝑁 ) = ( ( 2 ↑ 𝑁 ) · ( ( 𝐴 − 1 ) ↑ 𝑁 ) ) )
47	46	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴 ) → ( ( 2 · ( 𝐴 − 1 ) ) ↑ 𝑁 ) = ( ( 2 ↑ 𝑁 ) · ( ( 𝐴 − 1 ) ↑ 𝑁 ) ) )
48	42 47	breqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( ( 2 ↑ 𝑁 ) · ( ( 𝐴 − 1 ) ↑ 𝑁 ) ) )