Metamath Proof Explorer

Theorem nexple

Description: A lower bound for an exponentiation. (Contributed by Thierry Arnoux, 19-Aug-2017)

Ref Expression
Assertion nexple ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝐴 ≤ ( 𝐵 ↑ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 ∈ ℕ ) → 𝐴 ∈ ℕ )
2 simpl2 ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 ∈ ℕ ) → 𝐵 ∈ ℝ )
3 simpl3 ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 ∈ ℕ ) → 2 ≤ 𝐵 )
4 id ⊢ ( 𝑘 = 1 → 𝑘 = 1 )
5 oveq2 ⊢ ( 𝑘 = 1 → ( 𝐵 ↑ 𝑘 ) = ( 𝐵 ↑ 1 ) )
6 4 5 breq12d ⊢ ( 𝑘 = 1 → ( 𝑘 ≤ ( 𝐵 ↑ 𝑘 ) ↔ 1 ≤ ( 𝐵 ↑ 1 ) ) )
7 6 imbi2d ⊢ ( 𝑘 = 1 → ( ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝑘 ≤ ( 𝐵 ↑ 𝑘 ) ) ↔ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 1 ≤ ( 𝐵 ↑ 1 ) ) ) )
8 id ⊢ ( 𝑘 = 𝑛 → 𝑘 = 𝑛 )
9 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐵 ↑ 𝑘 ) = ( 𝐵 ↑ 𝑛 ) )
10 8 9 breq12d ⊢ ( 𝑘 = 𝑛 → ( 𝑘 ≤ ( 𝐵 ↑ 𝑘 ) ↔ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) )
11 10 imbi2d ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝑘 ≤ ( 𝐵 ↑ 𝑘 ) ) ↔ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) ) )
12 id ⊢ ( 𝑘 = ( 𝑛 + 1 ) → 𝑘 = ( 𝑛 + 1 ) )
13 oveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐵 ↑ 𝑘 ) = ( 𝐵 ↑ ( 𝑛 + 1 ) ) )
14 12 13 breq12d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝑘 ≤ ( 𝐵 ↑ 𝑘 ) ↔ ( 𝑛 + 1 ) ≤ ( 𝐵 ↑ ( 𝑛 + 1 ) ) ) )
15 14 imbi2d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝑘 ≤ ( 𝐵 ↑ 𝑘 ) ) ↔ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → ( 𝑛 + 1 ) ≤ ( 𝐵 ↑ ( 𝑛 + 1 ) ) ) ) )
16 id ⊢ ( 𝑘 = 𝐴 → 𝑘 = 𝐴 )
17 oveq2 ⊢ ( 𝑘 = 𝐴 → ( 𝐵 ↑ 𝑘 ) = ( 𝐵 ↑ 𝐴 ) )
18 16 17 breq12d ⊢ ( 𝑘 = 𝐴 → ( 𝑘 ≤ ( 𝐵 ↑ 𝑘 ) ↔ 𝐴 ≤ ( 𝐵 ↑ 𝐴 ) ) )
19 18 imbi2d ⊢ ( 𝑘 = 𝐴 → ( ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝑘 ≤ ( 𝐵 ↑ 𝑘 ) ) ↔ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝐴 ≤ ( 𝐵 ↑ 𝐴 ) ) ) )
20 simpl ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
21 1nn0 ⊢ 1 ∈ ℕ0
22 21 a1i ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 1 ∈ ℕ0 )
23 1red ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 1 ∈ ℝ )
24 2re ⊢ 2 ∈ ℝ
25 24 a1i ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 2 ∈ ℝ )
26 1le2 ⊢ 1 ≤ 2
27 26 a1i ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 1 ≤ 2 )
28 simpr ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 2 ≤ 𝐵 )
29 23 25 20 27 28 letrd ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 1 ≤ 𝐵 )
30 20 22 29 expge1d ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 1 ≤ ( 𝐵 ↑ 1 ) )
31 simp1 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 𝑛 ∈ ℕ )
32 31 nnnn0d ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 𝑛 ∈ ℕ0 )
33 32 nn0red ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 𝑛 ∈ ℝ )
34 1red ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 1 ∈ ℝ )
35 33 34 readdcld ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 + 1 ) ∈ ℝ )
36 20 3ad2ant2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 𝐵 ∈ ℝ )
37 33 36 remulcld ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 · 𝐵 ) ∈ ℝ )
38 36 32 reexpcld ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝐵 ↑ 𝑛 ) ∈ ℝ )
39 38 36 remulcld ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( ( 𝐵 ↑ 𝑛 ) · 𝐵 ) ∈ ℝ )
40 24 a1i ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 2 ∈ ℝ )
41 33 40 remulcld ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 · 2 ) ∈ ℝ )
42 31 nnge1d ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 1 ≤ 𝑛 )
43 34 33 33 42 leadd2dd ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 + 1 ) ≤ ( 𝑛 + 𝑛 ) )
44 33 recnd ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 𝑛 ∈ ℂ )
45 44 times2d ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 · 2 ) = ( 𝑛 + 𝑛 ) )
46 43 45 breqtrrd ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 + 1 ) ≤ ( 𝑛 · 2 ) )
47 32 nn0ge0d ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 0 ≤ 𝑛 )
48 simp2r ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 2 ≤ 𝐵 )
49 40 36 33 47 48 lemul2ad ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 · 2 ) ≤ ( 𝑛 · 𝐵 ) )
50 35 41 37 46 49 letrd ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 + 1 ) ≤ ( 𝑛 · 𝐵 ) )
51 0red ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 0 ∈ ℝ )
52 0le2 ⊢ 0 ≤ 2
53 52 a1i ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 0 ≤ 2 )
54 51 25 20 53 28 letrd ⊢ ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 0 ≤ 𝐵 )
55 54 3ad2ant2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 0 ≤ 𝐵 )
56 simp3 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) )
57 33 38 36 55 56 lemul1ad ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 · 𝐵 ) ≤ ( ( 𝐵 ↑ 𝑛 ) · 𝐵 ) )
58 35 37 39 50 57 letrd ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 + 1 ) ≤ ( ( 𝐵 ↑ 𝑛 ) · 𝐵 ) )
59 36 recnd ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → 𝐵 ∈ ℂ )
60 59 32 expp1d ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝐵 ↑ ( 𝑛 + 1 ) ) = ( ( 𝐵 ↑ 𝑛 ) · 𝐵 ) )
61 58 60 breqtrrd ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( 𝑛 + 1 ) ≤ ( 𝐵 ↑ ( 𝑛 + 1 ) ) )
62 61 3exp ⊢ ( 𝑛 ∈ ℕ → ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → ( 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) → ( 𝑛 + 1 ) ≤ ( 𝐵 ↑ ( 𝑛 + 1 ) ) ) ) )
63 62 a2d ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝑛 ≤ ( 𝐵 ↑ 𝑛 ) ) → ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → ( 𝑛 + 1 ) ≤ ( 𝐵 ↑ ( 𝑛 + 1 ) ) ) ) )
64 7 11 15 19 30 63 nnind ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝐴 ≤ ( 𝐵 ↑ 𝐴 ) ) )
65 64 3impib ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝐴 ≤ ( 𝐵 ↑ 𝐴 ) )
66 1 2 3 65 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 ∈ ℕ ) → 𝐴 ≤ ( 𝐵 ↑ 𝐴 ) )
67 0le1 ⊢ 0 ≤ 1
68 67 a1i ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 = 0 ) → 0 ≤ 1 )
69 simpr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 = 0 ) → 𝐴 = 0 )
70 69 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 = 0 ) → ( 𝐵 ↑ 𝐴 ) = ( 𝐵 ↑ 0 ) )
71 simpl2 ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 = 0 ) → 𝐵 ∈ ℝ )
72 71 recnd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 = 0 ) → 𝐵 ∈ ℂ )
73 72 exp0d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 = 0 ) → ( 𝐵 ↑ 0 ) = 1 )
74 70 73 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 = 0 ) → ( 𝐵 ↑ 𝐴 ) = 1 )
75 68 69 74 3brtr4d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) ∧ 𝐴 = 0 ) → 𝐴 ≤ ( 𝐵 ↑ 𝐴 ) )
76 elnn0 ⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
77 76 biimpi ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
78 77 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
79 66 75 78 mpjaodan ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵 ) → 𝐴 ≤ ( 𝐵 ↑ 𝐴 ) )