Metamath Proof Explorer

Theorem nexple

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

Ref Expression
Assertion nexple ⊢A∈ℕ0∧B∈ℝ∧2≤B→A≤BA

Proof

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