Theorem nnlog2ge0lt1

Description: A positive integer is 1 iff its binary logarithm is between 0 and 1. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	nnlog2ge0lt1	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = 1 ↔ ( 0 ≤ ( 2 logb 𝑁 ) ∧ ( 2 logb 𝑁 ) < 1 ) ) )

Proof

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 ) ) )