Metamath Proof Explorer

Theorem flodddiv4

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

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

Proof

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