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 KKmod20K=2K2+1

Proof

Step Hyp Ref Expression
1 zre KK
2 1red K1
3 1 2 resubcld KK1
4 2rp 2+
5 4 a1i K2+
6 1 lem1d KK1K
7 3 1 5 6 lediv1dd KK12K2
8 1 rehalfcld KK2
9 5 rpreccld K12+
10 8 9 ltaddrpd KK2<K2+12
11 zcn KK
12 2 recnd K1
13 2cnd K2
14 5 rpne0d K20
15 11 12 13 14 divsubdird KK12=K212
16 15 oveq1d KK12+1=K2-12+1
17 11 halfcld KK2
18 13 14 reccld K12
19 17 18 12 subadd23d KK2-12+1=K2+1-12
20 1mhlfehlf 112=12
21 20 oveq2i K2+1-12=K2+12
22 21 a1i KK2+1-12=K2+12
23 16 19 22 3eqtrrd KK2+12=K12+1
24 10 23 breqtrd KK2<K12+1
25 7 24 jca KK12K2K2<K12+1
26 25 adantr KKmod20K12K2K2<K12+1
27 1 adantr KKmod20K
28 27 rehalfcld KKmod20K2
29 11 12 npcand KK-1+1=K
30 29 oveq1d KK-1+12=K2
31 30 adantr KKmod20K-1+12=K2
32 simpr KKmod20Kmod20
33 32 neneqd KKmod20¬Kmod2=0
34 mod0 K2+Kmod2=0K2
35 1 5 34 syl2anc KKmod2=0K2
36 35 adantr KKmod20Kmod2=0K2
37 33 36 mtbid KKmod20¬K2
38 31 37 eqneltrd KKmod20¬K-1+12
39 simpl KKmod20K
40 1zzd KKmod201
41 39 40 zsubcld KKmod20K1
42 zeo2 K1K12¬K-1+12
43 41 42 syl KKmod20K12¬K-1+12
44 38 43 mpbird KKmod20K12
45 flbi K2K12K2=K12K12K2K2<K12+1
46 28 44 45 syl2anc KKmod20K2=K12K12K2K2<K12+1
47 26 46 mpbird KKmod20K2=K12
48 47 oveq2d KKmod202K2=2K12
49 48 oveq1d KKmod202K2+1=2K12+1
50 11 12 subcld KK1
51 50 13 14 divcan2d K2K12=K1
52 51 oveq1d K2K12+1=K-1+1
53 52 adantr KKmod202K12+1=K-1+1
54 29 adantr KKmod20K-1+1=K
55 49 53 54 3eqtrrd KKmod20K=2K2+1