Metamath Proof Explorer

Theorem blen1b

Description: The binary length of a nonnegative integer is 1 if the integer is 0 or 1. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion blen1b 
|- ( N e. NN0 -> ( ( #b ` N ) = 1 <-> ( N = 0 \/ N = 1 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 blennn 
 |-  ( N e. NN -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
3 2 eqeq1d 
 |-  ( N e. NN -> ( ( #b ` N ) = 1 <-> ( ( |_ ` ( 2 logb N ) ) + 1 ) = 1 ) )
4 2rp 
 |-  2 e. RR+
5 4 a1i 
 |-  ( N e. NN -> 2 e. RR+ )
6 nnrp 
 |-  ( N e. NN -> N e. RR+ )
7 1ne2 
 |-  1 =/= 2
8 7 necomi 
 |-  2 =/= 1
9 8 a1i 
 |-  ( N e. NN -> 2 =/= 1 )
10 relogbcl 
 |-  ( ( 2 e. RR+ /\ N e. RR+ /\ 2 =/= 1 ) -> ( 2 logb N ) e. RR )
11 5 6 9 10 syl3anc 
 |-  ( N e. NN -> ( 2 logb N ) e. RR )
12 11 flcld 
 |-  ( N e. NN -> ( |_ ` ( 2 logb N ) ) e. ZZ )
13 12 zcnd 
 |-  ( N e. NN -> ( |_ ` ( 2 logb N ) ) e. CC )
14 1cnd 
 |-  ( N e. NN -> 1 e. CC )
15 13 14 14 addlsub 
 |-  ( N e. NN -> ( ( ( |_ ` ( 2 logb N ) ) + 1 ) = 1 <-> ( |_ ` ( 2 logb N ) ) = ( 1 - 1 ) ) )
16 1m1e0 
 |-  ( 1 - 1 ) = 0
17 16 a1i 
 |-  ( N e. NN -> ( 1 - 1 ) = 0 )
18 17 eqeq2d 
 |-  ( N e. NN -> ( ( |_ ` ( 2 logb N ) ) = ( 1 - 1 ) <-> ( |_ ` ( 2 logb N ) ) = 0 ) )
19 0z 
 |-  0 e. ZZ
20 flbi 
 |-  ( ( ( 2 logb N ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( 2 logb N ) ) = 0 <-> ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < ( 0 + 1 ) ) ) )
21 11 19 20 sylancl 
 |-  ( N e. NN -> ( ( |_ ` ( 2 logb N ) ) = 0 <-> ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < ( 0 + 1 ) ) ) )
22 15 18 21 3bitrd 
 |-  ( N e. NN -> ( ( ( |_ ` ( 2 logb N ) ) + 1 ) = 1 <-> ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < ( 0 + 1 ) ) ) )
23 0p1e1 
 |-  ( 0 + 1 ) = 1
24 23 breq2i 
 |-  ( ( 2 logb N ) < ( 0 + 1 ) <-> ( 2 logb N ) < 1 )
25 24 anbi2i 
 |-  ( ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < ( 0 + 1 ) ) <-> ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) )
26 nnlog2ge0lt1 
 |-  ( N e. NN -> ( N = 1 <-> ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) ) )
27 26 biimpar 
 |-  ( ( N e. NN /\ ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) ) -> N = 1 )
28 27 olcd 
 |-  ( ( N e. NN /\ ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) ) -> ( N = 0 \/ N = 1 ) )
29 28 ex 
 |-  ( N e. NN -> ( ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) -> ( N = 0 \/ N = 1 ) ) )
30 25 29 syl5bi 
 |-  ( N e. NN -> ( ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < ( 0 + 1 ) ) -> ( N = 0 \/ N = 1 ) ) )
31 22 30 sylbid 
 |-  ( N e. NN -> ( ( ( |_ ` ( 2 logb N ) ) + 1 ) = 1 -> ( N = 0 \/ N = 1 ) ) )
32 3 31 sylbid 
 |-  ( N e. NN -> ( ( #b ` N ) = 1 -> ( N = 0 \/ N = 1 ) ) )
33 orc 
 |-  ( N = 0 -> ( N = 0 \/ N = 1 ) )
34 33 a1d 
 |-  ( N = 0 -> ( ( #b ` N ) = 1 -> ( N = 0 \/ N = 1 ) ) )
35 32 34 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( ( #b ` N ) = 1 -> ( N = 0 \/ N = 1 ) ) )
36 1 35 sylbi 
 |-  ( N e. NN0 -> ( ( #b ` N ) = 1 -> ( N = 0 \/ N = 1 ) ) )
37 fveq2 
 |-  ( N = 0 -> ( #b ` N ) = ( #b ` 0 ) )
38 blen0 
 |-  ( #b ` 0 ) = 1
39 37 38 eqtrdi 
 |-  ( N = 0 -> ( #b ` N ) = 1 )
40 fveq2 
 |-  ( N = 1 -> ( #b ` N ) = ( #b ` 1 ) )
41 blen1 
 |-  ( #b ` 1 ) = 1
42 40 41 eqtrdi 
 |-  ( N = 1 -> ( #b ` N ) = 1 )
43 39 42 jaoi 
 |-  ( ( N = 0 \/ N = 1 ) -> ( #b ` N ) = 1 )
44 36 43 impbid1 
 |-  ( N e. NN0 -> ( ( #b ` N ) = 1 <-> ( N = 0 \/ N = 1 ) ) )