Step | Hyp | Ref
| Expression |
1 | | imassrn 6028 |
. . . . 5
โข (๐น โ ๐ด) โ ran ๐น |
2 | | simpll 766 |
. . . . . . 7
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ โ) |
3 | | simprl1 1219 |
. . . . . . 7
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ (๐ผโ๐)) |
4 | | simplr1 1216 |
. . . . . . . 8
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ด โ (๐ผโ๐)) |
5 | | simprl2 1220 |
. . . . . . . 8
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ ๐ด) |
6 | 4, 5 | sseldd 3949 |
. . . . . . 7
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ (๐ผโ๐)) |
7 | | simprr 772 |
. . . . . . 7
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ ๐) |
8 | | axcontlem10.1 |
. . . . . . . 8
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} |
9 | | axcontlem10.2 |
. . . . . . . 8
โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} |
10 | 8, 9 | axcontlem2 27963 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โ ๐น:๐ทโ1-1-ontoโ(0[,)+โ)) |
11 | 2, 3, 6, 7, 10 | syl31anc 1374 |
. . . . . 6
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐น:๐ทโ1-1-ontoโ(0[,)+โ)) |
12 | | f1ofo 6795 |
. . . . . 6
โข (๐น:๐ทโ1-1-ontoโ(0[,)+โ) โ ๐น:๐ทโontoโ(0[,)+โ)) |
13 | | forn 6763 |
. . . . . 6
โข (๐น:๐ทโontoโ(0[,)+โ) โ ran ๐น = (0[,)+โ)) |
14 | 11, 12, 13 | 3syl 18 |
. . . . 5
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ran ๐น = (0[,)+โ)) |
15 | 1, 14 | sseqtrid 4000 |
. . . 4
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐น โ ๐ด) โ (0[,)+โ)) |
16 | | rge0ssre 13382 |
. . . 4
โข
(0[,)+โ) โ โ |
17 | 15, 16 | sstrdi 3960 |
. . 3
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐น โ ๐ด) โ โ) |
18 | | imassrn 6028 |
. . . . 5
โข (๐น โ ๐ต) โ ran ๐น |
19 | 18, 14 | sseqtrid 4000 |
. . . 4
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐น โ ๐ต) โ (0[,)+โ)) |
20 | 19, 16 | sstrdi 3960 |
. . 3
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐น โ ๐ต) โ โ) |
21 | 8, 9 | axcontlem9 27970 |
. . 3
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)๐ โค ๐) |
22 | | dedekindle 11327 |
. . 3
โข (((๐น โ ๐ด) โ โ โง (๐น โ ๐ต) โ โ โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)๐ โค ๐) โ โ๐ โ โ โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) |
23 | 17, 20, 21, 22 | syl3anc 1372 |
. 2
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ โ๐ โ โ โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) |
24 | | simpr 486 |
. . . . . . . 8
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง ๐ โ โ) โ ๐ โ โ) |
25 | | simprl3 1221 |
. . . . . . . . . . 11
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ต โ โ
) |
26 | 25 | ad2antrr 725 |
. . . . . . . . . 10
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง ๐ โ โ) โ ๐ต โ โ
) |
27 | | n0 4310 |
. . . . . . . . . 10
โข (๐ต โ โ
โ
โ๐ ๐ โ ๐ต) |
28 | 26, 27 | sylib 217 |
. . . . . . . . 9
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง ๐ โ โ) โ โ๐ ๐ โ ๐ต) |
29 | | 0red 11166 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โ 0 โ โ) |
30 | | f1of 6788 |
. . . . . . . . . . . . . . . 16
โข (๐น:๐ทโ1-1-ontoโ(0[,)+โ) โ ๐น:๐ทโถ(0[,)+โ)) |
31 | 11, 30 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐น:๐ทโถ(0[,)+โ)) |
32 | 8 | axcontlem4 27965 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ด โ ๐ท) |
33 | 32, 5 | sseldd 3949 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ ๐ท) |
34 | 31, 33 | ffvelcdmd 7040 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐นโ๐) โ (0[,)+โ)) |
35 | 16, 34 | sselid 3946 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐นโ๐) โ โ) |
36 | 35 | ad2antrr 725 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โ (๐นโ๐) โ โ) |
37 | | simprl 770 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โ ๐ โ โ) |
38 | | elrege0 13380 |
. . . . . . . . . . . . . . 15
โข ((๐นโ๐) โ (0[,)+โ) โ ((๐นโ๐) โ โ โง 0 โค (๐นโ๐))) |
39 | 38 | simprbi 498 |
. . . . . . . . . . . . . 14
โข ((๐นโ๐) โ (0[,)+โ) โ 0 โค (๐นโ๐)) |
40 | 34, 39 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ 0 โค (๐นโ๐)) |
41 | 40 | ad2antrr 725 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โ 0 โค (๐นโ๐)) |
42 | | f1of1 6787 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐น:๐ทโ1-1-ontoโ(0[,)+โ) โ ๐น:๐ทโ1-1โ(0[,)+โ)) |
43 | 11, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐น:๐ทโ1-1โ(0[,)+โ)) |
44 | | f1elima 7214 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐น:๐ทโ1-1โ(0[,)+โ) โง ๐ โ ๐ท โง ๐ด โ ๐ท) โ ((๐นโ๐) โ (๐น โ ๐ด) โ ๐ โ ๐ด)) |
45 | 43, 33, 32, 44 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ((๐นโ๐) โ (๐น โ ๐ด) โ ๐ โ ๐ด)) |
46 | 5, 45 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐นโ๐) โ (๐น โ ๐ด)) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โ (๐นโ๐) โ (๐น โ ๐ด)) |
48 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
49 | 43 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ๐ โ ๐ต) โ ๐น:๐ทโ1-1โ(0[,)+โ)) |
50 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐) โ ๐ โ (๐ผโ๐)) |
51 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐) โ ๐ โ ๐ด) |
52 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐) โ ๐ โ ๐) |
53 | 50, 51, 52 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐) โ (๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ โ ๐)) |
54 | 8 | axcontlem3 27964 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง (๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ โ ๐)) โ ๐ต โ ๐ท) |
55 | 53, 54 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ต โ ๐ท) |
56 | 55 | sselda 3948 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ๐ โ ๐ต) โ ๐ โ ๐ท) |
57 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ๐ โ ๐ต) โ ๐ต โ ๐ท) |
58 | | f1elima 7214 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐น:๐ทโ1-1โ(0[,)+โ) โง ๐ โ ๐ท โง ๐ต โ ๐ท) โ ((๐นโ๐) โ (๐น โ ๐ต) โ ๐ โ ๐ต)) |
59 | 49, 56, 57, 58 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ๐ โ ๐ต) โ ((๐นโ๐) โ (๐น โ ๐ต) โ ๐ โ ๐ต)) |
60 | 48, 59 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ๐ โ ๐ต) โ (๐นโ๐) โ (๐น โ ๐ต)) |
61 | 60 | adantrl 715 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โ (๐นโ๐) โ (๐น โ ๐ต)) |
62 | 47, 61 | jca 513 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โ ((๐นโ๐) โ (๐น โ ๐ด) โง (๐นโ๐) โ (๐น โ ๐ต))) |
63 | | breq1 5112 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐นโ๐) โ (๐ โค ๐ โ (๐นโ๐) โค ๐)) |
64 | 63 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐นโ๐) โ ((๐ โค ๐ โง ๐ โค ๐) โ ((๐นโ๐) โค ๐ โง ๐ โค ๐))) |
65 | | breq2 5113 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐นโ๐) โ (๐ โค ๐ โ ๐ โค (๐นโ๐))) |
66 | 65 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐นโ๐) โ (((๐นโ๐) โค ๐ โง ๐ โค ๐) โ ((๐นโ๐) โค ๐ โง ๐ โค (๐นโ๐)))) |
67 | 64, 66 | rspc2va 3593 |
. . . . . . . . . . . . . . 15
โข ((((๐นโ๐) โ (๐น โ ๐ด) โง (๐นโ๐) โ (๐น โ ๐ต)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โ ((๐นโ๐) โค ๐ โง ๐ โค (๐นโ๐))) |
68 | 62, 67 | sylan 581 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โ ((๐นโ๐) โค ๐ โง ๐ โค (๐นโ๐))) |
69 | 68 | an32s 651 |
. . . . . . . . . . . . 13
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โ ((๐นโ๐) โค ๐ โง ๐ โค (๐นโ๐))) |
70 | 69 | simpld 496 |
. . . . . . . . . . . 12
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โ (๐นโ๐) โค ๐) |
71 | 29, 36, 37, 41, 70 | letrd 11320 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง (๐ โ โ โง ๐ โ ๐ต)) โ 0 โค ๐) |
72 | 71 | expr 458 |
. . . . . . . . . 10
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง ๐ โ โ) โ (๐ โ ๐ต โ 0 โค ๐)) |
73 | 72 | exlimdv 1937 |
. . . . . . . . 9
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง ๐ โ โ) โ (โ๐ ๐ โ ๐ต โ 0 โค ๐)) |
74 | 28, 73 | mpd 15 |
. . . . . . . 8
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง ๐ โ โ) โ 0 โค ๐) |
75 | | elrege0 13380 |
. . . . . . . 8
โข (๐ โ (0[,)+โ) โ
(๐ โ โ โง 0
โค ๐)) |
76 | 24, 74, 75 | sylanbrc 584 |
. . . . . . 7
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โง ๐ โ โ) โ ๐ โ (0[,)+โ)) |
77 | 76 | ex 414 |
. . . . . 6
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โ (๐ โ โ โ ๐ โ (0[,)+โ))) |
78 | 8 | ssrab3 4044 |
. . . . . . . . 9
โข ๐ท โ (๐ผโ๐) |
79 | | simpr 486 |
. . . . . . . . . 10
โข
((โ๐ โ
(๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โ ๐ โ
(0[,)+โ)) |
80 | | f1ocnvdm 7235 |
. . . . . . . . . 10
โข ((๐น:๐ทโ1-1-ontoโ(0[,)+โ) โง ๐ โ (0[,)+โ)) โ (โก๐นโ๐) โ ๐ท) |
81 | 11, 79, 80 | syl2an 597 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ))) โ (โก๐นโ๐) โ ๐ท) |
82 | 78, 81 | sselid 3946 |
. . . . . . . 8
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ))) โ (โก๐นโ๐) โ (๐ผโ๐)) |
83 | 2, 3, 6 | 3jca 1129 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐))) |
84 | 83, 7 | jca 513 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐)) |
85 | 84 | adantr 482 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ ((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐)) |
86 | 32 | sselda 3948 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ๐ โ ๐ด) โ ๐ โ ๐ท) |
87 | 86 | adantrr 716 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โ ๐ท) |
88 | 87 | adantrl 715 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ ๐ โ ๐ท) |
89 | | simplr 768 |
. . . . . . . . . . . . . . 15
โข
(((โ๐ โ
(๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โ (0[,)+โ)) |
90 | 11, 89, 80 | syl2an 597 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ (โก๐นโ๐) โ ๐ท) |
91 | 55 | sselda 3948 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ๐ โ ๐ต) โ ๐ โ ๐ท) |
92 | 91 | adantrl 715 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โ ๐ท) |
93 | 92 | adantrl 715 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ ๐ โ ๐ท) |
94 | 88, 90, 93 | 3jca 1129 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ (๐ โ ๐ท โง (โก๐นโ๐) โ ๐ท โง ๐ โ ๐ท)) |
95 | 85, 94 | jca 513 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ (((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง (โก๐นโ๐) โ ๐ท โง ๐ โ ๐ท))) |
96 | | f1ofun 6790 |
. . . . . . . . . . . . . . . . . . 19
โข (๐น:๐ทโ1-1-ontoโ(0[,)+โ) โ Fun ๐น) |
97 | 11, 96 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ Fun ๐น) |
98 | | fdm 6681 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐น:๐ทโถ(0[,)+โ) โ dom ๐น = ๐ท) |
99 | 11, 30, 98 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ dom ๐น = ๐ท) |
100 | 32, 99 | sseqtrrd 3989 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ด โ dom ๐น) |
101 | | funfvima2 7185 |
. . . . . . . . . . . . . . . . . 18
โข ((Fun
๐น โง ๐ด โ dom ๐น) โ (๐ โ ๐ด โ (๐นโ๐) โ (๐น โ ๐ด))) |
102 | 97, 100, 101 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐ โ ๐ด โ (๐นโ๐) โ (๐น โ ๐ด))) |
103 | 55, 99 | sseqtrrd 3989 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ต โ dom ๐น) |
104 | | funfvima2 7185 |
. . . . . . . . . . . . . . . . . 18
โข ((Fun
๐น โง ๐ต โ dom ๐น) โ (๐ โ ๐ต โ (๐นโ๐) โ (๐น โ ๐ต))) |
105 | 97, 103, 104 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐ โ ๐ต โ (๐นโ๐) โ (๐น โ ๐ต))) |
106 | 102, 105 | anim12d 610 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ((๐ โ ๐ด โง ๐ โ ๐ต) โ ((๐นโ๐) โ (๐น โ ๐ด) โง (๐นโ๐) โ (๐น โ ๐ต)))) |
107 | 106 | imp 408 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ((๐นโ๐) โ (๐น โ ๐ด) โง (๐นโ๐) โ (๐น โ ๐ต))) |
108 | 107 | adantrl 715 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ ((๐นโ๐) โ (๐น โ ๐ด) โง (๐นโ๐) โ (๐น โ ๐ต))) |
109 | | simprll 778 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) |
110 | | breq1 5112 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐นโ๐) โ (๐ โค ๐ โ (๐นโ๐) โค ๐)) |
111 | 110 | anbi1d 631 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐นโ๐) โ ((๐ โค ๐ โง ๐ โค ๐) โ ((๐นโ๐) โค ๐ โง ๐ โค ๐))) |
112 | | breq2 5113 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐นโ๐) โ (๐ โค ๐ โ ๐ โค (๐นโ๐))) |
113 | 112 | anbi2d 630 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐นโ๐) โ (((๐นโ๐) โค ๐ โง ๐ โค ๐) โ ((๐นโ๐) โค ๐ โง ๐ โค (๐นโ๐)))) |
114 | 111, 113 | rspc2v 3592 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ (๐น โ ๐ด) โง (๐นโ๐) โ (๐น โ ๐ต)) โ (โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โ ((๐นโ๐) โค ๐ โง ๐ โค (๐นโ๐)))) |
115 | 108, 109,
114 | sylc 65 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ ((๐นโ๐) โค ๐ โง ๐ โค (๐นโ๐))) |
116 | | f1ocnvfv2 7227 |
. . . . . . . . . . . . . . . 16
โข ((๐น:๐ทโ1-1-ontoโ(0[,)+โ) โง ๐ โ (0[,)+โ)) โ (๐นโ(โก๐นโ๐)) = ๐) |
117 | 11, 89, 116 | syl2an 597 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ (๐นโ(โก๐นโ๐)) = ๐) |
118 | 117 | breq2d 5121 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ ((๐นโ๐) โค (๐นโ(โก๐นโ๐)) โ (๐นโ๐) โค ๐)) |
119 | 117 | breq1d 5119 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ ((๐นโ(โก๐นโ๐)) โค (๐นโ๐) โ ๐ โค (๐นโ๐))) |
120 | 118, 119 | anbi12d 632 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ (((๐นโ๐) โค (๐นโ(โก๐นโ๐)) โง (๐นโ(โก๐นโ๐)) โค (๐นโ๐)) โ ((๐นโ๐) โค ๐ โง ๐ โค (๐นโ๐)))) |
121 | 115, 120 | mpbird 257 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ ((๐นโ๐) โค (๐นโ(โก๐นโ๐)) โง (๐นโ(โก๐นโ๐)) โค (๐นโ๐))) |
122 | 8, 9 | axcontlem8 27969 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง (โก๐นโ๐) โ ๐ท โง ๐ โ ๐ท)) โ (((๐นโ๐) โค (๐นโ(โก๐นโ๐)) โง (๐นโ(โก๐นโ๐)) โค (๐นโ๐)) โ (โก๐นโ๐) Btwn โจ๐, ๐โฉ)) |
123 | 95, 121, 122 | sylc 65 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง ((โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ)) โง (๐ โ ๐ด โง ๐ โ ๐ต))) โ (โก๐นโ๐) Btwn โจ๐, ๐โฉ) |
124 | 123 | anassrs 469 |
. . . . . . . . . 10
โข
(((((๐ โ
โ โง (๐ด โ
(๐ผโ๐) โง
๐ต โ
(๐ผโ๐) โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ))) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ (โก๐นโ๐) Btwn โจ๐, ๐โฉ) |
125 | 124 | ralrimivva 3194 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ))) โ โ๐ โ ๐ด โ๐ โ ๐ต (โก๐นโ๐) Btwn โจ๐, ๐โฉ) |
126 | | opeq1 4834 |
. . . . . . . . . . 11
โข (๐ = ๐ฅ โ โจ๐, ๐โฉ = โจ๐ฅ, ๐โฉ) |
127 | 126 | breq2d 5121 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ ((โก๐นโ๐) Btwn โจ๐, ๐โฉ โ (โก๐นโ๐) Btwn โจ๐ฅ, ๐โฉ)) |
128 | | opeq2 4835 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ โจ๐ฅ, ๐โฉ = โจ๐ฅ, ๐ฆโฉ) |
129 | 128 | breq2d 5121 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ ((โก๐นโ๐) Btwn โจ๐ฅ, ๐โฉ โ (โก๐นโ๐) Btwn โจ๐ฅ, ๐ฆโฉ)) |
130 | 127, 129 | cbvral2vw 3226 |
. . . . . . . . 9
โข
(โ๐ โ
๐ด โ๐ โ ๐ต (โก๐นโ๐) Btwn โจ๐, ๐โฉ โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต (โก๐นโ๐) Btwn โจ๐ฅ, ๐ฆโฉ) |
131 | 125, 130 | sylib 217 |
. . . . . . . 8
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ))) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต (โก๐นโ๐) Btwn โจ๐ฅ, ๐ฆโฉ) |
132 | | breq1 5112 |
. . . . . . . . . 10
โข (๐ = (โก๐นโ๐) โ (๐ Btwn โจ๐ฅ, ๐ฆโฉ โ (โก๐นโ๐) Btwn โจ๐ฅ, ๐ฆโฉ)) |
133 | 132 | 2ralbidv 3209 |
. . . . . . . . 9
โข (๐ = (โก๐นโ๐) โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต (โก๐นโ๐) Btwn โจ๐ฅ, ๐ฆโฉ)) |
134 | 133 | rspcev 3583 |
. . . . . . . 8
โข (((โก๐นโ๐) โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต (โก๐นโ๐) Btwn โจ๐ฅ, ๐ฆโฉ) โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ) |
135 | 82, 131, 134 | syl2anc 585 |
. . . . . . 7
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โง ๐ โ (0[,)+โ))) โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ) |
136 | 135 | expr 458 |
. . . . . 6
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โ (๐ โ (0[,)+โ) โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ)) |
137 | 77, 136 | syld 47 |
. . . . 5
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐)) โ (๐ โ โ โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ)) |
138 | 137 | ex 414 |
. . . 4
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โ (๐ โ โ โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ))) |
139 | 138 | com23 86 |
. . 3
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐ โ โ โ (โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ))) |
140 | 139 | rexlimdv 3147 |
. 2
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (โ๐ โ โ โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)(๐ โค ๐ โง ๐ โค ๐) โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ)) |
141 | 23, 140 | mpd 15 |
1
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ) |