Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
β’ (π β π β β) |
2 | | poimir.i |
. . 3
β’ πΌ = ((0[,]1) βm
(1...π)) |
3 | | poimir.r |
. . 3
β’ π
=
(βtβ((1...π) Γ {(topGenβran
(,))})) |
4 | | poimir.1 |
. . 3
β’ (π β πΉ β ((π
βΎt πΌ) Cn π
)) |
5 | | poimir.2 |
. . 3
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β ((πΉβπ§)βπ) β€ 0) |
6 | | poimir.3 |
. . 3
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β 0 β€ ((πΉβπ§)βπ)) |
7 | 1, 2, 3, 4, 5, 6 | poimirlem32 36139 |
. 2
β’ (π β βπ β πΌ βπ β (1...π)βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
8 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(1...π) β
V |
9 | | retopon 24143 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(topGenβran (,)) β (TopOnββ) |
10 | 3 | pttoponconst 22964 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((1...π) β V
β§ (topGenβran (,)) β (TopOnββ)) β π
β (TopOnβ(β
βm (1...π)))) |
11 | 8, 9, 10 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π
β (TopOnβ(β
βm (1...π))) |
12 | 11 | topontopi 22280 |
. . . . . . . . . . . . . . . . . . . 20
β’ π
β Top |
13 | | reex 11149 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ β
β V |
14 | | unitssre 13423 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (0[,]1)
β β |
15 | | mapss 8834 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((β
β V β§ (0[,]1) β β) β ((0[,]1) βm
(1...π)) β (β
βm (1...π))) |
16 | 13, 14, 15 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((0[,]1)
βm (1...π))
β (β βm (1...π)) |
17 | 2, 16 | eqsstri 3983 |
. . . . . . . . . . . . . . . . . . . 20
β’ πΌ β (β
βm (1...π)) |
18 | 11 | toponunii 22281 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β
βm (1...π))
= βͺ π
|
19 | 18 | restuni 22529 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β Top β§ πΌ β (β
βm (1...π))) β πΌ = βͺ (π
βΎt πΌ)) |
20 | 12, 17, 19 | mp2an 691 |
. . . . . . . . . . . . . . . . . . 19
β’ πΌ = βͺ
(π
βΎt
πΌ) |
21 | 20, 18 | cnf 22613 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β ((π
βΎt πΌ) Cn π
) β πΉ:πΌβΆ(β βm
(1...π))) |
22 | 4, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:πΌβΆ(β βm
(1...π))) |
23 | 22 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β πΌ) β (πΉβπ) β (β βm
(1...π))) |
24 | | elmapi 8794 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β (β βm
(1...π)) β (πΉβπ):(1...π)βΆβ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β πΌ) β (πΉβπ):(1...π)βΆβ) |
26 | 25 | ffvelcdmda 7040 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β πΌ) β§ π β (1...π)) β ((πΉβπ)βπ) β β) |
27 | | recn 11148 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ)βπ) β β β ((πΉβπ)βπ) β β) |
28 | | absrpcl 15180 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ)βπ) β β β§ ((πΉβπ)βπ) β 0) β (absβ((πΉβπ)βπ)) β
β+) |
29 | 28 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) β 0 β (absβ((πΉβπ)βπ)) β
β+)) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) β 0 β (absβ((πΉβπ)βπ)) β
β+)) |
31 | | ltsubrp 12958 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ)βπ) β β β§ (absβ((πΉβπ)βπ)) β β+) β
(((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ)βπ)) |
32 | | ltaddrp 12959 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ)βπ) β β β§ (absβ((πΉβπ)βπ)) β β+) β ((πΉβπ)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) |
33 | 31, 32 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ)βπ) β β β§ (absβ((πΉβπ)βπ)) β β+) β
((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ)βπ) β§ ((πΉβπ)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) |
34 | 33 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ)βπ) β β β ((absβ((πΉβπ)βπ)) β β+ β
((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ)βπ) β§ ((πΉβπ)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
35 | 30, 34 | syld 47 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) β 0 β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ)βπ) β§ ((πΉβπ)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
36 | 27 | abscld 15328 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉβπ)βπ) β β β (absβ((πΉβπ)βπ)) β β) |
37 | | resubcl 11472 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ)βπ) β β β§ (absβ((πΉβπ)βπ)) β β) β (((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) β β) |
38 | 36, 37 | mpdan 686 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) β β) |
39 | 38 | rexrd 11212 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) β
β*) |
40 | | readdcl 11141 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉβπ)βπ) β β β§ (absβ((πΉβπ)βπ)) β β) β (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) β β) |
41 | 36, 40 | mpdan 686 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) β β) |
42 | 41 | rexrd 11212 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) β
β*) |
43 | | rexr 11208 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ)βπ) β β β ((πΉβπ)βπ) β
β*) |
44 | | elioo5 13328 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) β β* β§ (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) β β* β§ ((πΉβπ)βπ) β β*) β (((πΉβπ)βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ)βπ) β§ ((πΉβπ)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
45 | 39, 42, 43, 44 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ)βπ) β§ ((πΉβπ)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
46 | 35, 45 | sylibrd 259 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) β 0 β ((πΉβπ)βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
47 | 26, 46 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((πΉβπ)βπ) β 0 β ((πΉβπ)βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
48 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
49 | 48 | fveq1d 6849 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β ((πΉβπ₯)βπ) = ((πΉβπ)βπ)) |
50 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β πΌ β¦ ((πΉβπ₯)βπ)) = (π₯ β πΌ β¦ ((πΉβπ₯)βπ)) |
51 | | fvex 6860 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ)βπ) β V |
52 | 49, 50, 51 | fvmpt 6953 |
. . . . . . . . . . . . . . 15
β’ (π β πΌ β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) = ((πΉβπ)βπ)) |
53 | 52 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π β πΌ β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β ((πΉβπ)βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
54 | 53 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β ((πΉβπ)βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
55 | 47, 54 | sylibrd 259 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((πΉβπ)βπ) β 0 β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
56 | | iooretop 24145 |
. . . . . . . . . . . . 13
β’ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β (topGenβran
(,)) |
57 | | resttopon 22528 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β (TopOnβ(β
βm (1...π))) β§ πΌ β (β βm
(1...π))) β (π
βΎt πΌ) β (TopOnβπΌ)) |
58 | 11, 17, 57 | mp2an 691 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
βΎt πΌ) β (TopOnβπΌ) |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β (π
βΎt πΌ) β (TopOnβπΌ)) |
60 | 22 | feqmptd 6915 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΉ = (π₯ β πΌ β¦ (πΉβπ₯))) |
61 | 60, 4 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π₯ β πΌ β¦ (πΉβπ₯)) β ((π
βΎt πΌ) Cn π
)) |
62 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β (π₯ β πΌ β¦ (πΉβπ₯)) β ((π
βΎt πΌ) Cn π
)) |
63 | 11 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β π
β (TopOnβ(β
βm (1...π)))) |
64 | | retop 24141 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(topGenβran (,)) β Top |
65 | 64 | fconst6 6737 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((1...π) Γ
{(topGenβran (,))}):(1...π)βΆTop |
66 | 18, 3 | ptpjcn 22978 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((1...π) β V
β§ ((1...π) Γ
{(topGenβran (,))}):(1...π)βΆTop β§ π β (1...π)) β (π§ β (β βm
(1...π)) β¦ (π§βπ)) β (π
Cn (((1...π) Γ {(topGenβran
(,))})βπ))) |
67 | 8, 65, 66 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β (π§ β (β βm
(1...π)) β¦ (π§βπ)) β (π
Cn (((1...π) Γ {(topGenβran
(,))})βπ))) |
68 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(topGenβran (,)) β V |
69 | 68 | fvconst2 7158 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...π) β (((1...π) Γ {(topGenβran
(,))})βπ) =
(topGenβran (,))) |
70 | 69 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β (π
Cn (((1...π) Γ {(topGenβran
(,))})βπ)) = (π
Cn (topGenβran
(,)))) |
71 | 67, 70 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β (π§ β (β βm
(1...π)) β¦ (π§βπ)) β (π
Cn (topGenβran
(,)))) |
72 | 71 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β (π§ β (β βm
(1...π)) β¦ (π§βπ)) β (π
Cn (topGenβran
(,)))) |
73 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (πΉβπ₯) β (π§βπ) = ((πΉβπ₯)βπ)) |
74 | 59, 62, 63, 72, 73 | cnmpt11 23030 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β (π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β ((π
βΎt πΌ) Cn (topGenβran
(,)))) |
75 | 20 | cncnpi 22645 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β ((π
βΎt πΌ) Cn (topGenβran (,))) β§ π β πΌ) β (π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β (((π
βΎt πΌ) CnP (topGenβran (,)))βπ)) |
76 | 74, 75 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (1...π)) β§ π β πΌ) β (π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β (((π
βΎt πΌ) CnP (topGenβran (,)))βπ)) |
77 | 76 | an32s 651 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β (((π
βΎt πΌ) CnP (topGenβran (,)))βπ)) |
78 | | iscnp 22604 |
. . . . . . . . . . . . . . . . 17
β’ (((π
βΎt πΌ) β (TopOnβπΌ) β§ (topGenβran (,))
β (TopOnββ) β§ π β πΌ) β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β (((π
βΎt πΌ) CnP (topGenβran (,)))βπ) β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)):πΌβΆβ β§ βπ§ β (topGenβran
(,))(((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β π§ β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β π§))))) |
79 | 58, 9, 78 | mp3an12 1452 |
. . . . . . . . . . . . . . . 16
β’ (π β πΌ β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β (((π
βΎt πΌ) CnP (topGenβran (,)))βπ) β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)):πΌβΆβ β§ βπ§ β (topGenβran
(,))(((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β π§ β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β π§))))) |
80 | 79 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β πΌ) β§ π β (1...π)) β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β (((π
βΎt πΌ) CnP (topGenβran (,)))βπ) β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)):πΌβΆβ β§ βπ§ β (topGenβran
(,))(((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β π§ β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β π§))))) |
81 | 77, 80 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β πΌ) β§ π β (1...π)) β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)):πΌβΆβ β§ βπ§ β (topGenβran
(,))(((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β π§ β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β π§)))) |
82 | 81 | simprd 497 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΌ) β§ π β (1...π)) β βπ§ β (topGenβran (,))(((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β π§ β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β π§))) |
83 | | eleq2 2827 |
. . . . . . . . . . . . . . 15
β’ (π§ = ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β π§ β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
84 | | sseq2 3975 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β π§ β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
85 | 84 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π§ = ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β ((π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β π§) β (π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))))) |
86 | 85 | rexbidv 3176 |
. . . . . . . . . . . . . . 15
β’ (π§ = ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β (βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β π§) β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))))) |
87 | 83, 86 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π§ = ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β ((((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β π§ β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β π§)) β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))))) |
88 | 87 | rspcv 3580 |
. . . . . . . . . . . . 13
β’
(((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β (topGenβran (,)) β
(βπ§ β
(topGenβran (,))(((π₯
β πΌ β¦ ((πΉβπ₯)βπ))βπ) β π§ β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β π§)) β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))))) |
89 | 56, 82, 88 | mpsyl 68 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))))) |
90 | 55, 89 | syld 47 |
. . . . . . . . . . 11
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((πΉβπ)βπ) β 0 β βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))))) |
91 | | 0re 11164 |
. . . . . . . . . . . 12
β’ 0 β
β |
92 | | letric 11262 |
. . . . . . . . . . . 12
β’ ((((πΉβπ)βπ) β β β§ 0 β β)
β (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))) |
93 | 26, 91, 92 | sylancl 587 |
. . . . . . . . . . 11
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))) |
94 | 90, 93 | jctird 528 |
. . . . . . . . . 10
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((πΉβπ)βπ) β 0 β (βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))))) |
95 | | r19.41v 3186 |
. . . . . . . . . . 11
β’
(βπ£ β
(π
βΎt
πΌ)((π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))) β (βπ£ β (π
βΎt πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ)))) |
96 | | anass 470 |
. . . . . . . . . . . 12
β’ (((π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))) β (π β π£ β§ (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))))) |
97 | 96 | rexbii 3098 |
. . . . . . . . . . 11
β’
(βπ£ β
(π
βΎt
πΌ)((π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))) β βπ£ β (π
βΎt πΌ)(π β π£ β§ (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))))) |
98 | 95, 97 | bitr3i 277 |
. . . . . . . . . 10
β’
((βπ£ β
(π
βΎt
πΌ)(π β π£ β§ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))) β βπ£ β (π
βΎt πΌ)(π β π£ β§ (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))))) |
99 | 94, 98 | syl6ib 251 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((πΉβπ)βπ) β 0 β βπ£ β (π
βΎt πΌ)(π β π£ β§ (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ)))))) |
100 | 58 | topontopi 22280 |
. . . . . . . . . . . . 13
β’ (π
βΎt πΌ) β Top |
101 | 20 | eltopss 22272 |
. . . . . . . . . . . . 13
β’ (((π
βΎt πΌ) β Top β§ π£ β (π
βΎt πΌ)) β π£ β πΌ) |
102 | 100, 101 | mpan 689 |
. . . . . . . . . . . 12
β’ (π£ β (π
βΎt πΌ) β π£ β πΌ) |
103 | | fvex 6860 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ₯)βπ) β V |
104 | 103, 50 | dmmpti 6650 |
. . . . . . . . . . . . . . . . 17
β’ dom
(π₯ β πΌ β¦ ((πΉβπ₯)βπ)) = πΌ |
105 | 104 | sseq2i 3978 |
. . . . . . . . . . . . . . . 16
β’ (π£ β dom (π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£ β πΌ) |
106 | | funmpt 6544 |
. . . . . . . . . . . . . . . . 17
β’ Fun
(π₯ β πΌ β¦ ((πΉβπ₯)βπ)) |
107 | | funimass4 6912 |
. . . . . . . . . . . . . . . . 17
β’ ((Fun
(π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β§ π£ β dom (π₯ β πΌ β¦ ((πΉβπ₯)βπ))) β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ§ β π£ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ§) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
108 | 106, 107 | mpan 689 |
. . . . . . . . . . . . . . . 16
β’ (π£ β dom (π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ§ β π£ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ§) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
109 | 105, 108 | sylbir 234 |
. . . . . . . . . . . . . . 15
β’ (π£ β πΌ β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ§ β π£ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ§) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
110 | | ssel2 3944 |
. . . . . . . . . . . . . . . . 17
β’ ((π£ β πΌ β§ π§ β π£) β π§ β πΌ) |
111 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
112 | 111 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π§ β ((πΉβπ₯)βπ) = ((πΉβπ§)βπ)) |
113 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉβπ§)βπ) β V |
114 | 112, 50, 113 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β πΌ β ((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ§) = ((πΉβπ§)βπ)) |
115 | 114 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β πΌ β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ§) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β ((πΉβπ§)βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
116 | | eliooord 13330 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉβπ§)βπ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) |
117 | 115, 116 | syl6bi 253 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β πΌ β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ§) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
118 | 110, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π£ β πΌ β§ π§ β π£) β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ§) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
119 | 118 | ralimdva 3165 |
. . . . . . . . . . . . . . 15
β’ (π£ β πΌ β (βπ§ β π£ ((π₯ β πΌ β¦ ((πΉβπ₯)βπ))βπ§) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
120 | 109, 119 | sylbid 239 |
. . . . . . . . . . . . . 14
β’ (π£ β πΌ β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
121 | 120 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β πΌ) β§ π β (1...π)) β§ π£ β πΌ) β (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))))) |
122 | | absnid 15190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((πΉβπ)βπ) β β β§ ((πΉβπ)βπ) β€ 0) β (absβ((πΉβπ)βπ)) = -((πΉβπ)βπ)) |
123 | 122 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((πΉβπ)βπ) β β β§ ((πΉβπ)βπ) β€ 0) β (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) = (((πΉβπ)βπ) + -((πΉβπ)βπ))) |
124 | 27 | negidd 11509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) + -((πΉβπ)βπ)) = 0) |
125 | 124 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((πΉβπ)βπ) β β β§ ((πΉβπ)βπ) β€ 0) β (((πΉβπ)βπ) + -((πΉβπ)βπ)) = 0) |
126 | 123, 125 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((πΉβπ)βπ) β β β§ ((πΉβπ)βπ) β€ 0) β (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) = 0) |
127 | 26, 126 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β πΌ) β§ π β (1...π)) β§ ((πΉβπ)βπ) β€ 0) β (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) = 0) |
128 | 127 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ ((πΉβπ)βπ) β€ 0) β§ π§ β πΌ) β (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) = 0) |
129 | 128 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ ((πΉβπ)βπ) β€ 0) β§ π§ β πΌ) β (((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) β ((πΉβπ§)βπ) < 0)) |
130 | 22 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π§ β πΌ) β (πΉβπ§) β (β βm
(1...π))) |
131 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΉβπ§) β (β βm
(1...π)) β (πΉβπ§):(1...π)βΆβ) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π§ β πΌ) β (πΉβπ§):(1...π)βΆβ) |
133 | 132 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π§ β πΌ) β§ π β (1...π)) β ((πΉβπ§)βπ) β β) |
134 | 133 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (1...π)) β§ π§ β πΌ) β ((πΉβπ§)βπ) β β) |
135 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (1...π)) β§ π§ β πΌ) β 0 β β) |
136 | 134, 135 | ltnled 11309 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (1...π)) β§ π§ β πΌ) β (((πΉβπ§)βπ) < 0 β Β¬ 0 β€ ((πΉβπ§)βπ))) |
137 | 136 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β πΌ) β§ π β (1...π)) β§ π§ β πΌ) β (((πΉβπ§)βπ) < 0 β Β¬ 0 β€ ((πΉβπ§)βπ))) |
138 | 137 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ ((πΉβπ)βπ) β€ 0) β§ π§ β πΌ) β (((πΉβπ§)βπ) < 0 β Β¬ 0 β€ ((πΉβπ§)βπ))) |
139 | 129, 138 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ ((πΉβπ)βπ) β€ 0) β§ π§ β πΌ) β (((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) β Β¬ 0 β€ ((πΉβπ§)βπ))) |
140 | 139 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ ((πΉβπ)βπ) β€ 0) β§ π§ β πΌ) β (((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) β Β¬ 0 β€ ((πΉβπ§)βπ))) |
141 | 110, 140 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ ((πΉβπ)βπ) β€ 0) β§ (π£ β πΌ β§ π§ β π£)) β (((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) β Β¬ 0 β€ ((πΉβπ§)βπ))) |
142 | 141 | anassrs 469 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π β πΌ) β§ π β (1...π)) β§ ((πΉβπ)βπ) β€ 0) β§ π£ β πΌ) β§ π§ β π£) β (((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))) β Β¬ 0 β€ ((πΉβπ§)βπ))) |
143 | 142 | adantld 492 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π β πΌ) β§ π β (1...π)) β§ ((πΉβπ)βπ) β€ 0) β§ π£ β πΌ) β§ π§ β π£) β (((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β Β¬ 0 β€ ((πΉβπ§)βπ))) |
144 | 143 | ralimdva 3165 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ ((πΉβπ)βπ) β€ 0) β§ π£ β πΌ) β (βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ))) |
145 | 144 | an32s 651 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ π£ β πΌ) β§ ((πΉβπ)βπ) β€ 0) β (βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ))) |
146 | 145 | impancom 453 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ π£ β πΌ) β§ βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) β (((πΉβπ)βπ) β€ 0 β βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ))) |
147 | | absid 15188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((πΉβπ)βπ) β β β§ 0 β€ ((πΉβπ)βπ)) β (absβ((πΉβπ)βπ)) = ((πΉβπ)βπ)) |
148 | 147 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((πΉβπ)βπ) β β β§ 0 β€ ((πΉβπ)βπ)) β (((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) = (((πΉβπ)βπ) β ((πΉβπ)βπ))) |
149 | 27 | subidd 11507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πΉβπ)βπ) β β β (((πΉβπ)βπ) β ((πΉβπ)βπ)) = 0) |
150 | 149 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((πΉβπ)βπ) β β β§ 0 β€ ((πΉβπ)βπ)) β (((πΉβπ)βπ) β ((πΉβπ)βπ)) = 0) |
151 | 148, 150 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((πΉβπ)βπ) β β β§ 0 β€ ((πΉβπ)βπ)) β (((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) = 0) |
152 | 26, 151 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β πΌ) β§ π β (1...π)) β§ 0 β€ ((πΉβπ)βπ)) β (((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) = 0) |
153 | 152 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ 0 β€ ((πΉβπ)βπ)) β§ π§ β πΌ) β (((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) = 0) |
154 | 153 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ 0 β€ ((πΉβπ)βπ)) β§ π§ β πΌ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β 0 < ((πΉβπ§)βπ))) |
155 | 135, 134 | ltnled 11309 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (1...π)) β§ π§ β πΌ) β (0 < ((πΉβπ§)βπ) β Β¬ ((πΉβπ§)βπ) β€ 0)) |
156 | 155 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β πΌ) β§ π β (1...π)) β§ π§ β πΌ) β (0 < ((πΉβπ§)βπ) β Β¬ ((πΉβπ§)βπ) β€ 0)) |
157 | 156 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ 0 β€ ((πΉβπ)βπ)) β§ π§ β πΌ) β (0 < ((πΉβπ§)βπ) β Β¬ ((πΉβπ§)βπ) β€ 0)) |
158 | 154, 157 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ 0 β€ ((πΉβπ)βπ)) β§ π§ β πΌ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β Β¬ ((πΉβπ§)βπ) β€ 0)) |
159 | 158 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ 0 β€ ((πΉβπ)βπ)) β§ π§ β πΌ) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β Β¬ ((πΉβπ§)βπ) β€ 0)) |
160 | 110, 159 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ 0 β€ ((πΉβπ)βπ)) β§ (π£ β πΌ β§ π§ β π£)) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β Β¬ ((πΉβπ§)βπ) β€ 0)) |
161 | 160 | anassrs 469 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π β πΌ) β§ π β (1...π)) β§ 0 β€ ((πΉβπ)βπ)) β§ π£ β πΌ) β§ π§ β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β Β¬ ((πΉβπ§)βπ) β€ 0)) |
162 | 161 | adantrd 493 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π β πΌ) β§ π β (1...π)) β§ 0 β€ ((πΉβπ)βπ)) β§ π£ β πΌ) β§ π§ β π£) β (((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β Β¬ ((πΉβπ§)βπ) β€ 0)) |
163 | 162 | ralimdva 3165 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ 0 β€ ((πΉβπ)βπ)) β§ π£ β πΌ) β (βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)) |
164 | 163 | an32s 651 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ π£ β πΌ) β§ 0 β€ ((πΉβπ)βπ)) β (βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)) |
165 | 164 | impancom 453 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ π£ β πΌ) β§ βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) β (0 β€ ((πΉβπ)βπ) β βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)) |
166 | 146, 165 | orim12d 964 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β πΌ) β§ π β (1...π)) β§ π£ β πΌ) β§ βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ))))) β ((((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ)) β (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0))) |
167 | 166 | expimpd 455 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β πΌ) β§ π β (1...π)) β§ π£ β πΌ) β ((βπ§ β π£ ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ))) < ((πΉβπ§)βπ) β§ ((πΉβπ§)βπ) < (((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))) β (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0))) |
168 | 121, 167 | syland 604 |
. . . . . . . . . . . 12
β’ ((((π β§ π β πΌ) β§ π β (1...π)) β§ π£ β πΌ) β ((((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))) β (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0))) |
169 | 102, 168 | sylan2 594 |
. . . . . . . . . . 11
β’ ((((π β§ π β πΌ) β§ π β (1...π)) β§ π£ β (π
βΎt πΌ)) β ((((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ))) β (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0))) |
170 | 169 | anim2d 613 |
. . . . . . . . . 10
β’ ((((π β§ π β πΌ) β§ π β (1...π)) β§ π£ β (π
βΎt πΌ)) β ((π β π£ β§ (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ)))) β (π β π£ β§ (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)))) |
171 | 170 | reximdva 3166 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (βπ£ β (π
βΎt πΌ)(π β π£ β§ (((π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β π£) β ((((πΉβπ)βπ) β (absβ((πΉβπ)βπ)))(,)(((πΉβπ)βπ) + (absβ((πΉβπ)βπ)))) β§ (((πΉβπ)βπ) β€ 0 β¨ 0 β€ ((πΉβπ)βπ)))) β βπ£ β (π
βΎt πΌ)(π β π£ β§ (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)))) |
172 | 99, 171 | syld 47 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((πΉβπ)βπ) β 0 β βπ£ β (π
βΎt πΌ)(π β π£ β§ (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)))) |
173 | | ralnex 3076 |
. . . . . . . . . . . . . 14
β’
(βπ§ β
π£ Β¬ 0π((πΉβπ§)βπ) β Β¬ βπ§ β π£ 0π((πΉβπ§)βπ)) |
174 | 173 | rexbii 3098 |
. . . . . . . . . . . . 13
β’
(βπ β {
β€ , β‘ β€ }βπ§ β π£ Β¬ 0π((πΉβπ§)βπ) β βπ β { β€ , β‘ β€ } Β¬ βπ§ β π£ 0π((πΉβπ§)βπ)) |
175 | | letsr 18489 |
. . . . . . . . . . . . . . 15
β’ β€
β TosetRel |
176 | 175 | elexi 3467 |
. . . . . . . . . . . . . 14
β’ β€
β V |
177 | 176 | cnvex 7867 |
. . . . . . . . . . . . . 14
β’ β‘ β€ β V |
178 | | breq 5112 |
. . . . . . . . . . . . . . . 16
β’ (π = β€ β (0π((πΉβπ§)βπ) β 0 β€ ((πΉβπ§)βπ))) |
179 | 178 | notbid 318 |
. . . . . . . . . . . . . . 15
β’ (π = β€ β (Β¬ 0π((πΉβπ§)βπ) β Β¬ 0 β€ ((πΉβπ§)βπ))) |
180 | 179 | ralbidv 3175 |
. . . . . . . . . . . . . 14
β’ (π = β€ β (βπ§ β π£ Β¬ 0π((πΉβπ§)βπ) β βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ))) |
181 | | breq 5112 |
. . . . . . . . . . . . . . . . 17
β’ (π = β‘ β€ β (0π((πΉβπ§)βπ) β 0β‘ β€ ((πΉβπ§)βπ))) |
182 | | c0ex 11156 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
V |
183 | 182, 113 | brcnv 5843 |
. . . . . . . . . . . . . . . . 17
β’ (0β‘ β€ ((πΉβπ§)βπ) β ((πΉβπ§)βπ) β€ 0) |
184 | 181, 183 | bitrdi 287 |
. . . . . . . . . . . . . . . 16
β’ (π = β‘ β€ β (0π((πΉβπ§)βπ) β ((πΉβπ§)βπ) β€ 0)) |
185 | 184 | notbid 318 |
. . . . . . . . . . . . . . 15
β’ (π = β‘ β€ β (Β¬ 0π((πΉβπ§)βπ) β Β¬ ((πΉβπ§)βπ) β€ 0)) |
186 | 185 | ralbidv 3175 |
. . . . . . . . . . . . . 14
β’ (π = β‘ β€ β (βπ§ β π£ Β¬ 0π((πΉβπ§)βπ) β βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)) |
187 | 176, 177,
180, 186 | rexpr 4667 |
. . . . . . . . . . . . 13
β’
(βπ β {
β€ , β‘ β€ }βπ§ β π£ Β¬ 0π((πΉβπ§)βπ) β (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)) |
188 | | rexnal 3104 |
. . . . . . . . . . . . 13
β’
(βπ β {
β€ , β‘ β€ } Β¬ βπ§ β π£ 0π((πΉβπ§)βπ) β Β¬ βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) |
189 | 174, 187,
188 | 3bitr3i 301 |
. . . . . . . . . . . 12
β’
((βπ§ β
π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0) β Β¬ βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) |
190 | 189 | anbi2i 624 |
. . . . . . . . . . 11
β’ ((π β π£ β§ (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)) β (π β π£ β§ Β¬ βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
191 | | annim 405 |
. . . . . . . . . . 11
β’ ((π β π£ β§ Β¬ βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) β Β¬ (π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
192 | 190, 191 | bitri 275 |
. . . . . . . . . 10
β’ ((π β π£ β§ (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)) β Β¬ (π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
193 | 192 | rexbii 3098 |
. . . . . . . . 9
β’
(βπ£ β
(π
βΎt
πΌ)(π β π£ β§ (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)) β βπ£ β (π
βΎt πΌ) Β¬ (π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
194 | | rexnal 3104 |
. . . . . . . . 9
β’
(βπ£ β
(π
βΎt
πΌ) Β¬ (π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) β Β¬ βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
195 | 193, 194 | bitri 275 |
. . . . . . . 8
β’
(βπ£ β
(π
βΎt
πΌ)(π β π£ β§ (βπ§ β π£ Β¬ 0 β€ ((πΉβπ§)βπ) β¨ βπ§ β π£ Β¬ ((πΉβπ§)βπ) β€ 0)) β Β¬ βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
196 | 172, 195 | syl6ib 251 |
. . . . . . 7
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((πΉβπ)βπ) β 0 β Β¬ βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) |
197 | 196 | necon4ad 2963 |
. . . . . 6
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) β ((πΉβπ)βπ) = 0)) |
198 | 197 | ralimdva 3165 |
. . . . 5
β’ ((π β§ π β πΌ) β (βπ β (1...π)βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) β βπ β (1...π)((πΉβπ)βπ) = 0)) |
199 | 25 | ffnd 6674 |
. . . . 5
β’ ((π β§ π β πΌ) β (πΉβπ) Fn (1...π)) |
200 | 198, 199 | jctild 527 |
. . . 4
β’ ((π β§ π β πΌ) β (βπ β (1...π)βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) β ((πΉβπ) Fn (1...π) β§ βπ β (1...π)((πΉβπ)βπ) = 0))) |
201 | | fconstfv 7167 |
. . . . 5
β’ ((πΉβπ):(1...π)βΆ{0} β ((πΉβπ) Fn (1...π) β§ βπ β (1...π)((πΉβπ)βπ) = 0)) |
202 | 182 | fconst2 7159 |
. . . . 5
β’ ((πΉβπ):(1...π)βΆ{0} β (πΉβπ) = ((1...π) Γ {0})) |
203 | 201, 202 | bitr3i 277 |
. . . 4
β’ (((πΉβπ) Fn (1...π) β§ βπ β (1...π)((πΉβπ)βπ) = 0) β (πΉβπ) = ((1...π) Γ {0})) |
204 | 200, 203 | syl6ib 251 |
. . 3
β’ ((π β§ π β πΌ) β (βπ β (1...π)βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) β (πΉβπ) = ((1...π) Γ {0}))) |
205 | 204 | reximdva 3166 |
. 2
β’ (π β (βπ β πΌ βπ β (1...π)βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) β βπ β πΌ (πΉβπ) = ((1...π) Γ {0}))) |
206 | 7, 205 | mpd 15 |
1
β’ (π β βπ β πΌ (πΉβπ) = ((1...π) Γ {0})) |