Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . 4
⊢ (𝑁 = ((2 · 𝑀) + 1) → (𝑁 / 4) = (((2 · 𝑀) + 1) / 4)) |
2 | | 2cnd 10970 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 2 ∈
ℂ) |
3 | | zcn 11259 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
4 | 2, 3 | mulcld 9939 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → (2
· 𝑀) ∈
ℂ) |
5 | | 1cnd 9935 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 1 ∈
ℂ) |
6 | | 4cn 10975 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
7 | | 4ne0 10994 |
. . . . . . . 8
⊢ 4 ≠
0 |
8 | 6, 7 | pm3.2i 470 |
. . . . . . 7
⊢ (4 ∈
ℂ ∧ 4 ≠ 0) |
9 | 8 | a1i 11 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → (4 ∈
ℂ ∧ 4 ≠ 0)) |
10 | | divdir 10589 |
. . . . . 6
⊢ (((2
· 𝑀) ∈ ℂ
∧ 1 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0)) → (((2
· 𝑀) + 1) / 4) =
(((2 · 𝑀) / 4) + (1
/ 4))) |
11 | 4, 5, 9, 10 | syl3anc 1318 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (((2
· 𝑀) + 1) / 4) =
(((2 · 𝑀) / 4) + (1
/ 4))) |
12 | | 2t2e4 11054 |
. . . . . . . . . 10
⊢ (2
· 2) = 4 |
13 | 12 | eqcomi 2619 |
. . . . . . . . 9
⊢ 4 = (2
· 2) |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 4 = (2
· 2)) |
15 | 14 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → ((2
· 𝑀) / 4) = ((2
· 𝑀) / (2 ·
2))) |
16 | | 2ne0 10990 |
. . . . . . . . 9
⊢ 2 ≠
0 |
17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 2 ≠
0) |
18 | 3, 2, 2, 17, 17 | divcan5d 10706 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → ((2
· 𝑀) / (2 ·
2)) = (𝑀 /
2)) |
19 | 15, 18 | eqtrd 2644 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → ((2
· 𝑀) / 4) = (𝑀 / 2)) |
20 | 19 | oveq1d 6564 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (((2
· 𝑀) / 4) + (1 / 4))
= ((𝑀 / 2) + (1 /
4))) |
21 | 11, 20 | eqtrd 2644 |
. . . 4
⊢ (𝑀 ∈ ℤ → (((2
· 𝑀) + 1) / 4) =
((𝑀 / 2) + (1 /
4))) |
22 | 1, 21 | sylan9eqr 2666 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (𝑁 / 4) = ((𝑀 / 2) + (1 / 4))) |
23 | 22 | fveq2d 6107 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) →
(⌊‘(𝑁 / 4)) =
(⌊‘((𝑀 / 2) +
(1 / 4)))) |
24 | | iftrue 4042 |
. . . . . . 7
⊢ (2
∥ 𝑀 → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (𝑀 / 2)) |
25 | 24 | adantr 480 |
. . . . . 6
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (𝑀 / 2)) |
26 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
27 | | 0le1 10430 |
. . . . . . . . 9
⊢ 0 ≤
1 |
28 | | 4re 10974 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
29 | | 4pos 10993 |
. . . . . . . . 9
⊢ 0 <
4 |
30 | | divge0 10771 |
. . . . . . . . 9
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ (4 ∈ ℝ ∧ 0 < 4)) →
0 ≤ (1 / 4)) |
31 | 26, 27, 28, 29, 30 | mp4an 705 |
. . . . . . . 8
⊢ 0 ≤ (1
/ 4) |
32 | | 1lt4 11076 |
. . . . . . . . 9
⊢ 1 <
4 |
33 | | recgt1 10798 |
. . . . . . . . . 10
⊢ ((4
∈ ℝ ∧ 0 < 4) → (1 < 4 ↔ (1 / 4) <
1)) |
34 | 28, 29, 33 | mp2an 704 |
. . . . . . . . 9
⊢ (1 < 4
↔ (1 / 4) < 1) |
35 | 32, 34 | mpbi 219 |
. . . . . . . 8
⊢ (1 / 4)
< 1 |
36 | 31, 35 | pm3.2i 470 |
. . . . . . 7
⊢ (0 ≤
(1 / 4) ∧ (1 / 4) < 1) |
37 | | 2z 11286 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
38 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 2 ∈
ℤ) |
39 | | id 22 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℤ) |
40 | | dvdsval2 14824 |
. . . . . . . . . 10
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ 𝑀 ∈ ℤ) → (2 ∥ 𝑀 ↔ (𝑀 / 2) ∈ ℤ)) |
41 | 38, 17, 39, 40 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (2
∥ 𝑀 ↔ (𝑀 / 2) ∈
ℤ)) |
42 | 41 | biimpac 502 |
. . . . . . . 8
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → (𝑀 / 2) ∈
ℤ) |
43 | | 4nn 11064 |
. . . . . . . . 9
⊢ 4 ∈
ℕ |
44 | | nnrecre 10934 |
. . . . . . . . 9
⊢ (4 ∈
ℕ → (1 / 4) ∈ ℝ) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . 8
⊢ (1 / 4)
∈ ℝ |
46 | | flbi2 12480 |
. . . . . . . 8
⊢ (((𝑀 / 2) ∈ ℤ ∧ (1 /
4) ∈ ℝ) → ((⌊‘((𝑀 / 2) + (1 / 4))) = (𝑀 / 2) ↔ (0 ≤ (1 / 4) ∧ (1 / 4)
< 1))) |
47 | 42, 45, 46 | sylancl 693 |
. . . . . . 7
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) →
((⌊‘((𝑀 / 2) +
(1 / 4))) = (𝑀 / 2) ↔
(0 ≤ (1 / 4) ∧ (1 / 4) < 1))) |
48 | 36, 47 | mpbiri 247 |
. . . . . 6
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) →
(⌊‘((𝑀 / 2) +
(1 / 4))) = (𝑀 /
2)) |
49 | 25, 48 | eqtr4d 2647 |
. . . . 5
⊢ ((2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
50 | | iffalse 4045 |
. . . . . . 7
⊢ (¬ 2
∥ 𝑀 → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = ((𝑀 − 1) / 2)) |
51 | 50 | adantr 480 |
. . . . . 6
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = ((𝑀 − 1) / 2)) |
52 | | odd2np1 14903 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → (¬ 2
∥ 𝑀 ↔
∃𝑥 ∈ ℤ ((2
· 𝑥) + 1) = 𝑀)) |
53 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℂ |
54 | | 2cnne0 11119 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
55 | | divcan5 10606 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((2 · 1) / (2 · 2)) = (1 /
2)) |
56 | 53, 54, 54, 55 | mp3an 1416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 1) / (2 · 2)) = (1 / 2) |
57 | | 2t1e2 11053 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 1) = 2 |
58 | 57, 12 | oveq12i 6561 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 1) / (2 · 2)) = (2 / 4) |
59 | 56, 58 | eqtr3i 2634 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 / 2) =
(2 / 4) |
60 | 59 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 / 2)
+ (1 / 4)) = ((2 / 4) + (1 / 4)) |
61 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℂ |
62 | 61, 53, 6, 7 | divdiri 10661 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2 + 1)
/ 4) = ((2 / 4) + (1 / 4)) |
63 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 + 1) =
3 |
64 | 63 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2 + 1)
/ 4) = (3 / 4) |
65 | 60, 62, 64 | 3eqtr2i 2638 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 / 2)
+ (1 / 4)) = (3 / 4) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → ((1 / 2)
+ (1 / 4)) = (3 / 4)) |
67 | 66 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → (𝑥 + ((1 / 2) + (1 / 4))) = (𝑥 + (3 / 4))) |
68 | 67 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ →
(⌊‘(𝑥 + ((1 /
2) + (1 / 4)))) = (⌊‘(𝑥 + (3 / 4)))) |
69 | | 3re 10971 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℝ |
70 | | 0re 9919 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
71 | | 3pos 10991 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
3 |
72 | 70, 69, 71 | ltleii 10039 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
3 |
73 | | divge0 10771 |
. . . . . . . . . . . . . . . . 17
⊢ (((3
∈ ℝ ∧ 0 ≤ 3) ∧ (4 ∈ ℝ ∧ 0 < 4)) →
0 ≤ (3 / 4)) |
74 | 69, 72, 28, 29, 73 | mp4an 705 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤ (3
/ 4) |
75 | | 3lt4 11074 |
. . . . . . . . . . . . . . . . 17
⊢ 3 <
4 |
76 | | nnrp 11718 |
. . . . . . . . . . . . . . . . . . 19
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
77 | 43, 76 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℝ+ |
78 | | divlt1lt 11775 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
∈ ℝ ∧ 4 ∈ ℝ+) → ((3 / 4) < 1
↔ 3 < 4)) |
79 | 69, 77, 78 | mp2an 704 |
. . . . . . . . . . . . . . . . 17
⊢ ((3 / 4)
< 1 ↔ 3 < 4) |
80 | 75, 79 | mpbir 220 |
. . . . . . . . . . . . . . . 16
⊢ (3 / 4)
< 1 |
81 | 74, 80 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (0 ≤
(3 / 4) ∧ (3 / 4) < 1) |
82 | 69, 28, 7 | redivcli 10671 |
. . . . . . . . . . . . . . . 16
⊢ (3 / 4)
∈ ℝ |
83 | | flbi2 12480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ (3 / 4)
∈ ℝ) → ((⌊‘(𝑥 + (3 / 4))) = 𝑥 ↔ (0 ≤ (3 / 4) ∧ (3 / 4) <
1))) |
84 | 82, 83 | mpan2 703 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ →
((⌊‘(𝑥 + (3 /
4))) = 𝑥 ↔ (0 ≤ (3
/ 4) ∧ (3 / 4) < 1))) |
85 | 81, 84 | mpbiri 247 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ →
(⌊‘(𝑥 + (3 /
4))) = 𝑥) |
86 | 68, 85 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ →
(⌊‘(𝑥 + ((1 /
2) + (1 / 4)))) = 𝑥) |
87 | 86 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (⌊‘(𝑥 + ((1 / 2) + (1 / 4)))) = 𝑥) |
88 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 = ((2 · 𝑥) + 1) → (𝑀 / 2) = (((2 · 𝑥) + 1) / 2)) |
89 | 88 | eqcoms 2618 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑥) + 1) = 𝑀 → (𝑀 / 2) = (((2 · 𝑥) + 1) / 2)) |
90 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → 2 ∈
ℤ) |
91 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℤ) |
92 | 90, 91 | zmulcld 11364 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → (2
· 𝑥) ∈
ℤ) |
93 | 92 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → (2
· 𝑥) ∈
ℂ) |
94 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → 1 ∈
ℂ) |
95 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → (2 ∈
ℂ ∧ 2 ≠ 0)) |
96 | | divdir 10589 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝑥) ∈ ℂ
∧ 1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2
· 𝑥) + 1) / 2) =
(((2 · 𝑥) / 2) + (1
/ 2))) |
97 | 93, 94, 95, 96 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) / 2) =
(((2 · 𝑥) / 2) + (1
/ 2))) |
98 | | zcn 11259 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
99 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → 2 ∈
ℂ) |
100 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → 2 ≠
0) |
101 | 98, 99, 100 | divcan3d 10685 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → ((2
· 𝑥) / 2) = 𝑥) |
102 | 101 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) / 2) + (1 / 2))
= (𝑥 + (1 /
2))) |
103 | 97, 102 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) / 2) =
(𝑥 + (1 /
2))) |
104 | 89, 103 | sylan9eqr 2666 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (𝑀 / 2) = (𝑥 + (1 / 2))) |
105 | 104 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 / 2) + (1 / 4)) = ((𝑥 + (1 / 2)) + (1 / 4))) |
106 | | halfcn 11124 |
. . . . . . . . . . . . . . . . 17
⊢ (1 / 2)
∈ ℂ |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → (1 / 2)
∈ ℂ) |
108 | 6, 7 | reccli 10634 |
. . . . . . . . . . . . . . . . 17
⊢ (1 / 4)
∈ ℂ |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → (1 / 4)
∈ ℂ) |
110 | 98, 107, 109 | addassd 9941 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → ((𝑥 + (1 / 2)) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 /
4)))) |
111 | 110 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑥 + (1 / 2)) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 / 4)))) |
112 | 105, 111 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 / 2) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 / 4)))) |
113 | 112 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (⌊‘((𝑀 / 2) + (1 / 4))) =
(⌊‘(𝑥 + ((1 /
2) + (1 / 4))))) |
114 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 = ((2 · 𝑥) + 1) → (𝑀 − 1) = (((2 · 𝑥) + 1) −
1)) |
115 | 114 | eqcoms 2618 |
. . . . . . . . . . . . . . 15
⊢ (((2
· 𝑥) + 1) = 𝑀 → (𝑀 − 1) = (((2 · 𝑥) + 1) −
1)) |
116 | | pncan1 10333 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑥) ∈ ℂ
→ (((2 · 𝑥) +
1) − 1) = (2 · 𝑥)) |
117 | 93, 116 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) − 1)
= (2 · 𝑥)) |
118 | 115, 117 | sylan9eqr 2666 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → (𝑀 − 1) = (2 · 𝑥)) |
119 | 118 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = ((2 · 𝑥) / 2)) |
120 | 101 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((2 · 𝑥) / 2) = 𝑥) |
121 | 119, 120 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = 𝑥) |
122 | 87, 113, 121 | 3eqtr4rd 2655 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ ((2
· 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
123 | 122 | ex 449 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + 1) = 𝑀 → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 /
4))))) |
124 | 123 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (((2
· 𝑥) + 1) = 𝑀 → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 /
4))))) |
125 | 124 | rexlimdva 3013 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ →
(∃𝑥 ∈ ℤ
((2 · 𝑥) + 1) =
𝑀 → ((𝑀 − 1) / 2) =
(⌊‘((𝑀 / 2) +
(1 / 4))))) |
126 | 52, 125 | sylbid 229 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → (¬ 2
∥ 𝑀 → ((𝑀 − 1) / 2) =
(⌊‘((𝑀 / 2) +
(1 / 4))))) |
127 | 126 | impcom 445 |
. . . . . 6
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → ((𝑀 − 1) / 2) =
(⌊‘((𝑀 / 2) +
(1 / 4)))) |
128 | 51, 127 | eqtrd 2644 |
. . . . 5
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑀 ∈ ℤ) → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
129 | 49, 128 | pm2.61ian 827 |
. . . 4
⊢ (𝑀 ∈ ℤ → if(2
∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 /
4)))) |
130 | 129 | eqcomd 2616 |
. . 3
⊢ (𝑀 ∈ ℤ →
(⌊‘((𝑀 / 2) +
(1 / 4))) = if(2 ∥ 𝑀,
(𝑀 / 2), ((𝑀 − 1) /
2))) |
131 | 130 | adantr 480 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) →
(⌊‘((𝑀 / 2) +
(1 / 4))) = if(2 ∥ 𝑀,
(𝑀 / 2), ((𝑀 − 1) /
2))) |
132 | 23, 131 | eqtrd 2644 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) →
(⌊‘(𝑁 / 4)) =
if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2))) |