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 < 𝐵 ) → ∃ 𝑘 ∈ ℕ 𝐴 < ( 𝐵𝑘 ) )