Step | Hyp | Ref
| Expression |
1 | | knoppcnlem11.t |
. . . . . 6
β’ π = (π₯ β β β¦
(absβ((ββ(π₯ + (1 / 2))) β π₯))) |
2 | | knoppcnlem11.f |
. . . . . 6
β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) |
3 | | knoppcnlem11.n |
. . . . . . 7
β’ (π β π β β) |
4 | 3 | adantr 481 |
. . . . . 6
β’ ((π β§ π β β0) β π β
β) |
5 | | knoppcnlem11.1 |
. . . . . . 7
β’ (π β πΆ β β) |
6 | 5 | adantr 481 |
. . . . . 6
β’ ((π β§ π β β0) β πΆ β
β) |
7 | | simpr 485 |
. . . . . 6
β’ ((π β§ π β β0) β π β
β0) |
8 | 1, 2, 4, 6, 7 | knoppcnlem7 35467 |
. . . . 5
β’ ((π β§ π β β0) β (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ) = (π€ β β β¦ (seq0( + , (πΉβπ€))βπ))) |
9 | | eqidd 2733 |
. . . . . . . 8
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β ((πΉβπ€)βπ) = ((πΉβπ€)βπ)) |
10 | | simplr 767 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π€ β β) β π β
β0) |
11 | | elnn0uz 12869 |
. . . . . . . . 9
β’ (π β β0
β π β
(β€β₯β0)) |
12 | 10, 11 | sylib 217 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π€ β β) β π β
(β€β₯β0)) |
13 | 4 | ad2antrr 724 |
. . . . . . . . . 10
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β π β β) |
14 | 6 | ad2antrr 724 |
. . . . . . . . . 10
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β πΆ β β) |
15 | | simplr 767 |
. . . . . . . . . 10
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β π€ β β) |
16 | | elfzuz 13499 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β
(β€β₯β0)) |
17 | | nn0uz 12866 |
. . . . . . . . . . . 12
β’
β0 = (β€β₯β0) |
18 | 16, 17 | eleqtrrdi 2844 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β β0) |
19 | 18 | adantl 482 |
. . . . . . . . . 10
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β π β β0) |
20 | 1, 2, 13, 14, 15, 19 | knoppcnlem3 35463 |
. . . . . . . . 9
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β ((πΉβπ€)βπ) β β) |
21 | 20 | recnd 11244 |
. . . . . . . 8
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β ((πΉβπ€)βπ) β β) |
22 | 9, 12, 21 | fsumser 15678 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π€ β β) β
Ξ£π β (0...π)((πΉβπ€)βπ) = (seq0( + , (πΉβπ€))βπ)) |
23 | 22 | eqcomd 2738 |
. . . . . 6
β’ (((π β§ π β β0) β§ π€ β β) β (seq0( +
, (πΉβπ€))βπ) = Ξ£π β (0...π)((πΉβπ€)βπ)) |
24 | 23 | mpteq2dva 5248 |
. . . . 5
β’ ((π β§ π β β0) β (π€ β β β¦ (seq0( +
, (πΉβπ€))βπ)) = (π€ β β β¦ Ξ£π β (0...π)((πΉβπ€)βπ))) |
25 | 8, 24 | eqtrd 2772 |
. . . 4
β’ ((π β§ π β β0) β (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ) = (π€ β β β¦ Ξ£π β (0...π)((πΉβπ€)βπ))) |
26 | | eqid 2732 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
27 | | retopon 24287 |
. . . . . . 7
β’
(topGenβran (,)) β (TopOnββ) |
28 | 27 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β0) β
(topGenβran (,)) β (TopOnββ)) |
29 | | fzfid 13940 |
. . . . . 6
β’ ((π β§ π β β0) β
(0...π) β
Fin) |
30 | 4 | adantr 481 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β (0...π)) β π β β) |
31 | 6 | adantr 481 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β (0...π)) β πΆ β β) |
32 | 18 | adantl 482 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β (0...π)) β π β β0) |
33 | 1, 2, 30, 31, 32 | knoppcnlem10 35470 |
. . . . . 6
β’ (((π β§ π β β0) β§ π β (0...π)) β (π€ β β β¦ ((πΉβπ€)βπ)) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
34 | 26, 28, 29, 33 | fsumcn 24393 |
. . . . 5
β’ ((π β§ π β β0) β (π€ β β β¦
Ξ£π β (0...π)((πΉβπ€)βπ)) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
35 | | ax-resscn 11169 |
. . . . . . 7
β’ β
β β |
36 | | ssid 4004 |
. . . . . . 7
β’ β
β β |
37 | 35, 36 | pm3.2i 471 |
. . . . . 6
β’ (β
β β β§ β β β) |
38 | 26 | tgioo2 24326 |
. . . . . . 7
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
39 | 26 | cnfldtopon 24306 |
. . . . . . . 8
β’
(TopOpenββfld) β
(TopOnββ) |
40 | 39 | toponrestid 22430 |
. . . . . . 7
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
41 | 26, 38, 40 | cncfcn 24433 |
. . . . . 6
β’ ((β
β β β§ β β β) β (ββcnββ) = ((topGenβran (,)) Cn
(TopOpenββfld))) |
42 | 37, 41 | ax-mp 5 |
. . . . 5
β’
(ββcnββ) =
((topGenβran (,)) Cn
(TopOpenββfld)) |
43 | 34, 42 | eleqtrrdi 2844 |
. . . 4
β’ ((π β§ π β β0) β (π€ β β β¦
Ξ£π β (0...π)((πΉβπ€)βπ)) β (ββcnββ)) |
44 | 25, 43 | eqeltrd 2833 |
. . 3
β’ ((π β§ π β β0) β (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ) β (ββcnββ)) |
45 | 44 | fmpttd 7116 |
. 2
β’ (π β (π β β0 β¦ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ)):β0βΆ(ββcnββ)) |
46 | | 0z 12571 |
. . . . . 6
β’ 0 β
β€ |
47 | | seqfn 13980 |
. . . . . 6
β’ (0 β
β€ β seq0( βf + , (π β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn
(β€β₯β0)) |
48 | 46, 47 | ax-mp 5 |
. . . . 5
β’ seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn
(β€β₯β0) |
49 | 17 | fneq2i 6647 |
. . . . 5
β’ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn β0 β seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn
(β€β₯β0)) |
50 | 48, 49 | mpbir 230 |
. . . 4
β’ seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn β0 |
51 | | dffn5 6950 |
. . . 4
β’ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn β0 β seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) = (π β β0 β¦ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ))) |
52 | 50, 51 | mpbi 229 |
. . 3
β’ seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) = (π β β0 β¦ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ)) |
53 | 52 | feq1i 6708 |
. 2
β’ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))):β0βΆ(ββcnββ) β (π β β0 β¦ (seq0(
βf + , (π β
β0 β¦ (π§
β β β¦ ((πΉβπ§)βπ))))βπ)):β0βΆ(ββcnββ)) |
54 | 45, 53 | sylibr 233 |
1
β’ (π β seq0( βf
+ , (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))):β0βΆ(ββcnββ)) |