Step |
Hyp |
Ref |
Expression |
1 |
|
nnre |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ ) |
2 |
1
|
3ad2ant2 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝑁 ∈ ℝ ) |
3 |
|
eluzelre |
⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℝ ) |
4 |
3
|
3ad2ant1 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝐵 ∈ ℝ ) |
5 |
|
eluz2nn |
⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℕ ) |
6 |
|
nnnn0 |
⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 ) |
7 |
6
|
nn0ge0d |
⊢ ( 𝐵 ∈ ℕ → 0 ≤ 𝐵 ) |
8 |
5 7
|
syl |
⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 𝐵 ) |
9 |
8
|
3ad2ant1 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 0 ≤ 𝐵 ) |
10 |
|
nnrp |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ ) |
11 |
|
relogbzcl |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℝ+ ) → ( 𝐵 logb 𝑁 ) ∈ ℝ ) |
12 |
10 11
|
sylan2 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐵 logb 𝑁 ) ∈ ℝ ) |
13 |
12
|
3adant3 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 logb 𝑁 ) ∈ ℝ ) |
14 |
4 9 13
|
recxpcld |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) ∈ ℝ ) |
15 |
|
eluzelre |
⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) → 𝐾 ∈ ℝ ) |
16 |
15
|
3ad2ant3 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝐾 ∈ ℝ ) |
17 |
4 9 16
|
recxpcld |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 ↑𝑐 𝐾 ) ∈ ℝ ) |
18 |
1
|
leidd |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ≤ 𝑁 ) |
19 |
18
|
adantl |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ≤ 𝑁 ) |
20 |
|
eluz2cnn0n1 |
⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ) |
21 |
|
nncn |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ ) |
22 |
|
nnne0 |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 ) |
23 |
|
eldifsn |
⊢ ( 𝑁 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) |
24 |
21 22 23
|
sylanbrc |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℂ ∖ { 0 } ) ) |
25 |
|
cxplogb |
⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑁 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) = 𝑁 ) |
26 |
20 24 25
|
syl2an |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) = 𝑁 ) |
27 |
19 26
|
breqtrrd |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ≤ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) ) |
28 |
27
|
3adant3 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝑁 ≤ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) ) |
29 |
|
eluz2 |
⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ↔ ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 ) ) |
30 |
12
|
adantl |
⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → ( 𝐵 logb 𝑁 ) ∈ ℝ ) |
31 |
|
flltp1 |
⊢ ( ( 𝐵 logb 𝑁 ) ∈ ℝ → ( 𝐵 logb 𝑁 ) < ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) |
32 |
30 31
|
syl |
⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → ( 𝐵 logb 𝑁 ) < ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) |
33 |
|
zre |
⊢ ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ → ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℝ ) |
34 |
33
|
adantr |
⊢ ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℝ ) |
35 |
34
|
adantr |
⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℝ ) |
36 |
|
zre |
⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ ) |
37 |
36
|
adantl |
⊢ ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℝ ) |
38 |
37
|
adantr |
⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → 𝐾 ∈ ℝ ) |
39 |
|
ltletr |
⊢ ( ( ( 𝐵 logb 𝑁 ) ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( ( 𝐵 logb 𝑁 ) < ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) ) |
40 |
30 35 38 39
|
syl3anc |
⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → ( ( ( 𝐵 logb 𝑁 ) < ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) ) |
41 |
32 40
|
mpand |
⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 → ( 𝐵 logb 𝑁 ) < 𝐾 ) ) |
42 |
41
|
ex |
⊢ ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 → ( 𝐵 logb 𝑁 ) < 𝐾 ) ) ) |
43 |
42
|
com23 |
⊢ ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 → ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) ) ) |
44 |
43
|
3impia |
⊢ ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 ) → ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) ) |
45 |
44
|
com12 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) ) |
46 |
29 45
|
syl5bi |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) ) |
47 |
46
|
3impia |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) |
48 |
|
eluz2gt1 |
⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐵 ) |
49 |
3 48
|
jca |
⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) |
50 |
49
|
3ad2ant1 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) |
51 |
|
cxplt |
⊢ ( ( ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( ( 𝐵 logb 𝑁 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) ) → ( ( 𝐵 logb 𝑁 ) < 𝐾 ↔ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) < ( 𝐵 ↑𝑐 𝐾 ) ) ) |
52 |
50 13 16 51
|
syl12anc |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( ( 𝐵 logb 𝑁 ) < 𝐾 ↔ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) < ( 𝐵 ↑𝑐 𝐾 ) ) ) |
53 |
47 52
|
mpbid |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) < ( 𝐵 ↑𝑐 𝐾 ) ) |
54 |
2 14 17 28 53
|
lelttrd |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝑁 < ( 𝐵 ↑𝑐 𝐾 ) ) |
55 |
|
eluzelcn |
⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℂ ) |
56 |
55
|
3ad2ant1 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝐵 ∈ ℂ ) |
57 |
|
eluz2n0 |
⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ≠ 0 ) |
58 |
57
|
3ad2ant1 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝐵 ≠ 0 ) |
59 |
|
eluzelz |
⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) → 𝐾 ∈ ℤ ) |
60 |
59
|
3ad2ant3 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝐾 ∈ ℤ ) |
61 |
|
cxpexpz |
⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐾 ∈ ℤ ) → ( 𝐵 ↑𝑐 𝐾 ) = ( 𝐵 ↑ 𝐾 ) ) |
62 |
61
|
breq2d |
⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 < ( 𝐵 ↑𝑐 𝐾 ) ↔ 𝑁 < ( 𝐵 ↑ 𝐾 ) ) ) |
63 |
56 58 60 62
|
syl3anc |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝑁 < ( 𝐵 ↑𝑐 𝐾 ) ↔ 𝑁 < ( 𝐵 ↑ 𝐾 ) ) ) |
64 |
54 63
|
mpbid |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝑁 < ( 𝐵 ↑ 𝐾 ) ) |