Step | Hyp | Ref
| Expression |
1 | | stoweidlem53.1 |
. . . 4
β’
β²π‘π |
2 | | stoweidlem53.2 |
. . . 4
β’
β²π‘π |
3 | | stoweidlem53.3 |
. . . 4
β’ πΎ = (topGenβran
(,)) |
4 | | stoweidlem53.4 |
. . . 4
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
5 | | stoweidlem53.5 |
. . . 4
β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} |
6 | | stoweidlem53.6 |
. . . 4
β’ π = βͺ
π½ |
7 | | stoweidlem53.7 |
. . . 4
β’ πΆ = (π½ Cn πΎ) |
8 | | stoweidlem53.8 |
. . . 4
β’ (π β π½ β Comp) |
9 | | stoweidlem53.9 |
. . . 4
β’ (π β π΄ β πΆ) |
10 | | stoweidlem53.10 |
. . . 4
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
11 | | stoweidlem53.11 |
. . . 4
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
12 | | stoweidlem53.12 |
. . . 4
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
13 | | stoweidlem53.13 |
. . . 4
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
14 | | stoweidlem53.14 |
. . . 4
β’ (π β π β π½) |
15 | | stoweidlem53.16 |
. . . 4
β’ (π β π β π) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | stoweidlem50 44365 |
. . 3
β’ (π β βπ’(π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) |
17 | | nfv 1918 |
. . . . . 6
β’
β²π‘ π’ β Fin |
18 | | nfcv 2908 |
. . . . . . 7
β’
β²π‘π’ |
19 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π‘(ββπ) = 0 |
20 | | nfra1 3270 |
. . . . . . . . . . . . 13
β’
β²π‘βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) |
21 | 19, 20 | nfan 1903 |
. . . . . . . . . . . 12
β’
β²π‘((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)) |
22 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π‘π΄ |
23 | 21, 22 | nfrabw 3443 |
. . . . . . . . . . 11
β’
β²π‘{β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
24 | 4, 23 | nfcxfr 2906 |
. . . . . . . . . 10
β’
β²π‘π |
25 | | nfrab1 3429 |
. . . . . . . . . . 11
β’
β²π‘{π‘ β π β£ 0 < (ββπ‘)} |
26 | 25 | nfeq2 2925 |
. . . . . . . . . 10
β’
β²π‘ π€ = {π‘ β π β£ 0 < (ββπ‘)} |
27 | 24, 26 | nfrexw 3299 |
. . . . . . . . 9
β’
β²π‘ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)} |
28 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π‘π½ |
29 | 27, 28 | nfrabw 3443 |
. . . . . . . 8
β’
β²π‘{π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} |
30 | 5, 29 | nfcxfr 2906 |
. . . . . . 7
β’
β²π‘π |
31 | 18, 30 | nfss 3941 |
. . . . . 6
β’
β²π‘ π’ β π |
32 | | nfcv 2908 |
. . . . . . . 8
β’
β²π‘π |
33 | 32, 1 | nfdif 4090 |
. . . . . . 7
β’
β²π‘(π β π) |
34 | | nfcv 2908 |
. . . . . . 7
β’
β²π‘βͺ π’ |
35 | 33, 34 | nfss 3941 |
. . . . . 6
β’
β²π‘(π β π) β βͺ π’ |
36 | 17, 31, 35 | nf3an 1905 |
. . . . 5
β’
β²π‘(π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’) |
37 | 2, 36 | nfan 1903 |
. . . 4
β’
β²π‘(π β§ (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) |
38 | | nfv 1918 |
. . . . 5
β’
β²π€π |
39 | | nfv 1918 |
. . . . . 6
β’
β²π€ π’ β Fin |
40 | | nfcv 2908 |
. . . . . . 7
β’
β²π€π’ |
41 | | nfrab1 3429 |
. . . . . . . 8
β’
β²π€{π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} |
42 | 5, 41 | nfcxfr 2906 |
. . . . . . 7
β’
β²π€π |
43 | 40, 42 | nfss 3941 |
. . . . . 6
β’
β²π€ π’ β π |
44 | | nfv 1918 |
. . . . . 6
β’
β²π€(π β π) β βͺ π’ |
45 | 39, 43, 44 | nf3an 1905 |
. . . . 5
β’
β²π€(π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’) |
46 | 38, 45 | nfan 1903 |
. . . 4
β’
β²π€(π β§ (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) |
47 | | nfv 1918 |
. . . . 5
β’
β²βπ |
48 | | nfv 1918 |
. . . . . 6
β’
β²β π’ β Fin |
49 | | nfcv 2908 |
. . . . . . 7
β’
β²βπ’ |
50 | | nfre1 3271 |
. . . . . . . . 9
β’
β²βββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)} |
51 | | nfcv 2908 |
. . . . . . . . 9
β’
β²βπ½ |
52 | 50, 51 | nfrabw 3443 |
. . . . . . . 8
β’
β²β{π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} |
53 | 5, 52 | nfcxfr 2906 |
. . . . . . 7
β’
β²βπ |
54 | 49, 53 | nfss 3941 |
. . . . . 6
β’
β²β π’ β π |
55 | | nfv 1918 |
. . . . . 6
β’
β²β(π β π) β βͺ π’ |
56 | 48, 54, 55 | nf3an 1905 |
. . . . 5
β’
β²β(π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’) |
57 | 47, 56 | nfan 1903 |
. . . 4
β’
β²β(π β§ (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) |
58 | | eqid 2737 |
. . . 4
β’ (π€ β π’ β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) = (π€ β π’ β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
59 | | cmptop 22762 |
. . . . . . . 8
β’ (π½ β Comp β π½ β Top) |
60 | 8, 59 | syl 17 |
. . . . . . 7
β’ (π β π½ β Top) |
61 | | retop 24141 |
. . . . . . . 8
β’
(topGenβran (,)) β Top |
62 | 3, 61 | eqeltri 2834 |
. . . . . . 7
β’ πΎ β Top |
63 | | cnfex 43307 |
. . . . . . 7
β’ ((π½ β Top β§ πΎ β Top) β (π½ Cn πΎ) β V) |
64 | 60, 62, 63 | sylancl 587 |
. . . . . 6
β’ (π β (π½ Cn πΎ) β V) |
65 | 9, 7 | sseqtrdi 3999 |
. . . . . 6
β’ (π β π΄ β (π½ Cn πΎ)) |
66 | 64, 65 | ssexd 5286 |
. . . . 5
β’ (π β π΄ β V) |
67 | 66 | adantr 482 |
. . . 4
β’ ((π β§ (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) β π΄ β V) |
68 | | simpr1 1195 |
. . . 4
β’ ((π β§ (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) β π’ β Fin) |
69 | | simpr2 1196 |
. . . 4
β’ ((π β§ (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) β π’ β π) |
70 | | simpr3 1197 |
. . . 4
β’ ((π β§ (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) β (π β π) β βͺ π’) |
71 | | stoweidlem53.15 |
. . . . 5
β’ (π β (π β π) β β
) |
72 | 71 | adantr 482 |
. . . 4
β’ ((π β§ (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) β (π β π) β β
) |
73 | 37, 46, 57, 4, 5, 58, 67, 68, 69, 70, 72 | stoweidlem35 44350 |
. . 3
β’ ((π β§ (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) β βπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |
74 | 16, 73 | exlimddv 1939 |
. 2
β’ (π β βπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |
75 | | nfv 1918 |
. . . . . 6
β’
β²ππ |
76 | | nfv 1918 |
. . . . . . 7
β’
β²π π β β |
77 | | nfv 1918 |
. . . . . . . 8
β’
β²π π:(1...π)βΆπ |
78 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π(π β π) |
79 | | nfre1 3271 |
. . . . . . . . 9
β’
β²πβπ β (1...π)0 < ((πβπ)βπ‘) |
80 | 78, 79 | nfralw 3297 |
. . . . . . . 8
β’
β²πβπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘) |
81 | 77, 80 | nfan 1903 |
. . . . . . 7
β’
β²π(π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)) |
82 | 76, 81 | nfan 1903 |
. . . . . 6
β’
β²π(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))) |
83 | 75, 82 | nfan 1903 |
. . . . 5
β’
β²π(π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |
84 | | nfv 1918 |
. . . . . . 7
β’
β²π‘ π β β |
85 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π‘π |
86 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π‘(1...π) |
87 | 85, 86, 24 | nff 6669 |
. . . . . . . 8
β’
β²π‘ π:(1...π)βΆπ |
88 | | nfra1 3270 |
. . . . . . . 8
β’
β²π‘βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘) |
89 | 87, 88 | nfan 1903 |
. . . . . . 7
β’
β²π‘(π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)) |
90 | 84, 89 | nfan 1903 |
. . . . . 6
β’
β²π‘(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))) |
91 | 2, 90 | nfan 1903 |
. . . . 5
β’
β²π‘(π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |
92 | | eqid 2737 |
. . . . 5
β’ (π‘ β π β¦ ((1 / π) Β· Ξ£π¦ β (1...π)((πβπ¦)βπ‘))) = (π‘ β π β¦ ((1 / π) Β· Ξ£π¦ β (1...π)((πβπ¦)βπ‘))) |
93 | | simprl 770 |
. . . . 5
β’ ((π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) β π β β) |
94 | | simprrl 780 |
. . . . 5
β’ ((π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) β π:(1...π)βΆπ) |
95 | | simprrr 781 |
. . . . 5
β’ ((π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) β βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)) |
96 | 65 | adantr 482 |
. . . . 5
β’ ((π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) β π΄ β (π½ Cn πΎ)) |
97 | 10 | 3adant1r 1178 |
. . . . 5
β’ (((π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
98 | 11 | 3adant1r 1178 |
. . . . 5
β’ (((π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
99 | 12 | adantlr 714 |
. . . . 5
β’ (((π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
100 | | elssuni 4903 |
. . . . . . . . 9
β’ (π β π½ β π β βͺ π½) |
101 | 100, 6 | sseqtrrdi 4000 |
. . . . . . . 8
β’ (π β π½ β π β π) |
102 | 14, 101 | syl 17 |
. . . . . . 7
β’ (π β π β π) |
103 | 102, 15 | sseldd 3950 |
. . . . . 6
β’ (π β π β π) |
104 | 103 | adantr 482 |
. . . . 5
β’ ((π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) β π β π) |
105 | 83, 91, 3, 4, 92, 93, 94, 95, 6, 96, 97, 98, 99, 104 | stoweidlem44 44359 |
. . . 4
β’ ((π β§ (π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) |
106 | 105 | ex 414 |
. . 3
β’ (π β ((π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))) β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘)))) |
107 | 106 | exlimdvv 1938 |
. 2
β’ (π β (βπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))) β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘)))) |
108 | 74, 107 | mpd 15 |
1
β’ (π β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) |