This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ↑ 𝑁 ) ) )