Step | Hyp | Ref
| Expression |
1 | | oveq1 5857 |
. . . 4
⊢ (𝑁 = ((2 · 𝑀) + 1) → (𝑁 / 4) = (((2 · 𝑀) + 1) / 4)) |
2 | | 2cnd 8938 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 2 ∈
ℂ) |
3 | | zcn 9204 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
4 | 2, 3 | mulcld 7927 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → (2
· 𝑀) ∈
ℂ) |
5 | | 1cnd 7923 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 1 ∈
ℂ) |
6 | | 4cn 8943 |
. . . . . . 7
⊢ 4 ∈
ℂ |
7 | 6 | a1i 9 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 4 ∈
ℂ) |
8 | | 4ap0 8964 |
. . . . . . 7
⊢ 4 #
0 |
9 | 8 | a1i 9 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 4 #
0) |
10 | 4, 5, 7, 9 | divdirapd 8733 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (((2
· 𝑀) + 1) / 4) =
(((2 · 𝑀) / 4) + (1
/ 4))) |
11 | | 2t2e4 9019 |
. . . . . . . . . 10
⊢ (2
· 2) = 4 |
12 | 11 | eqcomi 2174 |
. . . . . . . . 9
⊢ 4 = (2
· 2) |
13 | 12 | a1i 9 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 4 = (2
· 2)) |
14 | 13 | oveq2d 5866 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → ((2
· 𝑀) / 4) = ((2
· 𝑀) / (2 ·
2))) |
15 | | 2ap0 8958 |
. . . . . . . . 9
⊢ 2 #
0 |
16 | 15 | a1i 9 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 2 #
0) |
17 | 3, 2, 2, 16, 16 | divcanap5d 8721 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → ((2
· 𝑀) / (2 ·
2)) = (𝑀 /
2)) |
18 | 14, 17 | eqtrd 2203 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → ((2
· 𝑀) / 4) = (𝑀 / 2)) |
19 | 18 | oveq1d 5865 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (((2
· 𝑀) / 4) + (1 / 4))
= ((𝑀 / 2) + (1 /
4))) |
20 | 10, 19 | eqtrd 2203 |
. . . 4
⊢ (𝑀 ∈ ℤ → (((2
· 𝑀) + 1) / 4) =
((𝑀 / 2) + (1 /
4))) |
21 | 1, 20 | sylan9eqr 2225 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (𝑁 / 4) = ((𝑀 / 2) + (1 / 4))) |
22 | 21 | fveq2d 5498 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) →
(⌊‘(𝑁 / 4)) =
(⌊‘((𝑀 / 2) +
(1 / 4)))) |
23 | | iftrue 3530 |
. . . . . . . 8
⊢ (2
∥ 𝑀 → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (𝑀 / 2)) |
24 | 23 | adantr 274 |
. . . . . . 7
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (𝑀 / 2)) |
25 | | 1re 7906 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
26 | | 0le1 8387 |
. . . . . . . . . 10
⊢ 0 ≤
1 |
27 | | 4re 8942 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
28 | | 4pos 8962 |
. . . . . . . . . 10
⊢ 0 <
4 |
29 | | divge0 8776 |
. . . . . . . . . 10
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ (4 ∈ ℝ ∧ 0 < 4)) →
0 ≤ (1 / 4)) |
30 | 25, 26, 27, 28, 29 | mp4an 425 |
. . . . . . . . 9
⊢ 0 ≤ (1
/ 4) |
31 | | 1lt4 9039 |
. . . . . . . . . 10
⊢ 1 <
4 |
32 | | recgt1 8800 |
. . . . . . . . . . 11
⊢ ((4
∈ ℝ ∧ 0 < 4) → (1 < 4 ↔ (1 / 4) <
1)) |
33 | 27, 28, 32 | mp2an 424 |
. . . . . . . . . 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 11835 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → (2
∥ 𝑀 ↔ (𝑀 / 2) ∈
ℤ)) |
37 | 36 | biimpac 296 |
. . . . . . . . 9
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → (𝑀 / 2) ∈
ℤ) |
38 | | 4nn 9028 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ |
39 | | nnrecq 9591 |
. . . . . . . . . 10
⊢ (4 ∈
ℕ → (1 / 4) ∈ ℚ) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . 9
⊢ (1 / 4)
∈ ℚ |
41 | | flqbi2 10234 |
. . . . . . . . 9
⊢ (((𝑀 / 2) ∈ ℤ ∧ (1 /
4) ∈ ℚ) → ((⌊‘((𝑀 / 2) + (1 / 4))) = (𝑀 / 2) ↔ (0 ≤ (1 / 4) ∧ (1 / 4)
< 1))) |
42 | 37, 40, 41 | sylancl 411 |
. . . . . . . 8
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) →
((⌊‘((𝑀 / 2) +
(1 / 4))) = (𝑀 / 2) ↔
(0 ≤ (1 / 4) ∧ (1 / 4) < 1))) |
43 | 35, 42 | mpbiri 167 |
. . . . . . 7
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) →
(⌊‘((𝑀 / 2) +
(1 / 4))) = (𝑀 /
2)) |
44 | 24, 43 | eqtr4d 2206 |
. . . . . 6
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
45 | 44 | expcom 115 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (2
∥ 𝑀 → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4))))) |
46 | | iffalse 3533 |
. . . . . . . 8
⊢ (¬ 2
∥ 𝑀 → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = ((𝑀 − 1) / 2)) |
47 | 46 | adantr 274 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = ((𝑀 − 1) / 2)) |
48 | | odd2np1 11819 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (¬ 2
∥ 𝑀 ↔
∃𝑥 ∈ ℤ ((2
· 𝑥) + 1) = 𝑀)) |
49 | | ax-1cn 7854 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℂ |
50 | | 2cn 8936 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℂ |
51 | 50, 15 | pm3.2i 270 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℂ ∧ 2 # 0) |
52 | | divcanap5 8618 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0) ∧ (2 ∈ ℂ
∧ 2 # 0)) → ((2 · 1) / (2 · 2)) = (1 /
2)) |
53 | 49, 51, 51, 52 | mp3an 1332 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
· 1) / (2 · 2)) = (1 / 2) |
54 | | 2t1e2 9018 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2
· 1) = 2 |
55 | 54, 11 | oveq12i 5862 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
· 1) / (2 · 2)) = (2 / 4) |
56 | 53, 55 | eqtr3i 2193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 / 2) =
(2 / 4) |
57 | 56 | oveq1i 5860 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1 / 2)
+ (1 / 4)) = ((2 / 4) + (1 / 4)) |
58 | 50, 49, 6, 8 | divdirapi 8673 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2 + 1)
/ 4) = ((2 / 4) + (1 / 4)) |
59 | | 2p1e3 8998 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 + 1) =
3 |
60 | 59 | oveq1i 5860 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2 + 1)
/ 4) = (3 / 4) |
61 | 57, 58, 60 | 3eqtr2i 2197 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 / 2)
+ (1 / 4)) = (3 / 4) |
62 | 61 | a1i 9 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → ((1 / 2)
+ (1 / 4)) = (3 / 4)) |
63 | 62 | oveq2d 5866 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → (𝑥 + ((1 / 2) + (1 / 4))) = (𝑥 + (3 / 4))) |
64 | 63 | fveq2d 5498 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ →
(⌊‘(𝑥 + ((1 /
2) + (1 / 4)))) = (⌊‘(𝑥 + (3 / 4)))) |
65 | | 3re 8939 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℝ |
66 | | 0re 7907 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
67 | | 3pos 8959 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 <
3 |
68 | 66, 65, 67 | ltleii 8009 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
3 |
69 | | divge0 8776 |
. . . . . . . . . . . . . . . . . 18
⊢ (((3
∈ ℝ ∧ 0 ≤ 3) ∧ (4 ∈ ℝ ∧ 0 < 4)) →
0 ≤ (3 / 4)) |
70 | 65, 68, 27, 28, 69 | mp4an 425 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤ (3
/ 4) |
71 | | 3lt4 9037 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 <
4 |
72 | | nnrp 9607 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
73 | 38, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ∈
ℝ+ |
74 | | divlt1lt 9668 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((3
∈ ℝ ∧ 4 ∈ ℝ+) → ((3 / 4) < 1
↔ 3 < 4)) |
75 | 65, 73, 74 | mp2an 424 |
. . . . . . . . . . . . . . . . . 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 9228 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℤ |
79 | | znq 9570 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
∈ ℤ ∧ 4 ∈ ℕ) → (3 / 4) ∈
ℚ) |
80 | 78, 38, 79 | mp2an 424 |
. . . . . . . . . . . . . . . . 17
⊢ (3 / 4)
∈ ℚ |
81 | | flqbi2 10234 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ (3 / 4)
∈ ℚ) → ((⌊‘(𝑥 + (3 / 4))) = 𝑥 ↔ (0 ≤ (3 / 4) ∧ (3 / 4) <
1))) |
82 | 80, 81 | mpan2 423 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ →
((⌊‘(𝑥 + (3 /
4))) = 𝑥 ↔ (0 ≤ (3
/ 4) ∧ (3 / 4) < 1))) |
83 | 77, 82 | mpbiri 167 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ →
(⌊‘(𝑥 + (3 /
4))) = 𝑥) |
84 | 64, 83 | eqtrd 2203 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ →
(⌊‘(𝑥 + ((1 /
2) + (1 / 4)))) = 𝑥) |
85 | 84 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (⌊‘(𝑥 + ((1 / 2) + (1 / 4)))) = 𝑥) |
86 | | oveq1 5857 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 = ((2 · 𝑥) + 1) → (𝑀 / 2) = (((2 · 𝑥) + 1) / 2)) |
87 | 86 | eqcoms 2173 |
. . . . . . . . . . . . . . . . 17
⊢ (((2
· 𝑥) + 1) = 𝑀 → (𝑀 / 2) = (((2 · 𝑥) + 1) / 2)) |
88 | | 2z 9227 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℤ |
89 | 88 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℤ → 2 ∈
ℤ) |
90 | | id 19 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℤ) |
91 | 89, 90 | zmulcld 9327 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → (2
· 𝑥) ∈
ℤ) |
92 | 91 | zcnd 9322 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → (2
· 𝑥) ∈
ℂ) |
93 | | 1cnd 7923 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → 1 ∈
ℂ) |
94 | | 2cnd 8938 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → 2 ∈
ℂ) |
95 | 15 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → 2 #
0) |
96 | 92, 93, 94, 95 | divdirapd 8733 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) / 2) =
(((2 · 𝑥) / 2) + (1
/ 2))) |
97 | | zcn 9204 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
98 | 97, 94, 95 | divcanap3d 8699 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → ((2
· 𝑥) / 2) = 𝑥) |
99 | 98 | oveq1d 5865 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) / 2) + (1 / 2))
= (𝑥 + (1 /
2))) |
100 | 96, 99 | eqtrd 2203 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) / 2) =
(𝑥 + (1 /
2))) |
101 | 87, 100 | sylan9eqr 2225 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (𝑀 / 2) = (𝑥 + (1 / 2))) |
102 | 101 | oveq1d 5865 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 / 2) + (1 / 4)) = ((𝑥 + (1 / 2)) + (1 / 4))) |
103 | | halfcn 9079 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 / 2)
∈ ℂ |
104 | 103 | a1i 9 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → (1 / 2)
∈ ℂ) |
105 | 6, 8 | recclapi 8646 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 / 4)
∈ ℂ |
106 | 105 | a1i 9 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → (1 / 4)
∈ ℂ) |
107 | 97, 104, 106 | addassd 7929 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → ((𝑥 + (1 / 2)) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 /
4)))) |
108 | 107 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑥 + (1 / 2)) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 / 4)))) |
109 | 102, 108 | eqtrd 2203 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 / 2) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 / 4)))) |
110 | 109 | fveq2d 5498 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (⌊‘((𝑀 / 2) + (1 / 4))) =
(⌊‘(𝑥 + ((1 /
2) + (1 / 4))))) |
111 | | oveq1 5857 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 = ((2 · 𝑥) + 1) → (𝑀 − 1) = (((2 · 𝑥) + 1) −
1)) |
112 | 111 | eqcoms 2173 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑥) + 1) = 𝑀 → (𝑀 − 1) = (((2 · 𝑥) + 1) −
1)) |
113 | | pncan1 8283 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
· 𝑥) ∈ ℂ
→ (((2 · 𝑥) +
1) − 1) = (2 · 𝑥)) |
114 | 92, 113 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) − 1)
= (2 · 𝑥)) |
115 | 112, 114 | sylan9eqr 2225 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (𝑀 − 1) = (2 · 𝑥)) |
116 | 115 | oveq1d 5865 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = ((2 · 𝑥) / 2)) |
117 | 98 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((2 · 𝑥) / 2) = 𝑥) |
118 | 116, 117 | eqtrd 2203 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = 𝑥) |
119 | 85, 110, 118 | 3eqtr4rd 2214 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
120 | 119 | ex 114 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) = 𝑀 → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 /
4))))) |
121 | 120 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (((2
· 𝑥) + 1) = 𝑀 → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 /
4))))) |
122 | 121 | rexlimdva 2587 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ →
(∃𝑥 ∈ ℤ
((2 · 𝑥) + 1) =
𝑀 → ((𝑀 − 1) / 2) =
(⌊‘((𝑀 / 2) +
(1 / 4))))) |
123 | 48, 122 | sylbid 149 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → (¬ 2
∥ 𝑀 → ((𝑀 − 1) / 2) =
(⌊‘((𝑀 / 2) +
(1 / 4))))) |
124 | 123 | impcom 124 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → ((𝑀 − 1) / 2) =
(⌊‘((𝑀 / 2) +
(1 / 4)))) |
125 | 47, 124 | eqtrd 2203 |
. . . . . 6
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
126 | 125 | expcom 115 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (¬ 2
∥ 𝑀 → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4))))) |
127 | | zeo3 11814 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (2
∥ 𝑀 ∨ ¬ 2
∥ 𝑀)) |
128 | 45, 126, 127 | mpjaod 713 |
. . . 4
⊢ (𝑀 ∈ ℤ → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
129 | 128 | eqcomd 2176 |
. . 3
⊢ (𝑀 ∈ ℤ →
(⌊‘((𝑀 / 2) +
(1 / 4))) = if(2 ∥ 𝑀,
(𝑀 / 2), ((𝑀 − 1) /
2))) |
130 | 129 | adantr 274 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) →
(⌊‘((𝑀 / 2) +
(1 / 4))) = if(2 ∥ 𝑀,
(𝑀 / 2), ((𝑀 − 1) /
2))) |
131 | 22, 130 | eqtrd 2203 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) →
(⌊‘(𝑁 / 4)) =
if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2))) |