Metamath Proof Explorer

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 
|- ( N e. NN -> ( N = 1 <-> ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) ) )

Proof

Step Hyp Ref Expression
1 0le0 
 |-  0 <_ 0
2 2cn 
 |-  2 e. CC
3 2ne0 
 |-  2 =/= 0
4 1ne2 
 |-  1 =/= 2
5 4 necomi 
 |-  2 =/= 1
6 logb1 
 |-  ( ( 2 e. CC /\ 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 
 |-  ( N = 1 -> ( 2 logb N ) = ( 2 logb 1 ) )
13 12 breq2d 
 |-  ( N = 1 -> ( 0 <_ ( 2 logb N ) <-> 0 <_ ( 2 logb 1 ) ) )
14 12 breq1d 
 |-  ( N = 1 -> ( ( 2 logb N ) < 1 <-> ( 2 logb 1 ) < 1 ) )
15 13 14 anbi12d 
 |-  ( N = 1 -> ( ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) <-> ( 0 <_ ( 2 logb 1 ) /\ ( 2 logb 1 ) < 1 ) ) )
16 11 15 mpbiri 
 |-  ( N = 1 -> ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) )
17 2z 
 |-  2 e. ZZ
18 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
19 17 18 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
20 19 a1i 
 |-  ( N e. NN -> 2 e. ( ZZ>= ` 2 ) )
21 nnrp 
 |-  ( N e. NN -> N e. RR+ )
22 logbge0b 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ N e. RR+ ) -> ( 0 <_ ( 2 logb N ) <-> 1 <_ N ) )
23 20 21 22 syl2anc 
 |-  ( N e. NN -> ( 0 <_ ( 2 logb N ) <-> 1 <_ N ) )
24 logblt1b 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ N e. RR+ ) -> ( ( 2 logb N ) < 1 <-> N < 2 ) )
25 20 21 24 syl2anc 
 |-  ( N e. NN -> ( ( 2 logb N ) < 1 <-> N < 2 ) )
26 23 25 anbi12d 
 |-  ( N e. NN -> ( ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) <-> ( 1 <_ N /\ N < 2 ) ) )
27 df-2 
 |-  2 = ( 1 + 1 )
28 27 breq2i 
 |-  ( N < 2 <-> N < ( 1 + 1 ) )
29 28 a1i 
 |-  ( N e. NN -> ( N < 2 <-> N < ( 1 + 1 ) ) )
30 29 anbi2d 
 |-  ( N e. NN -> ( ( 1 <_ N /\ N < 2 ) <-> ( 1 <_ N /\ N < ( 1 + 1 ) ) ) )
31 nnre 
 |-  ( N e. NN -> N e. RR )
32 1zzd 
 |-  ( N e. NN -> 1 e. ZZ )
33 flbi 
 |-  ( ( N e. RR /\ 1 e. ZZ ) -> ( ( |_ ` N ) = 1 <-> ( 1 <_ N /\ N < ( 1 + 1 ) ) ) )
34 31 32 33 syl2anc 
 |-  ( N e. NN -> ( ( |_ ` N ) = 1 <-> ( 1 <_ N /\ N < ( 1 + 1 ) ) ) )
35 30 34 bitr4d 
 |-  ( N e. NN -> ( ( 1 <_ N /\ N < 2 ) <-> ( |_ ` N ) = 1 ) )
36 nnz 
 |-  ( N e. NN -> N e. ZZ )
37 flid 
 |-  ( N e. ZZ -> ( |_ ` N ) = N )
38 36 37 syl 
 |-  ( N e. NN -> ( |_ ` N ) = N )
39 38 eqcomd 
 |-  ( N e. NN -> N = ( |_ ` N ) )
40 39 adantr 
 |-  ( ( N e. NN /\ ( |_ ` N ) = 1 ) -> N = ( |_ ` N ) )
41 simpr 
 |-  ( ( N e. NN /\ ( |_ ` N ) = 1 ) -> ( |_ ` N ) = 1 )
42 40 41 eqtrd 
 |-  ( ( N e. NN /\ ( |_ ` N ) = 1 ) -> N = 1 )
43 42 ex 
 |-  ( N e. NN -> ( ( |_ ` N ) = 1 -> N = 1 ) )
44 35 43 sylbid 
 |-  ( N e. NN -> ( ( 1 <_ N /\ N < 2 ) -> N = 1 ) )
45 26 44 sylbid 
 |-  ( N e. NN -> ( ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) -> N = 1 ) )
46 16 45 impbid2 
 |-  ( N e. NN -> ( N = 1 <-> ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) ) )