Metamath Proof Explorer

Theorem efexple

Description: Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014)

Ref Expression
Assertion efexple ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 ↑ 𝑁 ) ≤ 𝐵 ↔ 𝑁 ≤ ( ⌊ ‘ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
2 0lt1 ⊢ 0 < 1
3 0re ⊢ 0 ∈ ℝ
4 1re ⊢ 1 ∈ ℝ
5 lttr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 < 𝐴 ) → 0 < 𝐴 ) )
6 3 4 5 mp3an12 ⊢ ( 𝐴 ∈ ℝ → ( ( 0 < 1 ∧ 1 < 𝐴 ) → 0 < 𝐴 ) )
7 2 6 mpani ⊢ ( 𝐴 ∈ ℝ → ( 1 < 𝐴 → 0 < 𝐴 ) )
8 7 imp ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 𝐴 )
9 1 8 elrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ+ )
10 9 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℝ+ )
11 simp2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → 𝑁 ∈ ℤ )
12 reexplog ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) = ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) )
13 10 11 12 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 ↑ 𝑁 ) = ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) )
14 reeflog ⊢ ( 𝐵 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
15 14 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
16 15 eqcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 = ( exp ‘ ( log ‘ 𝐵 ) ) )
17 13 16 breq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 ↑ 𝑁 ) ≤ 𝐵 ↔ ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) ≤ ( exp ‘ ( log ‘ 𝐵 ) ) ) )
18 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
19 18 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → 𝑁 ∈ ℝ )
20 rplogcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
21 20 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
22 21 rpred ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℝ )
23 19 22 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝑁 · ( log ‘ 𝐴 ) ) ∈ ℝ )
24 relogcl ⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
25 24 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ 𝐵 ) ∈ ℝ )
26 efle ⊢ ( ( ( 𝑁 · ( log ‘ 𝐴 ) ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( ( 𝑁 · ( log ‘ 𝐴 ) ) ≤ ( log ‘ 𝐵 ) ↔ ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) ≤ ( exp ‘ ( log ‘ 𝐵 ) ) ) )
27 23 25 26 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝑁 · ( log ‘ 𝐴 ) ) ≤ ( log ‘ 𝐵 ) ↔ ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) ≤ ( exp ‘ ( log ‘ 𝐵 ) ) ) )
28 19 25 21 lemuldivd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝑁 · ( log ‘ 𝐴 ) ) ≤ ( log ‘ 𝐵 ) ↔ 𝑁 ≤ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐴 ) ) ) )
29 25 21 rerpdivcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( log ‘ 𝐵 ) / ( log ‘ 𝐴 ) ) ∈ ℝ )
30 flge ⊢ ( ( ( ( log ‘ 𝐵 ) / ( log ‘ 𝐴 ) ) ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐴 ) ) ↔ 𝑁 ≤ ( ⌊ ‘ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐴 ) ) ) ) )
31 29 11 30 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝑁 ≤ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐴 ) ) ↔ 𝑁 ≤ ( ⌊ ‘ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐴 ) ) ) ) )
32 28 31 bitrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝑁 · ( log ‘ 𝐴 ) ) ≤ ( log ‘ 𝐵 ) ↔ 𝑁 ≤ ( ⌊ ‘ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐴 ) ) ) ) )
33 17 27 32 3bitr2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 ↑ 𝑁 ) ≤ 𝐵 ↔ 𝑁 ≤ ( ⌊ ‘ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐴 ) ) ) ) )