| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . 4
⊢ (𝑁 = ((2 · 𝑀) + 1) → (𝑁 / 4) = (((2 · 𝑀) + 1) / 4)) |
| 2 | | 2cnd 12344 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 2 ∈
ℂ) |
| 3 | | zcn 12618 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
| 4 | 2, 3 | mulcld 11281 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → (2
· 𝑀) ∈
ℂ) |
| 5 | | 1cnd 11256 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 1 ∈
ℂ) |
| 6 | | 4cn 12351 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
| 7 | | 4ne0 12374 |
. . . . . . . 8
⊢ 4 ≠
0 |
| 8 | 6, 7 | pm3.2i 470 |
. . . . . . 7
⊢ (4 ∈
ℂ ∧ 4 ≠ 0) |
| 9 | 8 | a1i 11 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → (4 ∈
ℂ ∧ 4 ≠ 0)) |
| 10 | | divdir 11947 |
. . . . . 6
⊢ (((2
· 𝑀) ∈ ℂ
∧ 1 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0)) → (((2
· 𝑀) + 1) / 4) =
(((2 · 𝑀) / 4) + (1
/ 4))) |
| 11 | 4, 5, 9, 10 | syl3anc 1373 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (((2
· 𝑀) + 1) / 4) =
(((2 · 𝑀) / 4) + (1
/ 4))) |
| 12 | | 2t2e4 12430 |
. . . . . . . . . 10
⊢ (2
· 2) = 4 |
| 13 | 12 | eqcomi 2746 |
. . . . . . . . 9
⊢ 4 = (2
· 2) |
| 14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 4 = (2
· 2)) |
| 15 | 14 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → ((2
· 𝑀) / 4) = ((2
· 𝑀) / (2 ·
2))) |
| 16 | | 2ne0 12370 |
. . . . . . . . 9
⊢ 2 ≠
0 |
| 17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 2 ≠
0) |
| 18 | 3, 2, 2, 17, 17 | divcan5d 12069 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → ((2
· 𝑀) / (2 ·
2)) = (𝑀 /
2)) |
| 19 | 15, 18 | eqtrd 2777 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → ((2
· 𝑀) / 4) = (𝑀 / 2)) |
| 20 | 19 | oveq1d 7446 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (((2
· 𝑀) / 4) + (1 / 4))
= ((𝑀 / 2) + (1 /
4))) |
| 21 | 11, 20 | eqtrd 2777 |
. . . 4
⊢ (𝑀 ∈ ℤ → (((2
· 𝑀) + 1) / 4) =
((𝑀 / 2) + (1 /
4))) |
| 22 | 1, 21 | sylan9eqr 2799 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (𝑁 / 4) = ((𝑀 / 2) + (1 / 4))) |
| 23 | 22 | fveq2d 6910 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) →
(⌊‘(𝑁 / 4)) =
(⌊‘((𝑀 / 2) +
(1 / 4)))) |
| 24 | | iftrue 4531 |
. . . . . . 7
⊢ (2
∥ 𝑀 → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (𝑀 / 2)) |
| 25 | 24 | adantr 480 |
. . . . . 6
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (𝑀 / 2)) |
| 26 | | 1re 11261 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
| 27 | | 0le1 11786 |
. . . . . . . . 9
⊢ 0 ≤
1 |
| 28 | | 4re 12350 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
| 29 | | 4pos 12373 |
. . . . . . . . 9
⊢ 0 <
4 |
| 30 | | divge0 12137 |
. . . . . . . . 9
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ (4 ∈ ℝ ∧ 0 < 4)) →
0 ≤ (1 / 4)) |
| 31 | 26, 27, 28, 29, 30 | mp4an 693 |
. . . . . . . 8
⊢ 0 ≤ (1
/ 4) |
| 32 | | 1lt4 12442 |
. . . . . . . . 9
⊢ 1 <
4 |
| 33 | | recgt1 12164 |
. . . . . . . . . 10
⊢ ((4
∈ ℝ ∧ 0 < 4) → (1 < 4 ↔ (1 / 4) <
1)) |
| 34 | 28, 29, 33 | mp2an 692 |
. . . . . . . . 9
⊢ (1 < 4
↔ (1 / 4) < 1) |
| 35 | 32, 34 | mpbi 230 |
. . . . . . . 8
⊢ (1 / 4)
< 1 |
| 36 | 31, 35 | pm3.2i 470 |
. . . . . . 7
⊢ (0 ≤
(1 / 4) ∧ (1 / 4) < 1) |
| 37 | | evend2 16394 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (2
∥ 𝑀 ↔ (𝑀 / 2) ∈
ℤ)) |
| 38 | 37 | biimpac 478 |
. . . . . . . 8
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → (𝑀 / 2) ∈
ℤ) |
| 39 | | 4nn 12349 |
. . . . . . . . 9
⊢ 4 ∈
ℕ |
| 40 | | nnrecre 12308 |
. . . . . . . . 9
⊢ (4 ∈
ℕ → (1 / 4) ∈ ℝ) |
| 41 | 39, 40 | ax-mp 5 |
. . . . . . . 8
⊢ (1 / 4)
∈ ℝ |
| 42 | | flbi2 13857 |
. . . . . . . 8
⊢ (((𝑀 / 2) ∈ ℤ ∧ (1 /
4) ∈ ℝ) → ((⌊‘((𝑀 / 2) + (1 / 4))) = (𝑀 / 2) ↔ (0 ≤ (1 / 4) ∧ (1 / 4)
< 1))) |
| 43 | 38, 41, 42 | sylancl 586 |
. . . . . . 7
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) →
((⌊‘((𝑀 / 2) +
(1 / 4))) = (𝑀 / 2) ↔
(0 ≤ (1 / 4) ∧ (1 / 4) < 1))) |
| 44 | 36, 43 | mpbiri 258 |
. . . . . 6
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) →
(⌊‘((𝑀 / 2) +
(1 / 4))) = (𝑀 /
2)) |
| 45 | 25, 44 | eqtr4d 2780 |
. . . . 5
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
| 46 | | iffalse 4534 |
. . . . . . 7
⊢ (¬ 2
∥ 𝑀 → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = ((𝑀 − 1) / 2)) |
| 47 | 46 | adantr 480 |
. . . . . 6
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = ((𝑀 − 1) / 2)) |
| 48 | | odd2np1 16378 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → (¬ 2
∥ 𝑀 ↔
∃𝑥 ∈ ℤ ((2
· 𝑥) + 1) = 𝑀)) |
| 49 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℂ |
| 50 | | 2cnne0 12476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
| 51 | | divcan5 11969 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((2 · 1) / (2 · 2)) = (1 /
2)) |
| 52 | 49, 50, 50, 51 | mp3an 1463 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 1) / (2 · 2)) = (1 / 2) |
| 53 | | 2t1e2 12429 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 1) = 2 |
| 54 | 53, 12 | oveq12i 7443 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 1) / (2 · 2)) = (2 / 4) |
| 55 | 52, 54 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 / 2) =
(2 / 4) |
| 56 | 55 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 / 2)
+ (1 / 4)) = ((2 / 4) + (1 / 4)) |
| 57 | | 2cn 12341 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℂ |
| 58 | 57, 49, 6, 7 | divdiri 12024 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2 + 1)
/ 4) = ((2 / 4) + (1 / 4)) |
| 59 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 + 1) =
3 |
| 60 | 59 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2 + 1)
/ 4) = (3 / 4) |
| 61 | 56, 58, 60 | 3eqtr2i 2771 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 / 2)
+ (1 / 4)) = (3 / 4) |
| 62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → ((1 / 2)
+ (1 / 4)) = (3 / 4)) |
| 63 | 62 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → (𝑥 + ((1 / 2) + (1 / 4))) = (𝑥 + (3 / 4))) |
| 64 | 63 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ →
(⌊‘(𝑥 + ((1 /
2) + (1 / 4)))) = (⌊‘(𝑥 + (3 / 4)))) |
| 65 | | 3re 12346 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℝ |
| 66 | | 0re 11263 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
| 67 | | 3pos 12371 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
3 |
| 68 | 66, 65, 67 | ltleii 11384 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
3 |
| 69 | | divge0 12137 |
. . . . . . . . . . . . . . . . 17
⊢ (((3
∈ ℝ ∧ 0 ≤ 3) ∧ (4 ∈ ℝ ∧ 0 < 4)) →
0 ≤ (3 / 4)) |
| 70 | 65, 68, 28, 29, 69 | mp4an 693 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤ (3
/ 4) |
| 71 | | 3lt4 12440 |
. . . . . . . . . . . . . . . . 17
⊢ 3 <
4 |
| 72 | | nnrp 13046 |
. . . . . . . . . . . . . . . . . . 19
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
| 73 | 39, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℝ+ |
| 74 | | divlt1lt 13104 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
∈ ℝ ∧ 4 ∈ ℝ+) → ((3 / 4) < 1
↔ 3 < 4)) |
| 75 | 65, 73, 74 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ ((3 / 4)
< 1 ↔ 3 < 4) |
| 76 | 71, 75 | mpbir 231 |
. . . . . . . . . . . . . . . 16
⊢ (3 / 4)
< 1 |
| 77 | 70, 76 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (0 ≤
(3 / 4) ∧ (3 / 4) < 1) |
| 78 | 65, 28, 7 | redivcli 12034 |
. . . . . . . . . . . . . . . 16
⊢ (3 / 4)
∈ ℝ |
| 79 | | flbi2 13857 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ (3 / 4)
∈ ℝ) → ((⌊‘(𝑥 + (3 / 4))) = 𝑥 ↔ (0 ≤ (3 / 4) ∧ (3 / 4) <
1))) |
| 80 | 78, 79 | mpan2 691 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ →
((⌊‘(𝑥 + (3 /
4))) = 𝑥 ↔ (0 ≤ (3
/ 4) ∧ (3 / 4) < 1))) |
| 81 | 77, 80 | mpbiri 258 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ →
(⌊‘(𝑥 + (3 /
4))) = 𝑥) |
| 82 | 64, 81 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ →
(⌊‘(𝑥 + ((1 /
2) + (1 / 4)))) = 𝑥) |
| 83 | 82 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (⌊‘(𝑥 + ((1 / 2) + (1 / 4)))) = 𝑥) |
| 84 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 = ((2 · 𝑥) + 1) → (𝑀 / 2) = (((2 · 𝑥) + 1) / 2)) |
| 85 | 84 | eqcoms 2745 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑥) + 1) = 𝑀 → (𝑀 / 2) = (((2 · 𝑥) + 1) / 2)) |
| 86 | | 2z 12649 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℤ |
| 87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → 2 ∈
ℤ) |
| 88 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℤ) |
| 89 | 87, 88 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → (2
· 𝑥) ∈
ℤ) |
| 90 | 89 | zcnd 12723 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → (2
· 𝑥) ∈
ℂ) |
| 91 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → 1 ∈
ℂ) |
| 92 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → (2 ∈
ℂ ∧ 2 ≠ 0)) |
| 93 | | divdir 11947 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝑥) ∈ ℂ
∧ 1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2
· 𝑥) + 1) / 2) =
(((2 · 𝑥) / 2) + (1
/ 2))) |
| 94 | 90, 91, 92, 93 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) / 2) =
(((2 · 𝑥) / 2) + (1
/ 2))) |
| 95 | | zcn 12618 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
| 96 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → 2 ∈
ℂ) |
| 97 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → 2 ≠
0) |
| 98 | 95, 96, 97 | divcan3d 12048 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → ((2
· 𝑥) / 2) = 𝑥) |
| 99 | 98 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) / 2) + (1 / 2))
= (𝑥 + (1 /
2))) |
| 100 | 94, 99 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) / 2) =
(𝑥 + (1 /
2))) |
| 101 | 85, 100 | sylan9eqr 2799 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (𝑀 / 2) = (𝑥 + (1 / 2))) |
| 102 | 101 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 / 2) + (1 / 4)) = ((𝑥 + (1 / 2)) + (1 / 4))) |
| 103 | | halfcn 12481 |
. . . . . . . . . . . . . . . . 17
⊢ (1 / 2)
∈ ℂ |
| 104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → (1 / 2)
∈ ℂ) |
| 105 | 6, 7 | reccli 11997 |
. . . . . . . . . . . . . . . . 17
⊢ (1 / 4)
∈ ℂ |
| 106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → (1 / 4)
∈ ℂ) |
| 107 | 95, 104, 106 | addassd 11283 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → ((𝑥 + (1 / 2)) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 /
4)))) |
| 108 | 107 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑥 + (1 / 2)) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 / 4)))) |
| 109 | 102, 108 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 / 2) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 / 4)))) |
| 110 | 109 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (⌊‘((𝑀 / 2) + (1 / 4))) =
(⌊‘(𝑥 + ((1 /
2) + (1 / 4))))) |
| 111 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 = ((2 · 𝑥) + 1) → (𝑀 − 1) = (((2 · 𝑥) + 1) −
1)) |
| 112 | 111 | eqcoms 2745 |
. . . . . . . . . . . . . . 15
⊢ (((2
· 𝑥) + 1) = 𝑀 → (𝑀 − 1) = (((2 · 𝑥) + 1) −
1)) |
| 113 | | pncan1 11687 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑥) ∈ ℂ
→ (((2 · 𝑥) +
1) − 1) = (2 · 𝑥)) |
| 114 | 90, 113 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) − 1)
= (2 · 𝑥)) |
| 115 | 112, 114 | sylan9eqr 2799 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (𝑀 − 1) = (2 · 𝑥)) |
| 116 | 115 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = ((2 · 𝑥) / 2)) |
| 117 | 98 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((2 · 𝑥) / 2) = 𝑥) |
| 118 | 116, 117 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = 𝑥) |
| 119 | 83, 110, 118 | 3eqtr4rd 2788 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
| 120 | 119 | ex 412 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) = 𝑀 → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 /
4))))) |
| 121 | 120 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (((2
· 𝑥) + 1) = 𝑀 → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 /
4))))) |
| 122 | 121 | rexlimdva 3155 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ →
(∃𝑥 ∈ ℤ
((2 · 𝑥) + 1) =
𝑀 → ((𝑀 − 1) / 2) =
(⌊‘((𝑀 / 2) +
(1 / 4))))) |
| 123 | 48, 122 | sylbid 240 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → (¬ 2
∥ 𝑀 → ((𝑀 − 1) / 2) =
(⌊‘((𝑀 / 2) +
(1 / 4))))) |
| 124 | 123 | impcom 407 |
. . . . . 6
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → ((𝑀 − 1) / 2) =
(⌊‘((𝑀 / 2) +
(1 / 4)))) |
| 125 | 47, 124 | eqtrd 2777 |
. . . . 5
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
| 126 | 45, 125 | pm2.61ian 812 |
. . . 4
⊢ (𝑀 ∈ ℤ → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
| 127 | 126 | eqcomd 2743 |
. . 3
⊢ (𝑀 ∈ ℤ →
(⌊‘((𝑀 / 2) +
(1 / 4))) = if(2 ∥ 𝑀,
(𝑀 / 2), ((𝑀 − 1) /
2))) |
| 128 | 127 | adantr 480 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) →
(⌊‘((𝑀 / 2) +
(1 / 4))) = if(2 ∥ 𝑀,
(𝑀 / 2), ((𝑀 − 1) /
2))) |
| 129 | 23, 128 | eqtrd 2777 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) →
(⌊‘(𝑁 / 4)) =
if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2))) |