Step | Hyp | Ref
| Expression |
1 | | stoweidlem57.2 |
. . . . . . . . . 10
β’
β²π‘π |
2 | | stoweidlem57.3 |
. . . . . . . . . . 11
β’
β²π‘π |
3 | | stoweidlem57.1 |
. . . . . . . . . . . 12
β’
β²π‘π· |
4 | 3 | nfcri 2885 |
. . . . . . . . . . 11
β’
β²π‘ π β π· |
5 | 2, 4 | nfan 1895 |
. . . . . . . . . 10
β’
β²π‘(π β§ π β π·) |
6 | | stoweidlem57.6 |
. . . . . . . . . 10
β’ πΎ = (topGenβran
(,)) |
7 | | stoweidlem57.10 |
. . . . . . . . . . 11
β’ (π β π½ β Comp) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β π½ β Comp) |
9 | | stoweidlem57.7 |
. . . . . . . . . 10
β’ π = βͺ
π½ |
10 | | stoweidlem57.8 |
. . . . . . . . . 10
β’ πΆ = (π½ Cn πΎ) |
11 | | stoweidlem57.11 |
. . . . . . . . . . 11
β’ (π β π΄ β πΆ) |
12 | 11 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β π΄ β πΆ) |
13 | | stoweidlem57.12 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
14 | 13 | 3adant1r 1175 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
15 | | stoweidlem57.13 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
16 | 15 | 3adant1r 1175 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
17 | | stoweidlem57.14 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) |
18 | 17 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β β) β (π‘ β π β¦ π) β π΄) |
19 | | stoweidlem57.15 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
20 | 19 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
21 | | stoweidlem57.9 |
. . . . . . . . . . . 12
β’ π = (π β π΅) |
22 | | stoweidlem57.16 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β (Clsdβπ½)) |
23 | | cmptop 23286 |
. . . . . . . . . . . . . . 15
β’ (π½ β Comp β π½ β Top) |
24 | 9 | iscld 22918 |
. . . . . . . . . . . . . . 15
β’ (π½ β Top β (π΅ β (Clsdβπ½) β (π΅ β π β§ (π β π΅) β π½))) |
25 | 7, 23, 24 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β (π΅ β (Clsdβπ½) β (π΅ β π β§ (π β π΅) β π½))) |
26 | 22, 25 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β (π΅ β π β§ (π β π΅) β π½)) |
27 | 26 | simprd 495 |
. . . . . . . . . . . 12
β’ (π β (π β π΅) β π½) |
28 | 21, 27 | eqeltrid 2832 |
. . . . . . . . . . 11
β’ (π β π β π½) |
29 | 28 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β π β π½) |
30 | | stoweidlem57.17 |
. . . . . . . . . . . . . 14
β’ (π β π· β (Clsdβπ½)) |
31 | 9 | cldss 22920 |
. . . . . . . . . . . . . 14
β’ (π· β (Clsdβπ½) β π· β π) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π· β π) |
33 | 32 | sselda 3978 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β π β π) |
34 | | stoweidlem57.18 |
. . . . . . . . . . . . . 14
β’ (π β (π΅ β© π·) = β
) |
35 | | disjr 4445 |
. . . . . . . . . . . . . 14
β’ ((π΅ β© π·) = β
β βπ β π· Β¬ π β π΅) |
36 | 34, 35 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β βπ β π· Β¬ π β π΅) |
37 | 36 | r19.21bi 3243 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β Β¬ π β π΅) |
38 | 33, 37 | eldifd 3955 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β π β (π β π΅)) |
39 | 38, 21 | eleqtrrdi 2839 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β π β π) |
40 | 1, 5, 6, 8, 9, 10,
12, 14, 16, 18, 20, 29, 39 | stoweidlem56 45367 |
. . . . . . . . 9
β’ ((π β§ π β π·) β βπ€ β π½ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) |
41 | | simpl 482 |
. . . . . . . . . . 11
β’ ((π€ β π½ β§ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) β π€ β π½) |
42 | | simprll 778 |
. . . . . . . . . . 11
β’ ((π€ β π½ β§ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) β π β π€) |
43 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π€ β π½ β§ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) β βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))) |
44 | | stoweidlem57.5 |
. . . . . . . . . . . . 13
β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} |
45 | 44 | reqabi 3449 |
. . . . . . . . . . . 12
β’ (π€ β π β (π€ β π½ β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) |
46 | 41, 43, 45 | sylanbrc 582 |
. . . . . . . . . . 11
β’ ((π€ β π½ β§ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) β π€ β π) |
47 | 41, 42, 46 | jca32 515 |
. . . . . . . . . 10
β’ ((π€ β π½ β§ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) β (π€ β π½ β§ (π β π€ β§ π€ β π))) |
48 | 47 | reximi2 3074 |
. . . . . . . . 9
β’
(βπ€ β
π½ ((π β π€ β§ π€ β π) β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))) β βπ€ β π½ (π β π€ β§ π€ β π)) |
49 | | rexex 3071 |
. . . . . . . . 9
β’
(βπ€ β
π½ (π β π€ β§ π€ β π) β βπ€(π β π€ β§ π€ β π)) |
50 | 40, 48, 49 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ π β π·) β βπ€(π β π€ β§ π€ β π)) |
51 | | nfcv 2898 |
. . . . . . . . 9
β’
β²π€π |
52 | | nfrab1 3446 |
. . . . . . . . . 10
β’
β²π€{π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} |
53 | 44, 52 | nfcxfr 2896 |
. . . . . . . . 9
β’
β²π€π |
54 | 51, 53 | elunif 44301 |
. . . . . . . 8
β’ (π β βͺ π
β βπ€(π β π€ β§ π€ β π)) |
55 | 50, 54 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β π·) β π β βͺ π) |
56 | 55 | ex 412 |
. . . . . 6
β’ (π β (π β π· β π β βͺ π)) |
57 | 56 | ssrdv 3984 |
. . . . 5
β’ (π β π· β βͺ π) |
58 | | cmpcld 23293 |
. . . . . . . 8
β’ ((π½ β Comp β§ π· β (Clsdβπ½)) β (π½ βΎt π·) β Comp) |
59 | 7, 30, 58 | syl2anc 583 |
. . . . . . 7
β’ (π β (π½ βΎt π·) β Comp) |
60 | 7, 23 | syl 17 |
. . . . . . . 8
β’ (π β π½ β Top) |
61 | 9 | cmpsub 23291 |
. . . . . . . 8
β’ ((π½ β Top β§ π· β π) β ((π½ βΎt π·) β Comp β βπ β π« π½(π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’))) |
62 | 60, 32, 61 | syl2anc 583 |
. . . . . . 7
β’ (π β ((π½ βΎt π·) β Comp β βπ β π« π½(π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’))) |
63 | 59, 62 | mpbid 231 |
. . . . . 6
β’ (π β βπ β π« π½(π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’)) |
64 | | ssrab2 4073 |
. . . . . . . 8
β’ {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} β π½ |
65 | 44, 64 | eqsstri 4012 |
. . . . . . 7
β’ π β π½ |
66 | 44, 7 | rabexd 5329 |
. . . . . . . 8
β’ (π β π β V) |
67 | | elpwg 4601 |
. . . . . . . 8
β’ (π β V β (π β π« π½ β π β π½)) |
68 | 66, 67 | syl 17 |
. . . . . . 7
β’ (π β (π β π« π½ β π β π½)) |
69 | 65, 68 | mpbiri 258 |
. . . . . 6
β’ (π β π β π« π½) |
70 | | unieq 4914 |
. . . . . . . . 9
β’ (π = π β βͺ π = βͺ
π) |
71 | 70 | sseq2d 4010 |
. . . . . . . 8
β’ (π = π β (π· β βͺ π β π· β βͺ π)) |
72 | | pweq 4612 |
. . . . . . . . . 10
β’ (π = π β π« π = π« π) |
73 | 72 | ineq1d 4207 |
. . . . . . . . 9
β’ (π = π β (π« π β© Fin) = (π« π β© Fin)) |
74 | 73 | rexeqdv 3321 |
. . . . . . . 8
β’ (π = π β (βπ’ β (π« π β© Fin)π· β βͺ π’ β βπ’ β (π« π β© Fin)π· β βͺ π’)) |
75 | 71, 74 | imbi12d 344 |
. . . . . . 7
β’ (π = π β ((π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’) β (π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’))) |
76 | 75 | rspccva 3606 |
. . . . . 6
β’
((βπ β
π« π½(π· β βͺ π
β βπ’ β
(π« π β©
Fin)π· β βͺ π’)
β§ π β π«
π½) β (π· β βͺ π
β βπ’ β
(π« π β©
Fin)π· β βͺ π’)) |
77 | 63, 69, 76 | syl2anc 583 |
. . . . 5
β’ (π β (π· β βͺ π β βπ’ β (π« π β© Fin)π· β βͺ π’)) |
78 | 57, 77 | mpd 15 |
. . . 4
β’ (π β βπ’ β (π« π β© Fin)π· β βͺ π’) |
79 | | elinel1 4191 |
. . . . . . . . 9
β’ (π’ β (π« π β© Fin) β π’ β π« π) |
80 | | elpwi 4605 |
. . . . . . . . . . 11
β’ (π’ β π« π β π’ β π) |
81 | 80 | ssdifssd 4138 |
. . . . . . . . . 10
β’ (π’ β π« π β (π’ β {β
}) β π) |
82 | | vex 3473 |
. . . . . . . . . . . 12
β’ π’ β V |
83 | | difexg 5323 |
. . . . . . . . . . . 12
β’ (π’ β V β (π’ β {β
}) β
V) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π’ β {β
}) β
V |
85 | 84 | elpw 4602 |
. . . . . . . . . 10
β’ ((π’ β {β
}) β
π« π β (π’ β {β
}) β
π) |
86 | 81, 85 | sylibr 233 |
. . . . . . . . 9
β’ (π’ β π« π β (π’ β {β
}) β π« π) |
87 | 79, 86 | syl 17 |
. . . . . . . 8
β’ (π’ β (π« π β© Fin) β (π’ β {β
}) β
π« π) |
88 | | elinel2 4192 |
. . . . . . . . 9
β’ (π’ β (π« π β© Fin) β π’ β Fin) |
89 | | diffi 9195 |
. . . . . . . . 9
β’ (π’ β Fin β (π’ β {β
}) β
Fin) |
90 | 88, 89 | syl 17 |
. . . . . . . 8
β’ (π’ β (π« π β© Fin) β (π’ β {β
}) β
Fin) |
91 | 87, 90 | elind 4190 |
. . . . . . 7
β’ (π’ β (π« π β© Fin) β (π’ β {β
}) β
(π« π β©
Fin)) |
92 | 91 | 3ad2ant2 1132 |
. . . . . 6
β’ ((π β§ π’ β (π« π β© Fin) β§ π· β βͺ π’) β (π’ β {β
}) β (π« π β© Fin)) |
93 | | unidif0 5354 |
. . . . . . . . 9
β’ βͺ (π’
β {β
}) = βͺ π’ |
94 | 93 | sseq2i 4007 |
. . . . . . . 8
β’ (π· β βͺ (π’
β {β
}) β π·
β βͺ π’) |
95 | 94 | biimpri 227 |
. . . . . . 7
β’ (π· β βͺ π’
β π· β βͺ (π’
β {β
})) |
96 | 95 | 3ad2ant3 1133 |
. . . . . 6
β’ ((π β§ π’ β (π« π β© Fin) β§ π· β βͺ π’) β π· β βͺ (π’ β
{β
})) |
97 | | eldifsni 4789 |
. . . . . . . 8
β’ (π€ β (π’ β {β
}) β π€ β β
) |
98 | 97 | rgen 3058 |
. . . . . . 7
β’
βπ€ β
(π’ β {β
})π€ β β
|
99 | 98 | a1i 11 |
. . . . . 6
β’ ((π β§ π’ β (π« π β© Fin) β§ π· β βͺ π’) β βπ€ β (π’ β {β
})π€ β β
) |
100 | | unieq 4914 |
. . . . . . . . 9
β’ (π = (π’ β {β
}) β βͺ π =
βͺ (π’ β {β
})) |
101 | 100 | sseq2d 4010 |
. . . . . . . 8
β’ (π = (π’ β {β
}) β (π· β βͺ π β π· β βͺ (π’ β
{β
}))) |
102 | | raleq 3317 |
. . . . . . . 8
β’ (π = (π’ β {β
}) β (βπ€ β π π€ β β
β βπ€ β (π’ β {β
})π€ β β
)) |
103 | 101, 102 | anbi12d 630 |
. . . . . . 7
β’ (π = (π’ β {β
}) β ((π· β βͺ π
β§ βπ€ β
π π€ β β
) β (π· β βͺ (π’ β {β
}) β§
βπ€ β (π’ β {β
})π€ β
β
))) |
104 | 103 | rspcev 3607 |
. . . . . 6
β’ (((π’ β {β
}) β
(π« π β© Fin)
β§ (π· β βͺ (π’
β {β
}) β§ βπ€ β (π’ β {β
})π€ β β
)) β βπ β (π« π β© Fin)(π· β βͺ π β§ βπ€ β π π€ β β
)) |
105 | 92, 96, 99, 104 | syl12anc 836 |
. . . . 5
β’ ((π β§ π’ β (π« π β© Fin) β§ π· β βͺ π’) β βπ β (π« π β© Fin)(π· β βͺ π β§ βπ€ β π π€ β β
)) |
106 | 105 | rexlimdv3a 3154 |
. . . 4
β’ (π β (βπ’ β (π« π β© Fin)π· β βͺ π’ β βπ β (π« π β© Fin)(π· β βͺ π β§ βπ€ β π π€ β β
))) |
107 | 78, 106 | mpd 15 |
. . 3
β’ (π β βπ β (π« π β© Fin)(π· β βͺ π β§ βπ€ β π π€ β β
)) |
108 | | nfv 1910 |
. . . . . 6
β’
β²βπ |
109 | | nfcv 2898 |
. . . . . . . . . . . 12
β’
β²ββ+ |
110 | | nfre1 3277 |
. . . . . . . . . . . 12
β’
β²βββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)) |
111 | 109, 110 | nfralw 3303 |
. . . . . . . . . . 11
β’
β²ββπ β β+
ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)) |
112 | | nfcv 2898 |
. . . . . . . . . . 11
β’
β²βπ½ |
113 | 111, 112 | nfrabw 3463 |
. . . . . . . . . 10
β’
β²β{π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} |
114 | 44, 113 | nfcxfr 2896 |
. . . . . . . . 9
β’
β²βπ |
115 | 114 | nfpw 4617 |
. . . . . . . 8
β’
β²βπ« π |
116 | | nfcv 2898 |
. . . . . . . 8
β’
β²βFin |
117 | 115, 116 | nfin 4212 |
. . . . . . 7
β’
β²β(π« π β© Fin) |
118 | 117 | nfcri 2885 |
. . . . . 6
β’
β²β π β (π« π β© Fin) |
119 | | nfv 1910 |
. . . . . 6
β’
β²β(π· β βͺ π
β§ βπ€ β
π π€ β β
) |
120 | 108, 118,
119 | nf3an 1897 |
. . . . 5
β’
β²β(π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) |
121 | | nfcv 2898 |
. . . . . . . . . . . 12
β’
β²π‘β+ |
122 | | nfcv 2898 |
. . . . . . . . . . . . 13
β’
β²π‘π΄ |
123 | | nfra1 3276 |
. . . . . . . . . . . . . 14
β’
β²π‘βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) |
124 | | nfra1 3276 |
. . . . . . . . . . . . . 14
β’
β²π‘βπ‘ β π€ (ββπ‘) < π |
125 | | nfra1 3276 |
. . . . . . . . . . . . . 14
β’
β²π‘βπ‘ β (π β π)(1 β π) < (ββπ‘) |
126 | 123, 124,
125 | nf3an 1897 |
. . . . . . . . . . . . 13
β’
β²π‘(βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)) |
127 | 122, 126 | nfrexw 3305 |
. . . . . . . . . . . 12
β’
β²π‘ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)) |
128 | 121, 127 | nfralw 3303 |
. . . . . . . . . . 11
β’
β²π‘βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)) |
129 | | nfcv 2898 |
. . . . . . . . . . 11
β’
β²π‘π½ |
130 | 128, 129 | nfrabw 3463 |
. . . . . . . . . 10
β’
β²π‘{π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} |
131 | 44, 130 | nfcxfr 2896 |
. . . . . . . . 9
β’
β²π‘π |
132 | 131 | nfpw 4617 |
. . . . . . . 8
β’
β²π‘π« π |
133 | | nfcv 2898 |
. . . . . . . 8
β’
β²π‘Fin |
134 | 132, 133 | nfin 4212 |
. . . . . . 7
β’
β²π‘(π« π β© Fin) |
135 | 134 | nfcri 2885 |
. . . . . 6
β’
β²π‘ π β (π« π β© Fin) |
136 | | nfcv 2898 |
. . . . . . . 8
β’
β²π‘βͺ π |
137 | 3, 136 | nfss 3970 |
. . . . . . 7
β’
β²π‘ π· β βͺ π |
138 | | nfv 1910 |
. . . . . . 7
β’
β²π‘βπ€ β π π€ β β
|
139 | 137, 138 | nfan 1895 |
. . . . . 6
β’
β²π‘(π· β βͺ π
β§ βπ€ β
π π€ β β
) |
140 | 2, 135, 139 | nf3an 1897 |
. . . . 5
β’
β²π‘(π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) |
141 | | nfv 1910 |
. . . . . 6
β’
β²π€π |
142 | 53 | nfpw 4617 |
. . . . . . . 8
β’
β²π€π« π |
143 | | nfcv 2898 |
. . . . . . . 8
β’
β²π€Fin |
144 | 142, 143 | nfin 4212 |
. . . . . . 7
β’
β²π€(π« π β© Fin) |
145 | 144 | nfcri 2885 |
. . . . . 6
β’
β²π€ π β (π« π β© Fin) |
146 | | nfv 1910 |
. . . . . . 7
β’
β²π€ π· β βͺ π |
147 | | nfra1 3276 |
. . . . . . 7
β’
β²π€βπ€ β π π€ β β
|
148 | 146, 147 | nfan 1895 |
. . . . . 6
β’
β²π€(π· β βͺ π
β§ βπ€ β
π π€ β β
) |
149 | 141, 145,
148 | nf3an 1897 |
. . . . 5
β’
β²π€(π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) |
150 | | stoweidlem57.4 |
. . . . 5
β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
151 | | simp2 1135 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π β (π« π β© Fin)) |
152 | | simp3l 1199 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π· β βͺ π) |
153 | | stoweidlem57.19 |
. . . . . 6
β’ (π β π· β β
) |
154 | 153 | 3ad2ant1 1131 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π· β β
) |
155 | | stoweidlem57.20 |
. . . . . 6
β’ (π β πΈ β
β+) |
156 | 155 | 3ad2ant1 1131 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β πΈ β
β+) |
157 | 26 | simpld 494 |
. . . . . 6
β’ (π β π΅ β π) |
158 | 157 | 3ad2ant1 1131 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π΅ β π) |
159 | 66 | 3ad2ant1 1131 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π β V) |
160 | | retop 24665 |
. . . . . . . . 9
β’
(topGenβran (,)) β Top |
161 | 6, 160 | eqeltri 2824 |
. . . . . . . 8
β’ πΎ β Top |
162 | | cnfex 44313 |
. . . . . . . 8
β’ ((π½ β Top β§ πΎ β Top) β (π½ Cn πΎ) β V) |
163 | 60, 161, 162 | sylancl 585 |
. . . . . . 7
β’ (π β (π½ Cn πΎ) β V) |
164 | 11, 10 | sseqtrdi 4028 |
. . . . . . 7
β’ (π β π΄ β (π½ Cn πΎ)) |
165 | 163, 164 | ssexd 5318 |
. . . . . 6
β’ (π β π΄ β V) |
166 | 165 | 3ad2ant1 1131 |
. . . . 5
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β π΄ β V) |
167 | 120, 140,
149, 21, 150, 44, 151, 152, 154, 156, 158, 159, 166 | stoweidlem39 45350 |
. . . 4
β’ ((π β§ π β (π« π β© Fin) β§ (π· β βͺ π β§ βπ€ β π π€ β β
)) β βπ β β βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
168 | 167 | rexlimdv3a 3154 |
. . 3
β’ (π β (βπ β (π« π β© Fin)(π· β βͺ π β§ βπ€ β π π€ β β
) β βπ β β βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))))) |
169 | 107, 168 | mpd 15 |
. 2
β’ (π β βπ β β βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
170 | | nfv 1910 |
. . . . . . 7
β’
β²π(π β§ π β β) |
171 | | nfv 1910 |
. . . . . . . 8
β’
β²π π£:(1...π)βΆπ |
172 | | nfv 1910 |
. . . . . . . 8
β’
β²π π· β βͺ ran π£ |
173 | | nfv 1910 |
. . . . . . . . . 10
β’
β²π π¦:(1...π)βΆπ |
174 | | nfra1 3276 |
. . . . . . . . . 10
β’
β²πβπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
175 | 173, 174 | nfan 1895 |
. . . . . . . . 9
β’
β²π(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
176 | 175 | nfex 2312 |
. . . . . . . 8
β’
β²πβπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
177 | 171, 172,
176 | nf3an 1897 |
. . . . . . 7
β’
β²π(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
178 | 170, 177 | nfan 1895 |
. . . . . 6
β’
β²π((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
179 | | nfv 1910 |
. . . . . . . 8
β’
β²π‘ π β β |
180 | 2, 179 | nfan 1895 |
. . . . . . 7
β’
β²π‘(π β§ π β β) |
181 | | nfcv 2898 |
. . . . . . . . 9
β’
β²π‘π£ |
182 | | nfcv 2898 |
. . . . . . . . 9
β’
β²π‘(1...π) |
183 | 181, 182,
131 | nff 6712 |
. . . . . . . 8
β’
β²π‘ π£:(1...π)βΆπ |
184 | | nfcv 2898 |
. . . . . . . . 9
β’
β²π‘βͺ ran π£ |
185 | 3, 184 | nfss 3970 |
. . . . . . . 8
β’
β²π‘ π· β βͺ ran π£ |
186 | | nfcv 2898 |
. . . . . . . . . . 11
β’
β²π‘π¦ |
187 | 123, 122 | nfrabw 3463 |
. . . . . . . . . . . 12
β’
β²π‘{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
188 | 150, 187 | nfcxfr 2896 |
. . . . . . . . . . 11
β’
β²π‘π |
189 | 186, 182,
188 | nff 6712 |
. . . . . . . . . 10
β’
β²π‘ π¦:(1...π)βΆπ |
190 | | nfra1 3276 |
. . . . . . . . . . . 12
β’
β²π‘βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) |
191 | | nfra1 3276 |
. . . . . . . . . . . 12
β’
β²π‘βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘) |
192 | 190, 191 | nfan 1895 |
. . . . . . . . . . 11
β’
β²π‘(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
193 | 182, 192 | nfralw 3303 |
. . . . . . . . . 10
β’
β²π‘βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
194 | 189, 193 | nfan 1895 |
. . . . . . . . 9
β’
β²π‘(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
195 | 194 | nfex 2312 |
. . . . . . . 8
β’
β²π‘βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
196 | 183, 185,
195 | nf3an 1897 |
. . . . . . 7
β’
β²π‘(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
197 | 180, 196 | nfan 1895 |
. . . . . 6
β’
β²π‘((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
198 | | nfv 1910 |
. . . . . . 7
β’
β²π¦(π β§ π β β) |
199 | | nfv 1910 |
. . . . . . . 8
β’
β²π¦ π£:(1...π)βΆπ |
200 | | nfv 1910 |
. . . . . . . 8
β’
β²π¦ π· β βͺ ran π£ |
201 | | nfe1 2140 |
. . . . . . . 8
β’
β²π¦βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
202 | 199, 200,
201 | nf3an 1897 |
. . . . . . 7
β’
β²π¦(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
203 | 198, 202 | nfan 1895 |
. . . . . 6
β’
β²π¦((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
204 | | nfv 1910 |
. . . . . . 7
β’
β²π€(π β§ π β β) |
205 | | nfcv 2898 |
. . . . . . . . 9
β’
β²π€π£ |
206 | | nfcv 2898 |
. . . . . . . . 9
β’
β²π€(1...π) |
207 | 205, 206,
53 | nff 6712 |
. . . . . . . 8
β’
β²π€ π£:(1...π)βΆπ |
208 | | nfv 1910 |
. . . . . . . 8
β’
β²π€ π· β βͺ ran π£ |
209 | | nfv 1910 |
. . . . . . . 8
β’
β²π€βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
210 | 207, 208,
209 | nf3an 1897 |
. . . . . . 7
β’
β²π€(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
211 | 204, 210 | nfan 1895 |
. . . . . 6
β’
β²π€((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) |
212 | | eqid 2727 |
. . . . . 6
β’ {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
213 | | eqid 2727 |
. . . . . 6
β’ (π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}, π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) = (π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}, π β {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
214 | | eqid 2727 |
. . . . . 6
β’ (π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘))) = (π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘))) |
215 | | eqid 2727 |
. . . . . 6
β’ (π‘ β π β¦ (seq1( Β· , ((π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘)))βπ‘))βπ)) = (π‘ β π β¦ (seq1( Β· , ((π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘)))βπ‘))βπ)) |
216 | | simp1ll 1234 |
. . . . . . 7
β’ ((((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β§ π β π΄ β§ π β π΄) β π) |
217 | 216, 15 | syld3an1 1408 |
. . . . . 6
β’ ((((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
218 | 11 | sselda 3978 |
. . . . . . . 8
β’ ((π β§ π β π΄) β π β πΆ) |
219 | 6, 9, 10, 218 | fcnre 44310 |
. . . . . . 7
β’ ((π β§ π β π΄) β π:πβΆβ) |
220 | 219 | ad4ant14 751 |
. . . . . 6
β’ ((((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β§ π β π΄) β π:πβΆβ) |
221 | | simplr 768 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π β β) |
222 | | simpr1 1192 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π£:(1...π)βΆπ) |
223 | 9 | cldss 22920 |
. . . . . . . 8
β’ (π΅ β (Clsdβπ½) β π΅ β π) |
224 | 22, 223 | syl 17 |
. . . . . . 7
β’ (π β π΅ β π) |
225 | 224 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π΅ β π) |
226 | | simpr2 1193 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π· β βͺ ran
π£) |
227 | 32 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π· β π) |
228 | | feq3 6699 |
. . . . . . . . . . . 12
β’ (π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β (π¦:(1...π)βΆπ β π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)})) |
229 | 150, 228 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π¦:(1...π)βΆπ β π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}) |
230 | 229 | biimpi 215 |
. . . . . . . . . 10
β’ (π¦:(1...π)βΆπ β π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)}) |
231 | 230 | anim1i 614 |
. . . . . . . . 9
β’ ((π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) β (π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
232 | 231 | eximi 1830 |
. . . . . . . 8
β’
(βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) β βπ¦(π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
233 | 232 | 3ad2ant3 1133 |
. . . . . . 7
β’ ((π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ¦(π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
234 | 233 | adantl 481 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β βπ¦(π¦:(1...π)βΆ{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
235 | 7 | uniexd 7741 |
. . . . . . . 8
β’ (π β βͺ π½
β V) |
236 | 9, 235 | eqeltrid 2832 |
. . . . . . 7
β’ (π β π β V) |
237 | 236 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β π β V) |
238 | 155 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β πΈ β
β+) |
239 | | stoweidlem57.21 |
. . . . . . 7
β’ (π β πΈ < (1 / 3)) |
240 | 239 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β πΈ < (1 / 3)) |
241 | 178, 197,
203, 211, 9, 212, 213, 214, 215, 44, 217, 220, 221, 222, 225, 226, 227, 234, 237, 238, 240 | stoweidlem54 45365 |
. . . . 5
β’ (((π β§ π β β) β§ (π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))))) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) |
242 | 241 | ex 412 |
. . . 4
β’ ((π β§ π β β) β ((π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) |
243 | 242 | exlimdv 1929 |
. . 3
β’ ((π β§ π β β) β (βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) |
244 | 243 | rexlimdva 3150 |
. 2
β’ (π β (βπ β β βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran
π£ β§ βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) |
245 | 169, 244 | mpd 15 |
1
β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) |