Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.r |
. . . . 5
โข ๐
= (๐ฅ โ (1...๐ป) โฆ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2)))) |
2 | 1 | elrnmpt 5908 |
. . . 4
โข (๐ฆ โ V โ (๐ฆ โ ran ๐
โ โ๐ฅ โ (1...๐ป)๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))))) |
3 | 2 | elv 3450 |
. . 3
โข (๐ฆ โ ran ๐
โ โ๐ฅ โ (1...๐ป)๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2)))) |
4 | | iftrue 4491 |
. . . . . . . . 9
โข ((๐ฅ ยท 2) < (๐ / 2) โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = (๐ฅ ยท 2)) |
5 | 4 | eqeq2d 2749 |
. . . . . . . 8
โข ((๐ฅ ยท 2) < (๐ / 2) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ = (๐ฅ ยท 2))) |
6 | 5 | adantr 482 |
. . . . . . 7
โข (((๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ = (๐ฅ ยท 2))) |
7 | | elfz1b 13439 |
. . . . . . . . . . . 12
โข (๐ฅ โ (1...๐ป) โ (๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป)) |
8 | | id 22 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
9 | | 2nn 12160 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โ |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โ โ 2 โ
โ) |
11 | 8, 10 | nnmulcld 12140 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โ โ (๐ฅ ยท 2) โ
โ) |
12 | 11 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โ (๐ฅ ยท 2) โ โ) |
13 | 12 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โง ๐ โง (๐ฅ ยท 2) < (๐ / 2)) โ (๐ฅ ยท 2) โ โ) |
14 | | gausslemma2d.h |
. . . . . . . . . . . . . . . . . 18
โข ๐ป = ((๐ โ 1) / 2) |
15 | 14 | eleq1i 2829 |
. . . . . . . . . . . . . . . . 17
โข (๐ป โ โ โ ((๐ โ 1) / 2) โ
โ) |
16 | 15 | biimpi 215 |
. . . . . . . . . . . . . . . 16
โข (๐ป โ โ โ ((๐ โ 1) / 2) โ
โ) |
17 | 16 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โ ((๐ โ 1) / 2) โ
โ) |
18 | 17 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โง ๐ โง (๐ฅ ยท 2) < (๐ / 2)) โ ((๐ โ 1) / 2) โ
โ) |
19 | | gausslemma2d.p |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ โ (โ โ
{2})) |
20 | | nnoddn2prm 16618 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง ยฌ 2 โฅ ๐)) |
21 | | nnz 12456 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โค) |
22 | 21 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (๐ โ โค โง ยฌ 2
โฅ ๐)) |
23 | 20, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (โ โ {2})
โ (๐ โ โค
โง ยฌ 2 โฅ ๐)) |
24 | | nnz 12456 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ โ โ โ ๐ฅ โ
โค) |
25 | | 2z 12466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 2 โ
โค |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ โ โ โ 2 โ
โค) |
27 | 24, 26 | zmulcld 12546 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ โ โ (๐ฅ ยท 2) โ
โค) |
28 | 27 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โ (๐ฅ ยท 2) โ โค) |
29 | 23, 28 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (โ โ {2})
โง (๐ฅ โ โ
โง ๐ป โ โ
โง ๐ฅ โค ๐ป)) โ ((๐ โ โค โง ยฌ 2 โฅ ๐) โง (๐ฅ ยท 2) โ
โค)) |
30 | | df-3an 1090 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง (๐ฅ ยท 2) โ โค)
โ ((๐ โ โค
โง ยฌ 2 โฅ ๐)
โง (๐ฅ ยท 2) โ
โค)) |
31 | 29, 30 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง (๐ฅ โ โ
โง ๐ป โ โ
โง ๐ฅ โค ๐ป)) โ (๐ โ โค โง ยฌ 2 โฅ ๐ โง (๐ฅ ยท 2) โ
โค)) |
32 | 31 | ex 414 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โ โ {2})
โ ((๐ฅ โ โ
โง ๐ป โ โ
โง ๐ฅ โค ๐ป) โ (๐ โ โค โง ยฌ 2 โฅ ๐ โง (๐ฅ ยท 2) โ
โค))) |
33 | 19, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โ (๐ โ โค โง ยฌ 2 โฅ ๐ โง (๐ฅ ยท 2) โ
โค))) |
34 | 33 | impcom 409 |
. . . . . . . . . . . . . . . 16
โข (((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โง ๐) โ (๐ โ โค โง ยฌ 2 โฅ ๐ โง (๐ฅ ยท 2) โ
โค)) |
35 | | ltoddhalfle 16178 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง (๐ฅ ยท 2) โ โค)
โ ((๐ฅ ยท 2) <
(๐ / 2) โ (๐ฅ ยท 2) โค ((๐ โ 1) /
2))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โง ๐) โ ((๐ฅ ยท 2) < (๐ / 2) โ (๐ฅ ยท 2) โค ((๐ โ 1) / 2))) |
37 | 36 | biimp3a 1470 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โง ๐ โง (๐ฅ ยท 2) < (๐ / 2)) โ (๐ฅ ยท 2) โค ((๐ โ 1) / 2)) |
38 | 13, 18, 37 | 3jca 1129 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โง ๐ โง (๐ฅ ยท 2) < (๐ / 2)) โ ((๐ฅ ยท 2) โ โ โง ((๐ โ 1) / 2) โ โ
โง (๐ฅ ยท 2) โค
((๐ โ 1) /
2))) |
39 | 38 | 3exp 1120 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โ (๐ โ ((๐ฅ ยท 2) < (๐ / 2) โ ((๐ฅ ยท 2) โ โ โง ((๐ โ 1) / 2) โ โ
โง (๐ฅ ยท 2) โค
((๐ โ 1) /
2))))) |
40 | 7, 39 | sylbi 216 |
. . . . . . . . . . 11
โข (๐ฅ โ (1...๐ป) โ (๐ โ ((๐ฅ ยท 2) < (๐ / 2) โ ((๐ฅ ยท 2) โ โ โง ((๐ โ 1) / 2) โ โ
โง (๐ฅ ยท 2) โค
((๐ โ 1) /
2))))) |
41 | 40 | impcom 409 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...๐ป)) โ ((๐ฅ ยท 2) < (๐ / 2) โ ((๐ฅ ยท 2) โ โ โง ((๐ โ 1) / 2) โ โ
โง (๐ฅ ยท 2) โค
((๐ โ 1) /
2)))) |
42 | 41 | impcom 409 |
. . . . . . . . 9
โข (((๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ ((๐ฅ ยท 2) โ โ โง ((๐ โ 1) / 2) โ โ
โง (๐ฅ ยท 2) โค
((๐ โ 1) /
2))) |
43 | 14 | oveq2i 7361 |
. . . . . . . . . . 11
โข
(1...๐ป) =
(1...((๐ โ 1) /
2)) |
44 | 43 | eleq2i 2830 |
. . . . . . . . . 10
โข ((๐ฅ ยท 2) โ (1...๐ป) โ (๐ฅ ยท 2) โ (1...((๐ โ 1) / 2))) |
45 | | elfz1b 13439 |
. . . . . . . . . 10
โข ((๐ฅ ยท 2) โ (1...((๐ โ 1) / 2)) โ ((๐ฅ ยท 2) โ โ
โง ((๐ โ 1) / 2)
โ โ โง (๐ฅ
ยท 2) โค ((๐
โ 1) / 2))) |
46 | 44, 45 | bitri 275 |
. . . . . . . . 9
โข ((๐ฅ ยท 2) โ (1...๐ป) โ ((๐ฅ ยท 2) โ โ โง ((๐ โ 1) / 2) โ โ
โง (๐ฅ ยท 2) โค
((๐ โ 1) /
2))) |
47 | 42, 46 | sylibr 233 |
. . . . . . . 8
โข (((๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ฅ ยท 2) โ (1...๐ป)) |
48 | | eleq1 2826 |
. . . . . . . 8
โข (๐ฆ = (๐ฅ ยท 2) โ (๐ฆ โ (1...๐ป) โ (๐ฅ ยท 2) โ (1...๐ป))) |
49 | 47, 48 | syl5ibrcom 247 |
. . . . . . 7
โข (((๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ฆ = (๐ฅ ยท 2) โ ๐ฆ โ (1...๐ป))) |
50 | 6, 49 | sylbid 239 |
. . . . . 6
โข (((๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ โ (1...๐ป))) |
51 | | iffalse 4494 |
. . . . . . . . 9
โข (ยฌ
(๐ฅ ยท 2) < (๐ / 2) โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = (๐ โ (๐ฅ ยท 2))) |
52 | 51 | eqeq2d 2749 |
. . . . . . . 8
โข (ยฌ
(๐ฅ ยท 2) < (๐ / 2) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ = (๐ โ (๐ฅ ยท 2)))) |
53 | 52 | adantr 482 |
. . . . . . 7
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ = (๐ โ (๐ฅ ยท 2)))) |
54 | | eldifi 4085 |
. . . . . . . . . . . . 13
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
55 | | prmz 16486 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โค) |
56 | 19, 54, 55 | 3syl 18 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
57 | 56 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ ๐ โ โค) |
58 | | elfzelz 13370 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (1...๐ป) โ ๐ฅ โ โค) |
59 | 25 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (1...๐ป) โ 2 โ โค) |
60 | 58, 59 | zmulcld 12546 |
. . . . . . . . . . . 12
โข (๐ฅ โ (1...๐ป) โ (๐ฅ ยท 2) โ โค) |
61 | 60 | ad2antll 728 |
. . . . . . . . . . 11
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ฅ ยท 2) โ โค) |
62 | 57, 61 | zsubcld 12545 |
. . . . . . . . . 10
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ โ (๐ฅ ยท 2)) โ
โค) |
63 | 55 | zred 12540 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
64 | 14 | breq2i 5112 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โค ๐ป โ ๐ฅ โค ((๐ โ 1) / 2)) |
65 | | nnre 12094 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
66 | 65 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ โ โง ๐ โ โ) โ ๐ฅ โ
โ) |
67 | | peano2rem 11402 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ โ 1) โ
โ) |
69 | | 2re 12161 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 2 โ
โ |
70 | | 2pos 12190 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 0 <
2 |
71 | 69, 70 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (2 โ
โ โง 0 < 2) |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ โ โง ๐ โ โ) โ (2
โ โ โง 0 < 2)) |
73 | | lemuldiv 11969 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ โ โง (๐ โ 1) โ โ โง
(2 โ โ โง 0 < 2)) โ ((๐ฅ ยท 2) โค (๐ โ 1) โ ๐ฅ โค ((๐ โ 1) / 2))) |
74 | 66, 68, 72, 73 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฅ โ โ โง ๐ โ โ) โ ((๐ฅ ยท 2) โค (๐ โ 1) โ ๐ฅ โค ((๐ โ 1) / 2))) |
75 | 64, 74 | bitr4id 290 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ โค ๐ป โ (๐ฅ ยท 2) โค (๐ โ 1))) |
76 | 11 | nnred 12102 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ โ โ (๐ฅ ยท 2) โ
โ) |
77 | 76 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ ยท 2) โ
โ) |
78 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
79 | 77, 68, 78 | lesub2d 11697 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฅ โ โ โง ๐ โ โ) โ ((๐ฅ ยท 2) โค (๐ โ 1) โ (๐ โ (๐ โ 1)) โค (๐ โ (๐ฅ ยท 2)))) |
80 | | recn 11075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ ๐ โ
โ) |
81 | | 1cnd 11084 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ 1 โ
โ) |
82 | 80, 81 | nncand 11451 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ (๐ โ (๐ โ 1)) = 1) |
83 | 82 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ โ (๐ โ 1)) = 1) |
84 | 83 | breq1d 5114 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ โ โง ๐ โ โ) โ ((๐ โ (๐ โ 1)) โค (๐ โ (๐ฅ ยท 2)) โ 1 โค (๐ โ (๐ฅ ยท 2)))) |
85 | 84 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฅ โ โ โง ๐ โ โ) โ ((๐ โ (๐ โ 1)) โค (๐ โ (๐ฅ ยท 2)) โ 1 โค (๐ โ (๐ฅ ยท 2)))) |
86 | 79, 85 | sylbid 239 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฅ โ โ โง ๐ โ โ) โ ((๐ฅ ยท 2) โค (๐ โ 1) โ 1 โค (๐ โ (๐ฅ ยท 2)))) |
87 | 75, 86 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ โค ๐ป โ 1 โค (๐ โ (๐ฅ ยท 2)))) |
88 | 87 | impancom 453 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ โ โง ๐ฅ โค ๐ป) โ (๐ โ โ โ 1 โค (๐ โ (๐ฅ ยท 2)))) |
89 | 88 | 3adant2 1132 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โ โง ๐ป โ โ โง ๐ฅ โค ๐ป) โ (๐ โ โ โ 1 โค (๐ โ (๐ฅ ยท 2)))) |
90 | 7, 89 | sylbi 216 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ (1...๐ป) โ (๐ โ โ โ 1 โค (๐ โ (๐ฅ ยท 2)))) |
91 | 90 | com12 32 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ฅ โ (1...๐ป) โ 1 โค (๐ โ (๐ฅ ยท 2)))) |
92 | 63, 91 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ฅ โ (1...๐ป) โ 1 โค (๐ โ (๐ฅ ยท 2)))) |
93 | 19, 54, 92 | 3syl 18 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ โ (1...๐ป) โ 1 โค (๐ โ (๐ฅ ยท 2)))) |
94 | 93 | imp 408 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1...๐ป)) โ 1 โค (๐ โ (๐ฅ ยท 2))) |
95 | 94 | adantl 483 |
. . . . . . . . . 10
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ 1 โค (๐ โ (๐ฅ ยท 2))) |
96 | | elnnz1 12460 |
. . . . . . . . . 10
โข ((๐ โ (๐ฅ ยท 2)) โ โ โ ((๐ โ (๐ฅ ยท 2)) โ โค โง 1 โค
(๐ โ (๐ฅ ยท 2)))) |
97 | 62, 95, 96 | sylanbrc 584 |
. . . . . . . . 9
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ โ (๐ฅ ยท 2)) โ
โ) |
98 | 7 | simp2bi 1147 |
. . . . . . . . . 10
โข (๐ฅ โ (1...๐ป) โ ๐ป โ โ) |
99 | 98 | ad2antll 728 |
. . . . . . . . 9
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ ๐ป โ โ) |
100 | | nnre 12094 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โ) |
101 | 100 | rehalfcld 12334 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (๐ / 2) โ
โ) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (๐ / 2) โ
โ) |
103 | 60 | zred 12540 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ (1...๐ป) โ (๐ฅ ยท 2) โ โ) |
104 | | lenlt 11167 |
. . . . . . . . . . . . . . 15
โข (((๐ / 2) โ โ โง
(๐ฅ ยท 2) โ
โ) โ ((๐ / 2)
โค (๐ฅ ยท 2) โ
ยฌ (๐ฅ ยท 2) <
(๐ / 2))) |
105 | 102, 103,
104 | syl2an 597 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ ((๐ / 2) โค (๐ฅ ยท 2) โ ยฌ (๐ฅ ยท 2) < (๐ / 2))) |
106 | 22, 60 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ ((๐ โ โค โง ยฌ 2 โฅ ๐) โง (๐ฅ ยท 2) โ
โค)) |
107 | 106, 30 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ (๐ โ โค โง ยฌ 2 โฅ ๐ โง (๐ฅ ยท 2) โ
โค)) |
108 | | halfleoddlt 16179 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง (๐ฅ ยท 2) โ โค)
โ ((๐ / 2) โค (๐ฅ ยท 2) โ (๐ / 2) < (๐ฅ ยท 2))) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ ((๐ / 2) โค (๐ฅ ยท 2) โ (๐ / 2) < (๐ฅ ยท 2))) |
110 | 109 | biimpa 478 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โง (๐ / 2) โค (๐ฅ ยท 2)) โ (๐ / 2) < (๐ฅ ยท 2)) |
111 | | nncn 12095 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ๐ โ
โ) |
112 | | subhalfhalf 12321 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (๐ โ (๐ / 2)) = (๐ / 2)) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ (๐ โ (๐ / 2)) = (๐ / 2)) |
114 | 113 | breq1d 5114 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ((๐ โ (๐ / 2)) < (๐ฅ ยท 2) โ (๐ / 2) < (๐ฅ ยท 2))) |
115 | 114 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โง (๐ / 2) โค (๐ฅ ยท 2)) โ ((๐ โ (๐ / 2)) < (๐ฅ ยท 2) โ (๐ / 2) < (๐ฅ ยท 2))) |
116 | 110, 115 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โง (๐ / 2) โค (๐ฅ ยท 2)) โ (๐ โ (๐ / 2)) < (๐ฅ ยท 2)) |
117 | 100 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ ๐ โ โ) |
118 | 101 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ (๐ / 2) โ โ) |
119 | 103 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ (๐ฅ ยท 2) โ โ) |
120 | 117, 118,
119 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ (๐ โ โ โง (๐ / 2) โ โ โง (๐ฅ ยท 2) โ
โ)) |
121 | 120 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โง (๐ / 2) โค (๐ฅ ยท 2)) โ (๐ โ โ โง (๐ / 2) โ โ โง (๐ฅ ยท 2) โ
โ)) |
122 | | ltsub23 11569 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง (๐ / 2) โ โ โง
(๐ฅ ยท 2) โ
โ) โ ((๐ โ
(๐ / 2)) < (๐ฅ ยท 2) โ (๐ โ (๐ฅ ยท 2)) < (๐ / 2))) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โง (๐ / 2) โค (๐ฅ ยท 2)) โ ((๐ โ (๐ / 2)) < (๐ฅ ยท 2) โ (๐ โ (๐ฅ ยท 2)) < (๐ / 2))) |
124 | 116, 123 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โง (๐ / 2) โค (๐ฅ ยท 2)) โ (๐ โ (๐ฅ ยท 2)) < (๐ / 2)) |
125 | 21 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ ๐ โ โค) |
126 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ ยฌ 2 โฅ ๐) |
127 | 60 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ (๐ฅ ยท 2) โ โค) |
128 | 125, 127 | zsubcld 12545 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ (๐ โ (๐ฅ ยท 2)) โ
โค) |
129 | 125, 126,
128 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ (๐ โ โค โง ยฌ 2 โฅ ๐ โง (๐ โ (๐ฅ ยท 2)) โ
โค)) |
130 | 129 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โง (๐ / 2) โค (๐ฅ ยท 2)) โ (๐ โ โค โง ยฌ 2 โฅ ๐ โง (๐ โ (๐ฅ ยท 2)) โ
โค)) |
131 | | ltoddhalfle 16178 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง (๐ โ (๐ฅ ยท 2)) โ โค) โ ((๐ โ (๐ฅ ยท 2)) < (๐ / 2) โ (๐ โ (๐ฅ ยท 2)) โค ((๐ โ 1) / 2))) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โง (๐ / 2) โค (๐ฅ ยท 2)) โ ((๐ โ (๐ฅ ยท 2)) < (๐ / 2) โ (๐ โ (๐ฅ ยท 2)) โค ((๐ โ 1) / 2))) |
133 | 124, 132 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โง (๐ / 2) โค (๐ฅ ยท 2)) โ (๐ โ (๐ฅ ยท 2)) โค ((๐ โ 1) / 2)) |
134 | 133 | ex 414 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ ((๐ / 2) โค (๐ฅ ยท 2) โ (๐ โ (๐ฅ ยท 2)) โค ((๐ โ 1) / 2))) |
135 | 14 | breq2i 5112 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (๐ฅ ยท 2)) โค ๐ป โ (๐ โ (๐ฅ ยท 2)) โค ((๐ โ 1) / 2)) |
136 | 134, 135 | syl6ibr 252 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ ((๐ / 2) โค (๐ฅ ยท 2) โ (๐ โ (๐ฅ ยท 2)) โค ๐ป)) |
137 | 105, 136 | sylbird 260 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ฅ โ (1...๐ป)) โ (ยฌ (๐ฅ ยท 2) < (๐ / 2) โ (๐ โ (๐ฅ ยท 2)) โค ๐ป)) |
138 | 137 | ex 414 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ (๐ฅ โ (1...๐ป) โ (ยฌ (๐ฅ ยท 2) < (๐ / 2) โ (๐ โ (๐ฅ ยท 2)) โค ๐ป))) |
139 | 19, 20, 138 | 3syl 18 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ (1...๐ป) โ (ยฌ (๐ฅ ยท 2) < (๐ / 2) โ (๐ โ (๐ฅ ยท 2)) โค ๐ป))) |
140 | 139 | imp 408 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...๐ป)) โ (ยฌ (๐ฅ ยท 2) < (๐ / 2) โ (๐ โ (๐ฅ ยท 2)) โค ๐ป)) |
141 | 140 | impcom 409 |
. . . . . . . . 9
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ โ (๐ฅ ยท 2)) โค ๐ป) |
142 | | elfz1b 13439 |
. . . . . . . . 9
โข ((๐ โ (๐ฅ ยท 2)) โ (1...๐ป) โ ((๐ โ (๐ฅ ยท 2)) โ โ โง ๐ป โ โ โง (๐ โ (๐ฅ ยท 2)) โค ๐ป)) |
143 | 97, 99, 141, 142 | syl3anbrc 1344 |
. . . . . . . 8
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ โ (๐ฅ ยท 2)) โ (1...๐ป)) |
144 | | eleq1 2826 |
. . . . . . . 8
โข (๐ฆ = (๐ โ (๐ฅ ยท 2)) โ (๐ฆ โ (1...๐ป) โ (๐ โ (๐ฅ ยท 2)) โ (1...๐ป))) |
145 | 143, 144 | syl5ibrcom 247 |
. . . . . . 7
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ฆ = (๐ โ (๐ฅ ยท 2)) โ ๐ฆ โ (1...๐ป))) |
146 | 53, 145 | sylbid 239 |
. . . . . 6
โข ((ยฌ
(๐ฅ ยท 2) < (๐ / 2) โง (๐ โง ๐ฅ โ (1...๐ป))) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ โ (1...๐ป))) |
147 | 50, 146 | pm2.61ian 811 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1...๐ป)) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ โ (1...๐ป))) |
148 | 147 | rexlimdva 3151 |
. . . 4
โข (๐ โ (โ๐ฅ โ (1...๐ป)๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ โ (1...๐ป))) |
149 | | elfz1b 13439 |
. . . . . . . . . 10
โข (๐ฆ โ (1...๐ป) โ (๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป)) |
150 | | simp1 1137 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป) โ ๐ฆ โ โ) |
151 | | simpl 484 |
. . . . . . . . . . . . 13
โข ((2
โฅ ๐ฆ โง ๐) โ 2 โฅ ๐ฆ) |
152 | | nnehalf 16196 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง 2 โฅ
๐ฆ) โ (๐ฆ / 2) โ
โ) |
153 | 150, 151,
152 | syl2anr 598 |
. . . . . . . . . . . 12
โข (((2
โฅ ๐ฆ โง ๐) โง (๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป)) โ (๐ฆ / 2) โ โ) |
154 | | simpr2 1196 |
. . . . . . . . . . . 12
โข (((2
โฅ ๐ฆ โง ๐) โง (๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป)) โ ๐ป โ โ) |
155 | | nnre 12094 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
156 | 155 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (2
โฅ ๐ฆ โง ๐)) โ ๐ฆ โ โ) |
157 | | nnrp 12855 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ป โ โ โ ๐ป โ
โ+) |
158 | 157 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ โง ๐ป โ โ) โ ๐ป โ
โ+) |
159 | 158 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (2
โฅ ๐ฆ โง ๐)) โ ๐ป โ
โ+) |
160 | | 2rp 12849 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ+ |
161 | | 1le2 12296 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โค
2 |
162 | 160, 161 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . 18
โข (2 โ
โ+ โง 1 โค 2) |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (2
โฅ ๐ฆ โง ๐)) โ (2 โ
โ+ โง 1 โค 2)) |
164 | | ledivge1le 12915 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง ๐ป โ โ+
โง (2 โ โ+ โง 1 โค 2)) โ (๐ฆ โค ๐ป โ (๐ฆ / 2) โค ๐ป)) |
165 | 156, 159,
163, 164 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (2
โฅ ๐ฆ โง ๐)) โ (๐ฆ โค ๐ป โ (๐ฆ / 2) โค ๐ป)) |
166 | 165 | ex 414 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ โง ๐ป โ โ) โ ((2
โฅ ๐ฆ โง ๐) โ (๐ฆ โค ๐ป โ (๐ฆ / 2) โค ๐ป))) |
167 | 166 | com23 86 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ โ โง ๐ป โ โ) โ (๐ฆ โค ๐ป โ ((2 โฅ ๐ฆ โง ๐) โ (๐ฆ / 2) โค ๐ป))) |
168 | 167 | 3impia 1118 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป) โ ((2 โฅ ๐ฆ โง ๐) โ (๐ฆ / 2) โค ๐ป)) |
169 | 168 | impcom 409 |
. . . . . . . . . . . 12
โข (((2
โฅ ๐ฆ โง ๐) โง (๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป)) โ (๐ฆ / 2) โค ๐ป) |
170 | 153, 154,
169 | 3jca 1129 |
. . . . . . . . . . 11
โข (((2
โฅ ๐ฆ โง ๐) โง (๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป)) โ ((๐ฆ / 2) โ โ โง ๐ป โ โ โง (๐ฆ / 2) โค ๐ป)) |
171 | 170 | ex 414 |
. . . . . . . . . 10
โข ((2
โฅ ๐ฆ โง ๐) โ ((๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป) โ ((๐ฆ / 2) โ โ โง ๐ป โ โ โง (๐ฆ / 2) โค ๐ป))) |
172 | 149, 171 | biimtrid 241 |
. . . . . . . . 9
โข ((2
โฅ ๐ฆ โง ๐) โ (๐ฆ โ (1...๐ป) โ ((๐ฆ / 2) โ โ โง ๐ป โ โ โง (๐ฆ / 2) โค ๐ป))) |
173 | 172 | 3impia 1118 |
. . . . . . . 8
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ((๐ฆ / 2) โ โ โง ๐ป โ โ โง (๐ฆ / 2) โค ๐ป)) |
174 | | elfz1b 13439 |
. . . . . . . 8
โข ((๐ฆ / 2) โ (1...๐ป) โ ((๐ฆ / 2) โ โ โง ๐ป โ โ โง (๐ฆ / 2) โค ๐ป)) |
175 | 173, 174 | sylibr 233 |
. . . . . . 7
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ (๐ฆ / 2) โ (1...๐ป)) |
176 | | oveq1 7357 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ฆ / 2) โ (๐ฅ ยท 2) = ((๐ฆ / 2) ยท 2)) |
177 | 176 | breq1d 5114 |
. . . . . . . . . 10
โข (๐ฅ = (๐ฆ / 2) โ ((๐ฅ ยท 2) < (๐ / 2) โ ((๐ฆ / 2) ยท 2) < (๐ / 2))) |
178 | 176 | oveq2d 7366 |
. . . . . . . . . 10
โข (๐ฅ = (๐ฆ / 2) โ (๐ โ (๐ฅ ยท 2)) = (๐ โ ((๐ฆ / 2) ยท 2))) |
179 | 177, 176,
178 | ifbieq12d 4513 |
. . . . . . . . 9
โข (๐ฅ = (๐ฆ / 2) โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = if(((๐ฆ / 2) ยท 2) < (๐ / 2), ((๐ฆ / 2) ยท 2), (๐ โ ((๐ฆ / 2) ยท 2)))) |
180 | 179 | eqeq2d 2749 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ / 2) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ = if(((๐ฆ / 2) ยท 2) < (๐ / 2), ((๐ฆ / 2) ยท 2), (๐ โ ((๐ฆ / 2) ยท 2))))) |
181 | 180 | adantl 483 |
. . . . . . 7
โข (((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โง ๐ฅ = (๐ฆ / 2)) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ = if(((๐ฆ / 2) ยท 2) < (๐ / 2), ((๐ฆ / 2) ยท 2), (๐ โ ((๐ฆ / 2) ยท 2))))) |
182 | | elfzelz 13370 |
. . . . . . . . . . . . 13
โข (๐ฆ โ (1...๐ป) โ ๐ฆ โ โค) |
183 | 182 | zcnd 12541 |
. . . . . . . . . . . 12
โข (๐ฆ โ (1...๐ป) โ ๐ฆ โ โ) |
184 | 183 | 3ad2ant3 1136 |
. . . . . . . . . . 11
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ๐ฆ โ โ) |
185 | | 2cnd 12165 |
. . . . . . . . . . 11
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ 2 โ โ) |
186 | | 2ne0 12191 |
. . . . . . . . . . . 12
โข 2 โ
0 |
187 | 186 | a1i 11 |
. . . . . . . . . . 11
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ 2 โ 0) |
188 | 184, 185,
187 | divcan1d 11866 |
. . . . . . . . . 10
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ((๐ฆ / 2) ยท 2) = ๐ฆ) |
189 | 14 | breq2i 5112 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โค ๐ป โ ๐ฆ โค ((๐ โ 1) / 2)) |
190 | | nnz 12456 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ โ โ โ ๐ฆ โ
โค) |
191 | 19, 20, 22 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ โ โค โง ยฌ 2 โฅ ๐)) |
192 | 191 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((2
โฅ ๐ฆ โง ๐) โ (๐ โ โค โง ยฌ 2 โฅ ๐)) |
193 | 190, 192 | anim12ci 615 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ โง (2 โฅ
๐ฆ โง ๐)) โ ((๐ โ โค โง ยฌ 2 โฅ ๐) โง ๐ฆ โ โค)) |
194 | | df-3an 1090 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐ฆ โ โค) โ ((๐ โ โค โง ยฌ 2
โฅ ๐) โง ๐ฆ โ
โค)) |
195 | 193, 194 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ โง (2 โฅ
๐ฆ โง ๐)) โ (๐ โ โค โง ยฌ 2 โฅ ๐ โง ๐ฆ โ โค)) |
196 | | ltoddhalfle 16178 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐ฆ โ โค) โ (๐ฆ < (๐ / 2) โ ๐ฆ โค ((๐ โ 1) / 2))) |
197 | 195, 196 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ โง (2 โฅ
๐ฆ โง ๐)) โ (๐ฆ < (๐ / 2) โ ๐ฆ โค ((๐ โ 1) / 2))) |
198 | 197 | exbiri 810 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ โ ((2
โฅ ๐ฆ โง ๐) โ (๐ฆ โค ((๐ โ 1) / 2) โ ๐ฆ < (๐ / 2)))) |
199 | 198 | com23 86 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (๐ฆ โค ((๐ โ 1) / 2) โ ((2 โฅ ๐ฆ โง ๐) โ ๐ฆ < (๐ / 2)))) |
200 | 189, 199 | biimtrid 241 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ (๐ฆ โค ๐ป โ ((2 โฅ ๐ฆ โง ๐) โ ๐ฆ < (๐ / 2)))) |
201 | 200 | a1d 25 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (๐ป โ โ โ (๐ฆ โค ๐ป โ ((2 โฅ ๐ฆ โง ๐) โ ๐ฆ < (๐ / 2))))) |
202 | 201 | 3imp 1112 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป) โ ((2 โฅ ๐ฆ โง ๐) โ ๐ฆ < (๐ / 2))) |
203 | 149, 202 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ฆ โ (1...๐ป) โ ((2 โฅ ๐ฆ โง ๐) โ ๐ฆ < (๐ / 2))) |
204 | 203 | com12 32 |
. . . . . . . . . . 11
โข ((2
โฅ ๐ฆ โง ๐) โ (๐ฆ โ (1...๐ป) โ ๐ฆ < (๐ / 2))) |
205 | 204 | 3impia 1118 |
. . . . . . . . . 10
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ๐ฆ < (๐ / 2)) |
206 | 188, 205 | eqbrtrd 5126 |
. . . . . . . . 9
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ((๐ฆ / 2) ยท 2) < (๐ / 2)) |
207 | 206 | iftrued 4493 |
. . . . . . . 8
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ if(((๐ฆ / 2) ยท 2) < (๐ / 2), ((๐ฆ / 2) ยท 2), (๐ โ ((๐ฆ / 2) ยท 2))) = ((๐ฆ / 2) ยท 2)) |
208 | 207, 188 | eqtr2d 2779 |
. . . . . . 7
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ๐ฆ = if(((๐ฆ / 2) ยท 2) < (๐ / 2), ((๐ฆ / 2) ยท 2), (๐ โ ((๐ฆ / 2) ยท 2)))) |
209 | 175, 181,
208 | rspcedvd 3582 |
. . . . . 6
โข ((2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ โ๐ฅ โ (1...๐ป)๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2)))) |
210 | 209 | 3exp 1120 |
. . . . 5
โข (2
โฅ ๐ฆ โ (๐ โ (๐ฆ โ (1...๐ป) โ โ๐ฅ โ (1...๐ป)๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2)))))) |
211 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โ โ {2})
โ ๐ โ
โค) |
212 | 211 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ ๐ โ โค) |
213 | 190 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป) โ ๐ฆ โ โค) |
214 | 213 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ ๐ฆ โ โค) |
215 | 212, 214 | zsubcld 12545 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ (๐ โ ๐ฆ) โ โค) |
216 | 155 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ป โ โ)) โ ๐ฆ โ
โ) |
217 | 67 | rehalfcld 12334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ โ โ ((๐ โ 1) / 2) โ
โ) |
218 | 217 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ป โ โ)) โ ((๐ โ 1) / 2) โ
โ) |
219 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ป โ โ)) โ ๐ โ
โ) |
220 | 216, 218,
219 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ป โ โ)) โ (๐ฆ โ โ โง ((๐ โ 1) / 2) โ โ
โง ๐ โ
โ)) |
221 | 220 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ ((๐ฆ โ โ โง ๐ป โ โ) โ (๐ฆ โ โ โง ((๐ โ 1) / 2) โ โ
โง ๐ โ
โ))) |
222 | 54, 63, 221 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (โ โ {2})
โ ((๐ฆ โ โ
โง ๐ป โ โ)
โ (๐ฆ โ โ
โง ((๐ โ 1) / 2)
โ โ โง ๐
โ โ))) |
223 | 222 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โ ((๐ฆ โ โ
โง ๐ป โ โ)
โ (๐ฆ โ โ
โง ((๐ โ 1) / 2)
โ โ โง ๐
โ โ))) |
224 | 223 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ))
โ (๐ฆ โ โ
โง ((๐ โ 1) / 2)
โ โ โง ๐
โ โ)) |
225 | | lesub2 11584 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฆ โ โ โง ((๐ โ 1) / 2) โ โ
โง ๐ โ โ)
โ (๐ฆ โค ((๐ โ 1) / 2) โ (๐ โ ((๐ โ 1) / 2)) โค (๐ โ ๐ฆ))) |
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ))
โ (๐ฆ โค ((๐ โ 1) / 2) โ (๐ โ ((๐ โ 1) / 2)) โค (๐ โ ๐ฆ))) |
227 | 55 | zcnd 12541 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ ๐ โ
โ) |
228 | | 1cnd 11084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ โ โ 1 โ
โ) |
229 | | 2cnne0 12297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (2 โ
โ โง 2 โ 0) |
230 | 229 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ โ โ (2 โ
โ โง 2 โ 0)) |
231 | | divsubdir 11783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ โ โง 1 โ
โ โง (2 โ โ โง 2 โ 0)) โ ((๐ โ 1) / 2) = ((๐ / 2) โ (1 / 2))) |
232 | 228, 230,
231 | mpd3an23 1464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ โ โ ((๐ โ 1) / 2) = ((๐ / 2) โ (1 /
2))) |
233 | 232 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ (๐ โ ((๐ โ 1) / 2)) = (๐ โ ((๐ / 2) โ (1 / 2)))) |
234 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ โ โ ๐ โ
โ) |
235 | | halfcl 12312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ โ โ (๐ / 2) โ
โ) |
236 | | halfcn 12302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (1 / 2)
โ โ |
237 | 236 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ โ โ (1 / 2)
โ โ) |
238 | 234, 235,
237 | subsubd 11474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ (๐ โ ((๐ / 2) โ (1 / 2))) = ((๐ โ (๐ / 2)) + (1 / 2))) |
239 | 112 | oveq1d 7365 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ ((๐ โ (๐ / 2)) + (1 / 2)) = ((๐ / 2) + (1 / 2))) |
240 | 233, 238,
239 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ (๐ โ ((๐ โ 1) / 2)) = ((๐ / 2) + (1 / 2))) |
241 | 54, 227, 240 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (โ โ {2})
โ (๐ โ ((๐ โ 1) / 2)) = ((๐ / 2) + (1 /
2))) |
242 | 241 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ))
โ (๐ โ ((๐ โ 1) / 2)) = ((๐ / 2) + (1 /
2))) |
243 | 242 | breq1d 5114 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ))
โ ((๐ โ ((๐ โ 1) / 2)) โค (๐ โ ๐ฆ) โ ((๐ / 2) + (1 / 2)) โค (๐ โ ๐ฆ))) |
244 | | prmnn 16485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ ๐ โ
โ) |
245 | | halfre 12301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (1 / 2)
โ โ |
246 | 245 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ (1 / 2)
โ โ) |
247 | | nngt0 12118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ โ โ 0 <
๐) |
248 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ โ โ (2 โ
โ โง 0 < 2)) |
249 | | divgt0 11957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โ โ โง 0 <
๐) โง (2 โ โ
โง 0 < 2)) โ 0 < (๐ / 2)) |
250 | 100, 247,
248, 249 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ 0 <
(๐ / 2)) |
251 | | halfgt0 12303 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข 0 < (1
/ 2) |
252 | 251 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ 0 < (1
/ 2)) |
253 | 101, 246,
250, 252 | addgt0d 11664 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ 0 <
((๐ / 2) + (1 /
2))) |
254 | 54, 244, 253 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (โ โ {2})
โ 0 < ((๐ / 2) + (1
/ 2))) |
255 | 254 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ))
โ 0 < ((๐ / 2) + (1
/ 2))) |
256 | | 0red 11092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ฆ โ โ โง ๐ โ โ) โ 0 โ
โ) |
257 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ฆ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
258 | 257 | rehalfcld 12334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ / 2) โ
โ) |
259 | 245 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ฆ โ โ โง ๐ โ โ) โ (1 / 2)
โ โ) |
260 | 258, 259 | readdcld 11118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ฆ โ โ โง ๐ โ โ) โ ((๐ / 2) + (1 / 2)) โ
โ) |
261 | | resubcl 11399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ โ โง ๐ฆ โ โ) โ (๐ โ ๐ฆ) โ โ) |
262 | 261 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ โ ๐ฆ) โ โ) |
263 | 256, 260,
262 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ฆ โ โ โง ๐ โ โ) โ (0
โ โ โง ((๐ /
2) + (1 / 2)) โ โ โง (๐ โ ๐ฆ) โ โ)) |
264 | 263 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ฆ โ โ โ (๐ โ โ โ (0 โ
โ โง ((๐ / 2) + (1
/ 2)) โ โ โง (๐ โ ๐ฆ) โ โ))) |
265 | 155, 264 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ฆ โ โ โ (๐ โ โ โ (0 โ
โ โง ((๐ / 2) + (1
/ 2)) โ โ โง (๐ โ ๐ฆ) โ โ))) |
266 | 265 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ฆ โ โ โง ๐ป โ โ) โ (๐ โ โ โ (0 โ
โ โง ((๐ / 2) + (1
/ 2)) โ โ โง (๐ โ ๐ฆ) โ โ))) |
267 | 266 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ โ โ ((๐ฆ โ โ โง ๐ป โ โ) โ (0
โ โ โง ((๐ /
2) + (1 / 2)) โ โ โง (๐ โ ๐ฆ) โ โ))) |
268 | 54, 63, 267 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (โ โ {2})
โ ((๐ฆ โ โ
โง ๐ป โ โ)
โ (0 โ โ โง ((๐ / 2) + (1 / 2)) โ โ โง (๐ โ ๐ฆ) โ โ))) |
269 | 268 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โ ((๐ฆ โ โ
โง ๐ป โ โ)
โ (0 โ โ โง ((๐ / 2) + (1 / 2)) โ โ โง (๐ โ ๐ฆ) โ โ))) |
270 | 269 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ))
โ (0 โ โ โง ((๐ / 2) + (1 / 2)) โ โ โง (๐ โ ๐ฆ) โ โ)) |
271 | | ltletr 11181 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((0
โ โ โง ((๐ /
2) + (1 / 2)) โ โ โง (๐ โ ๐ฆ) โ โ) โ ((0 < ((๐ / 2) + (1 / 2)) โง ((๐ / 2) + (1 / 2)) โค (๐ โ ๐ฆ)) โ 0 < (๐ โ ๐ฆ))) |
272 | 270, 271 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ))
โ ((0 < ((๐ / 2) +
(1 / 2)) โง ((๐ / 2) +
(1 / 2)) โค (๐ โ
๐ฆ)) โ 0 < (๐ โ ๐ฆ))) |
273 | 255, 272 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ))
โ (((๐ / 2) + (1 / 2))
โค (๐ โ ๐ฆ) โ 0 < (๐ โ ๐ฆ))) |
274 | 243, 273 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ))
โ ((๐ โ ((๐ โ 1) / 2)) โค (๐ โ ๐ฆ) โ 0 < (๐ โ ๐ฆ))) |
275 | 226, 274 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฆ โ โ โง ๐ป โ โ) โง (๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ))
โ (๐ฆ โค ((๐ โ 1) / 2) โ 0 <
(๐ โ ๐ฆ))) |
276 | 275 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ โง ๐ป โ โ) โ ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โ (๐ฆ โค ((๐ โ 1) / 2) โ 0 <
(๐ โ ๐ฆ)))) |
277 | 276 | com23 86 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ โง ๐ป โ โ) โ (๐ฆ โค ((๐ โ 1) / 2) โ ((๐ โ (โ โ {2}) โง ยฌ 2
โฅ ๐ฆ) โ 0 <
(๐ โ ๐ฆ)))) |
278 | 189, 277 | biimtrid 241 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง ๐ป โ โ) โ (๐ฆ โค ๐ป โ ((๐ โ (โ โ {2}) โง ยฌ 2
โฅ ๐ฆ) โ 0 <
(๐ โ ๐ฆ)))) |
279 | 278 | 3impia 1118 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป) โ ((๐ โ (โ โ {2}) โง ยฌ 2
โฅ ๐ฆ) โ 0 <
(๐ โ ๐ฆ))) |
280 | 279 | impcom 409 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ 0 < (๐ โ ๐ฆ)) |
281 | | elnnz 12443 |
. . . . . . . . . . . . . . 15
โข ((๐ โ ๐ฆ) โ โ โ ((๐ โ ๐ฆ) โ โค โง 0 < (๐ โ ๐ฆ))) |
282 | 215, 280,
281 | sylanbrc 584 |
. . . . . . . . . . . . . 14
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ (๐ โ ๐ฆ) โ โ) |
283 | 23 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โ (๐ โ โค
โง ยฌ 2 โฅ ๐)) |
284 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โ ยฌ 2 โฅ ๐ฆ) |
285 | 284, 213 | anim12ci 615 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ (๐ฆ โ โค โง ยฌ 2 โฅ ๐ฆ)) |
286 | | omoe 16181 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โค โง ยฌ 2
โฅ ๐) โง (๐ฆ โ โค โง ยฌ 2
โฅ ๐ฆ)) โ 2
โฅ (๐ โ ๐ฆ)) |
287 | 283, 285,
286 | syl2an2r 684 |
. . . . . . . . . . . . . 14
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ 2 โฅ (๐ โ ๐ฆ)) |
288 | | nnehalf 16196 |
. . . . . . . . . . . . . 14
โข (((๐ โ ๐ฆ) โ โ โง 2 โฅ (๐ โ ๐ฆ)) โ ((๐ โ ๐ฆ) / 2) โ โ) |
289 | 282, 287,
288 | syl2anc 585 |
. . . . . . . . . . . . 13
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ ((๐ โ ๐ฆ) / 2) โ โ) |
290 | | simpr2 1196 |
. . . . . . . . . . . . 13
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ ๐ป โ โ) |
291 | | 1red 11090 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ 1 โ
โ) |
292 | 155 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป) โ ๐ฆ โ โ) |
293 | 292 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ ๐ฆ โ โ) |
294 | 54, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
295 | 294 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ ๐ โ โ) |
296 | | nnge1 12115 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ โ 1 โค
๐ฆ) |
297 | 296 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป) โ 1 โค ๐ฆ) |
298 | 297 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ 1 โค ๐ฆ) |
299 | 291, 293,
295, 298 | lesub2dd 11706 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ (๐ โ ๐ฆ) โค (๐ โ 1)) |
300 | 295, 293 | resubcld 11517 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ (๐ โ ๐ฆ) โ โ) |
301 | 54, 63, 67 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โ โ {2})
โ (๐ โ 1) โ
โ) |
302 | 301 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ (๐ โ 1) โ โ) |
303 | 71 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ (2 โ โ
โง 0 < 2)) |
304 | | lediv1 11954 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ ๐ฆ) โ โ โง (๐ โ 1) โ โ โง (2 โ
โ โง 0 < 2)) โ ((๐ โ ๐ฆ) โค (๐ โ 1) โ ((๐ โ ๐ฆ) / 2) โค ((๐ โ 1) / 2))) |
305 | 300, 302,
303, 304 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ ((๐ โ ๐ฆ) โค (๐ โ 1) โ ((๐ โ ๐ฆ) / 2) โค ((๐ โ 1) / 2))) |
306 | 299, 305 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ ((๐ โ ๐ฆ) / 2) โค ((๐ โ 1) / 2)) |
307 | 14 | breq2i 5112 |
. . . . . . . . . . . . . 14
โข (((๐ โ ๐ฆ) / 2) โค ๐ป โ ((๐ โ ๐ฆ) / 2) โค ((๐ โ 1) / 2)) |
308 | 306, 307 | sylibr 233 |
. . . . . . . . . . . . 13
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ ((๐ โ ๐ฆ) / 2) โค ๐ป) |
309 | 289, 290,
308 | 3jca 1129 |
. . . . . . . . . . . 12
โข (((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โง (๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป)) โ (((๐ โ ๐ฆ) / 2) โ โ โง ๐ป โ โ โง ((๐ โ ๐ฆ) / 2) โค ๐ป)) |
310 | 309 | ex 414 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โ ((๐ฆ โ โ
โง ๐ป โ โ
โง ๐ฆ โค ๐ป) โ (((๐ โ ๐ฆ) / 2) โ โ โง ๐ป โ โ โง ((๐ โ ๐ฆ) / 2) โค ๐ป))) |
311 | | elfz1b 13439 |
. . . . . . . . . . 11
โข (((๐ โ ๐ฆ) / 2) โ (1...๐ป) โ (((๐ โ ๐ฆ) / 2) โ โ โง ๐ป โ โ โง ((๐ โ ๐ฆ) / 2) โค ๐ป)) |
312 | 310, 149,
311 | 3imtr4g 296 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ๐ฆ)
โ (๐ฆ โ (1...๐ป) โ ((๐ โ ๐ฆ) / 2) โ (1...๐ป))) |
313 | 312 | ex 414 |
. . . . . . . . 9
โข (๐ โ (โ โ {2})
โ (ยฌ 2 โฅ ๐ฆ
โ (๐ฆ โ (1...๐ป) โ ((๐ โ ๐ฆ) / 2) โ (1...๐ป)))) |
314 | 19, 313 | syl 17 |
. . . . . . . 8
โข (๐ โ (ยฌ 2 โฅ ๐ฆ โ (๐ฆ โ (1...๐ป) โ ((๐ โ ๐ฆ) / 2) โ (1...๐ป)))) |
315 | 314 | 3imp21 1115 |
. . . . . . 7
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ((๐ โ ๐ฆ) / 2) โ (1...๐ป)) |
316 | | oveq1 7357 |
. . . . . . . . . . 11
โข (๐ฅ = ((๐ โ ๐ฆ) / 2) โ (๐ฅ ยท 2) = (((๐ โ ๐ฆ) / 2) ยท 2)) |
317 | 316 | breq1d 5114 |
. . . . . . . . . 10
โข (๐ฅ = ((๐ โ ๐ฆ) / 2) โ ((๐ฅ ยท 2) < (๐ / 2) โ (((๐ โ ๐ฆ) / 2) ยท 2) < (๐ / 2))) |
318 | 316 | oveq2d 7366 |
. . . . . . . . . 10
โข (๐ฅ = ((๐ โ ๐ฆ) / 2) โ (๐ โ (๐ฅ ยท 2)) = (๐ โ (((๐ โ ๐ฆ) / 2) ยท 2))) |
319 | 317, 316,
318 | ifbieq12d 4513 |
. . . . . . . . 9
โข (๐ฅ = ((๐ โ ๐ฆ) / 2) โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = if((((๐ โ ๐ฆ) / 2) ยท 2) < (๐ / 2), (((๐ โ ๐ฆ) / 2) ยท 2), (๐ โ (((๐ โ ๐ฆ) / 2) ยท 2)))) |
320 | 319 | eqeq2d 2749 |
. . . . . . . 8
โข (๐ฅ = ((๐ โ ๐ฆ) / 2) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ = if((((๐ โ ๐ฆ) / 2) ยท 2) < (๐ / 2), (((๐ โ ๐ฆ) / 2) ยท 2), (๐ โ (((๐ โ ๐ฆ) / 2) ยท 2))))) |
321 | 320 | adantl 483 |
. . . . . . 7
โข (((ยฌ
2 โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โง ๐ฅ = ((๐ โ ๐ฆ) / 2)) โ (๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ = if((((๐ โ ๐ฆ) / 2) ยท 2) < (๐ / 2), (((๐ โ ๐ฆ) / 2) ยท 2), (๐ โ (((๐ โ ๐ฆ) / 2) ยท 2))))) |
322 | 19, 54, 227 | 3syl 18 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
323 | 322 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ๐ โ โ) |
324 | 183 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ๐ฆ โ โ) |
325 | 323, 324 | subcld 11446 |
. . . . . . . . . . 11
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ (๐ โ ๐ฆ) โ โ) |
326 | | 2cnd 12165 |
. . . . . . . . . . 11
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ 2 โ โ) |
327 | 186 | a1i 11 |
. . . . . . . . . . 11
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ 2 โ 0) |
328 | 325, 326,
327 | divcan1d 11866 |
. . . . . . . . . 10
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ (((๐ โ ๐ฆ) / 2) ยท 2) = (๐ โ ๐ฆ)) |
329 | | zre 12437 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โค โ ๐ โ
โ) |
330 | | halfge0 12304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข 0 โค (1
/ 2) |
331 | | rehalfcl 12313 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ โ (๐ / 2) โ
โ) |
332 | 331 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ / 2) โ
โ) |
333 | 332, 259 | subge02d 11681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ฆ โ โ โง ๐ โ โ) โ (0 โค
(1 / 2) โ ((๐ / 2)
โ (1 / 2)) โค (๐ /
2))) |
334 | 330, 333 | mpbii 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฆ โ โ โง ๐ โ โ) โ ((๐ / 2) โ (1 / 2)) โค
(๐ / 2)) |
335 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ฆ โ โ โง ๐ โ โ) โ ๐ฆ โ
โ) |
336 | 245 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ โ (1 / 2)
โ โ) |
337 | 331, 336 | resubcld 11517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ โ โ ((๐ / 2) โ (1 / 2)) โ
โ) |
338 | 337 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ฆ โ โ โง ๐ โ โ) โ ((๐ / 2) โ (1 / 2)) โ
โ) |
339 | | letr 11183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ฆ โ โ โง ((๐ / 2) โ (1 / 2)) โ
โ โง (๐ / 2)
โ โ) โ ((๐ฆ
โค ((๐ / 2) โ (1 /
2)) โง ((๐ / 2) โ
(1 / 2)) โค (๐ / 2))
โ ๐ฆ โค (๐ / 2))) |
340 | 335, 338,
332, 339 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฆ โ โ โง ๐ โ โ) โ ((๐ฆ โค ((๐ / 2) โ (1 / 2)) โง ((๐ / 2) โ (1 / 2)) โค
(๐ / 2)) โ ๐ฆ โค (๐ / 2))) |
341 | 334, 340 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ฆ โค ((๐ / 2) โ (1 / 2)) โ ๐ฆ โค (๐ / 2))) |
342 | 80 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ฆ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
343 | | 1cnd 11084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ฆ โ โ โง ๐ โ โ) โ 1 โ
โ) |
344 | 229 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ฆ โ โ โง ๐ โ โ) โ (2
โ โ โง 2 โ 0)) |
345 | 342, 343,
344, 231 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฆ โ โ โง ๐ โ โ) โ ((๐ โ 1) / 2) = ((๐ / 2) โ (1 /
2))) |
346 | 345 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ฆ โค ((๐ โ 1) / 2) โ ๐ฆ โค ((๐ / 2) โ (1 / 2)))) |
347 | | lesub 11568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ / 2) โ โ โง ๐ โ โ โง ๐ฆ โ โ) โ ((๐ / 2) โค (๐ โ ๐ฆ) โ ๐ฆ โค (๐ โ (๐ / 2)))) |
348 | 332, 257,
335, 347 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฆ โ โ โง ๐ โ โ) โ ((๐ / 2) โค (๐ โ ๐ฆ) โ ๐ฆ โค (๐ โ (๐ / 2)))) |
349 | 258, 262 | lenltd 11235 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฆ โ โ โง ๐ โ โ) โ ((๐ / 2) โค (๐ โ ๐ฆ) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2))) |
350 | | 2cnd 12165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ โ โ โ 2 โ
โ) |
351 | 186 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ โ โ โ 2 โ
0) |
352 | 80, 350, 351 | divcan1d 11866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ โ ((๐ / 2) ยท 2) = ๐) |
353 | 352 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ โ โ ๐ = ((๐ / 2) ยท 2)) |
354 | 353 | oveq1d 7365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ โ (๐ โ (๐ / 2)) = (((๐ / 2) ยท 2) โ (๐ / 2))) |
355 | 331 | recnd 11117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ โ (๐ / 2) โ
โ) |
356 | 355, 350 | mulcomd 11110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ โ โ ((๐ / 2) ยท 2) = (2 ยท
(๐ / 2))) |
357 | 356 | oveq1d 7365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ โ (((๐ / 2) ยท 2) โ (๐ / 2)) = ((2 ยท (๐ / 2)) โ (๐ / 2))) |
358 | 350, 355 | mulsubfacd 11550 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ โ โ ((2
ยท (๐ / 2)) โ
(๐ / 2)) = ((2 โ 1)
ยท (๐ /
2))) |
359 | | 2m1e1 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (2
โ 1) = 1 |
360 | 359 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ โ (2
โ 1) = 1) |
361 | 360 | oveq1d 7365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ โ โ ((2
โ 1) ยท (๐ /
2)) = (1 ยท (๐ /
2))) |
362 | 355 | mulid2d 11107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ โ โ (1
ยท (๐ / 2)) = (๐ / 2)) |
363 | 358, 361,
362 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ โ ((2
ยท (๐ / 2)) โ
(๐ / 2)) = (๐ / 2)) |
364 | 354, 357,
363 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ โ โ (๐ โ (๐ / 2)) = (๐ / 2)) |
365 | 364 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ โ (๐ / 2)) = (๐ / 2)) |
366 | 365 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ฆ โค (๐ โ (๐ / 2)) โ ๐ฆ โค (๐ / 2))) |
367 | 348, 349,
366 | 3bitr3d 309 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ฆ โ โ โง ๐ โ โ) โ (ยฌ
(๐ โ ๐ฆ) < (๐ / 2) โ ๐ฆ โค (๐ / 2))) |
368 | 341, 346,
367 | 3imtr4d 294 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ฆ โค ((๐ โ 1) / 2) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2))) |
369 | 368 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ โ โ โ (๐ โ โ โ (๐ฆ โค ((๐ โ 1) / 2) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2)))) |
370 | 155, 369 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ โ โ (๐ โ โ โ (๐ฆ โค ((๐ โ 1) / 2) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2)))) |
371 | 370 | com3l 89 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ (๐ฆ โค ((๐ โ 1) / 2) โ (๐ฆ โ โ โ ยฌ (๐ โ ๐ฆ) < (๐ / 2)))) |
372 | 329, 371 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โค โ (๐ฆ โค ((๐ โ 1) / 2) โ (๐ฆ โ โ โ ยฌ (๐ โ ๐ฆ) < (๐ / 2)))) |
373 | 54, 55, 372 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ (๐ฆ โค ((๐ โ 1) / 2) โ (๐ฆ โ โ โ ยฌ
(๐ โ ๐ฆ) < (๐ / 2)))) |
374 | 19, 373 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ฆ โค ((๐ โ 1) / 2) โ (๐ฆ โ โ โ ยฌ (๐ โ ๐ฆ) < (๐ / 2)))) |
375 | 374 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข ((ยฌ 2
โฅ ๐ฆ โง ๐) โ (๐ฆ โค ((๐ โ 1) / 2) โ (๐ฆ โ โ โ ยฌ (๐ โ ๐ฆ) < (๐ / 2)))) |
376 | 375 | com13 88 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (๐ฆ โค ((๐ โ 1) / 2) โ ((ยฌ 2 โฅ
๐ฆ โง ๐) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2)))) |
377 | 189, 376 | biimtrid 241 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ (๐ฆ โค ๐ป โ ((ยฌ 2 โฅ ๐ฆ โง ๐) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2)))) |
378 | 377 | a1d 25 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (๐ป โ โ โ (๐ฆ โค ๐ป โ ((ยฌ 2 โฅ ๐ฆ โง ๐) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2))))) |
379 | 378 | 3imp 1112 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป) โ ((ยฌ 2 โฅ ๐ฆ โง ๐) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2))) |
380 | 379 | com12 32 |
. . . . . . . . . . . 12
โข ((ยฌ 2
โฅ ๐ฆ โง ๐) โ ((๐ฆ โ โ โง ๐ป โ โ โง ๐ฆ โค ๐ป) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2))) |
381 | 149, 380 | biimtrid 241 |
. . . . . . . . . . 11
โข ((ยฌ 2
โฅ ๐ฆ โง ๐) โ (๐ฆ โ (1...๐ป) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2))) |
382 | 381 | 3impia 1118 |
. . . . . . . . . 10
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ยฌ (๐ โ ๐ฆ) < (๐ / 2)) |
383 | 328, 382 | eqnbrtrd 5122 |
. . . . . . . . 9
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ยฌ (((๐ โ ๐ฆ) / 2) ยท 2) < (๐ / 2)) |
384 | 383 | iffalsed 4496 |
. . . . . . . 8
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ if((((๐ โ ๐ฆ) / 2) ยท 2) < (๐ / 2), (((๐ โ ๐ฆ) / 2) ยท 2), (๐ โ (((๐ โ ๐ฆ) / 2) ยท 2))) = (๐ โ (((๐ โ ๐ฆ) / 2) ยท 2))) |
385 | 328 | oveq2d 7366 |
. . . . . . . 8
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ (๐ โ (((๐ โ ๐ฆ) / 2) ยท 2)) = (๐ โ (๐ โ ๐ฆ))) |
386 | 322, 183 | anim12i 614 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ (1...๐ป)) โ (๐ โ โ โง ๐ฆ โ โ)) |
387 | 386 | 3adant1 1131 |
. . . . . . . . 9
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ (๐ โ โ โง ๐ฆ โ โ)) |
388 | | nncan 11364 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ฆ โ โ) โ (๐ โ (๐ โ ๐ฆ)) = ๐ฆ) |
389 | 387, 388 | syl 17 |
. . . . . . . 8
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ (๐ โ (๐ โ ๐ฆ)) = ๐ฆ) |
390 | 384, 385,
389 | 3eqtrrd 2783 |
. . . . . . 7
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ ๐ฆ = if((((๐ โ ๐ฆ) / 2) ยท 2) < (๐ / 2), (((๐ โ ๐ฆ) / 2) ยท 2), (๐ โ (((๐ โ ๐ฆ) / 2) ยท 2)))) |
391 | 315, 321,
390 | rspcedvd 3582 |
. . . . . 6
โข ((ยฌ 2
โฅ ๐ฆ โง ๐ โง ๐ฆ โ (1...๐ป)) โ โ๐ฅ โ (1...๐ป)๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2)))) |
392 | 391 | 3exp 1120 |
. . . . 5
โข (ยฌ 2
โฅ ๐ฆ โ (๐ โ (๐ฆ โ (1...๐ป) โ โ๐ฅ โ (1...๐ป)๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2)))))) |
393 | 210, 392 | pm2.61i 182 |
. . . 4
โข (๐ โ (๐ฆ โ (1...๐ป) โ โ๐ฅ โ (1...๐ป)๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))))) |
394 | 148, 393 | impbid 211 |
. . 3
โข (๐ โ (โ๐ฅ โ (1...๐ป)๐ฆ = if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) โ ๐ฆ โ (1...๐ป))) |
395 | 3, 394 | bitrid 283 |
. 2
โข (๐ โ (๐ฆ โ ran ๐
โ ๐ฆ โ (1...๐ป))) |
396 | 395 | eqrdv 2736 |
1
โข (๐ โ ran ๐
= (1...๐ป)) |