Step | Hyp | Ref
| Expression |
1 | | zeo 12520 |
. 2
โข (๐ โ โค โ ((๐ / 2) โ โค โจ
((๐ + 1) / 2) โ
โค)) |
2 | | peano2z 12475 |
. . . . . 6
โข (๐ โ โค โ (๐ + 1) โ
โค) |
3 | | zmulcl 12483 |
. . . . . 6
โข (((๐ / 2) โ โค โง
(๐ + 1) โ โค)
โ ((๐ / 2) ยท
(๐ + 1)) โ
โค) |
4 | 2, 3 | sylan2 594 |
. . . . 5
โข (((๐ / 2) โ โค โง ๐ โ โค) โ ((๐ / 2) ยท (๐ + 1)) โ
โค) |
5 | | zcn 12438 |
. . . . . . . 8
โข (๐ โ โค โ ๐ โ
โ) |
6 | 2 | zcnd 12541 |
. . . . . . . 8
โข (๐ โ โค โ (๐ + 1) โ
โ) |
7 | | 2cnne0 12297 |
. . . . . . . . 9
โข (2 โ
โ โง 2 โ 0) |
8 | 7 | a1i 11 |
. . . . . . . 8
โข (๐ โ โค โ (2 โ
โ โง 2 โ 0)) |
9 | | div23 11766 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ + 1) โ โ โง (2
โ โ โง 2 โ 0)) โ ((๐ ยท (๐ + 1)) / 2) = ((๐ / 2) ยท (๐ + 1))) |
10 | 5, 6, 8, 9 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ โค โ ((๐ ยท (๐ + 1)) / 2) = ((๐ / 2) ยท (๐ + 1))) |
11 | 10 | eleq1d 2823 |
. . . . . 6
โข (๐ โ โค โ (((๐ ยท (๐ + 1)) / 2) โ โค โ ((๐ / 2) ยท (๐ + 1)) โ
โค)) |
12 | 11 | adantl 483 |
. . . . 5
โข (((๐ / 2) โ โค โง ๐ โ โค) โ (((๐ ยท (๐ + 1)) / 2) โ โค โ ((๐ / 2) ยท (๐ + 1)) โ
โค)) |
13 | 4, 12 | mpbird 257 |
. . . 4
โข (((๐ / 2) โ โค โง ๐ โ โค) โ ((๐ ยท (๐ + 1)) / 2) โ โค) |
14 | 13 | ex 414 |
. . 3
โข ((๐ / 2) โ โค โ
(๐ โ โค โ
((๐ ยท (๐ + 1)) / 2) โ
โค)) |
15 | | zmulcl 12483 |
. . . . . 6
โข ((๐ โ โค โง ((๐ + 1) / 2) โ โค)
โ (๐ ยท ((๐ + 1) / 2)) โ
โค) |
16 | 15 | ancoms 460 |
. . . . 5
โข ((((๐ + 1) / 2) โ โค โง
๐ โ โค) โ
(๐ ยท ((๐ + 1) / 2)) โ
โค) |
17 | | divass 11765 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ + 1) โ โ โง (2
โ โ โง 2 โ 0)) โ ((๐ ยท (๐ + 1)) / 2) = (๐ ยท ((๐ + 1) / 2))) |
18 | 5, 6, 8, 17 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ โค โ ((๐ ยท (๐ + 1)) / 2) = (๐ ยท ((๐ + 1) / 2))) |
19 | 18 | eleq1d 2823 |
. . . . . 6
โข (๐ โ โค โ (((๐ ยท (๐ + 1)) / 2) โ โค โ (๐ ยท ((๐ + 1) / 2)) โ
โค)) |
20 | 19 | adantl 483 |
. . . . 5
โข ((((๐ + 1) / 2) โ โค โง
๐ โ โค) โ
(((๐ ยท (๐ + 1)) / 2) โ โค
โ (๐ ยท ((๐ + 1) / 2)) โ
โค)) |
21 | 16, 20 | mpbird 257 |
. . . 4
โข ((((๐ + 1) / 2) โ โค โง
๐ โ โค) โ
((๐ ยท (๐ + 1)) / 2) โ
โค) |
22 | 21 | ex 414 |
. . 3
โข (((๐ + 1) / 2) โ โค โ
(๐ โ โค โ
((๐ ยท (๐ + 1)) / 2) โ
โค)) |
23 | 14, 22 | jaoi 856 |
. 2
โข (((๐ / 2) โ โค โจ
((๐ + 1) / 2) โ
โค) โ (๐ โ
โค โ ((๐ ยท
(๐ + 1)) / 2) โ
โค)) |
24 | 1, 23 | mpcom 38 |
1
โข (๐ โ โค โ ((๐ ยท (๐ + 1)) / 2) โ โค) |