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 ⊢A∈ℝ∧B∈ℝ∧1<B→∃k∈ℕA<Bk

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∈ℂ→B1=B
10 8 9 syl ⊢B∈ℝ→B1=B
11 10 3ad2ant2 ⊢A∈ℝ∧B∈ℝ∧1<B→B1=B
12 11 adantr ⊢A∈ℝ∧B∈ℝ∧1<B∧A<1→B1=B
13 7 12 breqtrrd ⊢A∈ℝ∧B∈ℝ∧1<B∧A<1→A<B1
14 oveq2 ⊢k=1→Bk=B1
15 14 breq2d ⊢k=1→A<Bk↔A<B1
16 15 rspcev ⊢1∈ℕ∧A<B1→∃k∈ℕA<Bk
17 1 13 16 sylancr ⊢A∈ℝ∧B∈ℝ∧1<B∧A<1→∃k∈ℕA<Bk
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−1B−1∈ℝ
29 28 adantll ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A−1B−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−1B−1
37 34 35 36 syl2an ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→0≤A−1B−1
38 flge0nn0 ⊢A−1B−1∈ℝ∧0≤A−1B−1→A−1B−1∈ℕ0
39 29 37 38 syl2anc ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A−1B−1∈ℕ0
40 nn0p1nn ⊢A−1B−1∈ℕ0→A−1B−1+1∈ℕ
41 39 40 syl ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A−1B−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−1B−1∈ℕ0→A−1B−1+1∈ℕ0
45 39 44 syl ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A−1B−1+1∈ℕ0
46 45 nn0red ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A−1B−1+1∈ℝ
47 43 46 remulcld ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→B−1⁢A−1B−1+1∈ℝ
48 peano2re ⊢B−1⁢A−1B−1+1∈ℝ→B−1⁢A−1B−1+1+1∈ℝ
49 47 48 syl ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→B−1⁢A−1B−1+1+1∈ℝ
50 simprl ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→B∈ℝ
51 reexpcl ⊢B∈ℝ∧A−1B−1+1∈ℕ0→BA−1B−1+1∈ℝ
52 50 45 51 syl2anc ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→BA−1B−1+1∈ℝ
53 flltp1 ⊢A−1B−1∈ℝ→A−1B−1<A−1B−1+1
54 29 53 syl ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A−1B−1<A−1B−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−1B−1+1∈ℝ∧B−1∈ℝ∧0<B−1→A−1B−1<A−1B−1+1↔A−1<B−1⁢A−1B−1+1
58 55 46 43 56 57 syl112anc ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A−1B−1<A−1B−1+1↔A−1<B−1⁢A−1B−1+1
59 54 58 mpbid ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A−1<B−1⁢A−1B−1+1
60 ltsubadd ⊢A∈ℝ∧1∈ℝ∧B−1⁢A−1B−1+1∈ℝ→A−1<B−1⁢A−1B−1+1↔A<B−1⁢A−1B−1+1+1
61 2 60 mp3an2 ⊢A∈ℝ∧B−1⁢A−1B−1+1∈ℝ→A−1<B−1⁢A−1B−1+1↔A<B−1⁢A−1B−1+1+1
62 42 47 61 syl2anc ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A−1<B−1⁢A−1B−1+1↔A<B−1⁢A−1B−1+1+1
63 59 62 mpbid ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A<B−1⁢A−1B−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−1B−1+1∈ℕ0∧0≤B→B−1⁢A−1B−1+1+1≤BA−1B−1+1
75 50 45 73 74 syl3anc ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→B−1⁢A−1B−1+1+1≤BA−1B−1+1
76 42 49 52 63 75 ltletrd ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→A<BA−1B−1+1
77 oveq2 ⊢k=A−1B−1+1→Bk=BA−1B−1+1
78 77 breq2d ⊢k=A−1B−1+1→A<Bk↔A<BA−1B−1+1
79 78 rspcev ⊢A−1B−1+1∈ℕ∧A<BA−1B−1+1→∃k∈ℕA<Bk
80 41 76 79 syl2anc ⊢1≤A∧A∈ℝ∧B∈ℝ∧1<B→∃k∈ℕA<Bk
81 80 exp43 ⊢1≤A→A∈ℝ→B∈ℝ→1<B→∃k∈ℕA<Bk
82 81 com4l ⊢A∈ℝ→B∈ℝ→1<B→1≤A→∃k∈ℕA<Bk
83 82 3imp1 ⊢A∈ℝ∧B∈ℝ∧1<B∧1≤A→∃k∈ℕA<Bk
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<Bk