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

Metamath Proof Explorer

Theorem expnbnd

Description: Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007)

Ref Expression
Assertion expnbnd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ∃ 𝑘 ∈ ℕ 𝐴 < ( 𝐵 ↑ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 1nn ⊢ 1 ∈ ℕ
2 1re ⊢ 1 ∈ ℝ
3 lttr ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 < 1 ∧ 1 < 𝐵 ) → 𝐴 < 𝐵 ) )
4 2 3 mp3an2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 < 1 ∧ 1 < 𝐵 ) → 𝐴 < 𝐵 ) )
5 4 exp4b ⊢ ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ → ( 𝐴 < 1 → ( 1 < 𝐵 → 𝐴 < 𝐵 ) ) ) )
6 5 com34 ⊢ ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ → ( 1 < 𝐵 → ( 𝐴 < 1 → 𝐴 < 𝐵 ) ) ) )
7 6 3imp1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝐴 < 1 ) → 𝐴 < 𝐵 )
8 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
9 exp1 ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 1 ) = 𝐵 )
10 8 9 syl ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 ↑ 1 ) = 𝐵 )
11 10 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝐵 ↑ 1 ) = 𝐵 )
12 11 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝐴 < 1 ) → ( 𝐵 ↑ 1 ) = 𝐵 )
13 7 12 breqtrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝐴 < 1 ) → 𝐴 < ( 𝐵 ↑ 1 ) )
14 oveq2 ⊢ ( 𝑘 = 1 → ( 𝐵 ↑ 𝑘 ) = ( 𝐵 ↑ 1 ) )
15 14 breq2d ⊢ ( 𝑘 = 1 → ( 𝐴 < ( 𝐵 ↑ 𝑘 ) ↔ 𝐴 < ( 𝐵 ↑ 1 ) ) )
16 15 rspcev ⊢ ( ( 1 ∈ ℕ ∧ 𝐴 < ( 𝐵 ↑ 1 ) ) → ∃ 𝑘 ∈ ℕ 𝐴 < ( 𝐵 ↑ 𝑘 ) )
17 1 13 16 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝐴 < 1 ) → ∃ 𝑘 ∈ ℕ 𝐴 < ( 𝐵 ↑ 𝑘 ) )
18 peano2rem ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℝ )
19 18 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( 𝐴 − 1 ) ∈ ℝ )
20 peano2rem ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 − 1 ) ∈ ℝ )
21 20 adantr ⊢ ( ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝐵 − 1 ) ∈ ℝ )
22 21 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( 𝐵 − 1 ) ∈ ℝ )
23 posdif ⊢ ( ( 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < 𝐵 ↔ 0 < ( 𝐵 − 1 ) ) )
24 2 23 mpan ⊢ ( 𝐵 ∈ ℝ → ( 1 < 𝐵 ↔ 0 < ( 𝐵 − 1 ) ) )
25 24 biimpa ⊢ ( ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 0 < ( 𝐵 − 1 ) )
26 25 gt0ne0d ⊢ ( ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝐵 − 1 ) ≠ 0 )
27 26 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( 𝐵 − 1 ) ≠ 0 )
28 19 22 27 redivcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ∈ ℝ )
29 28 adantll ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ∈ ℝ )
30 18 adantl ⊢ ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) → ( 𝐴 − 1 ) ∈ ℝ )
31 subge0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 ≤ ( 𝐴 − 1 ) ↔ 1 ≤ 𝐴 ) )
32 2 31 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ ( 𝐴 − 1 ) ↔ 1 ≤ 𝐴 ) )
33 32 biimparc ⊢ ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) → 0 ≤ ( 𝐴 − 1 ) )
34 30 33 jca ⊢ ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 − 1 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 − 1 ) ) )
35 21 25 jca ⊢ ( ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( ( 𝐵 − 1 ) ∈ ℝ ∧ 0 < ( 𝐵 − 1 ) ) )
36 divge0 ⊢ ( ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 − 1 ) ) ∧ ( ( 𝐵 − 1 ) ∈ ℝ ∧ 0 < ( 𝐵 − 1 ) ) ) → 0 ≤ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) )
37 34 35 36 syl2an ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → 0 ≤ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) )
38 flge0nn0 ⊢ ( ( ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) → ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) ∈ ℕ0 )
39 29 37 38 syl2anc ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) ∈ ℕ0 )
40 nn0p1nn ⊢ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ∈ ℕ )
41 39 40 syl ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ∈ ℕ )
42 simplr ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → 𝐴 ∈ ℝ )
43 21 adantl ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( 𝐵 − 1 ) ∈ ℝ )
44 peano2nn0 ⊢ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ∈ ℕ0 )
45 39 44 syl ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ∈ ℕ0 )
46 45 nn0red ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ∈ ℝ )
47 43 46 remulcld ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ∈ ℝ )
48 peano2re ⊢ ( ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ∈ ℝ → ( ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) + 1 ) ∈ ℝ )
49 47 48 syl ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) + 1 ) ∈ ℝ )
50 simprl ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → 𝐵 ∈ ℝ )
51 reexpcl ⊢ ( ( 𝐵 ∈ ℝ ∧ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ∈ ℕ0 ) → ( 𝐵 ↑ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ∈ ℝ )
52 50 45 51 syl2anc ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( 𝐵 ↑ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ∈ ℝ )
53 flltp1 ⊢ ( ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ∈ ℝ → ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) < ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) )
54 29 53 syl ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) < ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) )
55 30 adantr ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( 𝐴 − 1 ) ∈ ℝ )
56 25 adantl ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → 0 < ( 𝐵 − 1 ) )
57 ltdivmul ⊢ ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ∈ ℝ ∧ ( ( 𝐵 − 1 ) ∈ ℝ ∧ 0 < ( 𝐵 − 1 ) ) ) → ( ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) < ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ↔ ( 𝐴 − 1 ) < ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ) )
58 55 46 43 56 57 syl112anc ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) < ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ↔ ( 𝐴 − 1 ) < ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ) )
59 54 58 mpbid ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( 𝐴 − 1 ) < ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) )
60 ltsubadd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ∈ ℝ ) → ( ( 𝐴 − 1 ) < ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ↔ 𝐴 < ( ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) + 1 ) ) )
61 2 60 mp3an2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ∈ ℝ ) → ( ( 𝐴 − 1 ) < ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ↔ 𝐴 < ( ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) + 1 ) ) )
62 42 47 61 syl2anc ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( 𝐴 − 1 ) < ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ↔ 𝐴 < ( ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) + 1 ) ) )
63 59 62 mpbid ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → 𝐴 < ( ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) + 1 ) )
64 0lt1 ⊢ 0 < 1
65 0re ⊢ 0 ∈ ℝ
66 lttr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 < 𝐵 ) → 0 < 𝐵 ) )
67 65 2 66 mp3an12 ⊢ ( 𝐵 ∈ ℝ → ( ( 0 < 1 ∧ 1 < 𝐵 ) → 0 < 𝐵 ) )
68 64 67 mpani ⊢ ( 𝐵 ∈ ℝ → ( 1 < 𝐵 → 0 < 𝐵 ) )
69 ltle ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐵 → 0 ≤ 𝐵 ) )
70 65 69 mpan ⊢ ( 𝐵 ∈ ℝ → ( 0 < 𝐵 → 0 ≤ 𝐵 ) )
71 68 70 syld ⊢ ( 𝐵 ∈ ℝ → ( 1 < 𝐵 → 0 ≤ 𝐵 ) )
72 71 imp ⊢ ( ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 0 ≤ 𝐵 )
73 72 adantl ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → 0 ≤ 𝐵 )
74 bernneq2 ⊢ ( ( 𝐵 ∈ ℝ ∧ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ∈ ℕ0 ∧ 0 ≤ 𝐵 ) → ( ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) + 1 ) ≤ ( 𝐵 ↑ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) )
75 50 45 73 74 syl3anc ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ( ( ( 𝐵 − 1 ) · ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) + 1 ) ≤ ( 𝐵 ↑ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) )
76 42 49 52 63 75 ltletrd ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → 𝐴 < ( 𝐵 ↑ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) )
77 oveq2 ⊢ ( 𝑘 = ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) → ( 𝐵 ↑ 𝑘 ) = ( 𝐵 ↑ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) )
78 77 breq2d ⊢ ( 𝑘 = ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) → ( 𝐴 < ( 𝐵 ↑ 𝑘 ) ↔ 𝐴 < ( 𝐵 ↑ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ) )
79 78 rspcev ⊢ ( ( ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ∈ ℕ ∧ 𝐴 < ( 𝐵 ↑ ( ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 𝐵 − 1 ) ) ) + 1 ) ) ) → ∃ 𝑘 ∈ ℕ 𝐴 < ( 𝐵 ↑ 𝑘 ) )
80 41 76 79 syl2anc ⊢ ( ( ( 1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) → ∃ 𝑘 ∈ ℕ 𝐴 < ( 𝐵 ↑ 𝑘 ) )
81 80 exp43 ⊢ ( 1 ≤ 𝐴 → ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ → ( 1 < 𝐵 → ∃ 𝑘 ∈ ℕ 𝐴 < ( 𝐵 ↑ 𝑘 ) ) ) ) )
82 81 com4l ⊢ ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ → ( 1 < 𝐵 → ( 1 ≤ 𝐴 → ∃ 𝑘 ∈ ℕ 𝐴 < ( 𝐵 ↑ 𝑘 ) ) ) ) )
83 82 3imp1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 1 ≤ 𝐴 ) → ∃ 𝑘 ∈ ℕ 𝐴 < ( 𝐵 ↑ 𝑘 ) )
84 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 𝐴 ∈ ℝ )
85 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 1 ∈ ℝ )
86 17 83 84 85 ltlecasei ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ∃ 𝑘 ∈ ℕ 𝐴 < ( 𝐵 ↑ 𝑘 ) )