Step |
Hyp |
Ref |
Expression |
1 |
|
0le0 |
⊢ 0 ≤ 0 |
2 |
|
2cn |
⊢ 2 ∈ ℂ |
3 |
|
2ne0 |
⊢ 2 ≠ 0 |
4 |
|
1ne2 |
⊢ 1 ≠ 2 |
5 |
4
|
necomi |
⊢ 2 ≠ 1 |
6 |
|
logb1 |
⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 1 ) = 0 ) |
7 |
2 3 5 6
|
mp3an |
⊢ ( 2 logb 1 ) = 0 |
8 |
1 7
|
breqtrri |
⊢ 0 ≤ ( 2 logb 1 ) |
9 |
|
0lt1 |
⊢ 0 < 1 |
10 |
7 9
|
eqbrtri |
⊢ ( 2 logb 1 ) < 1 |
11 |
8 10
|
pm3.2i |
⊢ ( 0 ≤ ( 2 logb 1 ) ∧ ( 2 logb 1 ) < 1 ) |
12 |
|
oveq2 |
⊢ ( 𝑁 = 1 → ( 2 logb 𝑁 ) = ( 2 logb 1 ) ) |
13 |
12
|
breq2d |
⊢ ( 𝑁 = 1 → ( 0 ≤ ( 2 logb 𝑁 ) ↔ 0 ≤ ( 2 logb 1 ) ) ) |
14 |
12
|
breq1d |
⊢ ( 𝑁 = 1 → ( ( 2 logb 𝑁 ) < 1 ↔ ( 2 logb 1 ) < 1 ) ) |
15 |
13 14
|
anbi12d |
⊢ ( 𝑁 = 1 → ( ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ↔ ( 0 ≤ ( 2 logb 1 ) ∧ ( 2 logb 1 ) < 1 ) ) ) |
16 |
11 15
|
mpbiri |
⊢ ( 𝑁 = 1 → ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ) |
17 |
|
2z |
⊢ 2 ∈ ℤ |
18 |
|
uzid |
⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) ) |
19 |
17 18
|
ax-mp |
⊢ 2 ∈ ( ℤ≥ ‘ 2 ) |
20 |
19
|
a1i |
⊢ ( 𝑁 ∈ ℕ → 2 ∈ ( ℤ≥ ‘ 2 ) ) |
21 |
|
nnrp |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ ) |
22 |
|
logbge0b |
⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℝ+ ) → ( 0 ≤ ( 2 logb 𝑁 ) ↔ 1 ≤ 𝑁 ) ) |
23 |
20 21 22
|
syl2anc |
⊢ ( 𝑁 ∈ ℕ → ( 0 ≤ ( 2 logb 𝑁 ) ↔ 1 ≤ 𝑁 ) ) |
24 |
|
logblt1b |
⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℝ+ ) → ( ( 2 logb 𝑁 ) < 1 ↔ 𝑁 < 2 ) ) |
25 |
20 21 24
|
syl2anc |
⊢ ( 𝑁 ∈ ℕ → ( ( 2 logb 𝑁 ) < 1 ↔ 𝑁 < 2 ) ) |
26 |
23 25
|
anbi12d |
⊢ ( 𝑁 ∈ ℕ → ( ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ↔ ( 1 ≤ 𝑁 ∧ 𝑁 < 2 ) ) ) |
27 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
28 |
27
|
breq2i |
⊢ ( 𝑁 < 2 ↔ 𝑁 < ( 1 + 1 ) ) |
29 |
28
|
a1i |
⊢ ( 𝑁 ∈ ℕ → ( 𝑁 < 2 ↔ 𝑁 < ( 1 + 1 ) ) ) |
30 |
29
|
anbi2d |
⊢ ( 𝑁 ∈ ℕ → ( ( 1 ≤ 𝑁 ∧ 𝑁 < 2 ) ↔ ( 1 ≤ 𝑁 ∧ 𝑁 < ( 1 + 1 ) ) ) ) |
31 |
|
nnre |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ ) |
32 |
|
1zzd |
⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℤ ) |
33 |
|
flbi |
⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℤ ) → ( ( ⌊ ‘ 𝑁 ) = 1 ↔ ( 1 ≤ 𝑁 ∧ 𝑁 < ( 1 + 1 ) ) ) ) |
34 |
31 32 33
|
syl2anc |
⊢ ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ 𝑁 ) = 1 ↔ ( 1 ≤ 𝑁 ∧ 𝑁 < ( 1 + 1 ) ) ) ) |
35 |
30 34
|
bitr4d |
⊢ ( 𝑁 ∈ ℕ → ( ( 1 ≤ 𝑁 ∧ 𝑁 < 2 ) ↔ ( ⌊ ‘ 𝑁 ) = 1 ) ) |
36 |
|
nnz |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ ) |
37 |
|
flid |
⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ 𝑁 ) = 𝑁 ) |
38 |
36 37
|
syl |
⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ 𝑁 ) = 𝑁 ) |
39 |
38
|
eqcomd |
⊢ ( 𝑁 ∈ ℕ → 𝑁 = ( ⌊ ‘ 𝑁 ) ) |
40 |
39
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( ⌊ ‘ 𝑁 ) = 1 ) → 𝑁 = ( ⌊ ‘ 𝑁 ) ) |
41 |
|
simpr |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( ⌊ ‘ 𝑁 ) = 1 ) → ( ⌊ ‘ 𝑁 ) = 1 ) |
42 |
40 41
|
eqtrd |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( ⌊ ‘ 𝑁 ) = 1 ) → 𝑁 = 1 ) |
43 |
42
|
ex |
⊢ ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ 𝑁 ) = 1 → 𝑁 = 1 ) ) |
44 |
35 43
|
sylbid |
⊢ ( 𝑁 ∈ ℕ → ( ( 1 ≤ 𝑁 ∧ 𝑁 < 2 ) → 𝑁 = 1 ) ) |
45 |
26 44
|
sylbid |
⊢ ( 𝑁 ∈ ℕ → ( ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) → 𝑁 = 1 ) ) |
46 |
16 45
|
impbid2 |
⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = 1 ↔ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ) ) |