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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 = ( ( 2 · 𝑀 ) + 1 ) ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) = if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ( 𝑁 = ( ( 2 · 𝑀 ) + 1 ) → ( 𝑁 / 4 ) = ( ( ( 2 · 𝑀 ) + 1 ) / 4 ) )
2 2cnd ( 𝑀 ∈ ℤ → 2 ∈ ℂ )
3 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
4 2 3 mulcld ( 𝑀 ∈ ℤ → ( 2 · 𝑀 ) ∈ ℂ )
5 1cnd ( 𝑀 ∈ ℤ → 1 ∈ ℂ )
6 4cn 4 ∈ ℂ
7 4ne0 4 ≠ 0
8 6 7 pm3.2i ( 4 ∈ ℂ ∧ 4 ≠ 0 )
9 8 a1i ( 𝑀 ∈ ℤ → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
10 divdir ( ( ( 2 · 𝑀 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( ( 2 · 𝑀 ) + 1 ) / 4 ) = ( ( ( 2 · 𝑀 ) / 4 ) + ( 1 / 4 ) ) )
11 4 5 9 10 syl3anc ( 𝑀 ∈ ℤ → ( ( ( 2 · 𝑀 ) + 1 ) / 4 ) = ( ( ( 2 · 𝑀 ) / 4 ) + ( 1 / 4 ) ) )
12 2t2e4 ( 2 · 2 ) = 4
13 12 eqcomi 4 = ( 2 · 2 )
14 13 a1i ( 𝑀 ∈ ℤ → 4 = ( 2 · 2 ) )
15 14 oveq2d ( 𝑀 ∈ ℤ → ( ( 2 · 𝑀 ) / 4 ) = ( ( 2 · 𝑀 ) / ( 2 · 2 ) ) )
16 2ne0 2 ≠ 0
17 16 a1i ( 𝑀 ∈ ℤ → 2 ≠ 0 )
18 3 2 2 17 17 divcan5d ( 𝑀 ∈ ℤ → ( ( 2 · 𝑀 ) / ( 2 · 2 ) ) = ( 𝑀 / 2 ) )
19 15 18 eqtrd ( 𝑀 ∈ ℤ → ( ( 2 · 𝑀 ) / 4 ) = ( 𝑀 / 2 ) )
20 19 oveq1d ( 𝑀 ∈ ℤ → ( ( ( 2 · 𝑀 ) / 4 ) + ( 1 / 4 ) ) = ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) )
21 11 20 eqtrd ( 𝑀 ∈ ℤ → ( ( ( 2 · 𝑀 ) + 1 ) / 4 ) = ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) )
22 1 21 sylan9eqr ( ( 𝑀 ∈ ℤ ∧ 𝑁 = ( ( 2 · 𝑀 ) + 1 ) ) → ( 𝑁 / 4 ) = ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) )
23 22 fveq2d ( ( 𝑀 ∈ ℤ ∧ 𝑁 = ( ( 2 · 𝑀 ) + 1 ) ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) = ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) )
24 iftrue ( 2 ∥ 𝑀 → if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) = ( 𝑀 / 2 ) )
25 24 adantr ( ( 2 ∥ 𝑀𝑀 ∈ ℤ ) → if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) = ( 𝑀 / 2 ) )
26 1re 1 ∈ ℝ
27 0le1 0 ≤ 1
28 4re 4 ∈ ℝ
29 4pos 0 < 4
30 divge0 ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → 0 ≤ ( 1 / 4 ) )
31 26 27 28 29 30 mp4an 0 ≤ ( 1 / 4 )
32 1lt4 1 < 4
33 recgt1 ( ( 4 ∈ ℝ ∧ 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 ( 𝑀 ∈ ℤ → ( 2 ∥ 𝑀 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
38 37 biimpac ( ( 2 ∥ 𝑀𝑀 ∈ ℤ ) → ( 𝑀 / 2 ) ∈ ℤ )
39 4nn 4 ∈ ℕ
40 nnrecre ( 4 ∈ ℕ → ( 1 / 4 ) ∈ ℝ )
41 39 40 ax-mp ( 1 / 4 ) ∈ ℝ
42 flbi2 ( ( ( 𝑀 / 2 ) ∈ ℤ ∧ ( 1 / 4 ) ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) = ( 𝑀 / 2 ) ↔ ( 0 ≤ ( 1 / 4 ) ∧ ( 1 / 4 ) < 1 ) ) )
43 38 41 42 sylancl ( ( 2 ∥ 𝑀𝑀 ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) = ( 𝑀 / 2 ) ↔ ( 0 ≤ ( 1 / 4 ) ∧ ( 1 / 4 ) < 1 ) ) )
44 36 43 mpbiri ( ( 2 ∥ 𝑀𝑀 ∈ ℤ ) → ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) = ( 𝑀 / 2 ) )
45 25 44 eqtr4d ( ( 2 ∥ 𝑀𝑀 ∈ ℤ ) → if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) = ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) )
46 iffalse ( ¬ 2 ∥ 𝑀 → if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) = ( ( 𝑀 − 1 ) / 2 ) )
47 46 adantr ( ( ¬ 2 ∥ 𝑀𝑀 ∈ ℤ ) → if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) = ( ( 𝑀 − 1 ) / 2 ) )
48 odd2np1 ( 𝑀 ∈ ℤ → ( ¬ 2 ∥ 𝑀 ↔ ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) )
49 ax-1cn 1 ∈ ℂ
50 2cnne0 ( 2 ∈ ℂ ∧ 2 ≠ 0 )
51 divcan5 ( ( 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( 1 / 2 ) )
52 49 50 50 51 mp3an ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( 1 / 2 )
53 2t1e2 ( 2 · 1 ) = 2
54 53 12 oveq12i ( ( 2 · 1 ) / ( 2 · 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 ∈ ℂ
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 ( 𝑥 ∈ ℤ → ( ( 1 / 2 ) + ( 1 / 4 ) ) = ( 3 / 4 ) )
63 62 oveq2d ( 𝑥 ∈ ℤ → ( 𝑥 + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) = ( 𝑥 + ( 3 / 4 ) ) )
64 63 fveq2d ( 𝑥 ∈ ℤ → ( ⌊ ‘ ( 𝑥 + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) ) = ( ⌊ ‘ ( 𝑥 + ( 3 / 4 ) ) ) )
65 3re 3 ∈ ℝ
66 0re 0 ∈ ℝ
67 3pos 0 < 3
68 66 65 67 ltleii 0 ≤ 3
69 divge0 ( ( ( 3 ∈ ℝ ∧ 0 ≤ 3 ) ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → 0 ≤ ( 3 / 4 ) )
70 65 68 28 29 69 mp4an 0 ≤ ( 3 / 4 )
71 3lt4 3 < 4
72 nnrp ( 4 ∈ ℕ → 4 ∈ ℝ+ )
73 39 72 ax-mp 4 ∈ ℝ+
74 divlt1lt ( ( 3 ∈ ℝ ∧ 4 ∈ ℝ+ ) → ( ( 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 ) ∈ ℝ
79 flbi2 ( ( 𝑥 ∈ ℤ ∧ ( 3 / 4 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 𝑥 + ( 3 / 4 ) ) ) = 𝑥 ↔ ( 0 ≤ ( 3 / 4 ) ∧ ( 3 / 4 ) < 1 ) ) )
80 78 79 mpan2 ( 𝑥 ∈ ℤ → ( ( ⌊ ‘ ( 𝑥 + ( 3 / 4 ) ) ) = 𝑥 ↔ ( 0 ≤ ( 3 / 4 ) ∧ ( 3 / 4 ) < 1 ) ) )
81 77 80 mpbiri ( 𝑥 ∈ ℤ → ( ⌊ ‘ ( 𝑥 + ( 3 / 4 ) ) ) = 𝑥 )
82 64 81 eqtrd ( 𝑥 ∈ ℤ → ( ⌊ ‘ ( 𝑥 + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) ) = 𝑥 )
83 82 adantr ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( ⌊ ‘ ( 𝑥 + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) ) = 𝑥 )
84 oveq1 ( 𝑀 = ( ( 2 · 𝑥 ) + 1 ) → ( 𝑀 / 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) / 2 ) )
85 84 eqcoms ( ( ( 2 · 𝑥 ) + 1 ) = 𝑀 → ( 𝑀 / 2 ) = ( ( ( 2 · 𝑥 ) + 1 ) / 2 ) )
86 2z 2 ∈ ℤ
87 86 a1i ( 𝑥 ∈ ℤ → 2 ∈ ℤ )
88 id ( 𝑥 ∈ ℤ → 𝑥 ∈ ℤ )
89 87 88 zmulcld ( 𝑥 ∈ ℤ → ( 2 · 𝑥 ) ∈ ℤ )
90 89 zcnd ( 𝑥 ∈ ℤ → ( 2 · 𝑥 ) ∈ ℂ )
91 1cnd ( 𝑥 ∈ ℤ → 1 ∈ ℂ )
92 50 a1i ( 𝑥 ∈ ℤ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
93 divdir ( ( ( 2 · 𝑥 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 2 · 𝑥 ) + 1 ) / 2 ) = ( ( ( 2 · 𝑥 ) / 2 ) + ( 1 / 2 ) ) )
94 90 91 92 93 syl3anc ( 𝑥 ∈ ℤ → ( ( ( 2 · 𝑥 ) + 1 ) / 2 ) = ( ( ( 2 · 𝑥 ) / 2 ) + ( 1 / 2 ) ) )
95 zcn ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
96 2cnd ( 𝑥 ∈ ℤ → 2 ∈ ℂ )
97 16 a1i ( 𝑥 ∈ ℤ → 2 ≠ 0 )
98 95 96 97 divcan3d ( 𝑥 ∈ ℤ → ( ( 2 · 𝑥 ) / 2 ) = 𝑥 )
99 98 oveq1d ( 𝑥 ∈ ℤ → ( ( ( 2 · 𝑥 ) / 2 ) + ( 1 / 2 ) ) = ( 𝑥 + ( 1 / 2 ) ) )
100 94 99 eqtrd ( 𝑥 ∈ ℤ → ( ( ( 2 · 𝑥 ) + 1 ) / 2 ) = ( 𝑥 + ( 1 / 2 ) ) )
101 85 100 sylan9eqr ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( 𝑀 / 2 ) = ( 𝑥 + ( 1 / 2 ) ) )
102 101 oveq1d ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) = ( ( 𝑥 + ( 1 / 2 ) ) + ( 1 / 4 ) ) )
103 halfcn ( 1 / 2 ) ∈ ℂ
104 103 a1i ( 𝑥 ∈ ℤ → ( 1 / 2 ) ∈ ℂ )
105 6 7 reccli ( 1 / 4 ) ∈ ℂ
106 105 a1i ( 𝑥 ∈ ℤ → ( 1 / 4 ) ∈ ℂ )
107 95 104 106 addassd ( 𝑥 ∈ ℤ → ( ( 𝑥 + ( 1 / 2 ) ) + ( 1 / 4 ) ) = ( 𝑥 + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) )
108 107 adantr ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( ( 𝑥 + ( 1 / 2 ) ) + ( 1 / 4 ) ) = ( 𝑥 + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) )
109 102 108 eqtrd ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) = ( 𝑥 + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) )
110 109 fveq2d ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) = ( ⌊ ‘ ( 𝑥 + ( ( 1 / 2 ) + ( 1 / 4 ) ) ) ) )
111 oveq1 ( 𝑀 = ( ( 2 · 𝑥 ) + 1 ) → ( 𝑀 − 1 ) = ( ( ( 2 · 𝑥 ) + 1 ) − 1 ) )
112 111 eqcoms ( ( ( 2 · 𝑥 ) + 1 ) = 𝑀 → ( 𝑀 − 1 ) = ( ( ( 2 · 𝑥 ) + 1 ) − 1 ) )
113 pncan1 ( ( 2 · 𝑥 ) ∈ ℂ → ( ( ( 2 · 𝑥 ) + 1 ) − 1 ) = ( 2 · 𝑥 ) )
114 90 113 syl ( 𝑥 ∈ ℤ → ( ( ( 2 · 𝑥 ) + 1 ) − 1 ) = ( 2 · 𝑥 ) )
115 112 114 sylan9eqr ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( 𝑀 − 1 ) = ( 2 · 𝑥 ) )
116 115 oveq1d ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( ( 𝑀 − 1 ) / 2 ) = ( ( 2 · 𝑥 ) / 2 ) )
117 98 adantr ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( ( 2 · 𝑥 ) / 2 ) = 𝑥 )
118 116 117 eqtrd ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( ( 𝑀 − 1 ) / 2 ) = 𝑥 )
119 83 110 118 3eqtr4rd ( ( 𝑥 ∈ ℤ ∧ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 ) → ( ( 𝑀 − 1 ) / 2 ) = ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) )
120 119 ex ( 𝑥 ∈ ℤ → ( ( ( 2 · 𝑥 ) + 1 ) = 𝑀 → ( ( 𝑀 − 1 ) / 2 ) = ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) ) )
121 120 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( ( 2 · 𝑥 ) + 1 ) = 𝑀 → ( ( 𝑀 − 1 ) / 2 ) = ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) ) )
122 121 rexlimdva ( 𝑀 ∈ ℤ → ( ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = 𝑀 → ( ( 𝑀 − 1 ) / 2 ) = ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) ) )
123 48 122 sylbid ( 𝑀 ∈ ℤ → ( ¬ 2 ∥ 𝑀 → ( ( 𝑀 − 1 ) / 2 ) = ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) ) )
124 123 impcom ( ( ¬ 2 ∥ 𝑀𝑀 ∈ ℤ ) → ( ( 𝑀 − 1 ) / 2 ) = ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) )
125 47 124 eqtrd ( ( ¬ 2 ∥ 𝑀𝑀 ∈ ℤ ) → if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) = ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) )
126 45 125 pm2.61ian ( 𝑀 ∈ ℤ → if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) = ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) )
127 126 eqcomd ( 𝑀 ∈ ℤ → ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) = if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) )
128 127 adantr ( ( 𝑀 ∈ ℤ ∧ 𝑁 = ( ( 2 · 𝑀 ) + 1 ) ) → ( ⌊ ‘ ( ( 𝑀 / 2 ) + ( 1 / 4 ) ) ) = if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) )
129 23 128 eqtrd ( ( 𝑀 ∈ ℤ ∧ 𝑁 = ( ( 2 · 𝑀 ) + 1 ) ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) = if ( 2 ∥ 𝑀 , ( 𝑀 / 2 ) , ( ( 𝑀 − 1 ) / 2 ) ) )