Metamath Proof Explorer

Theorem oddfl

Description: Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion oddfl 
|- ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> K = ( ( 2 x. ( |_ ` ( K / 2 ) ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( K e. ZZ -> K e. RR )
2 1red 
 |-  ( K e. ZZ -> 1 e. RR )
3 1 2 resubcld 
 |-  ( K e. ZZ -> ( K - 1 ) e. RR )
4 2rp 
 |-  2 e. RR+
5 4 a1i 
 |-  ( K e. ZZ -> 2 e. RR+ )
6 1 lem1d 
 |-  ( K e. ZZ -> ( K - 1 ) <_ K )
7 3 1 5 6 lediv1dd 
 |-  ( K e. ZZ -> ( ( K - 1 ) / 2 ) <_ ( K / 2 ) )
8 1 rehalfcld 
 |-  ( K e. ZZ -> ( K / 2 ) e. RR )
9 5 rpreccld 
 |-  ( K e. ZZ -> ( 1 / 2 ) e. RR+ )
10 8 9 ltaddrpd 
 |-  ( K e. ZZ -> ( K / 2 ) < ( ( K / 2 ) + ( 1 / 2 ) ) )
11 zcn 
 |-  ( K e. ZZ -> K e. CC )
12 2 recnd 
 |-  ( K e. ZZ -> 1 e. CC )
13 2cnd 
 |-  ( K e. ZZ -> 2 e. CC )
14 5 rpne0d 
 |-  ( K e. ZZ -> 2 =/= 0 )
15 11 12 13 14 divsubdird 
 |-  ( K e. ZZ -> ( ( K - 1 ) / 2 ) = ( ( K / 2 ) - ( 1 / 2 ) ) )
16 15 oveq1d 
 |-  ( K e. ZZ -> ( ( ( K - 1 ) / 2 ) + 1 ) = ( ( ( K / 2 ) - ( 1 / 2 ) ) + 1 ) )
17 11 halfcld 
 |-  ( K e. ZZ -> ( K / 2 ) e. CC )
18 13 14 reccld 
 |-  ( K e. ZZ -> ( 1 / 2 ) e. CC )
19 17 18 12 subadd23d 
 |-  ( K e. ZZ -> ( ( ( K / 2 ) - ( 1 / 2 ) ) + 1 ) = ( ( K / 2 ) + ( 1 - ( 1 / 2 ) ) ) )
20 1mhlfehlf 
 |-  ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
21 20 oveq2i 
 |-  ( ( K / 2 ) + ( 1 - ( 1 / 2 ) ) ) = ( ( K / 2 ) + ( 1 / 2 ) )
22 21 a1i 
 |-  ( K e. ZZ -> ( ( K / 2 ) + ( 1 - ( 1 / 2 ) ) ) = ( ( K / 2 ) + ( 1 / 2 ) ) )
23 16 19 22 3eqtrrd 
 |-  ( K e. ZZ -> ( ( K / 2 ) + ( 1 / 2 ) ) = ( ( ( K - 1 ) / 2 ) + 1 ) )
24 10 23 breqtrd 
 |-  ( K e. ZZ -> ( K / 2 ) < ( ( ( K - 1 ) / 2 ) + 1 ) )
25 7 24 jca 
 |-  ( K e. ZZ -> ( ( ( K - 1 ) / 2 ) <_ ( K / 2 ) /\ ( K / 2 ) < ( ( ( K - 1 ) / 2 ) + 1 ) ) )
26 25 adantr 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( ( ( K - 1 ) / 2 ) <_ ( K / 2 ) /\ ( K / 2 ) < ( ( ( K - 1 ) / 2 ) + 1 ) ) )
27 1 adantr 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> K e. RR )
28 27 rehalfcld 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( K / 2 ) e. RR )
29 11 12 npcand 
 |-  ( K e. ZZ -> ( ( K - 1 ) + 1 ) = K )
30 29 oveq1d 
 |-  ( K e. ZZ -> ( ( ( K - 1 ) + 1 ) / 2 ) = ( K / 2 ) )
31 30 adantr 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( ( ( K - 1 ) + 1 ) / 2 ) = ( K / 2 ) )
32 simpr 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( K mod 2 ) =/= 0 )
33 32 neneqd 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> -. ( K mod 2 ) = 0 )
34 mod0 
 |-  ( ( K e. RR /\ 2 e. RR+ ) -> ( ( K mod 2 ) = 0 <-> ( K / 2 ) e. ZZ ) )
35 1 5 34 syl2anc 
 |-  ( K e. ZZ -> ( ( K mod 2 ) = 0 <-> ( K / 2 ) e. ZZ ) )
36 35 adantr 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( ( K mod 2 ) = 0 <-> ( K / 2 ) e. ZZ ) )
37 33 36 mtbid 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> -. ( K / 2 ) e. ZZ )
38 31 37 eqneltrd 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> -. ( ( ( K - 1 ) + 1 ) / 2 ) e. ZZ )
39 simpl 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> K e. ZZ )
40 1zzd 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> 1 e. ZZ )
41 39 40 zsubcld 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( K - 1 ) e. ZZ )
42 zeo2 
 |-  ( ( K - 1 ) e. ZZ -> ( ( ( K - 1 ) / 2 ) e. ZZ <-> -. ( ( ( K - 1 ) + 1 ) / 2 ) e. ZZ ) )
43 41 42 syl 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( ( ( K - 1 ) / 2 ) e. ZZ <-> -. ( ( ( K - 1 ) + 1 ) / 2 ) e. ZZ ) )
44 38 43 mpbird 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( ( K - 1 ) / 2 ) e. ZZ )
45 flbi 
 |-  ( ( ( K / 2 ) e. RR /\ ( ( K - 1 ) / 2 ) e. ZZ ) -> ( ( |_ ` ( K / 2 ) ) = ( ( K - 1 ) / 2 ) <-> ( ( ( K - 1 ) / 2 ) <_ ( K / 2 ) /\ ( K / 2 ) < ( ( ( K - 1 ) / 2 ) + 1 ) ) ) )
46 28 44 45 syl2anc 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( ( |_ ` ( K / 2 ) ) = ( ( K - 1 ) / 2 ) <-> ( ( ( K - 1 ) / 2 ) <_ ( K / 2 ) /\ ( K / 2 ) < ( ( ( K - 1 ) / 2 ) + 1 ) ) ) )
47 26 46 mpbird 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( |_ ` ( K / 2 ) ) = ( ( K - 1 ) / 2 ) )
48 47 oveq2d 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( 2 x. ( |_ ` ( K / 2 ) ) ) = ( 2 x. ( ( K - 1 ) / 2 ) ) )
49 48 oveq1d 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( ( 2 x. ( |_ ` ( K / 2 ) ) ) + 1 ) = ( ( 2 x. ( ( K - 1 ) / 2 ) ) + 1 ) )
50 11 12 subcld 
 |-  ( K e. ZZ -> ( K - 1 ) e. CC )
51 50 13 14 divcan2d 
 |-  ( K e. ZZ -> ( 2 x. ( ( K - 1 ) / 2 ) ) = ( K - 1 ) )
52 51 oveq1d 
 |-  ( K e. ZZ -> ( ( 2 x. ( ( K - 1 ) / 2 ) ) + 1 ) = ( ( K - 1 ) + 1 ) )
53 52 adantr 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( ( 2 x. ( ( K - 1 ) / 2 ) ) + 1 ) = ( ( K - 1 ) + 1 ) )
54 29 adantr 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> ( ( K - 1 ) + 1 ) = K )
55 49 53 54 3eqtrrd 
 |-  ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> K = ( ( 2 x. ( |_ ` ( K / 2 ) ) ) + 1 ) )