Step | Hyp | Ref
| Expression |
1 | | halfnz 12512 |
. . 3
โข ยฌ (1
/ 2) โ โค |
2 | | 2cn 12162 |
. . . . . . 7
โข 2 โ
โ |
3 | | zcn 12438 |
. . . . . . . 8
โข (๐ด โ โค โ ๐ด โ
โ) |
4 | 3 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ด โ
โ) |
5 | | mulcl 11069 |
. . . . . . 7
โข ((2
โ โ โง ๐ด
โ โ) โ (2 ยท ๐ด) โ โ) |
6 | 2, 4, 5 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค) โ (2
ยท ๐ด) โ
โ) |
7 | | zcn 12438 |
. . . . . . . 8
โข (๐ต โ โค โ ๐ต โ
โ) |
8 | 7 | adantl 483 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ต โ
โ) |
9 | | mulcl 11069 |
. . . . . . 7
โข ((2
โ โ โง ๐ต
โ โ) โ (2 ยท ๐ต) โ โ) |
10 | 2, 8, 9 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค) โ (2
ยท ๐ต) โ
โ) |
11 | | 1cnd 11084 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค) โ 1 โ
โ) |
12 | 6, 10, 11 | subaddd 11464 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค) โ (((2
ยท ๐ด) โ (2
ยท ๐ต)) = 1 โ ((2
ยท ๐ต) + 1) = (2
ยท ๐ด))) |
13 | 2 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ต โ โค) โ 2 โ
โ) |
14 | 13, 4, 8 | subdid 11545 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ต โ โค) โ (2
ยท (๐ด โ ๐ต)) = ((2 ยท ๐ด) โ (2 ยท ๐ต))) |
15 | 14 | oveq1d 7365 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ต โ โค) โ ((2
ยท (๐ด โ ๐ต)) / 2) = (((2 ยท ๐ด) โ (2 ยท ๐ต)) / 2)) |
16 | | zsubcl 12476 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด โ ๐ต) โ โค) |
17 | | zcn 12438 |
. . . . . . . . . 10
โข ((๐ด โ ๐ต) โ โค โ (๐ด โ ๐ต) โ โ) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด โ ๐ต) โ โ) |
19 | | 2ne0 12191 |
. . . . . . . . . 10
โข 2 โ
0 |
20 | 19 | a1i 11 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ต โ โค) โ 2 โ
0) |
21 | 18, 13, 20 | divcan3d 11870 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ต โ โค) โ ((2
ยท (๐ด โ ๐ต)) / 2) = (๐ด โ ๐ต)) |
22 | 15, 21 | eqtr3d 2780 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค) โ (((2
ยท ๐ด) โ (2
ยท ๐ต)) / 2) = (๐ด โ ๐ต)) |
23 | 22, 16 | eqeltrd 2839 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค) โ (((2
ยท ๐ด) โ (2
ยท ๐ต)) / 2) โ
โค) |
24 | | oveq1 7357 |
. . . . . . 7
โข (((2
ยท ๐ด) โ (2
ยท ๐ต)) = 1 โ
(((2 ยท ๐ด) โ (2
ยท ๐ต)) / 2) = (1 /
2)) |
25 | 24 | eleq1d 2823 |
. . . . . 6
โข (((2
ยท ๐ด) โ (2
ยท ๐ต)) = 1 โ
((((2 ยท ๐ด) โ
(2 ยท ๐ต)) / 2) โ
โค โ (1 / 2) โ โค)) |
26 | 23, 25 | syl5ibcom 245 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค) โ (((2
ยท ๐ด) โ (2
ยท ๐ต)) = 1 โ (1
/ 2) โ โค)) |
27 | 12, 26 | sylbird 260 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค) โ (((2
ยท ๐ต) + 1) = (2
ยท ๐ด) โ (1 / 2)
โ โค)) |
28 | 27 | necon3bd 2956 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค) โ (ยฌ
(1 / 2) โ โค โ ((2 ยท ๐ต) + 1) โ (2 ยท ๐ด))) |
29 | 1, 28 | mpi 20 |
. 2
โข ((๐ด โ โค โง ๐ต โ โค) โ ((2
ยท ๐ต) + 1) โ (2
ยท ๐ด)) |
30 | 29 | necomd 2998 |
1
โข ((๐ด โ โค โง ๐ต โ โค) โ (2
ยท ๐ด) โ ((2
ยท ๐ต) +
1)) |