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 K mod 2 0 K = 2 K 2 + 1

Proof

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