Metamath Proof Explorer

Theorem expnbnd

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

Ref Expression
Assertion expnbnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < B → ∃ k ∈ ℕ A < B k

Proof

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