flodddiv4

Description: The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021)

		Ref	Expression
	Assertion	flodddiv4	$⊢ (M \in ℤ \land N = 2 \cdot M + 1) \to ⌊\frac{N}{4}⌋ = if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2})$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ N = 2 \cdot M + 1 \to \frac{N}{4} = \frac{2 \cdot M + 1}{4}$
2		2cnd	$⊢ M \in ℤ \to 2 \in ℂ$
3		zcn	$⊢ M \in ℤ \to M \in ℂ$
4	2 3	mulcld	$⊢ M \in ℤ \to 2 \cdot M \in ℂ$
5		1cnd	$⊢ M \in ℤ \to 1 \in ℂ$
6		4cn	$⊢ 4 \in ℂ$
7		4ne0	$⊢ 4 \neq 0$
8	6 7	pm3.2i	$⊢ (4 \in ℂ \land 4 \neq 0)$
9	8	a1i	$⊢ M \in ℤ \to (4 \in ℂ \land 4 \neq 0)$
10		divdir	$⊢ (2 \cdot M \in ℂ \land 1 \in ℂ \land (4 \in ℂ \land 4 \neq 0)) \to \frac{2 \cdot M + 1}{4} = (\frac{2 \cdot M}{4}) + (\frac{1}{4})$
11	4 5 9 10	syl3anc	$⊢ M \in ℤ \to \frac{2 \cdot M + 1}{4} = (\frac{2 \cdot M}{4}) + (\frac{1}{4})$
12		2t2e4	$⊢ 2 \cdot 2 = 4$
13	12	eqcomi	$⊢ 4 = 2 \cdot 2$
14	13	a1i	$⊢ M \in ℤ \to 4 = 2 \cdot 2$
15	14	oveq2d	$⊢ M \in ℤ \to \frac{2 \cdot M}{4} = \frac{2 \cdot M}{2 \cdot 2}$
16		2ne0	$⊢ 2 \neq 0$
17	16	a1i	$⊢ M \in ℤ \to 2 \neq 0$
18	3 2 2 17 17	divcan5d	$⊢ M \in ℤ \to \frac{2 \cdot M}{2 \cdot 2} = \frac{M}{2}$
19	15 18	eqtrd	$⊢ M \in ℤ \to \frac{2 \cdot M}{4} = \frac{M}{2}$
20	19	oveq1d	$⊢ M \in ℤ \to (\frac{2 \cdot M}{4}) + (\frac{1}{4}) = (\frac{M}{2}) + (\frac{1}{4})$
21	11 20	eqtrd	$⊢ M \in ℤ \to \frac{2 \cdot M + 1}{4} = (\frac{M}{2}) + (\frac{1}{4})$
22	1 21	sylan9eqr	$⊢ (M \in ℤ \land N = 2 \cdot M + 1) \to \frac{N}{4} = (\frac{M}{2}) + (\frac{1}{4})$
23	22	fveq2d	$⊢ (M \in ℤ \land N = 2 \cdot M + 1) \to ⌊\frac{N}{4}⌋ = ⌊(\frac{M}{2}) + (\frac{1}{4})⌋$
24		iftrue	$⊢ 2 ∥ M \to if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2}) = \frac{M}{2}$
25	24	adantr	$⊢ (2 ∥ M \land M \in ℤ) \to if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2}) = \frac{M}{2}$
26		1re	$⊢ 1 \in ℝ$
27		0le1	$⊢ 0 \leq 1$
28		4re	$⊢ 4 \in ℝ$
29		4pos	$⊢ 0 < 4$
30		divge0	$⊢ ((1 \in ℝ \land 0 \leq 1) \land (4 \in ℝ \land 0 < 4)) \to 0 \leq \frac{1}{4}$
31	26 27 28 29 30	mp4an	$⊢ 0 \leq \frac{1}{4}$
32		1lt4	$⊢ 1 < 4$
33		recgt1	$⊢ (4 \in ℝ \land 0 < 4) \to (1 < 4 \leftrightarrow \frac{1}{4} < 1)$
34	28 29 33	mp2an	$⊢ 1 < 4 \leftrightarrow \frac{1}{4} < 1$
35	32 34	mpbi	$⊢ \frac{1}{4} < 1$
36	31 35	pm3.2i	$⊢ (0 \leq \frac{1}{4} \land \frac{1}{4} < 1)$
37		evend2	$⊢ M \in ℤ \to (2 ∥ M \leftrightarrow \frac{M}{2} \in ℤ)$
38	37	biimpac	$⊢ (2 ∥ M \land M \in ℤ) \to \frac{M}{2} \in ℤ$
39		4nn	$⊢ 4 \in ℕ$
40		nnrecre	$⊢ 4 \in ℕ \to \frac{1}{4} \in ℝ$
41	39 40	ax-mp	$⊢ \frac{1}{4} \in ℝ$
42		flbi2	$⊢ (\frac{M}{2} \in ℤ \land \frac{1}{4} \in ℝ) \to (⌊(\frac{M}{2}) + (\frac{1}{4})⌋ = \frac{M}{2} \leftrightarrow (0 \leq \frac{1}{4} \land \frac{1}{4} < 1))$
43	38 41 42	sylancl	$⊢ (2 ∥ M \land M \in ℤ) \to (⌊(\frac{M}{2}) + (\frac{1}{4})⌋ = \frac{M}{2} \leftrightarrow (0 \leq \frac{1}{4} \land \frac{1}{4} < 1))$
44	36 43	mpbiri	$⊢ (2 ∥ M \land M \in ℤ) \to ⌊(\frac{M}{2}) + (\frac{1}{4})⌋ = \frac{M}{2}$
45	25 44	eqtr4d	$⊢ (2 ∥ M \land M \in ℤ) \to if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2}) = ⌊(\frac{M}{2}) + (\frac{1}{4})⌋$
46		iffalse	$⊢ \neg 2 ∥ M \to if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2}) = \frac{M - 1}{2}$
47	46	adantr	$⊢ (\neg 2 ∥ M \land M \in ℤ) \to if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2}) = \frac{M - 1}{2}$
48		odd2np1	$⊢ M \in ℤ \to (\neg 2 ∥ M \leftrightarrow \exists x \in ℤ 2 x + 1 = M)$
49		ax-1cn	$⊢ 1 \in ℂ$
50		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
51		divcan5	$⊢ (1 \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 \cdot 1}{2 \cdot 2} = \frac{1}{2}$
52	49 50 50 51	mp3an	$⊢ \frac{2 \cdot 1}{2 \cdot 2} = \frac{1}{2}$
53		2t1e2	$⊢ 2 \cdot 1 = 2$
54	53 12	oveq12i	$⊢ \frac{2 \cdot 1}{2 \cdot 2} = \frac{2}{4}$
55	52 54	eqtr3i	$⊢ \frac{1}{2} = \frac{2}{4}$
56	55	oveq1i	$⊢ (\frac{1}{2}) + (\frac{1}{4}) = (\frac{2}{4}) + (\frac{1}{4})$
57		2cn	$⊢ 2 \in ℂ$
58	57 49 6 7	divdiri	$⊢ \frac{2 + 1}{4} = (\frac{2}{4}) + (\frac{1}{4})$
59		2p1e3	$⊢ 2 + 1 = 3$
60	59	oveq1i	$⊢ \frac{2 + 1}{4} = \frac{3}{4}$
61	56 58 60	3eqtr2i	$⊢ (\frac{1}{2}) + (\frac{1}{4}) = \frac{3}{4}$
62	61	a1i	$⊢ x \in ℤ \to (\frac{1}{2}) + (\frac{1}{4}) = \frac{3}{4}$
63	62	oveq2d	$⊢ x \in ℤ \to x + (\frac{1}{2}) + (\frac{1}{4}) = x + (\frac{3}{4})$
64	63	fveq2d	$⊢ x \in ℤ \to ⌊x + (\frac{1}{2}) + (\frac{1}{4})⌋ = ⌊x + (\frac{3}{4})⌋$
65		3re	$⊢ 3 \in ℝ$
66		0re	$⊢ 0 \in ℝ$
67		3pos	$⊢ 0 < 3$
68	66 65 67	ltleii	$⊢ 0 \leq 3$
69		divge0	$⊢ ((3 \in ℝ \land 0 \leq 3) \land (4 \in ℝ \land 0 < 4)) \to 0 \leq \frac{3}{4}$
70	65 68 28 29 69	mp4an	$⊢ 0 \leq \frac{3}{4}$
71		3lt4	$⊢ 3 < 4$
72		nnrp	$⊢ 4 \in ℕ \to 4 \in ℝ^{+}$
73	39 72	ax-mp	$⊢ 4 \in ℝ^{+}$
74		divlt1lt	$⊢ (3 \in ℝ \land 4 \in ℝ^{+}) \to (\frac{3}{4} < 1 \leftrightarrow 3 < 4)$
75	65 73 74	mp2an	$⊢ \frac{3}{4} < 1 \leftrightarrow 3 < 4$
76	71 75	mpbir	$⊢ \frac{3}{4} < 1$
77	70 76	pm3.2i	$⊢ (0 \leq \frac{3}{4} \land \frac{3}{4} < 1)$
78	65 28 7	redivcli	$⊢ \frac{3}{4} \in ℝ$
79		flbi2	$⊢ (x \in ℤ \land \frac{3}{4} \in ℝ) \to (⌊x + (\frac{3}{4})⌋ = x \leftrightarrow (0 \leq \frac{3}{4} \land \frac{3}{4} < 1))$
80	78 79	mpan2	$⊢ x \in ℤ \to (⌊x + (\frac{3}{4})⌋ = x \leftrightarrow (0 \leq \frac{3}{4} \land \frac{3}{4} < 1))$
81	77 80	mpbiri	$⊢ x \in ℤ \to ⌊x + (\frac{3}{4})⌋ = x$
82	64 81	eqtrd	$⊢ x \in ℤ \to ⌊x + (\frac{1}{2}) + (\frac{1}{4})⌋ = x$
83	82	adantr	$⊢ (x \in ℤ \land 2 x + 1 = M) \to ⌊x + (\frac{1}{2}) + (\frac{1}{4})⌋ = x$
84		oveq1	$⊢ M = 2 x + 1 \to \frac{M}{2} = \frac{2 x + 1}{2}$
85	84	eqcoms	$⊢ 2 x + 1 = M \to \frac{M}{2} = \frac{2 x + 1}{2}$
86		2z	$⊢ 2 \in ℤ$
87	86	a1i	$⊢ x \in ℤ \to 2 \in ℤ$
88		id	$⊢ x \in ℤ \to x \in ℤ$
89	87 88	zmulcld	$⊢ x \in ℤ \to 2 x \in ℤ$
90	89	zcnd	$⊢ x \in ℤ \to 2 x \in ℂ$
91		1cnd	$⊢ x \in ℤ \to 1 \in ℂ$
92	50	a1i	$⊢ x \in ℤ \to (2 \in ℂ \land 2 \neq 0)$
93		divdir	$⊢ (2 x \in ℂ \land 1 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 x + 1}{2} = (\frac{2 x}{2}) + (\frac{1}{2})$
94	90 91 92 93	syl3anc	$⊢ x \in ℤ \to \frac{2 x + 1}{2} = (\frac{2 x}{2}) + (\frac{1}{2})$
95		zcn	$⊢ x \in ℤ \to x \in ℂ$
96		2cnd	$⊢ x \in ℤ \to 2 \in ℂ$
97	16	a1i	$⊢ x \in ℤ \to 2 \neq 0$
98	95 96 97	divcan3d	$⊢ x \in ℤ \to \frac{2 x}{2} = x$
99	98	oveq1d	$⊢ x \in ℤ \to (\frac{2 x}{2}) + (\frac{1}{2}) = x + (\frac{1}{2})$
100	94 99	eqtrd	$⊢ x \in ℤ \to \frac{2 x + 1}{2} = x + (\frac{1}{2})$
101	85 100	sylan9eqr	$⊢ (x \in ℤ \land 2 x + 1 = M) \to \frac{M}{2} = x + (\frac{1}{2})$
102	101	oveq1d	$⊢ (x \in ℤ \land 2 x + 1 = M) \to (\frac{M}{2}) + (\frac{1}{4}) = x + (\frac{1}{2}) + (\frac{1}{4})$
103		halfcn	$⊢ \frac{1}{2} \in ℂ$
104	103	a1i	$⊢ x \in ℤ \to \frac{1}{2} \in ℂ$
105	6 7	reccli	$⊢ \frac{1}{4} \in ℂ$
106	105	a1i	$⊢ x \in ℤ \to \frac{1}{4} \in ℂ$
107	95 104 106	addassd	$⊢ x \in ℤ \to x + (\frac{1}{2}) + (\frac{1}{4}) = x + (\frac{1}{2}) + (\frac{1}{4})$
108	107	adantr	$⊢ (x \in ℤ \land 2 x + 1 = M) \to x + (\frac{1}{2}) + (\frac{1}{4}) = x + (\frac{1}{2}) + (\frac{1}{4})$
109	102 108	eqtrd	$⊢ (x \in ℤ \land 2 x + 1 = M) \to (\frac{M}{2}) + (\frac{1}{4}) = x + (\frac{1}{2}) + (\frac{1}{4})$
110	109	fveq2d	$⊢ (x \in ℤ \land 2 x + 1 = M) \to ⌊(\frac{M}{2}) + (\frac{1}{4})⌋ = ⌊x + (\frac{1}{2}) + (\frac{1}{4})⌋$
111		oveq1	$⊢ M = 2 x + 1 \to M - 1 = 2 x + 1 - 1$
112	111	eqcoms	$⊢ 2 x + 1 = M \to M - 1 = 2 x + 1 - 1$
113		pncan1	$⊢ 2 x \in ℂ \to 2 x + 1 - 1 = 2 x$
114	90 113	syl	$⊢ x \in ℤ \to 2 x + 1 - 1 = 2 x$
115	112 114	sylan9eqr	$⊢ (x \in ℤ \land 2 x + 1 = M) \to M - 1 = 2 x$
116	115	oveq1d	$⊢ (x \in ℤ \land 2 x + 1 = M) \to \frac{M - 1}{2} = \frac{2 x}{2}$
117	98	adantr	$⊢ (x \in ℤ \land 2 x + 1 = M) \to \frac{2 x}{2} = x$
118	116 117	eqtrd	$⊢ (x \in ℤ \land 2 x + 1 = M) \to \frac{M - 1}{2} = x$
119	83 110 118	3eqtr4rd	$⊢ (x \in ℤ \land 2 x + 1 = M) \to \frac{M - 1}{2} = ⌊(\frac{M}{2}) + (\frac{1}{4})⌋$
120	119	ex	$⊢ x \in ℤ \to (2 x + 1 = M \to \frac{M - 1}{2} = ⌊(\frac{M}{2}) + (\frac{1}{4})⌋)$
121	120	adantl	$⊢ (M \in ℤ \land x \in ℤ) \to (2 x + 1 = M \to \frac{M - 1}{2} = ⌊(\frac{M}{2}) + (\frac{1}{4})⌋)$
122	121	rexlimdva	$⊢ M \in ℤ \to (\exists x \in ℤ 2 x + 1 = M \to \frac{M - 1}{2} = ⌊(\frac{M}{2}) + (\frac{1}{4})⌋)$
123	48 122	sylbid	$⊢ M \in ℤ \to (\neg 2 ∥ M \to \frac{M - 1}{2} = ⌊(\frac{M}{2}) + (\frac{1}{4})⌋)$
124	123	impcom	$⊢ (\neg 2 ∥ M \land M \in ℤ) \to \frac{M - 1}{2} = ⌊(\frac{M}{2}) + (\frac{1}{4})⌋$
125	47 124	eqtrd	$⊢ (\neg 2 ∥ M \land M \in ℤ) \to if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2}) = ⌊(\frac{M}{2}) + (\frac{1}{4})⌋$
126	45 125	pm2.61ian	$⊢ M \in ℤ \to if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2}) = ⌊(\frac{M}{2}) + (\frac{1}{4})⌋$
127	126	eqcomd	$⊢ M \in ℤ \to ⌊(\frac{M}{2}) + (\frac{1}{4})⌋ = if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2})$
128	127	adantr	$⊢ (M \in ℤ \land N = 2 \cdot M + 1) \to ⌊(\frac{M}{2}) + (\frac{1}{4})⌋ = if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2})$
129	23 128	eqtrd	$⊢ (M \in ℤ \land N = 2 \cdot M + 1) \to ⌊\frac{N}{4}⌋ = if (2 ∥ M, \frac{M}{2}, \frac{M - 1}{2})$

Metamath Proof Explorer

Theorem flodddiv4

Proof