Step | Hyp | Ref
| Expression |
1 | | knoppcnlem11.t |
. . . . . 6
β’ π = (π₯ β β β¦
(absβ((ββ(π₯ + (1 / 2))) β π₯))) |
2 | | knoppcnlem11.f |
. . . . . 6
β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) |
3 | | knoppcnlem11.n |
. . . . . . 7
β’ (π β π β β) |
4 | 3 | adantr 480 |
. . . . . 6
β’ ((π β§ π β β0) β π β
β) |
5 | | knoppcnlem11.1 |
. . . . . . 7
β’ (π β πΆ β β) |
6 | 5 | adantr 480 |
. . . . . 6
β’ ((π β§ π β β0) β πΆ β
β) |
7 | | simpr 484 |
. . . . . 6
β’ ((π β§ π β β0) β π β
β0) |
8 | 1, 2, 4, 6, 7 | knoppcnlem7 35679 |
. . . . 5
β’ ((π β§ π β β0) β (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ) = (π€ β β β¦ (seq0( + , (πΉβπ€))βπ))) |
9 | | eqidd 2732 |
. . . . . . . 8
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β ((πΉβπ€)βπ) = ((πΉβπ€)βπ)) |
10 | | simplr 766 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π€ β β) β π β
β0) |
11 | | elnn0uz 12872 |
. . . . . . . . 9
β’ (π β β0
β π β
(β€β₯β0)) |
12 | 10, 11 | sylib 217 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π€ β β) β π β
(β€β₯β0)) |
13 | 4 | ad2antrr 723 |
. . . . . . . . . 10
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β π β β) |
14 | 6 | ad2antrr 723 |
. . . . . . . . . 10
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β πΆ β β) |
15 | | simplr 766 |
. . . . . . . . . 10
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β π€ β β) |
16 | | elfzuz 13502 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β
(β€β₯β0)) |
17 | | nn0uz 12869 |
. . . . . . . . . . . 12
β’
β0 = (β€β₯β0) |
18 | 16, 17 | eleqtrrdi 2843 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β β0) |
19 | 18 | adantl 481 |
. . . . . . . . . 10
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β π β β0) |
20 | 1, 2, 13, 14, 15, 19 | knoppcnlem3 35675 |
. . . . . . . . 9
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β ((πΉβπ€)βπ) β β) |
21 | 20 | recnd 11247 |
. . . . . . . 8
β’ ((((π β§ π β β0) β§ π€ β β) β§ π β (0...π)) β ((πΉβπ€)βπ) β β) |
22 | 9, 12, 21 | fsumser 15681 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π€ β β) β
Ξ£π β (0...π)((πΉβπ€)βπ) = (seq0( + , (πΉβπ€))βπ)) |
23 | 22 | eqcomd 2737 |
. . . . . 6
β’ (((π β§ π β β0) β§ π€ β β) β (seq0( +
, (πΉβπ€))βπ) = Ξ£π β (0...π)((πΉβπ€)βπ)) |
24 | 23 | mpteq2dva 5249 |
. . . . 5
β’ ((π β§ π β β0) β (π€ β β β¦ (seq0( +
, (πΉβπ€))βπ)) = (π€ β β β¦ Ξ£π β (0...π)((πΉβπ€)βπ))) |
25 | 8, 24 | eqtrd 2771 |
. . . 4
β’ ((π β§ π β β0) β (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ) = (π€ β β β¦ Ξ£π β (0...π)((πΉβπ€)βπ))) |
26 | | eqid 2731 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
27 | | retopon 24501 |
. . . . . . 7
β’
(topGenβran (,)) β (TopOnββ) |
28 | 27 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β0) β
(topGenβran (,)) β (TopOnββ)) |
29 | | fzfid 13943 |
. . . . . 6
β’ ((π β§ π β β0) β
(0...π) β
Fin) |
30 | 4 | adantr 480 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β (0...π)) β π β β) |
31 | 6 | adantr 480 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β (0...π)) β πΆ β β) |
32 | 18 | adantl 481 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β (0...π)) β π β β0) |
33 | 1, 2, 30, 31, 32 | knoppcnlem10 35682 |
. . . . . 6
β’ (((π β§ π β β0) β§ π β (0...π)) β (π€ β β β¦ ((πΉβπ€)βπ)) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
34 | 26, 28, 29, 33 | fsumcn 24609 |
. . . . 5
β’ ((π β§ π β β0) β (π€ β β β¦
Ξ£π β (0...π)((πΉβπ€)βπ)) β ((topGenβran (,)) Cn
(TopOpenββfld))) |
35 | | ax-resscn 11170 |
. . . . . . 7
β’ β
β β |
36 | | ssid 4005 |
. . . . . . 7
β’ β
β β |
37 | 35, 36 | pm3.2i 470 |
. . . . . 6
β’ (β
β β β§ β β β) |
38 | 26 | tgioo2 24540 |
. . . . . . 7
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
39 | 26 | cnfldtopon 24520 |
. . . . . . . 8
β’
(TopOpenββfld) β
(TopOnββ) |
40 | 39 | toponrestid 22644 |
. . . . . . 7
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
41 | 26, 38, 40 | cncfcn 24651 |
. . . . . 6
β’ ((β
β β β§ β β β) β (ββcnββ) = ((topGenβran (,)) Cn
(TopOpenββfld))) |
42 | 37, 41 | ax-mp 5 |
. . . . 5
β’
(ββcnββ) =
((topGenβran (,)) Cn
(TopOpenββfld)) |
43 | 34, 42 | eleqtrrdi 2843 |
. . . 4
β’ ((π β§ π β β0) β (π€ β β β¦
Ξ£π β (0...π)((πΉβπ€)βπ)) β (ββcnββ)) |
44 | 25, 43 | eqeltrd 2832 |
. . 3
β’ ((π β§ π β β0) β (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ) β (ββcnββ)) |
45 | 44 | fmpttd 7117 |
. 2
β’ (π β (π β β0 β¦ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ)):β0βΆ(ββcnββ)) |
46 | | 0z 12574 |
. . . . . 6
β’ 0 β
β€ |
47 | | seqfn 13983 |
. . . . . 6
β’ (0 β
β€ β seq0( βf + , (π β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn
(β€β₯β0)) |
48 | 46, 47 | ax-mp 5 |
. . . . 5
β’ seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn
(β€β₯β0) |
49 | 17 | fneq2i 6648 |
. . . . 5
β’ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn β0 β seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn
(β€β₯β0)) |
50 | 48, 49 | mpbir 230 |
. . . 4
β’ seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) Fn β0 |
51 | | dffn5 6951 |
. . . 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 6709 |
. 2
β’ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))):β0βΆ(ββcnββ) β (π β β0 β¦ (seq0(
βf + , (π β
β0 β¦ (π§
β β β¦ ((πΉβπ§)βπ))))βπ)):β0βΆ(ββcnββ)) |
54 | 45, 53 | sylibr 233 |
1
β’ (π β seq0( βf
+ , (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))):β0βΆ(ββcnββ)) |