Theorem flodddiv4 11817

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

Assertion

Ref	Expression
flodddiv4	|- ( ( M e. ZZ /\ N = ( ( 2 x. M ) + 1 ) ) -> ( |_ ` ( N / 4 ) ) = if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) )

Proof of Theorem flodddiv4

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 5828	. . . 4 |- ( N = ( ( 2 x. M ) + 1 ) -> ( N / 4 ) = ( ( ( 2 x. M ) + 1 ) / 4 ) )
2		2cnd 8900	. . . . . . 7 |- ( M e. ZZ -> 2 e. CC )
3		zcn 9166	. . . . . . 7 |- ( M e. ZZ -> M e. CC )
4	2, 3	mulcld 7892	. . . . . 6 |- ( M e. ZZ -> ( 2 x. M ) e. CC )
5		1cnd 7888	. . . . . 6 |- ( M e. ZZ -> 1 e. CC )
6		4cn 8905	. . . . . . 7 |- 4 e. CC
7	6	a1i 9	. . . . . 6 |- ( M e. ZZ -> 4 e. CC )
8		4ap0 8926	. . . . . . 7 |- 4 # 0
9	8	a1i 9	. . . . . 6 |- ( M e. ZZ -> 4 # 0 )
10	4, 5, 7, 9	divdirapd 8696	. . . . 5 |- ( M e. ZZ -> ( ( ( 2 x. M ) + 1 ) / 4 ) = ( ( ( 2 x. M ) / 4 ) + ( 1 / 4 ) ) )
11		2t2e4 8981	. . . . . . . . . 10 |- ( 2 x. 2 ) = 4
12	11	eqcomi 2161	. . . . . . . . 9 |- 4 = ( 2 x. 2 )
13	12	a1i 9	. . . . . . . 8 |- ( M e. ZZ -> 4 = ( 2 x. 2 ) )
14	13	oveq2d 5837	. . . . . . 7 |- ( M e. ZZ -> ( ( 2 x. M ) / 4 ) = ( ( 2 x. M ) / ( 2 x. 2 ) ) )
15		2ap0 8920	. . . . . . . . 9 |- 2 # 0
16	15	a1i 9	. . . . . . . 8 |- ( M e. ZZ -> 2 # 0 )
17	3, 2, 2, 16, 16	divcanap5d 8684	. . . . . . 7 |- ( M e. ZZ -> ( ( 2 x. M ) / ( 2 x. 2 ) ) = ( M / 2 ) )
18	14, 17	eqtrd 2190	. . . . . 6 |- ( M e. ZZ -> ( ( 2 x. M ) / 4 ) = ( M / 2 ) )
19	18	oveq1d 5836	. . . . 5 |- ( M e. ZZ -> ( ( ( 2 x. M ) / 4 ) + ( 1 / 4 ) ) = ( ( M / 2 ) + ( 1 / 4 ) ) )
20	10, 19	eqtrd 2190	. . . 4 |- ( M e. ZZ -> ( ( ( 2 x. M ) + 1 ) / 4 ) = ( ( M / 2 ) + ( 1 / 4 ) ) )
21	1, 20	sylan9eqr 2212	. . 3 |- ( ( M e. ZZ /\ N = ( ( 2 x. M ) + 1 ) ) -> ( N / 4 ) = ( ( M / 2 ) + ( 1 / 4 ) ) )
22	21	fveq2d 5471	. 2 |- ( ( M e. ZZ /\ N = ( ( 2 x. M ) + 1 ) ) -> ( |_ ` ( N / 4 ) ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) )
23		iftrue 3510	. . . . . . . 8 |- ( 2 || M -> if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) = ( M / 2 ) )
24	23	adantr 274	. . . . . . 7 |- ( ( 2 || M /\ M e. ZZ ) -> if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) = ( M / 2 ) )
25		1re 7871	. . . . . . . . . 10 |- 1 e. RR
26		0le1 8350	. . . . . . . . . 10 |- 0 <_ 1
27		4re 8904	. . . . . . . . . 10 |- 4 e. RR
28		4pos 8924	. . . . . . . . . 10 |- 0 < 4
29		divge0 8738	. . . . . . . . . 10 |- ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( 4 e. RR /\ 0 < 4 ) ) -> 0 <_ ( 1 / 4 ) )
30	25, 26, 27, 28, 29	mp4an 424	. . . . . . . . 9 |- 0 <_ ( 1 / 4 )
31		1lt4 9001	. . . . . . . . . 10 |- 1 < 4
32		recgt1 8762	. . . . . . . . . . 11 |- ( ( 4 e. RR /\ 0 < 4 ) -> ( 1 < 4 <-> ( 1 / 4 ) < 1 ) )
33	27, 28, 32	mp2an 423	. . . . . . . . . 10 |- ( 1 < 4 <-> ( 1 / 4 ) < 1 )
34	31, 33	mpbi 144	. . . . . . . . 9 |- ( 1 / 4 ) < 1
35	30, 34	pm3.2i 270	. . . . . . . 8 |- ( 0 <_ ( 1 / 4 ) /\ ( 1 / 4 ) < 1 )
36		evend2 11772	. . . . . . . . . 10 |- ( M e. ZZ -> ( 2 || M <-> ( M / 2 ) e. ZZ ) )
37	36	biimpac 296	. . . . . . . . 9 |- ( ( 2 || M /\ M e. ZZ ) -> ( M / 2 ) e. ZZ )
38		4nn 8990	. . . . . . . . . 10 |- 4 e. NN
39		nnrecq 9547	. . . . . . . . . 10 |- ( 4 e. NN -> ( 1 / 4 ) e. QQ )
40	38, 39	ax-mp 5	. . . . . . . . 9 |- ( 1 / 4 ) e. QQ
41		flqbi2 10183	. . . . . . . . 9 |- ( ( ( M / 2 ) e. ZZ /\ ( 1 / 4 ) e. QQ ) -> ( ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) = ( M / 2 ) <-> ( 0 <_ ( 1 / 4 ) /\ ( 1 / 4 ) < 1 ) ) )
42	37, 40, 41	sylancl 410	. . . . . . . 8 |- ( ( 2 || M /\ M e. ZZ ) -> ( ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) = ( M / 2 ) <-> ( 0 <_ ( 1 / 4 ) /\ ( 1 / 4 ) < 1 ) ) )
43	35, 42	mpbiri 167	. . . . . . 7 |- ( ( 2 || M /\ M e. ZZ ) -> ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) = ( M / 2 ) )
44	24, 43	eqtr4d 2193	. . . . . 6 |- ( ( 2 || M /\ M e. ZZ ) -> if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) )
45	44	expcom 115	. . . . 5 |- ( M e. ZZ -> ( 2 || M -> if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) ) )
46		iffalse 3513	. . . . . . . 8 |- ( -. 2 || M -> if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) = ( ( M - 1 ) / 2 ) )
47	46	adantr 274	. . . . . . 7 |- ( ( -. 2 || M /\ M e. ZZ ) -> if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) = ( ( M - 1 ) / 2 ) )
48		odd2np1 11756	. . . . . . . . 9 |- ( M e. ZZ -> ( -. 2 || M <-> E. x e. ZZ ( ( 2 x. x ) + 1 ) = M ) )
49		ax-1cn 7819	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
50		2cn 8898	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 e. CC
51	50, 15	pm3.2i 270	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 2 e. CC /\ 2 # 0 )
52		divcanap5 8581	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 1 e. CC /\ ( 2 e. CC /\ 2 # 0 ) /\ ( 2 e. CC /\ 2 # 0 ) ) -> ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 1 / 2 ) )
53	49, 51, 51, 52	mp3an 1319	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 1 / 2 )
54		2t1e2 8980	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 2 x. 1 ) = 2
55	54, 11	oveq12i 5833	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 2 / 4 )
56	53, 55	eqtr3i 2180	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 / 2 ) = ( 2 / 4 )
57	56	oveq1i 5831	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1 / 2 ) + ( 1 / 4 ) ) = ( ( 2 / 4 ) + ( 1 / 4 ) )
58	50, 49, 6, 8	divdirapi 8636	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 + 1 ) / 4 ) = ( ( 2 / 4 ) + ( 1 / 4 ) )
59		2p1e3 8960	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 + 1 ) = 3
60	59	oveq1i 5831	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 + 1 ) / 4 ) = ( 3 / 4 )
61	57, 58, 60	3eqtr2i 2184	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 / 2 ) + ( 1 / 4 ) ) = ( 3 / 4 )
62	61	a1i 9	. . . . . . . . . . . . . . . . 17 |- ( x e. ZZ -> ( ( 1 / 2 ) + ( 1 / 4 ) ) = ( 3 / 4 ) )
63	62	oveq2d 5837	. . . . . . . . . . . . . . . 16 |- ( x e. ZZ -> ( x + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) = ( x + ( 3 / 4 ) ) )
64	63	fveq2d 5471	. . . . . . . . . . . . . . 15 |- ( x e. ZZ -> ( |_ ` ( x + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) ) = ( |_ ` ( x + ( 3 / 4 ) ) ) )
65		3re 8901	. . . . . . . . . . . . . . . . . 18 |- 3 e. RR
66		0re 7872	. . . . . . . . . . . . . . . . . . 19 |- 0 e. RR
67		3pos 8921	. . . . . . . . . . . . . . . . . . 19 |- 0 < 3
68	66, 65, 67	ltleii 7973	. . . . . . . . . . . . . . . . . 18 |- 0 <_ 3
69		divge0 8738	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 3 e. RR /\ 0 <_ 3 ) /\ ( 4 e. RR /\ 0 < 4 ) ) -> 0 <_ ( 3 / 4 ) )
70	65, 68, 27, 28, 69	mp4an 424	. . . . . . . . . . . . . . . . 17 |- 0 <_ ( 3 / 4 )
71		3lt4 8999	. . . . . . . . . . . . . . . . . 18 |- 3 < 4
72		nnrp 9563	. . . . . . . . . . . . . . . . . . . 20 |- ( 4 e. NN -> 4 e. RR+ )
73	38, 72	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- 4 e. RR+
74		divlt1lt 9624	. . . . . . . . . . . . . . . . . . 19 |- ( ( 3 e. RR /\ 4 e. RR+ ) -> ( ( 3 / 4 ) < 1 <-> 3 < 4 ) )
75	65, 73, 74	mp2an 423	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 / 4 ) < 1 <-> 3 < 4 )
76	71, 75	mpbir 145	. . . . . . . . . . . . . . . . 17 |- ( 3 / 4 ) < 1
77	70, 76	pm3.2i 270	. . . . . . . . . . . . . . . 16 |- ( 0 <_ ( 3 / 4 ) /\ ( 3 / 4 ) < 1 )
78		3z 9190	. . . . . . . . . . . . . . . . . 18 |- 3 e. ZZ
79		znq 9526	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 e. ZZ /\ 4 e. NN ) -> ( 3 / 4 ) e. QQ )
80	78, 38, 79	mp2an 423	. . . . . . . . . . . . . . . . 17 |- ( 3 / 4 ) e. QQ
81		flqbi2 10183	. . . . . . . . . . . . . . . . 17 |- ( ( x e. ZZ /\ ( 3 / 4 ) e. QQ ) -> ( ( |_ ` ( x + ( 3 / 4 ) ) ) = x <-> ( 0 <_ ( 3 / 4 ) /\ ( 3 / 4 ) < 1 ) ) )
82	80, 81	mpan2 422	. . . . . . . . . . . . . . . 16 |- ( x e. ZZ -> ( ( |_ ` ( x + ( 3 / 4 ) ) ) = x <-> ( 0 <_ ( 3 / 4 ) /\ ( 3 / 4 ) < 1 ) ) )
83	77, 82	mpbiri 167	. . . . . . . . . . . . . . 15 |- ( x e. ZZ -> ( |_ ` ( x + ( 3 / 4 ) ) ) = x )
84	64, 83	eqtrd 2190	. . . . . . . . . . . . . 14 |- ( x e. ZZ -> ( |_ ` ( x + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) ) = x )
85	84	adantr 274	. . . . . . . . . . . . 13 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( |_ ` ( x + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) ) = x )
86		oveq1 5828	. . . . . . . . . . . . . . . . . 18 |- ( M = ( ( 2 x. x ) + 1 ) -> ( M / 2 ) = ( ( ( 2 x. x ) + 1 ) / 2 ) )
87	86	eqcoms 2160	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2 x. x ) + 1 ) = M -> ( M / 2 ) = ( ( ( 2 x. x ) + 1 ) / 2 ) )
88		2z 9189	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 e. ZZ
89	88	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ZZ -> 2 e. ZZ )
90		id 19	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ZZ -> x e. ZZ )
91	89, 90	zmulcld 9286	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ZZ -> ( 2 x. x ) e. ZZ )
92	91	zcnd 9281	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ZZ -> ( 2 x. x ) e. CC )
93		1cnd 7888	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ZZ -> 1 e. CC )
94		2cnd 8900	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ZZ -> 2 e. CC )
95	15	a1i 9	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ZZ -> 2 # 0 )
96	92, 93, 94, 95	divdirapd 8696	. . . . . . . . . . . . . . . . . 18 |- ( x e. ZZ -> ( ( ( 2 x. x ) + 1 ) / 2 ) = ( ( ( 2 x. x ) / 2 ) + ( 1 / 2 ) ) )
97		zcn 9166	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ZZ -> x e. CC )
98	97, 94, 95	divcanap3d 8662	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ZZ -> ( ( 2 x. x ) / 2 ) = x )
99	98	oveq1d 5836	. . . . . . . . . . . . . . . . . 18 |- ( x e. ZZ -> ( ( ( 2 x. x ) / 2 ) + ( 1 / 2 ) ) = ( x + ( 1 / 2 ) ) )
100	96, 99	eqtrd 2190	. . . . . . . . . . . . . . . . 17 |- ( x e. ZZ -> ( ( ( 2 x. x ) + 1 ) / 2 ) = ( x + ( 1 / 2 ) ) )
101	87, 100	sylan9eqr 2212	. . . . . . . . . . . . . . . 16 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( M / 2 ) = ( x + ( 1 / 2 ) ) )
102	101	oveq1d 5836	. . . . . . . . . . . . . . 15 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( ( M / 2 ) + ( 1 / 4 ) ) = ( ( x + ( 1 / 2 ) ) + ( 1 / 4 ) ) )
103		halfcn 9041	. . . . . . . . . . . . . . . . . 18 |- ( 1 / 2 ) e. CC
104	103	a1i 9	. . . . . . . . . . . . . . . . 17 |- ( x e. ZZ -> ( 1 / 2 ) e. CC )
105	6, 8	recclapi 8609	. . . . . . . . . . . . . . . . . 18 |- ( 1 / 4 ) e. CC
106	105	a1i 9	. . . . . . . . . . . . . . . . 17 |- ( x e. ZZ -> ( 1 / 4 ) e. CC )
107	97, 104, 106	addassd 7894	. . . . . . . . . . . . . . . 16 |- ( x e. ZZ -> ( ( x + ( 1 / 2 ) ) + ( 1 / 4 ) ) = ( x + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) )
108	107	adantr 274	. . . . . . . . . . . . . . 15 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( ( x + ( 1 / 2 ) ) + ( 1 / 4 ) ) = ( x + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) )
109	102, 108	eqtrd 2190	. . . . . . . . . . . . . 14 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( ( M / 2 ) + ( 1 / 4 ) ) = ( x + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) )
110	109	fveq2d 5471	. . . . . . . . . . . . 13 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) = ( |_ ` ( x + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) ) )
111		oveq1 5828	. . . . . . . . . . . . . . . . 17 |- ( M = ( ( 2 x. x ) + 1 ) -> ( M - 1 ) = ( ( ( 2 x. x ) + 1 ) - 1 ) )
112	111	eqcoms 2160	. . . . . . . . . . . . . . . 16 |- ( ( ( 2 x. x ) + 1 ) = M -> ( M - 1 ) = ( ( ( 2 x. x ) + 1 ) - 1 ) )
113		pncan1 8246	. . . . . . . . . . . . . . . . 17 |- ( ( 2 x. x ) e. CC -> ( ( ( 2 x. x ) + 1 ) - 1 ) = ( 2 x. x ) )
114	92, 113	syl 14	. . . . . . . . . . . . . . . 16 |- ( x e. ZZ -> ( ( ( 2 x. x ) + 1 ) - 1 ) = ( 2 x. x ) )
115	112, 114	sylan9eqr 2212	. . . . . . . . . . . . . . 15 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( M - 1 ) = ( 2 x. x ) )
116	115	oveq1d 5836	. . . . . . . . . . . . . 14 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( ( M - 1 ) / 2 ) = ( ( 2 x. x ) / 2 ) )
117	98	adantr 274	. . . . . . . . . . . . . 14 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( ( 2 x. x ) / 2 ) = x )
118	116, 117	eqtrd 2190	. . . . . . . . . . . . 13 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( ( M - 1 ) / 2 ) = x )
119	85, 110, 118	3eqtr4rd 2201	. . . . . . . . . . . 12 |- ( ( x e. ZZ /\ ( ( 2 x. x ) + 1 ) = M ) -> ( ( M - 1 ) / 2 ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) )
120	119	ex 114	. . . . . . . . . . 11 |- ( x e. ZZ -> ( ( ( 2 x. x ) + 1 ) = M -> ( ( M - 1 ) / 2 ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) ) )
121	120	adantl 275	. . . . . . . . . 10 |- ( ( M e. ZZ /\ x e. ZZ ) -> ( ( ( 2 x. x ) + 1 ) = M -> ( ( M - 1 ) / 2 ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) ) )
122	121	rexlimdva 2574	. . . . . . . . 9 |- ( M e. ZZ -> ( E. x e. ZZ ( ( 2 x. x ) + 1 ) = M -> ( ( M - 1 ) / 2 ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) ) )
123	48, 122	sylbid 149	. . . . . . . 8 |- ( M e. ZZ -> ( -. 2 || M -> ( ( M - 1 ) / 2 ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) ) )
124	123	impcom 124	. . . . . . 7 |- ( ( -. 2 || M /\ M e. ZZ ) -> ( ( M - 1 ) / 2 ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) )
125	47, 124	eqtrd 2190	. . . . . 6 |- ( ( -. 2 || M /\ M e. ZZ ) -> if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) )
126	125	expcom 115	. . . . 5 |- ( M e. ZZ -> ( -. 2 || M -> if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) ) )
127		zeo3 11751	. . . . 5 |- ( M e. ZZ -> ( 2 || M \/ -. 2 || M ) )
128	45, 126, 127	mpjaod 708	. . . 4 |- ( M e. ZZ -> if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) = ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) )
129	128	eqcomd 2163	. . 3 |- ( M e. ZZ -> ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) = if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) )
130	129	adantr 274	. 2 |- ( ( M e. ZZ /\ N = ( ( 2 x. M ) + 1 ) ) -> ( |_ ` ( ( M / 2 ) + ( 1 / 4 ) ) ) = if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) )
131	22, 130	eqtrd 2190	1 |- ( ( M e. ZZ /\ N = ( ( 2 x. M ) + 1 ) ) -> ( |_ ` ( N / 4 ) ) = if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1335   e. wcel 2128   E.wrex 2436   ifcif 3505   class class class wbr 3965   ` cfv 5169  (class class class)co 5821   CCcc 7724   RRcr 7725   0cc0 7726   1c1 7727   + caddc 7729   x. cmul 7731   < clt 7906   <_ cle 7907   - cmin 8040   # cap 8450   / cdiv 8539   NNcn 8827   2c2 8878   3c3 8879   4c4 8880   ZZcz 9161   QQcq 9521   RR+crp 9553   |_cfl 10160   || cdvds 11676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4495  ax-cnex 7817  ax-resscn 7818  ax-1cn 7819  ax-1re 7820  ax-icn 7821  ax-addcl 7822  ax-addrcl 7823  ax-mulcl 7824  ax-mulrcl 7825  ax-addcom 7826  ax-mulcom 7827  ax-addass 7828  ax-mulass 7829  ax-distr 7830  ax-i2m1 7831  ax-0lt1 7832  ax-1rid 7833  ax-0id 7834  ax-rnegex 7835  ax-precex 7836  ax-cnre 7837  ax-pre-ltirr 7838  ax-pre-ltwlin 7839  ax-pre-lttrn 7840  ax-pre-apti 7841  ax-pre-ltadd 7842  ax-pre-mulgt0 7843  ax-pre-mulext 7844  ax-arch 7845

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-xor 1358  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-id 4253  df-po 4256  df-iso 4257  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-fv 5177  df-riota 5777  df-ov 5824  df-oprab 5825  df-mpo 5826  df-1st 6085  df-2nd 6086  df-pnf 7908  df-mnf 7909  df-xr 7910  df-ltxr 7911  df-le 7912  df-sub 8042  df-neg 8043  df-reap 8444  df-ap 8451  df-div 8540  df-inn 8828  df-2 8886  df-3 8887  df-4 8888  df-n0 9085  df-z 9162  df-q 9522  df-rp 9554  df-fl 10162  df-dvds 11677

This theorem is referenced by: (None)