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 ) )