Description: Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | oddfl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zre | |
|
2 | 1red | |
|
3 | 1 2 | resubcld | |
4 | 2rp | |
|
5 | 4 | a1i | |
6 | 1 | lem1d | |
7 | 3 1 5 6 | lediv1dd | |
8 | 1 | rehalfcld | |
9 | 5 | rpreccld | |
10 | 8 9 | ltaddrpd | |
11 | zcn | |
|
12 | 2 | recnd | |
13 | 2cnd | |
|
14 | 5 | rpne0d | |
15 | 11 12 13 14 | divsubdird | |
16 | 15 | oveq1d | |
17 | 11 | halfcld | |
18 | 13 14 | reccld | |
19 | 17 18 12 | subadd23d | |
20 | 1mhlfehlf | |
|
21 | 20 | oveq2i | |
22 | 21 | a1i | |
23 | 16 19 22 | 3eqtrrd | |
24 | 10 23 | breqtrd | |
25 | 7 24 | jca | |
26 | 25 | adantr | |
27 | 1 | adantr | |
28 | 27 | rehalfcld | |
29 | 11 12 | npcand | |
30 | 29 | oveq1d | |
31 | 30 | adantr | |
32 | simpr | |
|
33 | 32 | neneqd | |
34 | mod0 | |
|
35 | 1 5 34 | syl2anc | |
36 | 35 | adantr | |
37 | 33 36 | mtbid | |
38 | 31 37 | eqneltrd | |
39 | simpl | |
|
40 | 1zzd | |
|
41 | 39 40 | zsubcld | |
42 | zeo2 | |
|
43 | 41 42 | syl | |
44 | 38 43 | mpbird | |
45 | flbi | |
|
46 | 28 44 45 | syl2anc | |
47 | 26 46 | mpbird | |
48 | 47 | oveq2d | |
49 | 48 | oveq1d | |
50 | 11 12 | subcld | |
51 | 50 13 14 | divcan2d | |
52 | 51 | oveq1d | |
53 | 52 | adantr | |
54 | 29 | adantr | |
55 | 49 53 54 | 3eqtrrd | |