Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . 4
โข (๐ = ((2 ยท ๐) + 1) โ (๐ / 4) = (((2 ยท ๐) + 1) / 4)) |
2 | | 2cnd 12232 |
. . . . . . 7
โข (๐ โ โค โ 2 โ
โ) |
3 | | zcn 12505 |
. . . . . . 7
โข (๐ โ โค โ ๐ โ
โ) |
4 | 2, 3 | mulcld 11176 |
. . . . . 6
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
5 | | 1cnd 11151 |
. . . . . 6
โข (๐ โ โค โ 1 โ
โ) |
6 | | 4cn 12239 |
. . . . . . . 8
โข 4 โ
โ |
7 | | 4ne0 12262 |
. . . . . . . 8
โข 4 โ
0 |
8 | 6, 7 | pm3.2i 472 |
. . . . . . 7
โข (4 โ
โ โง 4 โ 0) |
9 | 8 | a1i 11 |
. . . . . 6
โข (๐ โ โค โ (4 โ
โ โง 4 โ 0)) |
10 | | divdir 11839 |
. . . . . 6
โข (((2
ยท ๐) โ โ
โง 1 โ โ โง (4 โ โ โง 4 โ 0)) โ (((2
ยท ๐) + 1) / 4) =
(((2 ยท ๐) / 4) + (1
/ 4))) |
11 | 4, 5, 9, 10 | syl3anc 1372 |
. . . . 5
โข (๐ โ โค โ (((2
ยท ๐) + 1) / 4) =
(((2 ยท ๐) / 4) + (1
/ 4))) |
12 | | 2t2e4 12318 |
. . . . . . . . . 10
โข (2
ยท 2) = 4 |
13 | 12 | eqcomi 2746 |
. . . . . . . . 9
โข 4 = (2
ยท 2) |
14 | 13 | a1i 11 |
. . . . . . . 8
โข (๐ โ โค โ 4 = (2
ยท 2)) |
15 | 14 | oveq2d 7374 |
. . . . . . 7
โข (๐ โ โค โ ((2
ยท ๐) / 4) = ((2
ยท ๐) / (2 ยท
2))) |
16 | | 2ne0 12258 |
. . . . . . . . 9
โข 2 โ
0 |
17 | 16 | a1i 11 |
. . . . . . . 8
โข (๐ โ โค โ 2 โ
0) |
18 | 3, 2, 2, 17, 17 | divcan5d 11958 |
. . . . . . 7
โข (๐ โ โค โ ((2
ยท ๐) / (2 ยท
2)) = (๐ /
2)) |
19 | 15, 18 | eqtrd 2777 |
. . . . . 6
โข (๐ โ โค โ ((2
ยท ๐) / 4) = (๐ / 2)) |
20 | 19 | oveq1d 7373 |
. . . . 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 6847 |
. 2
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ
(โโ(๐ / 4)) =
(โโ((๐ / 2) +
(1 / 4)))) |
24 | | iftrue 4493 |
. . . . . . 7
โข (2
โฅ ๐ โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = (๐ / 2)) |
25 | 24 | adantr 482 |
. . . . . 6
โข ((2
โฅ ๐ โง ๐ โ โค) โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = (๐ / 2)) |
26 | | 1re 11156 |
. . . . . . . . 9
โข 1 โ
โ |
27 | | 0le1 11679 |
. . . . . . . . 9
โข 0 โค
1 |
28 | | 4re 12238 |
. . . . . . . . 9
โข 4 โ
โ |
29 | | 4pos 12261 |
. . . . . . . . 9
โข 0 <
4 |
30 | | divge0 12025 |
. . . . . . . . 9
โข (((1
โ โ โง 0 โค 1) โง (4 โ โ โง 0 < 4)) โ
0 โค (1 / 4)) |
31 | 26, 27, 28, 29, 30 | mp4an 692 |
. . . . . . . 8
โข 0 โค (1
/ 4) |
32 | | 1lt4 12330 |
. . . . . . . . 9
โข 1 <
4 |
33 | | recgt1 12052 |
. . . . . . . . . 10
โข ((4
โ โ โง 0 < 4) โ (1 < 4 โ (1 / 4) <
1)) |
34 | 28, 29, 33 | mp2an 691 |
. . . . . . . . 9
โข (1 < 4
โ (1 / 4) < 1) |
35 | 32, 34 | mpbi 229 |
. . . . . . . 8
โข (1 / 4)
< 1 |
36 | 31, 35 | pm3.2i 472 |
. . . . . . 7
โข (0 โค
(1 / 4) โง (1 / 4) < 1) |
37 | | evend2 16240 |
. . . . . . . . 9
โข (๐ โ โค โ (2
โฅ ๐ โ (๐ / 2) โ
โค)) |
38 | 37 | biimpac 480 |
. . . . . . . 8
โข ((2
โฅ ๐ โง ๐ โ โค) โ (๐ / 2) โ
โค) |
39 | | 4nn 12237 |
. . . . . . . . 9
โข 4 โ
โ |
40 | | nnrecre 12196 |
. . . . . . . . 9
โข (4 โ
โ โ (1 / 4) โ โ) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . 8
โข (1 / 4)
โ โ |
42 | | flbi2 13723 |
. . . . . . . 8
โข (((๐ / 2) โ โค โง (1 /
4) โ โ) โ ((โโ((๐ / 2) + (1 / 4))) = (๐ / 2) โ (0 โค (1 / 4) โง (1 / 4)
< 1))) |
43 | 38, 41, 42 | sylancl 587 |
. . . . . . 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 4496 |
. . . . . . 7
โข (ยฌ 2
โฅ ๐ โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = ((๐ โ 1) / 2)) |
47 | 46 | adantr 482 |
. . . . . 6
โข ((ยฌ 2
โฅ ๐ โง ๐ โ โค) โ if(2
โฅ ๐, (๐ / 2), ((๐ โ 1) / 2)) = ((๐ โ 1) / 2)) |
48 | | odd2np1 16224 |
. . . . . . . 8
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ฅ โ โค ((2
ยท ๐ฅ) + 1) = ๐)) |
49 | | ax-1cn 11110 |
. . . . . . . . . . . . . . . . . . . . 21
โข 1 โ
โ |
50 | | 2cnne0 12364 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2 โ
โ โง 2 โ 0) |
51 | | divcan5 11858 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((1
โ โ โง (2 โ โ โง 2 โ 0) โง (2 โ โ
โง 2 โ 0)) โ ((2 ยท 1) / (2 ยท 2)) = (1 /
2)) |
52 | 49, 50, 50, 51 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . . 20
โข ((2
ยท 1) / (2 ยท 2)) = (1 / 2) |
53 | | 2t1e2 12317 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2
ยท 1) = 2 |
54 | 53, 12 | oveq12i 7370 |
. . . . . . . . . . . . . . . . . . . 20
โข ((2
ยท 1) / (2 ยท 2)) = (2 / 4) |
55 | 52, 54 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . . 19
โข (1 / 2) =
(2 / 4) |
56 | 55 | oveq1i 7368 |
. . . . . . . . . . . . . . . . . 18
โข ((1 / 2)
+ (1 / 4)) = ((2 / 4) + (1 / 4)) |
57 | | 2cn 12229 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ |
58 | 57, 49, 6, 7 | divdiri 11913 |
. . . . . . . . . . . . . . . . . 18
โข ((2 + 1)
/ 4) = ((2 / 4) + (1 / 4)) |
59 | | 2p1e3 12296 |
. . . . . . . . . . . . . . . . . . 19
โข (2 + 1) =
3 |
60 | 59 | oveq1i 7368 |
. . . . . . . . . . . . . . . . . 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 7374 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โค โ (๐ฅ + ((1 / 2) + (1 / 4))) = (๐ฅ + (3 / 4))) |
64 | 63 | fveq2d 6847 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โค โ
(โโ(๐ฅ + ((1 /
2) + (1 / 4)))) = (โโ(๐ฅ + (3 / 4)))) |
65 | | 3re 12234 |
. . . . . . . . . . . . . . . . 17
โข 3 โ
โ |
66 | | 0re 11158 |
. . . . . . . . . . . . . . . . . 18
โข 0 โ
โ |
67 | | 3pos 12259 |
. . . . . . . . . . . . . . . . . 18
โข 0 <
3 |
68 | 66, 65, 67 | ltleii 11279 |
. . . . . . . . . . . . . . . . 17
โข 0 โค
3 |
69 | | divge0 12025 |
. . . . . . . . . . . . . . . . 17
โข (((3
โ โ โง 0 โค 3) โง (4 โ โ โง 0 < 4)) โ
0 โค (3 / 4)) |
70 | 65, 68, 28, 29, 69 | mp4an 692 |
. . . . . . . . . . . . . . . 16
โข 0 โค (3
/ 4) |
71 | | 3lt4 12328 |
. . . . . . . . . . . . . . . . 17
โข 3 <
4 |
72 | | nnrp 12927 |
. . . . . . . . . . . . . . . . . . 19
โข (4 โ
โ โ 4 โ โ+) |
73 | 39, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
โข 4 โ
โ+ |
74 | | divlt1lt 12985 |
. . . . . . . . . . . . . . . . . 18
โข ((3
โ โ โง 4 โ โ+) โ ((3 / 4) < 1
โ 3 < 4)) |
75 | 65, 73, 74 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
โข ((3 / 4)
< 1 โ 3 < 4) |
76 | 71, 75 | mpbir 230 |
. . . . . . . . . . . . . . . 16
โข (3 / 4)
< 1 |
77 | 70, 76 | pm3.2i 472 |
. . . . . . . . . . . . . . 15
โข (0 โค
(3 / 4) โง (3 / 4) < 1) |
78 | 65, 28, 7 | redivcli 11923 |
. . . . . . . . . . . . . . . 16
โข (3 / 4)
โ โ |
79 | | flbi2 13723 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โค โง (3 / 4)
โ โ) โ ((โโ(๐ฅ + (3 / 4))) = ๐ฅ โ (0 โค (3 / 4) โง (3 / 4) <
1))) |
80 | 78, 79 | mpan2 690 |
. . . . . . . . . . . . . . 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 482 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ (โโ(๐ฅ + ((1 / 2) + (1 / 4)))) = ๐ฅ) |
84 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ((2 ยท ๐ฅ) + 1) โ (๐ / 2) = (((2 ยท ๐ฅ) + 1) / 2)) |
85 | 84 | eqcoms 2745 |
. . . . . . . . . . . . . . . 16
โข (((2
ยท ๐ฅ) + 1) = ๐ โ (๐ / 2) = (((2 ยท ๐ฅ) + 1) / 2)) |
86 | | 2z 12536 |
. . . . . . . . . . . . . . . . . . . . 21
โข 2 โ
โค |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ โค โ 2 โ
โค) |
88 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ โค โ ๐ฅ โ
โค) |
89 | 87, 88 | zmulcld 12614 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โค โ (2
ยท ๐ฅ) โ
โค) |
90 | 89 | zcnd 12609 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โค โ (2
ยท ๐ฅ) โ
โ) |
91 | | 1cnd 11151 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โค โ 1 โ
โ) |
92 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โค โ (2 โ
โ โง 2 โ 0)) |
93 | | divdir 11839 |
. . . . . . . . . . . . . . . . . 18
โข (((2
ยท ๐ฅ) โ โ
โง 1 โ โ โง (2 โ โ โง 2 โ 0)) โ (((2
ยท ๐ฅ) + 1) / 2) =
(((2 ยท ๐ฅ) / 2) + (1
/ 2))) |
94 | 90, 91, 92, 93 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ (((2
ยท ๐ฅ) + 1) / 2) =
(((2 ยท ๐ฅ) / 2) + (1
/ 2))) |
95 | | zcn 12505 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
96 | | 2cnd 12232 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โค โ 2 โ
โ) |
97 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โค โ 2 โ
0) |
98 | 95, 96, 97 | divcan3d 11937 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โค โ ((2
ยท ๐ฅ) / 2) = ๐ฅ) |
99 | 98 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 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 7373 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ ((๐ / 2) + (1 / 4)) = ((๐ฅ + (1 / 2)) + (1 / 4))) |
103 | | halfcn 12369 |
. . . . . . . . . . . . . . . . 17
โข (1 / 2)
โ โ |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ (1 / 2)
โ โ) |
105 | 6, 7 | reccli 11886 |
. . . . . . . . . . . . . . . . 17
โข (1 / 4)
โ โ |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ (1 / 4)
โ โ) |
107 | 95, 104, 106 | addassd 11178 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โค โ ((๐ฅ + (1 / 2)) + (1 / 4)) = (๐ฅ + ((1 / 2) + (1 /
4)))) |
108 | 107 | adantr 482 |
. . . . . . . . . . . . . 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 6847 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ (โโ((๐ / 2) + (1 / 4))) =
(โโ(๐ฅ + ((1 /
2) + (1 / 4))))) |
111 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
โข (๐ = ((2 ยท ๐ฅ) + 1) โ (๐ โ 1) = (((2 ยท ๐ฅ) + 1) โ
1)) |
112 | 111 | eqcoms 2745 |
. . . . . . . . . . . . . . 15
โข (((2
ยท ๐ฅ) + 1) = ๐ โ (๐ โ 1) = (((2 ยท ๐ฅ) + 1) โ
1)) |
113 | | pncan1 11580 |
. . . . . . . . . . . . . . . 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 7373 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โค โง ((2
ยท ๐ฅ) + 1) = ๐) โ ((๐ โ 1) / 2) = ((2 ยท ๐ฅ) / 2)) |
117 | 98 | adantr 482 |
. . . . . . . . . . . . 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 414 |
. . . . . . . . . 10
โข (๐ฅ โ โค โ (((2
ยท ๐ฅ) + 1) = ๐ โ ((๐ โ 1) / 2) = (โโ((๐ / 2) + (1 /
4))))) |
121 | 120 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ฅ โ โค) โ (((2
ยท ๐ฅ) + 1) = ๐ โ ((๐ โ 1) / 2) = (โโ((๐ / 2) + (1 /
4))))) |
122 | 121 | rexlimdva 3153 |
. . . . . . . 8
โข (๐ โ โค โ
(โ๐ฅ โ โค
((2 ยท ๐ฅ) + 1) =
๐ โ ((๐ โ 1) / 2) =
(โโ((๐ / 2) +
(1 / 4))))) |
123 | 48, 122 | sylbid 239 |
. . . . . . 7
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ ((๐ โ 1) / 2) =
(โโ((๐ / 2) +
(1 / 4))))) |
124 | 123 | impcom 409 |
. . . . . 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 811 |
. . . 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 482 |
. 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))) |