Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . 5
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ โ) |
2 | | simprl1 1219 |
. . . . 5
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ (๐ผโ๐)) |
3 | | simplr1 1216 |
. . . . . 6
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ด โ (๐ผโ๐)) |
4 | | simprl2 1220 |
. . . . . 6
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ ๐ด) |
5 | 3, 4 | sseldd 3949 |
. . . . 5
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ (๐ผโ๐)) |
6 | | simprr 772 |
. . . . 5
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ โ ๐) |
7 | | axcontlem9.1 |
. . . . . 6
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} |
8 | | axcontlem9.2 |
. . . . . 6
โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} |
9 | 7, 8 | axcontlem2 27963 |
. . . . 5
โข (((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โ ๐น:๐ทโ1-1-ontoโ(0[,)+โ)) |
10 | 1, 2, 5, 6, 9 | syl31anc 1374 |
. . . 4
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐น:๐ทโ1-1-ontoโ(0[,)+โ)) |
11 | | f1ofun 6790 |
. . . 4
โข (๐น:๐ทโ1-1-ontoโ(0[,)+โ) โ Fun ๐น) |
12 | | fvelima 6912 |
. . . . 5
โข ((Fun
๐น โง ๐ โ (๐น โ ๐ด)) โ โ๐ โ ๐ด (๐นโ๐) = ๐) |
13 | 12 | ex 414 |
. . . 4
โข (Fun
๐น โ (๐ โ (๐น โ ๐ด) โ โ๐ โ ๐ด (๐นโ๐) = ๐)) |
14 | 10, 11, 13 | 3syl 18 |
. . 3
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐ โ (๐น โ ๐ด) โ โ๐ โ ๐ด (๐นโ๐) = ๐)) |
15 | | fvelima 6912 |
. . . . 5
โข ((Fun
๐น โง ๐ โ (๐น โ ๐ต)) โ โ๐ โ ๐ต (๐นโ๐) = ๐) |
16 | 15 | ex 414 |
. . . 4
โข (Fun
๐น โ (๐ โ (๐น โ ๐ต) โ โ๐ โ ๐ต (๐นโ๐) = ๐)) |
17 | 10, 11, 16 | 3syl 18 |
. . 3
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐ โ (๐น โ ๐ต) โ โ๐ โ ๐ต (๐นโ๐) = ๐)) |
18 | | reeanv 3216 |
. . . 4
โข
(โ๐ โ
๐ด โ๐ โ ๐ต ((๐นโ๐) = ๐ โง (๐นโ๐) = ๐) โ (โ๐ โ ๐ด (๐นโ๐) = ๐ โง โ๐ โ ๐ต (๐นโ๐) = ๐)) |
19 | | simplr3 1218 |
. . . . . . . 8
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ) |
20 | | breq1 5112 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (๐ฅ Btwn โจ๐, ๐ฆโฉ โ ๐ Btwn โจ๐, ๐ฆโฉ)) |
21 | | opeq2 4835 |
. . . . . . . . . 10
โข (๐ฆ = ๐ โ โจ๐, ๐ฆโฉ = โจ๐, ๐โฉ) |
22 | 21 | breq2d 5121 |
. . . . . . . . 9
โข (๐ฆ = ๐ โ (๐ Btwn โจ๐, ๐ฆโฉ โ ๐ Btwn โจ๐, ๐โฉ)) |
23 | 20, 22 | rspc2v 3592 |
. . . . . . . 8
โข ((๐ โ ๐ด โง ๐ โ ๐ต) โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ โ ๐ Btwn โจ๐, ๐โฉ)) |
24 | 19, 23 | mpan9 508 |
. . . . . . 7
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ Btwn โจ๐, ๐โฉ) |
25 | | simplll 774 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โ โ) |
26 | 2 | adantr 482 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โ (๐ผโ๐)) |
27 | 5 | adantr 482 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โ (๐ผโ๐)) |
28 | 25, 26, 27 | 3jca 1129 |
. . . . . . . 8
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ (๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐))) |
29 | | simplrr 777 |
. . . . . . . 8
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โ ๐) |
30 | 7 | axcontlem4 27965 |
. . . . . . . . . . 11
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ด โ ๐ท) |
31 | 30 | sseld 3947 |
. . . . . . . . . 10
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐ โ ๐ด โ ๐ โ ๐ท)) |
32 | | simpl 484 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ))) |
33 | 7 | axcontlem3 27964 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง (๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ โ ๐)) โ ๐ต โ ๐ท) |
34 | 32, 2, 4, 6, 33 | syl13anc 1373 |
. . . . . . . . . . 11
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ๐ต โ ๐ท) |
35 | 34 | sseld 3947 |
. . . . . . . . . 10
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (๐ โ ๐ต โ ๐ โ ๐ท)) |
36 | 31, 35 | anim12d 610 |
. . . . . . . . 9
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ((๐ โ ๐ด โง ๐ โ ๐ต) โ (๐ โ ๐ท โง ๐ โ ๐ท))) |
37 | 36 | imp 408 |
. . . . . . . 8
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ (๐ โ ๐ท โง ๐ โ ๐ท)) |
38 | 7, 8 | axcontlem7 27968 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ Btwn โจ๐, ๐โฉ โ (๐นโ๐) โค (๐นโ๐))) |
39 | 28, 29, 37, 38 | syl21anc 837 |
. . . . . . 7
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ (๐ Btwn โจ๐, ๐โฉ โ (๐นโ๐) โค (๐นโ๐))) |
40 | 24, 39 | mpbid 231 |
. . . . . 6
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ (๐นโ๐) โค (๐นโ๐)) |
41 | | breq12 5114 |
. . . . . 6
โข (((๐นโ๐) = ๐ โง (๐นโ๐) = ๐) โ ((๐นโ๐) โค (๐นโ๐) โ ๐ โค ๐)) |
42 | 40, 41 | syl5ibcom 244 |
. . . . 5
โข ((((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ (((๐นโ๐) = ๐ โง (๐นโ๐) = ๐) โ ๐ โค ๐)) |
43 | 42 | rexlimdvva 3202 |
. . . 4
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ (โ๐ โ ๐ด โ๐ โ ๐ต ((๐นโ๐) = ๐ โง (๐นโ๐) = ๐) โ ๐ โค ๐)) |
44 | 18, 43 | biimtrrid 242 |
. . 3
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ((โ๐ โ ๐ด (๐นโ๐) = ๐ โง โ๐ โ ๐ต (๐นโ๐) = ๐) โ ๐ โค ๐)) |
45 | 14, 17, 44 | syl2and 609 |
. 2
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ ((๐ โ (๐น โ ๐ด) โง ๐ โ (๐น โ ๐ต)) โ ๐ โค ๐)) |
46 | 45 | ralrimivv 3192 |
1
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ
) โง ๐ โ ๐)) โ โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)๐ โค ๐) |