Step | Hyp | Ref
| Expression |
1 | | knoppcnlem9.t |
. . . 4
β’ π = (π₯ β β β¦
(absβ((ββ(π₯ + (1 / 2))) β π₯))) |
2 | | knoppcnlem9.f |
. . . 4
β’ πΉ = (π¦ β β β¦ (π β β0 β¦ ((πΆβπ) Β· (πβ(((2 Β· π)βπ) Β· π¦))))) |
3 | | knoppcnlem9.n |
. . . 4
β’ (π β π β β) |
4 | | knoppcnlem9.1 |
. . . 4
β’ (π β πΆ β β) |
5 | | knoppcnlem9.2 |
. . . 4
β’ (π β (absβπΆ) < 1) |
6 | 1, 2, 3, 4, 5 | knoppcnlem6 35369 |
. . 3
β’ (π β seq0( βf
+ , (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) β dom
(βπ’ββ)) |
7 | | seqex 13967 |
. . . 4
β’ seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) β V |
8 | 7 | eldm 5900 |
. . 3
β’ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))) β dom
(βπ’ββ) β βπseq0( βf + , (π β β0
β¦ (π§ β β
β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) |
9 | 6, 8 | sylib 217 |
. 2
β’ (π β βπseq0( βf + , (π β β0
β¦ (π§ β β
β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) |
10 | | simpr 485 |
. . . . 5
β’ ((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β seq0( βf + ,
(π β β0
β¦ (π§ β β β¦
((πΉβπ§)βπ))))(βπ’ββ)π) |
11 | | ulmcl 25892 |
. . . . . . . 8
β’ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π β π:ββΆβ) |
12 | 11 | feqmptd 6960 |
. . . . . . 7
β’ (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π β π = (π€ β β β¦ (πβπ€))) |
13 | 12 | adantl 482 |
. . . . . 6
β’ ((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β π = (π€ β β β¦ (πβπ€))) |
14 | | nn0uz 12863 |
. . . . . . . . 9
β’
β0 = (β€β₯β0) |
15 | | 0zd 12569 |
. . . . . . . . 9
β’ (((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β 0 β
β€) |
16 | | eqidd 2733 |
. . . . . . . . 9
β’ ((((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β§ π β β0) β ((πΉβπ€)βπ) = ((πΉβπ€)βπ)) |
17 | 3 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π€ β β) β§ π β β0) β π β
β) |
18 | 4 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π€ β β) β§ π β β0) β πΆ β
β) |
19 | | simplr 767 |
. . . . . . . . . . . 12
β’ (((π β§ π€ β β) β§ π β β0) β π€ β
β) |
20 | | simpr 485 |
. . . . . . . . . . . 12
β’ (((π β§ π€ β β) β§ π β β0) β π β
β0) |
21 | 1, 2, 17, 18, 19, 20 | knoppcnlem3 35366 |
. . . . . . . . . . 11
β’ (((π β§ π€ β β) β§ π β β0) β ((πΉβπ€)βπ) β β) |
22 | 21 | adantllr 717 |
. . . . . . . . . 10
β’ ((((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β§ π β β0) β ((πΉβπ€)βπ) β β) |
23 | 22 | recnd 11241 |
. . . . . . . . 9
β’ ((((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β§ π β β0) β ((πΉβπ€)βπ) β β) |
24 | 1, 2, 3, 4 | knoppcnlem8 35371 |
. . . . . . . . . . 11
β’ (π β seq0( βf
+ , (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ)))):β0βΆ(β
βm β)) |
25 | 24 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β seq0( βf +
, (π β β0
β¦ (π§ β β β¦
((πΉβπ§)βπ)))):β0βΆ(β
βm β)) |
26 | | simpr 485 |
. . . . . . . . . 10
β’ (((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β π€ β β) |
27 | | seqex 13967 |
. . . . . . . . . . 11
β’ seq0( + ,
(πΉβπ€)) β V |
28 | 27 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β seq0( + , (πΉβπ€)) β V) |
29 | 3 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π€ β β) β§ π β β0) β π β
β) |
30 | 4 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π€ β β) β§ π β β0) β πΆ β
β) |
31 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ (((π β§ π€ β β) β§ π β β0) β π β
β0) |
32 | 1, 2, 29, 30, 31 | knoppcnlem7 35370 |
. . . . . . . . . . . . 13
β’ (((π β§ π€ β β) β§ π β β0) β (seq0(
βf + , (π
β β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))βπ) = (π£ β β β¦ (seq0( + , (πΉβπ£))βπ))) |
33 | 32 | adantllr 717 |
. . . . . . . . . . . 12
β’ ((((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β§ π β β0) β (seq0(
βf + , (π β
β0 β¦ (π§
β β β¦ ((πΉβπ§)βπ))))βπ) = (π£ β β β¦ (seq0( + , (πΉβπ£))βπ))) |
34 | 33 | fveq1d 6893 |
. . . . . . . . . . 11
β’ ((((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β§ π β β0) β ((seq0(
βf + , (π β
β0 β¦ (π§
β β β¦ ((πΉβπ§)βπ))))βπ)βπ€) = ((π£ β β β¦ (seq0( + , (πΉβπ£))βπ))βπ€)) |
35 | | eqid 2732 |
. . . . . . . . . . . 12
β’ (π£ β β β¦ (seq0( +
, (πΉβπ£))βπ)) = (π£ β β β¦ (seq0( + , (πΉβπ£))βπ)) |
36 | | fveq2 6891 |
. . . . . . . . . . . . . 14
β’ (π£ = π€ β (πΉβπ£) = (πΉβπ€)) |
37 | 36 | seqeq3d 13973 |
. . . . . . . . . . . . 13
β’ (π£ = π€ β seq0( + , (πΉβπ£)) = seq0( + , (πΉβπ€))) |
38 | 37 | fveq1d 6893 |
. . . . . . . . . . . 12
β’ (π£ = π€ β (seq0( + , (πΉβπ£))βπ) = (seq0( + , (πΉβπ€))βπ)) |
39 | 26 | adantr 481 |
. . . . . . . . . . . 12
β’ ((((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β§ π β β0) β π€ β β) |
40 | | fvexd 6906 |
. . . . . . . . . . . 12
β’ ((((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β§ π β β0) β (seq0( + ,
(πΉβπ€))βπ) β V) |
41 | 35, 38, 39, 40 | fvmptd3 7021 |
. . . . . . . . . . 11
β’ ((((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β§ π β β0) β ((π£ β β β¦ (seq0( + ,
(πΉβπ£))βπ))βπ€) = (seq0( + , (πΉβπ€))βπ)) |
42 | 34, 41 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β§ π β β0) β ((seq0(
βf + , (π β
β0 β¦ (π§
β β β¦ ((πΉβπ§)βπ))))βπ)βπ€) = (seq0( + , (πΉβπ€))βπ)) |
43 | | simplr 767 |
. . . . . . . . . 10
β’ (((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β seq0( βf +
, (π β β0
β¦ (π§ β β β¦
((πΉβπ§)βπ))))(βπ’ββ)π) |
44 | 14, 15, 25, 26, 28, 42, 43 | ulmclm 25898 |
. . . . . . . . 9
β’ (((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β seq0( + , (πΉβπ€)) β (πβπ€)) |
45 | 14, 15, 16, 23, 44 | isumclim 15702 |
. . . . . . . 8
β’ (((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β Ξ£π β β0 ((πΉβπ€)βπ) = (πβπ€)) |
46 | 45 | eqcomd 2738 |
. . . . . . 7
β’ (((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β§ π€ β β) β (πβπ€) = Ξ£π β β0 ((πΉβπ€)βπ)) |
47 | 46 | mpteq2dva 5248 |
. . . . . 6
β’ ((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β (π€ β β β¦ (πβπ€)) = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ))) |
48 | | knoppcnlem9.w |
. . . . . . . 8
β’ π = (π€ β β β¦ Ξ£π β β0
((πΉβπ€)βπ)) |
49 | 48 | a1i 11 |
. . . . . . 7
β’ ((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β π = (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ))) |
50 | 49 | eqcomd 2738 |
. . . . . 6
β’ ((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β (π€ β β β¦ Ξ£π β β0 ((πΉβπ€)βπ)) = π) |
51 | 13, 47, 50 | 3eqtrd 2776 |
. . . . 5
β’ ((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β π = π) |
52 | 10, 51 | breqtrd 5174 |
. . . 4
β’ ((π β§ seq0( βf +
, (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) β seq0( βf + ,
(π β β0
β¦ (π§ β β β¦
((πΉβπ§)βπ))))(βπ’ββ)π) |
53 | 52 | ex 413 |
. . 3
β’ (π β (seq0( βf
+ , (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π β seq0( βf + ,
(π β β0
β¦ (π§ β β β¦
((πΉβπ§)βπ))))(βπ’ββ)π)) |
54 | 53 | exlimdv 1936 |
. 2
β’ (π β (βπseq0( βf + , (π β β0
β¦ (π§ β β
β¦ ((πΉβπ§)βπ))))(βπ’ββ)π β seq0( βf + ,
(π β β0
β¦ (π§ β β β¦
((πΉβπ§)βπ))))(βπ’ββ)π)) |
55 | 9, 54 | mpd 15 |
1
β’ (π β seq0( βf
+ , (π β
β0 β¦ (π§ β β β¦ ((πΉβπ§)βπ))))(βπ’ββ)π) |