Step | Hyp | Ref
| Expression |
1 | | stoweidlem43.1 |
. . 3
β’
β²ππ |
2 | | nfv 1918 |
. . 3
β’
β²πβπ(π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0) |
3 | | stoweidlem43.15 |
. . . . . 6
β’ (π β π β (π β π)) |
4 | 3 | eldifad 3926 |
. . . . 5
β’ (π β π β π) |
5 | | stoweidlem43.14 |
. . . . . . 7
β’ (π β π β π) |
6 | | stoweidlem43.13 |
. . . . . . 7
β’ (π β π β π½) |
7 | | elunii 4874 |
. . . . . . 7
β’ ((π β π β§ π β π½) β π β βͺ π½) |
8 | 5, 6, 7 | syl2anc 585 |
. . . . . 6
β’ (π β π β βͺ π½) |
9 | | stoweidlem43.6 |
. . . . . 6
β’ π = βͺ
π½ |
10 | 8, 9 | eleqtrrdi 2845 |
. . . . 5
β’ (π β π β π) |
11 | 3 | eldifbd 3927 |
. . . . . . 7
β’ (π β Β¬ π β π) |
12 | | nelne2 3039 |
. . . . . . 7
β’ ((π β π β§ Β¬ π β π) β π β π) |
13 | 5, 11, 12 | syl2anc 585 |
. . . . . 6
β’ (π β π β π) |
14 | 13 | necomd 2996 |
. . . . 5
β’ (π β π β π) |
15 | 4, 10, 14 | 3jca 1129 |
. . . 4
β’ (π β (π β π β§ π β π β§ π β π)) |
16 | | simpr2 1196 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π β π) |
17 | | stoweidlem43.2 |
. . . . . . . . 9
β’
β²π‘π |
18 | | nfv 1918 |
. . . . . . . . 9
β’
β²π‘(π β π β§ π β π β§ π β π) |
19 | 17, 18 | nfan 1903 |
. . . . . . . 8
β’
β²π‘(π β§ (π β π β§ π β π β§ π β π)) |
20 | | nfv 1918 |
. . . . . . . 8
β’
β²π‘βπ β π΄ (πβπ) β (πβπ) |
21 | 19, 20 | nfim 1900 |
. . . . . . 7
β’
β²π‘((π β§ (π β π β§ π β π β§ π β π)) β βπ β π΄ (πβπ) β (πβπ)) |
22 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π‘ = π β (π‘ β π β π β π)) |
23 | | neeq2 3004 |
. . . . . . . . . 10
β’ (π‘ = π β (π β π‘ β π β π)) |
24 | 22, 23 | 3anbi23d 1440 |
. . . . . . . . 9
β’ (π‘ = π β ((π β π β§ π‘ β π β§ π β π‘) β (π β π β§ π β π β§ π β π))) |
25 | 24 | anbi2d 630 |
. . . . . . . 8
β’ (π‘ = π β ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β (π β§ (π β π β§ π β π β§ π β π)))) |
26 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π‘ = π β (πβπ‘) = (πβπ)) |
27 | 26 | neeq2d 3001 |
. . . . . . . . 9
β’ (π‘ = π β ((πβπ) β (πβπ‘) β (πβπ) β (πβπ))) |
28 | 27 | rexbidv 3172 |
. . . . . . . 8
β’ (π‘ = π β (βπ β π΄ (πβπ) β (πβπ‘) β βπ β π΄ (πβπ) β (πβπ))) |
29 | 25, 28 | imbi12d 345 |
. . . . . . 7
β’ (π‘ = π β (((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) β ((π β§ (π β π β§ π β π β§ π β π)) β βπ β π΄ (πβπ) β (πβπ)))) |
30 | | simpr1 1195 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β π β π) |
31 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π = π β (π β π β π β π)) |
32 | | neeq1 3003 |
. . . . . . . . . . . 12
β’ (π = π β (π β π‘ β π β π‘)) |
33 | 31, 32 | 3anbi13d 1439 |
. . . . . . . . . . 11
β’ (π = π β ((π β π β§ π‘ β π β§ π β π‘) β (π β π β§ π‘ β π β§ π β π‘))) |
34 | 33 | anbi2d 630 |
. . . . . . . . . 10
β’ (π = π β ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β (π β§ (π β π β§ π‘ β π β§ π β π‘)))) |
35 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
36 | 35 | neeq1d 3000 |
. . . . . . . . . . 11
β’ (π = π β ((πβπ) β (πβπ‘) β (πβπ) β (πβπ‘))) |
37 | 36 | rexbidv 3172 |
. . . . . . . . . 10
β’ (π = π β (βπ β π΄ (πβπ) β (πβπ‘) β βπ β π΄ (πβπ) β (πβπ‘))) |
38 | 34, 37 | imbi12d 345 |
. . . . . . . . 9
β’ (π = π β (((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) β ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)))) |
39 | | stoweidlem43.12 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
40 | 39 | a1i 11 |
. . . . . . . . 9
β’ (π β π β ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘))) |
41 | 38, 40 | vtoclga 3536 |
. . . . . . . 8
β’ (π β π β ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘))) |
42 | 30, 41 | mpcom 38 |
. . . . . . 7
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
43 | 21, 29, 42 | vtoclg1f 3526 |
. . . . . 6
β’ (π β π β ((π β§ (π β π β§ π β π β§ π β π)) β βπ β π΄ (πβπ) β (πβπ))) |
44 | 16, 43 | mpcom 38 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β βπ β π΄ (πβπ) β (πβπ)) |
45 | | df-rex 3071 |
. . . . 5
β’
(βπ β
π΄ (πβπ) β (πβπ) β βπ(π β π΄ β§ (πβπ) β (πβπ))) |
46 | 44, 45 | sylib 217 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β βπ(π β π΄ β§ (πβπ) β (πβπ))) |
47 | 15, 46 | mpdan 686 |
. . 3
β’ (π β βπ(π β π΄ β§ (πβπ) β (πβπ))) |
48 | | nfv 1918 |
. . . . . 6
β’
β²π‘(π β π΄ β§ (πβπ) β (πβπ)) |
49 | 17, 48 | nfan 1903 |
. . . . 5
β’
β²π‘(π β§ (π β π΄ β§ (πβπ) β (πβπ))) |
50 | | nfcv 2904 |
. . . . 5
β’
β²π‘π |
51 | | eqid 2733 |
. . . . 5
β’ (π‘ β π β¦ ((πβπ‘) β (πβπ))) = (π‘ β π β¦ ((πβπ‘) β (πβπ))) |
52 | | stoweidlem43.4 |
. . . . . . 7
β’ πΎ = (topGenβran
(,)) |
53 | | eqid 2733 |
. . . . . . 7
β’ (π½ Cn πΎ) = (π½ Cn πΎ) |
54 | | stoweidlem43.8 |
. . . . . . . 8
β’ (π β π΄ β (π½ Cn πΎ)) |
55 | 54 | sselda 3948 |
. . . . . . 7
β’ ((π β§ π β π΄) β π β (π½ Cn πΎ)) |
56 | 52, 9, 53, 55 | fcnre 43322 |
. . . . . 6
β’ ((π β§ π β π΄) β π:πβΆβ) |
57 | 56 | adantlr 714 |
. . . . 5
β’ (((π β§ (π β π΄ β§ (πβπ) β (πβπ))) β§ π β π΄) β π:πβΆβ) |
58 | | stoweidlem43.9 |
. . . . . 6
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
59 | 58 | 3adant1r 1178 |
. . . . 5
β’ (((π β§ (π β π΄ β§ (πβπ) β (πβπ))) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
60 | | stoweidlem43.11 |
. . . . . 6
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
61 | 60 | adantlr 714 |
. . . . 5
β’ (((π β§ (π β π΄ β§ (πβπ) β (πβπ))) β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
62 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ))) β π β π) |
63 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ))) β π β π) |
64 | | simprl 770 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ))) β π β π΄) |
65 | | simprr 772 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ))) β (πβπ) β (πβπ)) |
66 | 49, 50, 51, 57, 59, 61, 62, 63, 64, 65 | stoweidlem23 44354 |
. . . 4
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ))) β ((π‘ β π β¦ ((πβπ‘) β (πβπ))) β π΄ β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) = 0)) |
67 | | eleq1 2822 |
. . . . . . . 8
β’ (π = (π‘ β π β¦ ((πβπ‘) β (πβπ))) β (π β π΄ β (π‘ β π β¦ ((πβπ‘) β (πβπ))) β π΄)) |
68 | | fveq1 6845 |
. . . . . . . . 9
β’ (π = (π‘ β π β¦ ((πβπ‘) β (πβπ))) β (πβπ) = ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ)) |
69 | | fveq1 6845 |
. . . . . . . . 9
β’ (π = (π‘ β π β¦ ((πβπ‘) β (πβπ))) β (πβπ) = ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ)) |
70 | 68, 69 | neeq12d 3002 |
. . . . . . . 8
β’ (π = (π‘ β π β¦ ((πβπ‘) β (πβπ))) β ((πβπ) β (πβπ) β ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ))) |
71 | 69 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = (π‘ β π β¦ ((πβπ‘) β (πβπ))) β ((πβπ) = 0 β ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) = 0)) |
72 | 67, 70, 71 | 3anbi123d 1437 |
. . . . . . 7
β’ (π = (π‘ β π β¦ ((πβπ‘) β (πβπ))) β ((π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0) β ((π‘ β π β¦ ((πβπ‘) β (πβπ))) β π΄ β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) = 0))) |
73 | 72 | spcegv 3558 |
. . . . . 6
β’ ((π‘ β π β¦ ((πβπ‘) β (πβπ))) β π΄ β (((π‘ β π β¦ ((πβπ‘) β (πβπ))) β π΄ β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) = 0) β βπ(π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0))) |
74 | 73 | 3ad2ant1 1134 |
. . . . 5
β’ (((π‘ β π β¦ ((πβπ‘) β (πβπ))) β π΄ β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) = 0) β (((π‘ β π β¦ ((πβπ‘) β (πβπ))) β π΄ β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) = 0) β βπ(π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0))) |
75 | 74 | pm2.43i 52 |
. . . 4
β’ (((π‘ β π β¦ ((πβπ‘) β (πβπ))) β π΄ β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) β§ ((π‘ β π β¦ ((πβπ‘) β (πβπ)))βπ) = 0) β βπ(π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) |
76 | 66, 75 | syl 17 |
. . 3
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ))) β βπ(π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) |
77 | 1, 2, 47, 76 | exlimdd 2214 |
. 2
β’ (π β βπ(π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) |
78 | | stoweidlem43.3 |
. . . . 5
β’
β²βπ |
79 | | nfmpt1 5217 |
. . . . 5
β’
β²π‘(π‘ β π β¦ (((π β π β¦ ((πβπ ) Β· (πβπ )))βπ‘) / sup(ran (π β π β¦ ((πβπ ) Β· (πβπ ))), β, < ))) |
80 | | nfcv 2904 |
. . . . 5
β’
β²π‘π |
81 | | nfcv 2904 |
. . . . 5
β’
β²π‘(π β π β¦ ((πβπ ) Β· (πβπ ))) |
82 | | nfv 1918 |
. . . . . 6
β’
β²π‘(π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0) |
83 | 17, 82 | nfan 1903 |
. . . . 5
β’
β²π‘(π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) |
84 | | stoweidlem43.5 |
. . . . 5
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
85 | | fveq2 6846 |
. . . . . . 7
β’ (π = π‘ β (πβπ ) = (πβπ‘)) |
86 | 85, 85 | oveq12d 7379 |
. . . . . 6
β’ (π = π‘ β ((πβπ ) Β· (πβπ )) = ((πβπ‘) Β· (πβπ‘))) |
87 | 86 | cbvmptv 5222 |
. . . . 5
β’ (π β π β¦ ((πβπ ) Β· (πβπ ))) = (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) |
88 | | eqid 2733 |
. . . . 5
β’ sup(ran
(π β π β¦ ((πβπ ) Β· (πβπ ))), β, < ) = sup(ran (π β π β¦ ((πβπ ) Β· (πβπ ))), β, < ) |
89 | | eqid 2733 |
. . . . 5
β’ (π‘ β π β¦ (((π β π β¦ ((πβπ ) Β· (πβπ )))βπ‘) / sup(ran (π β π β¦ ((πβπ ) Β· (πβπ ))), β, < ))) = (π‘ β π β¦ (((π β π β¦ ((πβπ ) Β· (πβπ )))βπ‘) / sup(ran (π β π β¦ ((πβπ ) Β· (πβπ ))), β, < ))) |
90 | | stoweidlem43.7 |
. . . . . 6
β’ (π β π½ β Comp) |
91 | 90 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) β π½ β Comp) |
92 | 54 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) β π΄ β (π½ Cn πΎ)) |
93 | | eleq1 2822 |
. . . . . . . . 9
β’ (π = π β (π β π΄ β π β π΄)) |
94 | 93 | 3anbi2d 1442 |
. . . . . . . 8
β’ (π = π β ((π β§ π β π΄ β§ π β π΄) β (π β§ π β π΄ β§ π β π΄))) |
95 | | fveq1 6845 |
. . . . . . . . . . 11
β’ (π = π β (πβπ‘) = (πβπ‘)) |
96 | 95 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π = π β ((πβπ‘) Β· (πβπ‘)) = ((πβπ‘) Β· (πβπ‘))) |
97 | 96 | mpteq2dv 5211 |
. . . . . . . . 9
β’ (π = π β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) = (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
98 | 97 | eleq1d 2819 |
. . . . . . . 8
β’ (π = π β ((π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄ β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄)) |
99 | 94, 98 | imbi12d 345 |
. . . . . . 7
β’ (π = π β (((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) β ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄))) |
100 | | stoweidlem43.10 |
. . . . . . 7
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
101 | 99, 100 | chvarvv 2003 |
. . . . . 6
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
102 | 101 | 3adant1r 1178 |
. . . . 5
β’ (((π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
103 | 60 | adantlr 714 |
. . . . 5
β’ (((π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
104 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) β π β π) |
105 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) β π β π) |
106 | | simpr1 1195 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) β π β π΄) |
107 | | simpr2 1196 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) β (πβπ) β (πβπ)) |
108 | | simpr3 1197 |
. . . . 5
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) β (πβπ) = 0) |
109 | 78, 79, 80, 81, 83, 52, 84, 9, 87, 88, 89, 91, 92, 102, 103, 104, 105, 106, 107, 108 | stoweidlem36 44367 |
. . . 4
β’ ((π β§ (π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0)) β ββ(β β π β§ 0 < (ββπ))) |
110 | 109 | ex 414 |
. . 3
β’ (π β ((π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0) β ββ(β β π β§ 0 < (ββπ)))) |
111 | 110 | exlimdv 1937 |
. 2
β’ (π β (βπ(π β π΄ β§ (πβπ) β (πβπ) β§ (πβπ) = 0) β ββ(β β π β§ 0 < (ββπ)))) |
112 | 77, 111 | mpd 15 |
1
β’ (π β ββ(β β π β§ 0 < (ββπ))) |