oddfl

Description: Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	oddfl	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to K = 2 ⌊\frac{K}{2}⌋ + 1$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ K \in ℤ \to K \in ℝ$
2		1red	$⊢ K \in ℤ \to 1 \in ℝ$
3	1 2	resubcld	$⊢ K \in ℤ \to K - 1 \in ℝ$
4		2rp	$⊢ 2 \in ℝ^{+}$
5	4	a1i	$⊢ K \in ℤ \to 2 \in ℝ^{+}$
6	1	lem1d	$⊢ K \in ℤ \to K - 1 \leq K$
7	3 1 5 6	lediv1dd	$⊢ K \in ℤ \to \frac{K - 1}{2} \leq \frac{K}{2}$
8	1	rehalfcld	$⊢ K \in ℤ \to \frac{K}{2} \in ℝ$
9	5	rpreccld	$⊢ K \in ℤ \to \frac{1}{2} \in ℝ^{+}$
10	8 9	ltaddrpd	$⊢ K \in ℤ \to \frac{K}{2} < (\frac{K}{2}) + (\frac{1}{2})$
11		zcn	$⊢ K \in ℤ \to K \in ℂ$
12	2	recnd	$⊢ K \in ℤ \to 1 \in ℂ$
13		2cnd	$⊢ K \in ℤ \to 2 \in ℂ$
14	5	rpne0d	$⊢ K \in ℤ \to 2 \neq 0$
15	11 12 13 14	divsubdird	$⊢ K \in ℤ \to \frac{K - 1}{2} = (\frac{K}{2}) - (\frac{1}{2})$
16	15	oveq1d	$⊢ K \in ℤ \to (\frac{K - 1}{2}) + 1 = (\frac{K}{2}) - (\frac{1}{2}) + 1$
17	11	halfcld	$⊢ K \in ℤ \to \frac{K}{2} \in ℂ$
18	13 14	reccld	$⊢ K \in ℤ \to \frac{1}{2} \in ℂ$
19	17 18 12	subadd23d	$⊢ K \in ℤ \to (\frac{K}{2}) - (\frac{1}{2}) + 1 = (\frac{K}{2}) + 1 - (\frac{1}{2})$
20		1mhlfehlf	$⊢ 1 - (\frac{1}{2}) = \frac{1}{2}$
21	20	oveq2i	$⊢ (\frac{K}{2}) + 1 - (\frac{1}{2}) = (\frac{K}{2}) + (\frac{1}{2})$
22	21	a1i	$⊢ K \in ℤ \to (\frac{K}{2}) + 1 - (\frac{1}{2}) = (\frac{K}{2}) + (\frac{1}{2})$
23	16 19 22	3eqtrrd	$⊢ K \in ℤ \to (\frac{K}{2}) + (\frac{1}{2}) = (\frac{K - 1}{2}) + 1$
24	10 23	breqtrd	$⊢ K \in ℤ \to \frac{K}{2} < (\frac{K - 1}{2}) + 1$
25	7 24	jca	$⊢ K \in ℤ \to (\frac{K - 1}{2} \leq \frac{K}{2} \land \frac{K}{2} < (\frac{K - 1}{2}) + 1)$
26	25	adantr	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to (\frac{K - 1}{2} \leq \frac{K}{2} \land \frac{K}{2} < (\frac{K - 1}{2}) + 1)$
27	1	adantr	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to K \in ℝ$
28	27	rehalfcld	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to \frac{K}{2} \in ℝ$
29	11 12	npcand	$⊢ K \in ℤ \to K - 1 + 1 = K$
30	29	oveq1d	$⊢ K \in ℤ \to \frac{K - 1 + 1}{2} = \frac{K}{2}$
31	30	adantr	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to \frac{K - 1 + 1}{2} = \frac{K}{2}$
32		simpr	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to K \mod 2 \neq 0$
33	32	neneqd	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to \neg K \mod 2 = 0$
34		mod0	$⊢ (K \in ℝ \land 2 \in ℝ^{+}) \to (K \mod 2 = 0 \leftrightarrow \frac{K}{2} \in ℤ)$
35	1 5 34	syl2anc	$⊢ K \in ℤ \to (K \mod 2 = 0 \leftrightarrow \frac{K}{2} \in ℤ)$
36	35	adantr	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to (K \mod 2 = 0 \leftrightarrow \frac{K}{2} \in ℤ)$
37	33 36	mtbid	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to \neg \frac{K}{2} \in ℤ$
38	31 37	eqneltrd	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to \neg \frac{K - 1 + 1}{2} \in ℤ$
39		simpl	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to K \in ℤ$
40		1zzd	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to 1 \in ℤ$
41	39 40	zsubcld	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to K - 1 \in ℤ$
42		zeo2	$⊢ K - 1 \in ℤ \to (\frac{K - 1}{2} \in ℤ \leftrightarrow \neg \frac{K - 1 + 1}{2} \in ℤ)$
43	41 42	syl	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to (\frac{K - 1}{2} \in ℤ \leftrightarrow \neg \frac{K - 1 + 1}{2} \in ℤ)$
44	38 43	mpbird	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to \frac{K - 1}{2} \in ℤ$
45		flbi	$⊢ (\frac{K}{2} \in ℝ \land \frac{K - 1}{2} \in ℤ) \to (⌊\frac{K}{2}⌋ = \frac{K - 1}{2} \leftrightarrow (\frac{K - 1}{2} \leq \frac{K}{2} \land \frac{K}{2} < (\frac{K - 1}{2}) + 1))$
46	28 44 45	syl2anc	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to (⌊\frac{K}{2}⌋ = \frac{K - 1}{2} \leftrightarrow (\frac{K - 1}{2} \leq \frac{K}{2} \land \frac{K}{2} < (\frac{K - 1}{2}) + 1))$
47	26 46	mpbird	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to ⌊\frac{K}{2}⌋ = \frac{K - 1}{2}$
48	47	oveq2d	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to 2 ⌊\frac{K}{2}⌋ = 2 (\frac{K - 1}{2})$
49	48	oveq1d	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to 2 ⌊\frac{K}{2}⌋ + 1 = 2 (\frac{K - 1}{2}) + 1$
50	11 12	subcld	$⊢ K \in ℤ \to K - 1 \in ℂ$
51	50 13 14	divcan2d	$⊢ K \in ℤ \to 2 (\frac{K - 1}{2}) = K - 1$
52	51	oveq1d	$⊢ K \in ℤ \to 2 (\frac{K - 1}{2}) + 1 = K - 1 + 1$
53	52	adantr	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to 2 (\frac{K - 1}{2}) + 1 = K - 1 + 1$
54	29	adantr	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to K - 1 + 1 = K$
55	49 53 54	3eqtrrd	$⊢ (K \in ℤ \land K \mod 2 \neq 0) \to K = 2 ⌊\frac{K}{2}⌋ + 1$

Metamath Proof Explorer

Theorem oddfl

Proof