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 ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → 𝐾 = ( ( 2 · ( ⌊ ‘ ( 𝐾 / 2 ) ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 zre ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
2 1red ( 𝐾 ∈ ℤ → 1 ∈ ℝ )
3 1 2 resubcld ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℝ )
4 2rp 2 ∈ ℝ+
5 4 a1i ( 𝐾 ∈ ℤ → 2 ∈ ℝ+ )
6 1 lem1d ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ≤ 𝐾 )
7 3 1 5 6 lediv1dd ( 𝐾 ∈ ℤ → ( ( 𝐾 − 1 ) / 2 ) ≤ ( 𝐾 / 2 ) )
8 1 rehalfcld ( 𝐾 ∈ ℤ → ( 𝐾 / 2 ) ∈ ℝ )
9 5 rpreccld ( 𝐾 ∈ ℤ → ( 1 / 2 ) ∈ ℝ+ )
10 8 9 ltaddrpd ( 𝐾 ∈ ℤ → ( 𝐾 / 2 ) < ( ( 𝐾 / 2 ) + ( 1 / 2 ) ) )
11 zcn ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
12 2 recnd ( 𝐾 ∈ ℤ → 1 ∈ ℂ )
13 2cnd ( 𝐾 ∈ ℤ → 2 ∈ ℂ )
14 5 rpne0d ( 𝐾 ∈ ℤ → 2 ≠ 0 )
15 11 12 13 14 divsubdird ( 𝐾 ∈ ℤ → ( ( 𝐾 − 1 ) / 2 ) = ( ( 𝐾 / 2 ) − ( 1 / 2 ) ) )
16 15 oveq1d ( 𝐾 ∈ ℤ → ( ( ( 𝐾 − 1 ) / 2 ) + 1 ) = ( ( ( 𝐾 / 2 ) − ( 1 / 2 ) ) + 1 ) )
17 11 halfcld ( 𝐾 ∈ ℤ → ( 𝐾 / 2 ) ∈ ℂ )
18 13 14 reccld ( 𝐾 ∈ ℤ → ( 1 / 2 ) ∈ ℂ )
19 17 18 12 subadd23d ( 𝐾 ∈ ℤ → ( ( ( 𝐾 / 2 ) − ( 1 / 2 ) ) + 1 ) = ( ( 𝐾 / 2 ) + ( 1 − ( 1 / 2 ) ) ) )
20 1mhlfehlf ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )
21 20 oveq2i ( ( 𝐾 / 2 ) + ( 1 − ( 1 / 2 ) ) ) = ( ( 𝐾 / 2 ) + ( 1 / 2 ) )
22 21 a1i ( 𝐾 ∈ ℤ → ( ( 𝐾 / 2 ) + ( 1 − ( 1 / 2 ) ) ) = ( ( 𝐾 / 2 ) + ( 1 / 2 ) ) )
23 16 19 22 3eqtrrd ( 𝐾 ∈ ℤ → ( ( 𝐾 / 2 ) + ( 1 / 2 ) ) = ( ( ( 𝐾 − 1 ) / 2 ) + 1 ) )
24 10 23 breqtrd ( 𝐾 ∈ ℤ → ( 𝐾 / 2 ) < ( ( ( 𝐾 − 1 ) / 2 ) + 1 ) )
25 7 24 jca ( 𝐾 ∈ ℤ → ( ( ( 𝐾 − 1 ) / 2 ) ≤ ( 𝐾 / 2 ) ∧ ( 𝐾 / 2 ) < ( ( ( 𝐾 − 1 ) / 2 ) + 1 ) ) )
26 25 adantr ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( ( ( 𝐾 − 1 ) / 2 ) ≤ ( 𝐾 / 2 ) ∧ ( 𝐾 / 2 ) < ( ( ( 𝐾 − 1 ) / 2 ) + 1 ) ) )
27 1 adantr ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → 𝐾 ∈ ℝ )
28 27 rehalfcld ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( 𝐾 / 2 ) ∈ ℝ )
29 11 12 npcand ( 𝐾 ∈ ℤ → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
30 29 oveq1d ( 𝐾 ∈ ℤ → ( ( ( 𝐾 − 1 ) + 1 ) / 2 ) = ( 𝐾 / 2 ) )
31 30 adantr ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( ( ( 𝐾 − 1 ) + 1 ) / 2 ) = ( 𝐾 / 2 ) )
32 simpr ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( 𝐾 mod 2 ) ≠ 0 )
33 32 neneqd ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ¬ ( 𝐾 mod 2 ) = 0 )
34 mod0 ( ( 𝐾 ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ( 𝐾 mod 2 ) = 0 ↔ ( 𝐾 / 2 ) ∈ ℤ ) )
35 1 5 34 syl2anc ( 𝐾 ∈ ℤ → ( ( 𝐾 mod 2 ) = 0 ↔ ( 𝐾 / 2 ) ∈ ℤ ) )
36 35 adantr ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( ( 𝐾 mod 2 ) = 0 ↔ ( 𝐾 / 2 ) ∈ ℤ ) )
37 33 36 mtbid ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ¬ ( 𝐾 / 2 ) ∈ ℤ )
38 31 37 eqneltrd ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ¬ ( ( ( 𝐾 − 1 ) + 1 ) / 2 ) ∈ ℤ )
39 simpl ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → 𝐾 ∈ ℤ )
40 1zzd ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → 1 ∈ ℤ )
41 39 40 zsubcld ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( 𝐾 − 1 ) ∈ ℤ )
42 zeo2 ( ( 𝐾 − 1 ) ∈ ℤ → ( ( ( 𝐾 − 1 ) / 2 ) ∈ ℤ ↔ ¬ ( ( ( 𝐾 − 1 ) + 1 ) / 2 ) ∈ ℤ ) )
43 41 42 syl ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( ( ( 𝐾 − 1 ) / 2 ) ∈ ℤ ↔ ¬ ( ( ( 𝐾 − 1 ) + 1 ) / 2 ) ∈ ℤ ) )
44 38 43 mpbird ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( ( 𝐾 − 1 ) / 2 ) ∈ ℤ )
45 flbi ( ( ( 𝐾 / 2 ) ∈ ℝ ∧ ( ( 𝐾 − 1 ) / 2 ) ∈ ℤ ) → ( ( ⌊ ‘ ( 𝐾 / 2 ) ) = ( ( 𝐾 − 1 ) / 2 ) ↔ ( ( ( 𝐾 − 1 ) / 2 ) ≤ ( 𝐾 / 2 ) ∧ ( 𝐾 / 2 ) < ( ( ( 𝐾 − 1 ) / 2 ) + 1 ) ) ) )
46 28 44 45 syl2anc ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( ( ⌊ ‘ ( 𝐾 / 2 ) ) = ( ( 𝐾 − 1 ) / 2 ) ↔ ( ( ( 𝐾 − 1 ) / 2 ) ≤ ( 𝐾 / 2 ) ∧ ( 𝐾 / 2 ) < ( ( ( 𝐾 − 1 ) / 2 ) + 1 ) ) ) )
47 26 46 mpbird ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( ⌊ ‘ ( 𝐾 / 2 ) ) = ( ( 𝐾 − 1 ) / 2 ) )
48 47 oveq2d ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( 2 · ( ⌊ ‘ ( 𝐾 / 2 ) ) ) = ( 2 · ( ( 𝐾 − 1 ) / 2 ) ) )
49 48 oveq1d ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( ( 2 · ( ⌊ ‘ ( 𝐾 / 2 ) ) ) + 1 ) = ( ( 2 · ( ( 𝐾 − 1 ) / 2 ) ) + 1 ) )
50 11 12 subcld ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℂ )
51 50 13 14 divcan2d ( 𝐾 ∈ ℤ → ( 2 · ( ( 𝐾 − 1 ) / 2 ) ) = ( 𝐾 − 1 ) )
52 51 oveq1d ( 𝐾 ∈ ℤ → ( ( 2 · ( ( 𝐾 − 1 ) / 2 ) ) + 1 ) = ( ( 𝐾 − 1 ) + 1 ) )
53 52 adantr ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( ( 2 · ( ( 𝐾 − 1 ) / 2 ) ) + 1 ) = ( ( 𝐾 − 1 ) + 1 ) )
54 29 adantr ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
55 49 53 54 3eqtrrd ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 mod 2 ) ≠ 0 ) → 𝐾 = ( ( 2 · ( ⌊ ‘ ( 𝐾 / 2 ) ) ) + 1 ) )