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 ) ) )