Step | Hyp | Ref
| Expression |
1 | | oveq1 5882 |
. . . 4
โข (๐ = ((2 ยท ๐) + 1) โ (๐ / 4) = (((2 ยท ๐) + 1) / 4)) |
2 | | 2cnd 8992 |
. . . . . . 7
โข (๐ โ โค โ 2 โ
โ) |
3 | | zcn 9258 |
. . . . . . 7
โข (๐ โ โค โ ๐ โ
โ) |
4 | 2, 3 | mulcld 7978 |
. . . . . 6
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
5 | | 1cnd 7973 |
. . . . . 6
โข (๐ โ โค โ 1 โ
โ) |
6 | | 4cn 8997 |
. . . . . . 7
โข 4 โ
โ |
7 | 6 | a1i 9 |
. . . . . 6
โข (๐ โ โค โ 4 โ
โ) |
8 | | 4ap0 9018 |
. . . . . . 7
โข 4 #
0 |
9 | 8 | a1i 9 |
. . . . . 6
โข (๐ โ โค โ 4 #
0) |
10 | 4, 5, 7, 9 | divdirapd 8786 |
. . . . 5
โข (๐ โ โค โ (((2
ยท ๐) + 1) / 4) =
(((2 ยท ๐) / 4) + (1
/ 4))) |
11 | | 2t2e4 9073 |
. . . . . . . . . 10
โข (2
ยท 2) = 4 |
12 | 11 | eqcomi 2181 |
. . . . . . . . 9
โข 4 = (2
ยท 2) |
13 | 12 | a1i 9 |
. . . . . . . 8
โข (๐ โ โค โ 4 = (2
ยท 2)) |
14 | 13 | oveq2d 5891 |
. . . . . . 7
โข (๐ โ โค โ ((2
ยท ๐) / 4) = ((2
ยท ๐) / (2 ยท
2))) |
15 | | 2ap0 9012 |
. . . . . . . . 9
โข 2 #
0 |
16 | 15 | a1i 9 |
. . . . . . . 8
โข (๐ โ โค โ 2 #
0) |
17 | 3, 2, 2, 16, 16 | divcanap5d 8774 |
. . . . . . 7
โข (๐ โ โค โ ((2
ยท ๐) / (2 ยท
2)) = (๐ /
2)) |
18 | 14, 17 | eqtrd 2210 |
. . . . . 6
โข (๐ โ โค โ ((2
ยท ๐) / 4) = (๐ / 2)) |
19 | 18 | oveq1d 5890 |
. . . . 5
โข (๐ โ โค โ (((2
ยท ๐) / 4) + (1 / 4))
= ((๐ / 2) + (1 /
4))) |
20 | 10, 19 | eqtrd 2210 |
. . . 4
โข (๐ โ โค โ (((2
ยท ๐) + 1) / 4) =
((๐ / 2) + (1 /
4))) |
21 | 1, 20 | sylan9eqr 2232 |
. . 3
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ (๐ / 4) = ((๐ / 2) + (1 / 4))) |
22 | 21 | fveq2d 5520 |
. 2
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ
(โโ(๐ / 4)) =
(โโ((๐ / 2) +
(1 / 4)))) |
23 | | iftrue 3540 |
. . . . . . . 8
โข (2
โฅ ๐ โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = (๐ / 2)) |
24 | 23 | adantr 276 |
. . . . . . 7
โข ((2
โฅ ๐ โง ๐ โ โค) โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = (๐ / 2)) |
25 | | 1re 7956 |
. . . . . . . . . 10
โข 1 โ
โ |
26 | | 0le1 8438 |
. . . . . . . . . 10
โข 0 โค
1 |
27 | | 4re 8996 |
. . . . . . . . . 10
โข 4 โ
โ |
28 | | 4pos 9016 |
. . . . . . . . . 10
โข 0 <
4 |
29 | | divge0 8830 |
. . . . . . . . . 10
โข (((1
โ โ โง 0 โค 1) โง (4 โ โ โง 0 < 4)) โ
0 โค (1 / 4)) |
30 | 25, 26, 27, 28, 29 | mp4an 427 |
. . . . . . . . 9
โข 0 โค (1
/ 4) |
31 | | 1lt4 9093 |
. . . . . . . . . 10
โข 1 <
4 |
32 | | recgt1 8854 |
. . . . . . . . . . 11
โข ((4
โ โ โง 0 < 4) โ (1 < 4 โ (1 / 4) <
1)) |
33 | 27, 28, 32 | mp2an 426 |
. . . . . . . . . 10
โข (1 < 4
โ (1 / 4) < 1) |
34 | 31, 33 | mpbi 145 |
. . . . . . . . 9
โข (1 / 4)
< 1 |
35 | 30, 34 | pm3.2i 272 |
. . . . . . . 8
โข (0 โค
(1 / 4) โง (1 / 4) < 1) |
36 | | evend2 11894 |
. . . . . . . . . 10
โข (๐ โ โค โ (2
โฅ ๐ โ (๐ / 2) โ
โค)) |
37 | 36 | biimpac 298 |
. . . . . . . . 9
โข ((2
โฅ ๐ โง ๐ โ โค) โ (๐ / 2) โ
โค) |
38 | | 4nn 9082 |
. . . . . . . . . 10
โข 4 โ
โ |
39 | | nnrecq 9645 |
. . . . . . . . . 10
โข (4 โ
โ โ (1 / 4) โ โ) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . 9
โข (1 / 4)
โ โ |
41 | | flqbi2 10291 |
. . . . . . . . 9
โข (((๐ / 2) โ โค โง (1 /
4) โ โ) โ ((โโ((๐ / 2) + (1 / 4))) = (๐ / 2) โ (0 โค (1 / 4) โง (1 / 4)
< 1))) |
42 | 37, 40, 41 | sylancl 413 |
. . . . . . . 8
โข ((2
โฅ ๐ โง ๐ โ โค) โ
((โโ((๐ / 2) +
(1 / 4))) = (๐ / 2) โ
(0 โค (1 / 4) โง (1 / 4) < 1))) |
43 | 35, 42 | mpbiri 168 |
. . . . . . 7
โข ((2
โฅ ๐ โง ๐ โ โค) โ
(โโ((๐ / 2) +
(1 / 4))) = (๐ /
2)) |
44 | 24, 43 | eqtr4d 2213 |
. . . . . 6
โข ((2
โฅ ๐ โง ๐ โ โค) โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = (โโ((๐ / 2) + (1 /
4)))) |
45 | 44 | expcom 116 |
. . . . 5
โข (๐ โ โค โ (2
โฅ ๐ โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = (โโ((๐ / 2) + (1 /
4))))) |
46 | | iffalse 3543 |
. . . . . . . 8
โข (ยฌ 2
โฅ ๐ โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = ((๐ โ 1) / 2)) |
47 | 46 | adantr 276 |
. . . . . . 7
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โค) โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = ((๐ โ 1) / 2)) |
48 | | odd2np1 11878 |
. . . . . . . . 9
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ฅ โ โค ((2
ยท ๐ฅ) + 1) = ๐)) |
49 | | ax-1cn 7904 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 1 โ
โ |
50 | | 2cn 8990 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 2 โ
โ |
51 | 50, 15 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (2 โ
โ โง 2 # 0) |
52 | | divcanap5 8671 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((1
โ โ โง (2 โ โ โง 2 # 0) โง (2 โ โ
โง 2 # 0)) โ ((2 ยท 1) / (2 ยท 2)) = (1 /
2)) |
53 | 49, 51, 51, 52 | mp3an 1337 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((2
ยท 1) / (2 ยท 2)) = (1 / 2) |
54 | | 2t1e2 9072 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (2
ยท 1) = 2 |
55 | 54, 11 | oveq12i 5887 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((2
ยท 1) / (2 ยท 2)) = (2 / 4) |
56 | 53, 55 | eqtr3i 2200 |
. . . . . . . . . . . . . . . . . . . 20
โข (1 / 2) =
(2 / 4) |
57 | 56 | oveq1i 5885 |
. . . . . . . . . . . . . . . . . . 19
โข ((1 / 2)
+ (1 / 4)) = ((2 / 4) + (1 / 4)) |
58 | 50, 49, 6, 8 | divdirapi 8726 |
. . . . . . . . . . . . . . . . . . 19
โข ((2 + 1)
/ 4) = ((2 / 4) + (1 / 4)) |
59 | | 2p1e3 9052 |
. . . . . . . . . . . . . . . . . . . 20
โข (2 + 1) =
3 |
60 | 59 | oveq1i 5885 |
. . . . . . . . . . . . . . . . . . 19
โข ((2 + 1)
/ 4) = (3 / 4) |
61 | 57, 58, 60 | 3eqtr2i 2204 |
. . . . . . . . . . . . . . . . . 18
โข ((1 / 2)
+ (1 / 4)) = (3 / 4) |
62 | 61 | a1i 9 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ ((1 / 2)
+ (1 / 4)) = (3 / 4)) |
63 | 62 | oveq2d 5891 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ (๐ฅ + ((1 / 2) + (1 / 4))) = (๐ฅ + (3 / 4))) |
64 | 63 | fveq2d 5520 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โค โ
(โโ(๐ฅ + ((1 /
2) + (1 / 4)))) = (โโ(๐ฅ + (3 / 4)))) |
65 | | 3re 8993 |
. . . . . . . . . . . . . . . . . 18
โข 3 โ
โ |
66 | | 0re 7957 |
. . . . . . . . . . . . . . . . . . 19
โข 0 โ
โ |
67 | | 3pos 9013 |
. . . . . . . . . . . . . . . . . . 19
โข 0 <
3 |
68 | 66, 65, 67 | ltleii 8060 |
. . . . . . . . . . . . . . . . . 18
โข 0 โค
3 |
69 | | divge0 8830 |
. . . . . . . . . . . . . . . . . 18
โข (((3
โ โ โง 0 โค 3) โง (4 โ โ โง 0 < 4)) โ
0 โค (3 / 4)) |
70 | 65, 68, 27, 28, 69 | mp4an 427 |
. . . . . . . . . . . . . . . . 17
โข 0 โค (3
/ 4) |
71 | | 3lt4 9091 |
. . . . . . . . . . . . . . . . . 18
โข 3 <
4 |
72 | | nnrp 9663 |
. . . . . . . . . . . . . . . . . . . 20
โข (4 โ
โ โ 4 โ โ+) |
73 | 38, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
โข 4 โ
โ+ |
74 | | divlt1lt 9724 |
. . . . . . . . . . . . . . . . . . 19
โข ((3
โ โ โง 4 โ โ+) โ ((3 / 4) < 1
โ 3 < 4)) |
75 | 65, 73, 74 | mp2an 426 |
. . . . . . . . . . . . . . . . . 18
โข ((3 / 4)
< 1 โ 3 < 4) |
76 | 71, 75 | mpbir 146 |
. . . . . . . . . . . . . . . . 17
โข (3 / 4)
< 1 |
77 | 70, 76 | pm3.2i 272 |
. . . . . . . . . . . . . . . 16
โข (0 โค
(3 / 4) โง (3 / 4) < 1) |
78 | | 3z 9282 |
. . . . . . . . . . . . . . . . . 18
โข 3 โ
โค |
79 | | znq 9624 |
. . . . . . . . . . . . . . . . . 18
โข ((3
โ โค โง 4 โ โ) โ (3 / 4) โ
โ) |
80 | 78, 38, 79 | mp2an 426 |
. . . . . . . . . . . . . . . . 17
โข (3 / 4)
โ โ |
81 | | flqbi2 10291 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ โค โง (3 / 4)
โ โ) โ ((โโ(๐ฅ + (3 / 4))) = ๐ฅ โ (0 โค (3 / 4) โง (3 / 4) <
1))) |
82 | 80, 81 | mpan2 425 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ
((โโ(๐ฅ + (3 /
4))) = ๐ฅ โ (0 โค (3
/ 4) โง (3 / 4) < 1))) |
83 | 77, 82 | mpbiri 168 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โค โ
(โโ(๐ฅ + (3 /
4))) = ๐ฅ) |
84 | 64, 83 | eqtrd 2210 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โค โ
(โโ(๐ฅ + ((1 /
2) + (1 / 4)))) = ๐ฅ) |
85 | 84 | adantr 276 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ (โโ(๐ฅ + ((1 / 2) + (1 / 4)))) = ๐ฅ) |
86 | | oveq1 5882 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ((2 ยท ๐ฅ) + 1) โ (๐ / 2) = (((2 ยท ๐ฅ) + 1) / 2)) |
87 | 86 | eqcoms 2180 |
. . . . . . . . . . . . . . . . 17
โข (((2
ยท ๐ฅ) + 1) = ๐ โ (๐ / 2) = (((2 ยท ๐ฅ) + 1) / 2)) |
88 | | 2z 9281 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 2 โ
โค |
89 | 88 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ โค โ 2 โ
โค) |
90 | | id 19 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ โค โ ๐ฅ โ
โค) |
91 | 89, 90 | zmulcld 9381 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ โค โ (2
ยท ๐ฅ) โ
โค) |
92 | 91 | zcnd 9376 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โค โ (2
ยท ๐ฅ) โ
โ) |
93 | | 1cnd 7973 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โค โ 1 โ
โ) |
94 | | 2cnd 8992 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โค โ 2 โ
โ) |
95 | 15 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โค โ 2 #
0) |
96 | 92, 93, 94, 95 | divdirapd 8786 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โค โ (((2
ยท ๐ฅ) + 1) / 2) =
(((2 ยท ๐ฅ) / 2) + (1
/ 2))) |
97 | | zcn 9258 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
98 | 97, 94, 95 | divcanap3d 8752 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โค โ ((2
ยท ๐ฅ) / 2) = ๐ฅ) |
99 | 98 | oveq1d 5890 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โค โ (((2
ยท ๐ฅ) / 2) + (1 / 2))
= (๐ฅ + (1 /
2))) |
100 | 96, 99 | eqtrd 2210 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ (((2
ยท ๐ฅ) + 1) / 2) =
(๐ฅ + (1 /
2))) |
101 | 87, 100 | sylan9eqr 2232 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ (๐ / 2) = (๐ฅ + (1 / 2))) |
102 | 101 | oveq1d 5890 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ ((๐ / 2) + (1 / 4)) = ((๐ฅ + (1 / 2)) + (1 / 4))) |
103 | | halfcn 9133 |
. . . . . . . . . . . . . . . . . 18
โข (1 / 2)
โ โ |
104 | 103 | a1i 9 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ (1 / 2)
โ โ) |
105 | 6, 8 | recclapi 8699 |
. . . . . . . . . . . . . . . . . 18
โข (1 / 4)
โ โ |
106 | 105 | a1i 9 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ (1 / 4)
โ โ) |
107 | 97, 104, 106 | addassd 7980 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ ((๐ฅ + (1 / 2)) + (1 / 4)) = (๐ฅ + ((1 / 2) + (1 /
4)))) |
108 | 107 | adantr 276 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ ((๐ฅ + (1 / 2)) + (1 / 4)) = (๐ฅ + ((1 / 2) + (1 / 4)))) |
109 | 102, 108 | eqtrd 2210 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ ((๐ / 2) + (1 / 4)) = (๐ฅ + ((1 / 2) + (1 / 4)))) |
110 | 109 | fveq2d 5520 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ (โโ((๐ / 2) + (1 / 4))) =
(โโ(๐ฅ + ((1 /
2) + (1 / 4))))) |
111 | | oveq1 5882 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ((2 ยท ๐ฅ) + 1) โ (๐ โ 1) = (((2 ยท ๐ฅ) + 1) โ
1)) |
112 | 111 | eqcoms 2180 |
. . . . . . . . . . . . . . . 16
โข (((2
ยท ๐ฅ) + 1) = ๐ โ (๐ โ 1) = (((2 ยท ๐ฅ) + 1) โ
1)) |
113 | | pncan1 8334 |
. . . . . . . . . . . . . . . . 17
โข ((2
ยท ๐ฅ) โ โ
โ (((2 ยท ๐ฅ) +
1) โ 1) = (2 ยท ๐ฅ)) |
114 | 92, 113 | syl 14 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ (((2
ยท ๐ฅ) + 1) โ 1)
= (2 ยท ๐ฅ)) |
115 | 112, 114 | sylan9eqr 2232 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ (๐ โ 1) = (2 ยท ๐ฅ)) |
116 | 115 | oveq1d 5890 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ ((๐ โ 1) / 2) = ((2 ยท ๐ฅ) / 2)) |
117 | 98 | adantr 276 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ ((2 ยท ๐ฅ) / 2) = ๐ฅ) |
118 | 116, 117 | eqtrd 2210 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ ((๐ โ 1) / 2) = ๐ฅ) |
119 | 85, 110, 118 | 3eqtr4rd 2221 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ ((๐ โ 1) / 2) = (โโ((๐ / 2) + (1 /
4)))) |
120 | 119 | ex 115 |
. . . . . . . . . . 11
โข (๐ฅ โ โค โ (((2
ยท ๐ฅ) + 1) = ๐ โ ((๐ โ 1) / 2) = (โโ((๐ / 2) + (1 /
4))))) |
121 | 120 | adantl 277 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ฅ โ โค) โ (((2
ยท ๐ฅ) + 1) = ๐ โ ((๐ โ 1) / 2) = (โโ((๐ / 2) + (1 /
4))))) |
122 | 121 | rexlimdva 2594 |
. . . . . . . . 9
โข (๐ โ โค โ
(โ๐ฅ โ โค
((2 ยท ๐ฅ) + 1) =
๐ โ ((๐ โ 1) / 2) =
(โโ((๐ / 2) +
(1 / 4))))) |
123 | 48, 122 | sylbid 150 |
. . . . . . . 8
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ ((๐ โ 1) / 2) =
(โโ((๐ / 2) +
(1 / 4))))) |
124 | 123 | impcom 125 |
. . . . . . 7
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โค) โ ((๐ โ 1) / 2) =
(โโ((๐ / 2) +
(1 / 4)))) |
125 | 47, 124 | eqtrd 2210 |
. . . . . 6
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โค) โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = (โโ((๐ / 2) + (1 /
4)))) |
126 | 125 | expcom 116 |
. . . . 5
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = (โโ((๐ / 2) + (1 /
4))))) |
127 | | zeo3 11873 |
. . . . 5
โข (๐ โ โค โ (2
โฅ ๐ โจ ยฌ 2
โฅ ๐)) |
128 | 45, 126, 127 | mpjaod 718 |
. . . 4
โข (๐ โ โค โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = (โโ((๐ / 2) + (1 /
4)))) |
129 | 128 | eqcomd 2183 |
. . 3
โข (๐ โ โค โ
(โโ((๐ / 2) +
(1 / 4))) = if(2 โฅ ๐,
(๐ / 2), ((๐ โ 1) /
2))) |
130 | 129 | adantr 276 |
. 2
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ
(โโ((๐ / 2) +
(1 / 4))) = if(2 โฅ ๐,
(๐ / 2), ((๐ โ 1) /
2))) |
131 | 22, 130 | eqtrd 2210 |
1
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ
(โโ(๐ / 4)) =
if(2 โฅ ๐, (๐ / 2), ((๐ โ 1) / 2))) |