Step | Hyp | Ref
| Expression |
1 | | uzssz 12791 |
. . . . . 6
β’
(β€β₯βπ) β β€ |
2 | | zssre 12513 |
. . . . . 6
β’ β€
β β |
3 | 1, 2 | sstri 3958 |
. . . . 5
β’
(β€β₯βπ) β β |
4 | 3 | a1i 11 |
. . . 4
β’ (π β
(β€β₯βπ) β β) |
5 | | ioodvbdlimc1lem2.m |
. . . . . . 7
β’ π = ((ββ(1 / (π΅ β π΄))) + 1) |
6 | | ioodvbdlimc1lem2.b |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
7 | | ioodvbdlimc1lem2.a |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
8 | 6, 7 | resubcld 11590 |
. . . . . . . . . 10
β’ (π β (π΅ β π΄) β β) |
9 | | ioodvbdlimc1lem2.altb |
. . . . . . . . . . . 12
β’ (π β π΄ < π΅) |
10 | 7, 6 | posdifd 11749 |
. . . . . . . . . . . 12
β’ (π β (π΄ < π΅ β 0 < (π΅ β π΄))) |
11 | 9, 10 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β 0 < (π΅ β π΄)) |
12 | 11 | gt0ne0d 11726 |
. . . . . . . . . 10
β’ (π β (π΅ β π΄) β 0) |
13 | 8, 12 | rereccld 11989 |
. . . . . . . . 9
β’ (π β (1 / (π΅ β π΄)) β β) |
14 | | 0red 11165 |
. . . . . . . . . 10
β’ (π β 0 β
β) |
15 | 8, 11 | recgt0d 12096 |
. . . . . . . . . 10
β’ (π β 0 < (1 / (π΅ β π΄))) |
16 | 14, 13, 15 | ltled 11310 |
. . . . . . . . 9
β’ (π β 0 β€ (1 / (π΅ β π΄))) |
17 | | flge0nn0 13732 |
. . . . . . . . 9
β’ (((1 /
(π΅ β π΄)) β β β§ 0 β€
(1 / (π΅ β π΄))) β (ββ(1 /
(π΅ β π΄))) β
β0) |
18 | 13, 16, 17 | syl2anc 585 |
. . . . . . . 8
β’ (π β (ββ(1 / (π΅ β π΄))) β
β0) |
19 | | peano2nn0 12460 |
. . . . . . . 8
β’
((ββ(1 / (π΅ β π΄))) β β0 β
((ββ(1 / (π΅
β π΄))) + 1) β
β0) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’ (π β ((ββ(1 /
(π΅ β π΄))) + 1) β
β0) |
21 | 5, 20 | eqeltrid 2842 |
. . . . . 6
β’ (π β π β
β0) |
22 | 21 | nn0zd 12532 |
. . . . 5
β’ (π β π β β€) |
23 | | eqid 2737 |
. . . . . 6
β’
(β€β₯βπ) = (β€β₯βπ) |
24 | 23 | uzsup 13775 |
. . . . 5
β’ (π β β€ β
sup((β€β₯βπ), β*, < ) =
+β) |
25 | 22, 24 | syl 17 |
. . . 4
β’ (π β
sup((β€β₯βπ), β*, < ) =
+β) |
26 | | ioodvbdlimc1lem2.f |
. . . . . . 7
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
27 | 26 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β πΉ:(π΄(,)π΅)βΆβ) |
28 | 7 | rexrd 11212 |
. . . . . . . 8
β’ (π β π΄ β
β*) |
29 | 28 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β π΄ β
β*) |
30 | 6 | rexrd 11212 |
. . . . . . . 8
β’ (π β π΅ β
β*) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β π΅ β
β*) |
32 | 7 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β π΄ β β) |
33 | | eluzelre 12781 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β β) |
34 | 33 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β π β β) |
35 | | 0red 11165 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπ)) β 0 β
β) |
36 | | 0red 11165 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β 0 β β) |
37 | | 1red 11163 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β 1 β β) |
38 | 36, 37 | readdcld 11191 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β (0 + 1) β
β) |
39 | 38 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπ)) β (0 + 1) β
β) |
40 | 36 | ltp1d 12092 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β 0 < (0 + 1)) |
41 | 40 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπ)) β 0 < (0 +
1)) |
42 | | eluzel2 12775 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπ) β π β β€) |
43 | 42 | zred 12614 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β π β β) |
44 | 43 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β π β β) |
45 | 13 | flcld 13710 |
. . . . . . . . . . . . . . . 16
β’ (π β (ββ(1 / (π΅ β π΄))) β β€) |
46 | 45 | zred 12614 |
. . . . . . . . . . . . . . 15
β’ (π β (ββ(1 / (π΅ β π΄))) β β) |
47 | | 1red 11163 |
. . . . . . . . . . . . . . 15
β’ (π β 1 β
β) |
48 | 18 | nn0ge0d 12483 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β€ (ββ(1 /
(π΅ β π΄)))) |
49 | 14, 46, 47, 48 | leadd1dd 11776 |
. . . . . . . . . . . . . 14
β’ (π β (0 + 1) β€
((ββ(1 / (π΅
β π΄))) +
1)) |
50 | 49, 5 | breqtrrdi 5152 |
. . . . . . . . . . . . 13
β’ (π β (0 + 1) β€ π) |
51 | 50 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β (0 + 1) β€ π) |
52 | | eluzle 12783 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β π β€ π) |
53 | 52 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β π β€ π) |
54 | 39, 44, 34, 51, 53 | letrd 11319 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπ)) β (0 + 1) β€ π) |
55 | 35, 39, 34, 41, 54 | ltletrd 11322 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β 0 < π) |
56 | 55 | gt0ne0d 11726 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β π β 0) |
57 | 34, 56 | rereccld 11989 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (1 / π) β
β) |
58 | 32, 57 | readdcld 11191 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (π΄ + (1 / π)) β β) |
59 | 34, 55 | elrpd 12961 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β π β β+) |
60 | 59 | rpreccld 12974 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (1 / π) β
β+) |
61 | 32, 60 | ltaddrpd 12997 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β π΄ < (π΄ + (1 / π))) |
62 | 21 | nn0red 12481 |
. . . . . . . . . . 11
β’ (π β π β β) |
63 | 14, 47 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ (π β (0 + 1) β
β) |
64 | 46, 47 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ (π β ((ββ(1 /
(π΅ β π΄))) + 1) β
β) |
65 | 14 | ltp1d 12092 |
. . . . . . . . . . . . . 14
β’ (π β 0 < (0 +
1)) |
66 | 14, 63, 64, 65, 49 | ltletrd 11322 |
. . . . . . . . . . . . 13
β’ (π β 0 < ((ββ(1
/ (π΅ β π΄))) + 1)) |
67 | 66, 5 | breqtrrdi 5152 |
. . . . . . . . . . . 12
β’ (π β 0 < π) |
68 | 67 | gt0ne0d 11726 |
. . . . . . . . . . 11
β’ (π β π β 0) |
69 | 62, 68 | rereccld 11989 |
. . . . . . . . . 10
β’ (π β (1 / π) β β) |
70 | 69 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β (1 / π) β β) |
71 | 32, 70 | readdcld 11191 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (π΄ + (1 / π)) β β) |
72 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β π΅ β β) |
73 | 62, 67 | elrpd 12961 |
. . . . . . . . . . 11
β’ (π β π β
β+) |
74 | 73 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β π β
β+) |
75 | | 1red 11163 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β 1 β
β) |
76 | | 0le1 11685 |
. . . . . . . . . . 11
β’ 0 β€
1 |
77 | 76 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β 0 β€
1) |
78 | 74, 59, 75, 77, 53 | lediv2ad 12986 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β (1 / π) β€ (1 / π)) |
79 | 57, 70, 32, 78 | leadd2dd 11777 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (π΄ + (1 / π)) β€ (π΄ + (1 / π))) |
80 | 5 | eqcomi 2746 |
. . . . . . . . . . . . 13
β’
((ββ(1 / (π΅ β π΄))) + 1) = π |
81 | 80 | oveq2i 7373 |
. . . . . . . . . . . 12
β’ (1 /
((ββ(1 / (π΅
β π΄))) + 1)) = (1 /
π) |
82 | 81, 69 | eqeltrid 2842 |
. . . . . . . . . . 11
β’ (π β (1 / ((ββ(1 /
(π΅ β π΄))) + 1)) β
β) |
83 | 13, 15 | elrpd 12961 |
. . . . . . . . . . . . 13
β’ (π β (1 / (π΅ β π΄)) β
β+) |
84 | 64, 66 | elrpd 12961 |
. . . . . . . . . . . . 13
β’ (π β ((ββ(1 /
(π΅ β π΄))) + 1) β
β+) |
85 | | 1rp 12926 |
. . . . . . . . . . . . . 14
β’ 1 β
β+ |
86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 1 β
β+) |
87 | | fllelt 13709 |
. . . . . . . . . . . . . . 15
β’ ((1 /
(π΅ β π΄)) β β β
((ββ(1 / (π΅
β π΄))) β€ (1 /
(π΅ β π΄)) β§ (1 / (π΅ β π΄)) < ((ββ(1 / (π΅ β π΄))) + 1))) |
88 | 13, 87 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((ββ(1 /
(π΅ β π΄))) β€ (1 / (π΅ β π΄)) β§ (1 / (π΅ β π΄)) < ((ββ(1 / (π΅ β π΄))) + 1))) |
89 | 88 | simprd 497 |
. . . . . . . . . . . . 13
β’ (π β (1 / (π΅ β π΄)) < ((ββ(1 / (π΅ β π΄))) + 1)) |
90 | 83, 84, 86, 89 | ltdiv2dd 43602 |
. . . . . . . . . . . 12
β’ (π β (1 / ((ββ(1 /
(π΅ β π΄))) + 1)) < (1 / (1 / (π΅ β π΄)))) |
91 | 8 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (π β (π΅ β π΄) β β) |
92 | 91, 12 | recrecd 11935 |
. . . . . . . . . . . 12
β’ (π β (1 / (1 / (π΅ β π΄))) = (π΅ β π΄)) |
93 | 90, 92 | breqtrd 5136 |
. . . . . . . . . . 11
β’ (π β (1 / ((ββ(1 /
(π΅ β π΄))) + 1)) < (π΅ β π΄)) |
94 | 82, 8, 7, 93 | ltadd2dd 11321 |
. . . . . . . . . 10
β’ (π β (π΄ + (1 / ((ββ(1 / (π΅ β π΄))) + 1))) < (π΄ + (π΅ β π΄))) |
95 | 5 | oveq2i 7373 |
. . . . . . . . . . . 12
β’ (1 /
π) = (1 /
((ββ(1 / (π΅
β π΄))) +
1)) |
96 | 95 | oveq2i 7373 |
. . . . . . . . . . 11
β’ (π΄ + (1 / π)) = (π΄ + (1 / ((ββ(1 / (π΅ β π΄))) + 1))) |
97 | 96 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π΄ + (1 / π)) = (π΄ + (1 / ((ββ(1 / (π΅ β π΄))) + 1)))) |
98 | 7 | recnd 11190 |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
99 | 6 | recnd 11190 |
. . . . . . . . . . . 12
β’ (π β π΅ β β) |
100 | 98, 99 | pncan3d 11522 |
. . . . . . . . . . 11
β’ (π β (π΄ + (π΅ β π΄)) = π΅) |
101 | 100 | eqcomd 2743 |
. . . . . . . . . 10
β’ (π β π΅ = (π΄ + (π΅ β π΄))) |
102 | 94, 97, 101 | 3brtr4d 5142 |
. . . . . . . . 9
β’ (π β (π΄ + (1 / π)) < π΅) |
103 | 102 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β (π΄ + (1 / π)) < π΅) |
104 | 58, 71, 72, 79, 103 | lelttrd 11320 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (π΄ + (1 / π)) < π΅) |
105 | 29, 31, 58, 61, 104 | eliood 43810 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β (π΄ + (1 / π)) β (π΄(,)π΅)) |
106 | 27, 105 | ffvelcdmd 7041 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β (πΉβ(π΄ + (1 / π))) β β) |
107 | | ioodvbdlimc1lem2.s |
. . . . 5
β’ π = (π β (β€β₯βπ) β¦ (πΉβ(π΄ + (1 / π)))) |
108 | 106, 107 | fmptd 7067 |
. . . 4
β’ (π β π:(β€β₯βπ)βΆβ) |
109 | | ioodvbdlimc1lem2.dmdv |
. . . . . 6
β’ (π β dom (β D πΉ) = (π΄(,)π΅)) |
110 | | ioodvbdlimc1lem2.dvbd |
. . . . . 6
β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) |
111 | 7, 6, 9, 26, 109, 110 | dvbdfbdioo 44245 |
. . . . 5
β’ (π β βπ β β βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) |
112 | 62 | adantr 482 |
. . . . . . . 8
β’ ((π β§ βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) β π β β) |
113 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
114 | 107 | fvmpt2 6964 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯βπ) β§ (πΉβ(π΄ + (1 / π))) β β) β (πβπ) = (πΉβ(π΄ + (1 / π)))) |
115 | 113, 106,
114 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β (πβπ) = (πΉβ(π΄ + (1 / π)))) |
116 | 115 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β (absβ(πβπ)) = (absβ(πΉβ(π΄ + (1 / π))))) |
117 | 116 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) β§ π β (β€β₯βπ)) β (absβ(πβπ)) = (absβ(πΉβ(π΄ + (1 / π))))) |
118 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) β§ π β (β€β₯βπ)) β βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) |
119 | 105 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) β§ π β (β€β₯βπ)) β (π΄ + (1 / π)) β (π΄(,)π΅)) |
120 | | 2fveq3 6852 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π΄ + (1 / π)) β (absβ(πΉβπ₯)) = (absβ(πΉβ(π΄ + (1 / π))))) |
121 | 120 | breq1d 5120 |
. . . . . . . . . . . . 13
β’ (π₯ = (π΄ + (1 / π)) β ((absβ(πΉβπ₯)) β€ π β (absβ(πΉβ(π΄ + (1 / π)))) β€ π)) |
122 | 121 | rspccva 3583 |
. . . . . . . . . . . 12
β’
((βπ₯ β
(π΄(,)π΅)(absβ(πΉβπ₯)) β€ π β§ (π΄ + (1 / π)) β (π΄(,)π΅)) β (absβ(πΉβ(π΄ + (1 / π)))) β€ π) |
123 | 118, 119,
122 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) β§ π β (β€β₯βπ)) β (absβ(πΉβ(π΄ + (1 / π)))) β€ π) |
124 | 117, 123 | eqbrtrd 5132 |
. . . . . . . . . 10
β’ (((π β§ βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) β§ π β (β€β₯βπ)) β (absβ(πβπ)) β€ π) |
125 | 124 | a1d 25 |
. . . . . . . . 9
β’ (((π β§ βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) β§ π β (β€β₯βπ)) β (π β€ π β (absβ(πβπ)) β€ π)) |
126 | 125 | ralrimiva 3144 |
. . . . . . . 8
β’ ((π β§ βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) β βπ β (β€β₯βπ)(π β€ π β (absβ(πβπ)) β€ π)) |
127 | | breq1 5113 |
. . . . . . . . . . 11
β’ (π = π β (π β€ π β π β€ π)) |
128 | 127 | imbi1d 342 |
. . . . . . . . . 10
β’ (π = π β ((π β€ π β (absβ(πβπ)) β€ π) β (π β€ π β (absβ(πβπ)) β€ π))) |
129 | 128 | ralbidv 3175 |
. . . . . . . . 9
β’ (π = π β (βπ β (β€β₯βπ)(π β€ π β (absβ(πβπ)) β€ π) β βπ β (β€β₯βπ)(π β€ π β (absβ(πβπ)) β€ π))) |
130 | 129 | rspcev 3584 |
. . . . . . . 8
β’ ((π β β β§
βπ β
(β€β₯βπ)(π β€ π β (absβ(πβπ)) β€ π)) β βπ β β βπ β (β€β₯βπ)(π β€ π β (absβ(πβπ)) β€ π)) |
131 | 112, 126,
130 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) β βπ β β βπ β (β€β₯βπ)(π β€ π β (absβ(πβπ)) β€ π)) |
132 | 131 | ex 414 |
. . . . . 6
β’ (π β (βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π β βπ β β βπ β (β€β₯βπ)(π β€ π β (absβ(πβπ)) β€ π))) |
133 | 132 | reximdv 3168 |
. . . . 5
β’ (π β (βπ β β βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π β βπ β β βπ β β βπ β (β€β₯βπ)(π β€ π β (absβ(πβπ)) β€ π))) |
134 | 111, 133 | mpd 15 |
. . . 4
β’ (π β βπ β β βπ β β βπ β (β€β₯βπ)(π β€ π β (absβ(πβπ)) β€ π)) |
135 | 4, 25, 108, 134 | limsupre 43956 |
. . 3
β’ (π β (lim supβπ) β
β) |
136 | 135 | recnd 11190 |
. 2
β’ (π β (lim supβπ) β
β) |
137 | | eluzelre 12781 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β π β β) |
138 | 137 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β π β β) |
139 | | 0red 11165 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β 0 β β) |
140 | 45 | peano2zd 12617 |
. . . . . . . . . . . . . 14
β’ (π β ((ββ(1 /
(π΅ β π΄))) + 1) β
β€) |
141 | 5, 140 | eqeltrid 2842 |
. . . . . . . . . . . . 13
β’ (π β π β β€) |
142 | 141 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β π β
β€) |
143 | 142 | zred 12614 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β π β
β) |
144 | 143 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β π β β) |
145 | 67 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β 0 < π) |
146 | | ioodvbdlimc1lem2.n |
. . . . . . . . . . . . . 14
β’ π = if(π β€ ((ββ(π / (π₯ / 2))) + 1), ((ββ(π / (π₯ / 2))) + 1), π) |
147 | | ioodvbdlimc1lem2.y |
. . . . . . . . . . . . . . . . . . . 20
β’ π = sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) |
148 | | ioomidp 43826 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β ((π΄ + π΅) / 2) β (π΄(,)π΅)) |
149 | 7, 6, 9, 148 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((π΄ + π΅) / 2) β (π΄(,)π΅)) |
150 | | ne0i 4299 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π΄ + π΅) / 2) β (π΄(,)π΅) β (π΄(,)π΅) β β
) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π΄(,)π΅) β β
) |
152 | | ioossre 13332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π΄(,)π΅) β β |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (π΄(,)π΅) β β) |
154 | | dvfre 25331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ:(π΄(,)π΅)βΆβ β§ (π΄(,)π΅) β β) β (β D πΉ):dom (β D πΉ)βΆβ) |
155 | 26, 153, 154 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (β D πΉ):dom (β D πΉ)βΆβ) |
156 | 109 | feq2d 6659 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((β D πΉ):dom (β D πΉ)βΆβ β (β
D πΉ):(π΄(,)π΅)βΆβ)) |
157 | 155, 156 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (β D πΉ):(π΄(,)π΅)βΆβ) |
158 | 157 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π₯ β (π΄(,)π΅)) β ((β D πΉ)βπ₯) β β) |
159 | 158 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β (π΄(,)π΅)) β ((β D πΉ)βπ₯) β β) |
160 | 159 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (π΄(,)π΅)) β (absβ((β D πΉ)βπ₯)) β β) |
161 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))) = (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))) |
162 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ sup(ran
(π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) = sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) |
163 | 151, 160,
110, 161, 162 | suprnmpt 43465 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) β β β§
βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ))) |
164 | 163 | simpld 496 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) β
β) |
165 | 147, 164 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
166 | 165 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β β+) β π β
β) |
167 | | rpre 12930 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β+
β π₯ β
β) |
168 | 167 | rehalfcld 12407 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β+
β (π₯ / 2) β
β) |
169 | 168 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β β+) β (π₯ / 2) β
β) |
170 | 167 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β+
β π₯ β
β) |
171 | 170 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β β+) β π₯ β
β) |
172 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β β+) β 2 β
β) |
173 | | rpne0 12938 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β+
β π₯ β
0) |
174 | 173 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β β+) β π₯ β 0) |
175 | | 2ne0 12264 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
0 |
176 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β β+) β 2 β
0) |
177 | 171, 172,
174, 176 | divne0d 11954 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β β+) β (π₯ / 2) β 0) |
178 | 166, 169,
177 | redivcld 11990 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β β+) β (π / (π₯ / 2)) β β) |
179 | 178 | flcld 13710 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β+) β
(ββ(π / (π₯ / 2))) β
β€) |
180 | 179 | peano2zd 12617 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β+) β
((ββ(π / (π₯ / 2))) + 1) β
β€) |
181 | 180, 142 | ifcld 4537 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β if(π β€ ((ββ(π / (π₯ / 2))) + 1), ((ββ(π / (π₯ / 2))) + 1), π) β β€) |
182 | 146, 181 | eqeltrid 2842 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β π β
β€) |
183 | 182 | zred 12614 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β π β
β) |
184 | 183 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β π β β) |
185 | 180 | zred 12614 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β
((ββ(π / (π₯ / 2))) + 1) β
β) |
186 | | max1 13111 |
. . . . . . . . . . . . . 14
β’ ((π β β β§
((ββ(π / (π₯ / 2))) + 1) β β)
β π β€ if(π β€ ((ββ(π / (π₯ / 2))) + 1), ((ββ(π / (π₯ / 2))) + 1), π)) |
187 | 143, 185,
186 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β π β€ if(π β€ ((ββ(π / (π₯ / 2))) + 1), ((ββ(π / (π₯ / 2))) + 1), π)) |
188 | 187, 146 | breqtrrdi 5152 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β π β€ π) |
189 | 188 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β π β€ π) |
190 | | eluzle 12783 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β π β€ π) |
191 | 190 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β π β€ π) |
192 | 144, 184,
138, 189, 191 | letrd 11319 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β π β€ π) |
193 | 139, 144,
138, 145, 192 | ltletrd 11322 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β 0 < π) |
194 | 193 | gt0ne0d 11726 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β π β 0) |
195 | 138, 194 | rereccld 11989 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β (1 / π) β β) |
196 | 138, 193 | recgt0d 12096 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β 0 < (1 / π)) |
197 | 195, 196 | elrpd 12961 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β (1 / π) β
β+) |
198 | 197 | adantr 482 |
. . . . 5
β’ ((((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β (1 / π) β
β+) |
199 | | ioodvbdlimc1lem2.ch |
. . . . . . . . 9
β’ (π β (((((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π))) |
200 | 199 | biimpi 215 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π))) |
201 | | simp-5l 784 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π₯ β β+)
β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π)) β π) |
202 | 200, 201 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π) |
203 | 202, 26 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
204 | 200 | simplrd 769 |
. . . . . . . . . . . . . . 15
β’ (π β π§ β (π΄(,)π΅)) |
205 | 203, 204 | ffvelcdmd 7041 |
. . . . . . . . . . . . . 14
β’ (π β (πΉβπ§) β β) |
206 | 205 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (π β (πΉβπ§) β β) |
207 | 202, 108 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π:(β€β₯βπ)βΆβ) |
208 | | simp-5r 785 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π₯ β β+)
β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π)) β π₯ β β+) |
209 | 200, 208 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π₯ β β+) |
210 | | eluz2 12776 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(β€β₯βπ) β (π β β€ β§ π β β€ β§ π β€ π)) |
211 | 142, 182,
188, 210 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β β+) β π β
(β€β₯βπ)) |
212 | 202, 209,
211 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (β€β₯βπ)) |
213 | | uzss 12793 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β
(β€β₯βπ)) |
214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βπ) β
(β€β₯βπ)) |
215 | | simp-4r 783 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π₯ β β+)
β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π)) β π β (β€β₯βπ)) |
216 | 200, 215 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (β€β₯βπ)) |
217 | 214, 216 | sseldd 3950 |
. . . . . . . . . . . . . . 15
β’ (π β π β (β€β₯βπ)) |
218 | 207, 217 | ffvelcdmd 7041 |
. . . . . . . . . . . . . 14
β’ (π β (πβπ) β β) |
219 | 218 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (π β (πβπ) β β) |
220 | 202, 136 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (lim supβπ) β
β) |
221 | 206, 219,
220 | npncand 11543 |
. . . . . . . . . . . 12
β’ (π β (((πΉβπ§) β (πβπ)) + ((πβπ) β (lim supβπ))) = ((πΉβπ§) β (lim supβπ))) |
222 | 221 | eqcomd 2743 |
. . . . . . . . . . 11
β’ (π β ((πΉβπ§) β (lim supβπ)) = (((πΉβπ§) β (πβπ)) + ((πβπ) β (lim supβπ)))) |
223 | 222 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π β (absβ((πΉβπ§) β (lim supβπ))) = (absβ(((πΉβπ§) β (πβπ)) + ((πβπ) β (lim supβπ))))) |
224 | 205, 218 | resubcld 11590 |
. . . . . . . . . . . . . 14
β’ (π β ((πΉβπ§) β (πβπ)) β β) |
225 | 202, 135 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (lim supβπ) β
β) |
226 | 218, 225 | resubcld 11590 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπ) β (lim supβπ)) β β) |
227 | 224, 226 | readdcld 11191 |
. . . . . . . . . . . . 13
β’ (π β (((πΉβπ§) β (πβπ)) + ((πβπ) β (lim supβπ))) β β) |
228 | 227 | recnd 11190 |
. . . . . . . . . . . 12
β’ (π β (((πΉβπ§) β (πβπ)) + ((πβπ) β (lim supβπ))) β β) |
229 | 228 | abscld 15328 |
. . . . . . . . . . 11
β’ (π β (absβ(((πΉβπ§) β (πβπ)) + ((πβπ) β (lim supβπ)))) β β) |
230 | 224 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (π β ((πΉβπ§) β (πβπ)) β β) |
231 | 230 | abscld 15328 |
. . . . . . . . . . . 12
β’ (π β (absβ((πΉβπ§) β (πβπ))) β β) |
232 | 226 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (π β ((πβπ) β (lim supβπ)) β β) |
233 | 232 | abscld 15328 |
. . . . . . . . . . . 12
β’ (π β (absβ((πβπ) β (lim supβπ))) β β) |
234 | 231, 233 | readdcld 11191 |
. . . . . . . . . . 11
β’ (π β ((absβ((πΉβπ§) β (πβπ))) + (absβ((πβπ) β (lim supβπ)))) β β) |
235 | 209 | rpred 12964 |
. . . . . . . . . . 11
β’ (π β π₯ β β) |
236 | 230, 232 | abstrid 15348 |
. . . . . . . . . . 11
β’ (π β (absβ(((πΉβπ§) β (πβπ)) + ((πβπ) β (lim supβπ)))) β€ ((absβ((πΉβπ§) β (πβπ))) + (absβ((πβπ) β (lim supβπ))))) |
237 | 235 | rehalfcld 12407 |
. . . . . . . . . . . . 13
β’ (π β (π₯ / 2) β β) |
238 | 206, 219 | abssubd 15345 |
. . . . . . . . . . . . . 14
β’ (π β (absβ((πΉβπ§) β (πβπ))) = (absβ((πβπ) β (πΉβπ§)))) |
239 | 202, 217,
115 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβπ) = (πΉβ(π΄ + (1 / π)))) |
240 | 239 | fvoveq1d 7384 |
. . . . . . . . . . . . . . 15
β’ (π β (absβ((πβπ) β (πΉβπ§))) = (absβ((πΉβ(π΄ + (1 / π))) β (πΉβπ§)))) |
241 | 202, 217,
106 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΉβ(π΄ + (1 / π))) β β) |
242 | 241, 205 | resubcld 11590 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((πΉβ(π΄ + (1 / π))) β (πΉβπ§)) β β) |
243 | 242 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((πΉβ(π΄ + (1 / π))) β (πΉβπ§)) β β) |
244 | 243 | abscld 15328 |
. . . . . . . . . . . . . . . 16
β’ (π β (absβ((πΉβ(π΄ + (1 / π))) β (πΉβπ§))) β β) |
245 | 202, 165 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
246 | 202, 217,
58 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ + (1 / π)) β β) |
247 | 152, 204 | sselid 3947 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π§ β β) |
248 | 246, 247 | resubcld 11590 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π΄ + (1 / π)) β π§) β β) |
249 | 245, 248 | remulcld 11192 |
. . . . . . . . . . . . . . . 16
β’ (π β (π Β· ((π΄ + (1 / π)) β π§)) β β) |
250 | 202, 7 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β β) |
251 | 202, 6 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΅ β β) |
252 | 202, 109 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom (β D πΉ) = (π΄(,)π΅)) |
253 | 163 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < )) |
254 | 147 | breq2i 5118 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((absβ((β D πΉ)βπ₯)) β€ π β (absβ((β D πΉ)βπ₯)) β€ sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < )) |
255 | 254 | ralbii 3097 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ₯ β
(π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < )) |
256 | 253, 255 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) |
257 | 202, 256 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) |
258 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ = π₯ β (absβ((β D πΉ)βπ€)) = (absβ((β D πΉ)βπ₯))) |
259 | 258 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = π₯ β ((absβ((β D πΉ)βπ€)) β€ π β (absβ((β D πΉ)βπ₯)) β€ π)) |
260 | 259 | cbvralvw 3228 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ€ β
(π΄(,)π΅)(absβ((β D πΉ)βπ€)) β€ π β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) |
261 | 257, 260 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ€ β (π΄(,)π΅)(absβ((β D πΉ)βπ€)) β€ π) |
262 | 247 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π§ β β*) |
263 | 202, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ β
β*) |
264 | 247, 250 | resubcld 11590 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π§ β π΄) β β) |
265 | 264 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π§ β π΄) β β) |
266 | 265 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (absβ(π§ β π΄)) β β) |
267 | 3, 217 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β β) |
268 | 202, 217,
56 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β 0) |
269 | 267, 268 | rereccld 11989 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1 / π) β β) |
270 | 264 | leabsd 15306 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π§ β π΄) β€ (absβ(π§ β π΄))) |
271 | 200 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (absβ(π§ β π΄)) < (1 / π)) |
272 | 264, 266,
269, 270, 271 | lelttrd 11320 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π§ β π΄) < (1 / π)) |
273 | 247, 250,
269 | ltsubadd2d 11760 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π§ β π΄) < (1 / π) β π§ < (π΄ + (1 / π)))) |
274 | 272, 273 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π§ < (π΄ + (1 / π))) |
275 | 202, 217,
104 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π΄ + (1 / π)) < π΅) |
276 | 262, 263,
246, 274, 275 | eliood 43810 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ + (1 / π)) β (π§(,)π΅)) |
277 | 250, 251,
203, 252, 245, 261, 204, 276 | dvbdfbdioolem1 44243 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((absβ((πΉβ(π΄ + (1 / π))) β (πΉβπ§))) β€ (π Β· ((π΄ + (1 / π)) β π§)) β§ (absβ((πΉβ(π΄ + (1 / π))) β (πΉβπ§))) β€ (π Β· (π΅ β π΄)))) |
278 | 277 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ (π β (absβ((πΉβ(π΄ + (1 / π))) β (πΉβπ§))) β€ (π Β· ((π΄ + (1 / π)) β π§))) |
279 | 202, 217,
57 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1 / π) β β) |
280 | 245, 279 | remulcld 11192 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π Β· (1 / π)) β β) |
281 | 157, 149 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((β D πΉ)β((π΄ + π΅) / 2)) β β) |
282 | 281 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((β D πΉ)β((π΄ + π΅) / 2)) β β) |
283 | 282 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (absβ((β D
πΉ)β((π΄ + π΅) / 2))) β β) |
284 | 282 | absge0d 15336 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β 0 β€
(absβ((β D πΉ)β((π΄ + π΅) / 2)))) |
285 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = ((π΄ + π΅) / 2) β (absβ((β D πΉ)βπ₯)) = (absβ((β D πΉ)β((π΄ + π΅) / 2)))) |
286 | 147 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ sup(ran
(π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) = π |
287 | 286 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = ((π΄ + π΅) / 2) β sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) = π) |
288 | 285, 287 | breq12d 5123 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = ((π΄ + π΅) / 2) β ((absβ((β D πΉ)βπ₯)) β€ sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) β
(absβ((β D πΉ)β((π΄ + π΅) / 2))) β€ π)) |
289 | 288 | rspcva 3582 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ + π΅) / 2) β (π΄(,)π΅) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < )) β
(absβ((β D πΉ)β((π΄ + π΅) / 2))) β€ π) |
290 | 149, 253,
289 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (absβ((β D
πΉ)β((π΄ + π΅) / 2))) β€ π) |
291 | 14, 283, 165, 284, 290 | letrd 11319 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β 0 β€ π) |
292 | 202, 291 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 0 β€ π) |
293 | 202, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π΄ β
β*) |
294 | | ioogtlb 43807 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β β*
β§ π΅ β
β* β§ π§
β (π΄(,)π΅)) β π΄ < π§) |
295 | 293, 263,
204, 294 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π΄ < π§) |
296 | 250, 247,
246, 295 | ltsub2dd 11775 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π΄ + (1 / π)) β π§) < ((π΄ + (1 / π)) β π΄)) |
297 | 202, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π΄ β β) |
298 | 279 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1 / π) β β) |
299 | 297, 298 | pncan2d 11521 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π΄ + (1 / π)) β π΄) = (1 / π)) |
300 | 296, 299 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π΄ + (1 / π)) β π§) < (1 / π)) |
301 | 248, 269,
300 | ltled 11310 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π΄ + (1 / π)) β π§) β€ (1 / π)) |
302 | 248, 269,
245, 292, 301 | lemul2ad 12102 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π Β· ((π΄ + (1 / π)) β π§)) β€ (π Β· (1 / π))) |
303 | 280 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π = 0) β (π Β· (1 / π)) β β) |
304 | 237 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π = 0) β (π₯ / 2) β β) |
305 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 0 β (π Β· (1 / π)) = (0 Β· (1 / π))) |
306 | 298 | mul02d 11360 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0 Β· (1 / π)) = 0) |
307 | 305, 306 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π = 0) β (π Β· (1 / π)) = 0) |
308 | 209 | rphalfcld 12976 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π₯ / 2) β
β+) |
309 | 308 | rpgt0d 12967 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 0 < (π₯ / 2)) |
310 | 309 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π = 0) β 0 < (π₯ / 2)) |
311 | 307, 310 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π = 0) β (π Β· (1 / π)) < (π₯ / 2)) |
312 | 303, 304,
311 | ltled 11310 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π = 0) β (π Β· (1 / π)) β€ (π₯ / 2)) |
313 | 245 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ Β¬ π = 0) β π β β) |
314 | 292 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ Β¬ π = 0) β 0 β€ π) |
315 | | neqne 2952 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬
π = 0 β π β 0) |
316 | 315 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ Β¬ π = 0) β π β 0) |
317 | 313, 314,
316 | ne0gt0d 11299 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ Β¬ π = 0) β 0 < π) |
318 | 280 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ 0 < π) β (π Β· (1 / π)) β β) |
319 | 3, 212 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β) |
320 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β 0 β
β) |
321 | 202, 209,
143 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β β) |
322 | 202, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β 0 < π) |
323 | 202, 209,
188 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β€ π) |
324 | 320, 321,
319, 322, 323 | ltletrd 11322 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β 0 < π) |
325 | 324 | gt0ne0d 11726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β 0) |
326 | 319, 325 | rereccld 11989 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1 / π) β β) |
327 | 245, 326 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π Β· (1 / π)) β β) |
328 | 327 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ 0 < π) β (π Β· (1 / π)) β β) |
329 | 237 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ 0 < π) β (π₯ / 2) β β) |
330 | 279 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ 0 < π) β (1 / π) β β) |
331 | 326 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ 0 < π) β (1 / π) β β) |
332 | 245 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ 0 < π) β π β β) |
333 | 292 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ 0 < π) β 0 β€ π) |
334 | 319, 324 | elrpd 12961 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β
β+) |
335 | 202, 217,
59 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β+) |
336 | | 1red 11163 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β 1 β
β) |
337 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β 0 β€ 1) |
338 | 216, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β€ π) |
339 | 334, 335,
336, 337, 338 | lediv2ad 12986 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1 / π) β€ (1 / π)) |
340 | 339 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ 0 < π) β (1 / π) β€ (1 / π)) |
341 | 330, 331,
332, 333, 340 | lemul2ad 12102 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ 0 < π) β (π Β· (1 / π)) β€ (π Β· (1 / π))) |
342 | 235 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π₯ β β) |
343 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β 2 β
β) |
344 | 209 | rpne0d 12969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π₯ β 0) |
345 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β 2 β 0) |
346 | 342, 343,
344, 345 | divne0d 11954 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π₯ / 2) β 0) |
347 | 245, 237,
346 | redivcld 11990 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π / (π₯ / 2)) β β) |
348 | 347 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ 0 < π) β (π / (π₯ / 2)) β β) |
349 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ 0 < π) β 0 < π) |
350 | 309 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ 0 < π) β 0 < (π₯ / 2)) |
351 | 332, 329,
349, 350 | divgt0d 12097 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ 0 < π) β 0 < (π / (π₯ / 2))) |
352 | 348, 351 | elrpd 12961 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β (π / (π₯ / 2)) β
β+) |
353 | 352 | rprecred 12975 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ 0 < π) β (1 / (π / (π₯ / 2))) β β) |
354 | 334 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β π β
β+) |
355 | | 1red 11163 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β 1 β β) |
356 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β 0 β€ 1) |
357 | 347 | flcld 13710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (ββ(π / (π₯ / 2))) β β€) |
358 | 357 | peano2zd 12617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((ββ(π / (π₯ / 2))) + 1) β β€) |
359 | 358 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((ββ(π / (π₯ / 2))) + 1) β β) |
360 | 202, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β β€) |
361 | 358, 360 | ifcld 4537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β if(π β€ ((ββ(π / (π₯ / 2))) + 1), ((ββ(π / (π₯ / 2))) + 1), π) β β€) |
362 | 146, 361 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π β β€) |
363 | 362 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β β) |
364 | | flltp1 13712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π / (π₯ / 2)) β β β (π / (π₯ / 2)) < ((ββ(π / (π₯ / 2))) + 1)) |
365 | 347, 364 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π / (π₯ / 2)) < ((ββ(π / (π₯ / 2))) + 1)) |
366 | 202, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β β) |
367 | | max2 13113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β β β§
((ββ(π / (π₯ / 2))) + 1) β β)
β ((ββ(π /
(π₯ / 2))) + 1) β€
if(π β€
((ββ(π / (π₯ / 2))) + 1),
((ββ(π / (π₯ / 2))) + 1), π)) |
368 | 366, 359,
367 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((ββ(π / (π₯ / 2))) + 1) β€ if(π β€ ((ββ(π / (π₯ / 2))) + 1), ((ββ(π / (π₯ / 2))) + 1), π)) |
369 | 368, 146 | breqtrrdi 5152 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((ββ(π / (π₯ / 2))) + 1) β€ π) |
370 | 347, 359,
363, 365, 369 | ltletrd 11322 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π / (π₯ / 2)) < π) |
371 | 347, 319,
370 | ltled 11310 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π / (π₯ / 2)) β€ π) |
372 | 371 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β (π / (π₯ / 2)) β€ π) |
373 | 352, 354,
355, 356, 372 | lediv2ad 12986 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ 0 < π) β (1 / π) β€ (1 / (π / (π₯ / 2)))) |
374 | 331, 353,
332, 333, 373 | lemul2ad 12102 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ 0 < π) β (π Β· (1 / π)) β€ (π Β· (1 / (π / (π₯ / 2))))) |
375 | 332 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β π β β) |
376 | 348 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β (π / (π₯ / 2)) β β) |
377 | 351 | gt0ne0d 11726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β (π / (π₯ / 2)) β 0) |
378 | 375, 376,
377 | divrecd 11941 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ 0 < π) β (π / (π / (π₯ / 2))) = (π Β· (1 / (π / (π₯ / 2))))) |
379 | 329 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β (π₯ / 2) β β) |
380 | 349 | gt0ne0d 11726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β π β 0) |
381 | 346 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 < π) β (π₯ / 2) β 0) |
382 | 375, 379,
380, 381 | ddcand 11958 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ 0 < π) β (π / (π / (π₯ / 2))) = (π₯ / 2)) |
383 | 378, 382 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ 0 < π) β (π Β· (1 / (π / (π₯ / 2)))) = (π₯ / 2)) |
384 | 374, 383 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ 0 < π) β (π Β· (1 / π)) β€ (π₯ / 2)) |
385 | 318, 328,
329, 341, 384 | letrd 11319 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ 0 < π) β (π Β· (1 / π)) β€ (π₯ / 2)) |
386 | 317, 385 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ π = 0) β (π Β· (1 / π)) β€ (π₯ / 2)) |
387 | 312, 386 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π Β· (1 / π)) β€ (π₯ / 2)) |
388 | 249, 280,
237, 302, 387 | letrd 11319 |
. . . . . . . . . . . . . . . 16
β’ (π β (π Β· ((π΄ + (1 / π)) β π§)) β€ (π₯ / 2)) |
389 | 244, 249,
237, 278, 388 | letrd 11319 |
. . . . . . . . . . . . . . 15
β’ (π β (absβ((πΉβ(π΄ + (1 / π))) β (πΉβπ§))) β€ (π₯ / 2)) |
390 | 240, 389 | eqbrtrd 5132 |
. . . . . . . . . . . . . 14
β’ (π β (absβ((πβπ) β (πΉβπ§))) β€ (π₯ / 2)) |
391 | 238, 390 | eqbrtrd 5132 |
. . . . . . . . . . . . 13
β’ (π β (absβ((πΉβπ§) β (πβπ))) β€ (π₯ / 2)) |
392 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π₯ β β+)
β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π)) β (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) |
393 | 200, 392 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) |
394 | 231, 233,
237, 237, 391, 393 | leltaddd 11784 |
. . . . . . . . . . . 12
β’ (π β ((absβ((πΉβπ§) β (πβπ))) + (absβ((πβπ) β (lim supβπ)))) < ((π₯ / 2) + (π₯ / 2))) |
395 | 342 | 2halvesd 12406 |
. . . . . . . . . . . 12
β’ (π β ((π₯ / 2) + (π₯ / 2)) = π₯) |
396 | 394, 395 | breqtrd 5136 |
. . . . . . . . . . 11
β’ (π β ((absβ((πΉβπ§) β (πβπ))) + (absβ((πβπ) β (lim supβπ)))) < π₯) |
397 | 229, 234,
235, 236, 396 | lelttrd 11320 |
. . . . . . . . . 10
β’ (π β (absβ(((πΉβπ§) β (πβπ)) + ((πβπ) β (lim supβπ)))) < π₯) |
398 | 223, 397 | eqbrtrd 5132 |
. . . . . . . . 9
β’ (π β (absβ((πΉβπ§) β (lim supβπ))) < π₯) |
399 | 199, 398 | sylbir 234 |
. . . . . . . 8
β’
((((((π β§ π₯ β β+)
β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π)) β (absβ((πΉβπ§) β (lim supβπ))) < π₯) |
400 | 399 | adantrl 715 |
. . . . . . 7
β’
((((((π β§ π₯ β β+)
β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (π§ β π΄ β§ (absβ(π§ β π΄)) < (1 / π))) β (absβ((πΉβπ§) β (lim supβπ))) < π₯) |
401 | 400 | ex 414 |
. . . . . 6
β’
(((((π β§ π₯ β β+)
β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β ((π§ β π΄ β§ (absβ(π§ β π΄)) < (1 / π)) β (absβ((πΉβπ§) β (lim supβπ))) < π₯)) |
402 | 401 | ralrimiva 3144 |
. . . . 5
β’ ((((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β βπ§ β (π΄(,)π΅)((π§ β π΄ β§ (absβ(π§ β π΄)) < (1 / π)) β (absβ((πΉβπ§) β (lim supβπ))) < π₯)) |
403 | | brimralrspcev 5171 |
. . . . 5
β’ (((1 /
π) β
β+ β§ βπ§ β (π΄(,)π΅)((π§ β π΄ β§ (absβ(π§ β π΄)) < (1 / π)) β (absβ((πΉβπ§) β (lim supβπ))) < π₯)) β βπ¦ β β+ βπ§ β (π΄(,)π΅)((π§ β π΄ β§ (absβ(π§ β π΄)) < π¦) β (absβ((πΉβπ§) β (lim supβπ))) < π₯)) |
404 | 198, 402,
403 | syl2anc 585 |
. . . 4
β’ ((((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β βπ¦ β β+ βπ§ β (π΄(,)π΅)((π§ β π΄ β§ (absβ(π§ β π΄)) < π¦) β (absβ((πΉβπ§) β (lim supβπ))) < π₯)) |
405 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β€ π) β π β€ π) |
406 | 405 | iftrued 4499 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β€ π) β if(π β€ π, π, π) = π) |
407 | | uzid 12785 |
. . . . . . . . . . . 12
β’ (π β β€ β π β
(β€β₯βπ)) |
408 | 182, 407 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β π β
(β€β₯βπ)) |
409 | 408 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β€ π) β π β (β€β₯βπ)) |
410 | 406, 409 | eqeltrd 2838 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β€ π) β if(π β€ π, π, π) β (β€β₯βπ)) |
411 | 410 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ π β€ π) β if(π β€ π, π, π) β (β€β₯βπ)) |
412 | | iffalse 4500 |
. . . . . . . . . 10
β’ (Β¬
π β€ π β if(π β€ π, π, π) = π) |
413 | 412 | adantl 483 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β if(π β€ π, π, π) = π) |
414 | 182 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β π β β€) |
415 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β π β β€) |
416 | 414 | zred 12614 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β π β β) |
417 | 415 | zred 12614 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β π β β) |
418 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β Β¬ π β€ π) |
419 | 416, 417 | ltnled 11309 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β (π < π β Β¬ π β€ π)) |
420 | 418, 419 | mpbird 257 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β π < π) |
421 | 416, 417,
420 | ltled 11310 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β π β€ π) |
422 | | eluz2 12776 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (π β β€ β§ π β β€ β§ π β€ π)) |
423 | 414, 415,
421, 422 | syl3anbrc 1344 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β π β (β€β₯βπ)) |
424 | 413, 423 | eqeltrd 2838 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β β€) β§ Β¬
π β€ π) β if(π β€ π, π, π) β (β€β₯βπ)) |
425 | 411, 424 | pm2.61dan 812 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β β€) β if(π β€ π, π, π) β (β€β₯βπ)) |
426 | 425 | adantr 482 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β β€) β§
βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2))) β if(π β€ π, π, π) β (β€β₯βπ)) |
427 | | simpr 486 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β β€) β§
βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2))) β βπ β (β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2))) |
428 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β β€) β π β
β€) |
429 | 182 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β β€) β π β
β€) |
430 | 429, 428 | ifcld 4537 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β β€) β if(π β€ π, π, π) β β€) |
431 | 428 | zred 12614 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β β€) β π β
β) |
432 | 429 | zred 12614 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β β€) β π β
β) |
433 | | max1 13111 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β π β€ if(π β€ π, π, π)) |
434 | 431, 432,
433 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β β€) β π β€ if(π β€ π, π, π)) |
435 | | eluz2 12776 |
. . . . . . . . . 10
β’ (if(π β€ π, π, π) β (β€β₯βπ) β (π β β€ β§ if(π β€ π, π, π) β β€ β§ π β€ if(π β€ π, π, π))) |
436 | 428, 430,
434, 435 | syl3anbrc 1344 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β β€) β if(π β€ π, π, π) β (β€β₯βπ)) |
437 | 436 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β β€) β§
βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2))) β if(π β€ π, π, π) β (β€β₯βπ)) |
438 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = if(π β€ π, π, π) β (πβπ) = (πβif(π β€ π, π, π))) |
439 | 438 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π = if(π β€ π, π, π) β ((πβπ) β β β (πβif(π β€ π, π, π)) β β)) |
440 | 438 | fvoveq1d 7384 |
. . . . . . . . . . 11
β’ (π = if(π β€ π, π, π) β (absβ((πβπ) β (lim supβπ))) = (absβ((πβif(π β€ π, π, π)) β (lim supβπ)))) |
441 | 440 | breq1d 5120 |
. . . . . . . . . 10
β’ (π = if(π β€ π, π, π) β ((absβ((πβπ) β (lim supβπ))) < (π₯ / 2) β (absβ((πβif(π β€ π, π, π)) β (lim supβπ))) < (π₯ / 2))) |
442 | 439, 441 | anbi12d 632 |
. . . . . . . . 9
β’ (π = if(π β€ π, π, π) β (((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β ((πβif(π β€ π, π, π)) β β β§ (absβ((πβif(π β€ π, π, π)) β (lim supβπ))) < (π₯ / 2)))) |
443 | 442 | rspccva 3583 |
. . . . . . . 8
β’
((βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ if(π β€ π, π, π) β (β€β₯βπ)) β ((πβif(π β€ π, π, π)) β β β§ (absβ((πβif(π β€ π, π, π)) β (lim supβπ))) < (π₯ / 2))) |
444 | 427, 437,
443 | syl2anc 585 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β β€) β§
βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2))) β ((πβif(π β€ π, π, π)) β β β§ (absβ((πβif(π β€ π, π, π)) β (lim supβπ))) < (π₯ / 2))) |
445 | 444 | simprd 497 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β β€) β§
βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2))) β (absβ((πβif(π β€ π, π, π)) β (lim supβπ))) < (π₯ / 2)) |
446 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = if(π β€ π, π, π) β (πβπ) = (πβif(π β€ π, π, π))) |
447 | 446 | fvoveq1d 7384 |
. . . . . . . 8
β’ (π = if(π β€ π, π, π) β (absβ((πβπ) β (lim supβπ))) = (absβ((πβif(π β€ π, π, π)) β (lim supβπ)))) |
448 | 447 | breq1d 5120 |
. . . . . . 7
β’ (π = if(π β€ π, π, π) β ((absβ((πβπ) β (lim supβπ))) < (π₯ / 2) β (absβ((πβif(π β€ π, π, π)) β (lim supβπ))) < (π₯ / 2))) |
449 | 448 | rspcev 3584 |
. . . . . 6
β’
((if(π β€ π, π, π) β (β€β₯βπ) β§ (absβ((πβif(π β€ π, π, π)) β (lim supβπ))) < (π₯ / 2)) β βπ β (β€β₯βπ)(absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) |
450 | 426, 445,
449 | syl2anc 585 |
. . . . 5
β’ ((((π β§ π₯ β β+) β§ π β β€) β§
βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2))) β βπ β (β€β₯βπ)(absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) |
451 | | ax-resscn 11115 |
. . . . . . . . . . . . . 14
β’ β
β β |
452 | 451 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β β
β) |
453 | 26, 452 | fssd 6691 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
454 | | dvcn 25301 |
. . . . . . . . . . . . . 14
β’
(((β β β β§ πΉ:(π΄(,)π΅)βΆβ β§ (π΄(,)π΅) β β) β§ dom (β D
πΉ) = (π΄(,)π΅)) β πΉ β ((π΄(,)π΅)βcnββ)) |
455 | 452, 453,
153, 109, 454 | syl31anc 1374 |
. . . . . . . . . . . . 13
β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) |
456 | | cncfcdm 24277 |
. . . . . . . . . . . . 13
β’ ((β
β β β§ πΉ
β ((π΄(,)π΅)βcnββ)) β (πΉ β ((π΄(,)π΅)βcnββ) β πΉ:(π΄(,)π΅)βΆβ)) |
457 | 452, 455,
456 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πΉ β ((π΄(,)π΅)βcnββ) β πΉ:(π΄(,)π΅)βΆβ)) |
458 | 26, 457 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) |
459 | | ioodvbdlimc1lem2.r |
. . . . . . . . . . . 12
β’ π
= (π β (β€β₯βπ) β¦ (π΄ + (1 / π))) |
460 | 105, 459 | fmptd 7067 |
. . . . . . . . . . 11
β’ (π β π
:(β€β₯βπ)βΆ(π΄(,)π΅)) |
461 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β¦ (πΉβ(π
βπ))) = (π β (β€β₯βπ) β¦ (πΉβ(π
βπ))) |
462 | | climrel 15381 |
. . . . . . . . . . . . 13
β’ Rel
β |
463 | 462 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β Rel β
) |
464 | | fvex 6860 |
. . . . . . . . . . . . . . . . 17
β’
(β€β₯βπ) β V |
465 | 464 | mptex 7178 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βπ) β¦ π΄) β V |
466 | 465 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (β€β₯βπ) β¦ π΄) β V) |
467 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β (π β (β€β₯βπ) β¦ π΄) = (π β (β€β₯βπ) β¦ π΄)) |
468 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (β€β₯βπ)) β§ π = π) β π΄ = π΄) |
469 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
470 | 7 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β π΄ β β) |
471 | 467, 468,
469, 470 | fvmptd 6960 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ π΄)βπ) = π΄) |
472 | 23, 141, 466, 98, 471 | climconst 15432 |
. . . . . . . . . . . . . 14
β’ (π β (π β (β€β₯βπ) β¦ π΄) β π΄) |
473 | 464 | mptex 7178 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βπ) β¦ (π΄ + (1 / π))) β V |
474 | 459, 473 | eqeltri 2834 |
. . . . . . . . . . . . . . 15
β’ π
β V |
475 | 474 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β π
β V) |
476 | | 1cnd 11157 |
. . . . . . . . . . . . . . 15
β’ (π β 1 β
β) |
477 | | elnnnn0b 12464 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π β β0
β§ 0 < π)) |
478 | 21, 67, 477 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
479 | | divcnvg 43942 |
. . . . . . . . . . . . . . 15
β’ ((1
β β β§ π
β β) β (π
β (β€β₯βπ) β¦ (1 / π)) β 0) |
480 | 476, 478,
479 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (π β (β€β₯βπ) β¦ (1 / π)) β 0) |
481 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β (π β (β€β₯βπ) β¦ π΄) = (π β (β€β₯βπ) β¦ π΄)) |
482 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (β€β₯βπ)) β§ π = π) β π΄ = π΄) |
483 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
484 | 7 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β π΄ β β) |
485 | 481, 482,
483, 484 | fvmptd 6960 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ π΄)βπ) = π΄) |
486 | 98 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯βπ)) β π΄ β β) |
487 | 485, 486 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ π΄)βπ) β β) |
488 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β (π β (β€β₯βπ) β¦ (1 / π)) = (π β (β€β₯βπ) β¦ (1 / π))) |
489 | | oveq2 7370 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (1 / π) = (1 / π)) |
490 | 489 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (β€β₯βπ)) β§ π = π) β (1 / π) = (1 / π)) |
491 | 3, 483 | sselid 3947 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (β€β₯βπ)) β π β β) |
492 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (β€β₯βπ)) β 0 β
β) |
493 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (β€β₯βπ)) β π β β) |
494 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (β€β₯βπ)) β 0 < π) |
495 | | eluzle 12783 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯βπ) β π β€ π) |
496 | 495 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (β€β₯βπ)) β π β€ π) |
497 | 492, 493,
491, 494, 496 | ltletrd 11322 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (β€β₯βπ)) β 0 < π) |
498 | 497 | gt0ne0d 11726 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (β€β₯βπ)) β π β 0) |
499 | 491, 498 | rereccld 11989 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β (1 / π) β
β) |
500 | 488, 490,
483, 499 | fvmptd 6960 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (1 / π))βπ) = (1 / π)) |
501 | 491 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β π β β) |
502 | 501, 498 | reccld 11931 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯βπ)) β (1 / π) β
β) |
503 | 500, 502 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (1 / π))βπ) β β) |
504 | 489 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π΄ + (1 / π)) = (π΄ + (1 / π))) |
505 | 484, 499 | readdcld 11191 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β (π΄ + (1 / π)) β β) |
506 | 459, 504,
483, 505 | fvmptd3 6976 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯βπ)) β (π
βπ) = (π΄ + (1 / π))) |
507 | 485, 500 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯βπ)) β (((π β (β€β₯βπ) β¦ π΄)βπ) + ((π β (β€β₯βπ) β¦ (1 / π))βπ)) = (π΄ + (1 / π))) |
508 | 506, 507 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯βπ)) β (π
βπ) = (((π β (β€β₯βπ) β¦ π΄)βπ) + ((π β (β€β₯βπ) β¦ (1 / π))βπ))) |
509 | 23, 141, 472, 475, 480, 487, 503, 508 | climadd 15521 |
. . . . . . . . . . . . 13
β’ (π β π
β (π΄ + 0)) |
510 | 98 | addid1d 11362 |
. . . . . . . . . . . . 13
β’ (π β (π΄ + 0) = π΄) |
511 | 509, 510 | breqtrd 5136 |
. . . . . . . . . . . 12
β’ (π β π
β π΄) |
512 | | releldm 5904 |
. . . . . . . . . . . 12
β’ ((Rel
β β§ π
β
π΄) β π
β dom β ) |
513 | 463, 511,
512 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β π
β dom β ) |
514 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
515 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π
βπ) = (π
βπ)) |
516 | 515 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((π
ββ) β (π
βπ)) = ((π
ββ) β (π
βπ))) |
517 | 516 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (absβ((π
ββ) β (π
βπ))) = (absβ((π
ββ) β (π
βπ)))) |
518 | 517 | breq1d 5120 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1)) β
(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1)))) |
519 | 514, 518 | raleqbidv 3322 |
. . . . . . . . . . . . . 14
β’ (π = π β (ββ β (β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1)) β
ββ β
(β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1)))) |
520 | 519 | cbvrabv 3420 |
. . . . . . . . . . . . 13
β’ {π β
(β€β₯βπ) β£ ββ β (β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))} = {π β
(β€β₯βπ) β£ ββ β (β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))} |
521 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (β = π β (π
ββ) = (π
βπ)) |
522 | 521 | fvoveq1d 7384 |
. . . . . . . . . . . . . . . . 17
β’ (β = π β (absβ((π
ββ) β (π
βπ))) = (absβ((π
βπ) β (π
βπ)))) |
523 | 522 | breq1d 5120 |
. . . . . . . . . . . . . . . 16
β’ (β = π β ((absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1)) β
(absβ((π
βπ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1)))) |
524 | 523 | cbvralvw 3228 |
. . . . . . . . . . . . . . 15
β’
(ββ β
(β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1)) β
βπ β
(β€β₯βπ)(absβ((π
βπ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))) |
525 | 524 | rgenw 3069 |
. . . . . . . . . . . . . 14
β’
βπ β
(β€β₯βπ)(ββ β (β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1)) β
βπ β
(β€β₯βπ)(absβ((π
βπ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))) |
526 | | rabbi 3435 |
. . . . . . . . . . . . . 14
β’
(βπ β
(β€β₯βπ)(ββ β (β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1)) β
βπ β
(β€β₯βπ)(absβ((π
βπ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))) β {π β
(β€β₯βπ) β£ ββ β (β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))} = {π β
(β€β₯βπ) β£ βπ β (β€β₯βπ)(absβ((π
βπ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))}) |
527 | 525, 526 | mpbi 229 |
. . . . . . . . . . . . 13
β’ {π β
(β€β₯βπ) β£ ββ β (β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))} = {π β
(β€β₯βπ) β£ βπ β (β€β₯βπ)(absβ((π
βπ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))} |
528 | 520, 527 | eqtri 2765 |
. . . . . . . . . . . 12
β’ {π β
(β€β₯βπ) β£ ββ β (β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))} = {π β
(β€β₯βπ) β£ βπ β (β€β₯βπ)(absβ((π
βπ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))} |
529 | 528 | infeq1i 9421 |
. . . . . . . . . . 11
β’
inf({π β
(β€β₯βπ) β£ ββ β (β€β₯βπ)(absβ((π
ββ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))}, β, < )
= inf({π β
(β€β₯βπ) β£ βπ β (β€β₯βπ)(absβ((π
βπ) β (π
βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))}, β, <
) |
530 | 7, 6, 9, 458, 109, 110, 22, 460, 461, 513, 529 | ioodvbdlimc1lem1 44246 |
. . . . . . . . . 10
β’ (π β (π β (β€β₯βπ) β¦ (πΉβ(π
βπ))) β (lim supβ(π β
(β€β₯βπ) β¦ (πΉβ(π
βπ))))) |
531 | 459 | fvmpt2 6964 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯βπ) β§ (π΄ + (1 / π)) β β) β (π
βπ) = (π΄ + (1 / π))) |
532 | 113, 58, 531 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯βπ)) β (π
βπ) = (π΄ + (1 / π))) |
533 | 532 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β (π΄ + (1 / π)) = (π
βπ)) |
534 | 533 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β (πΉβ(π΄ + (1 / π))) = (πΉβ(π
βπ))) |
535 | 534 | mpteq2dva 5210 |
. . . . . . . . . . 11
β’ (π β (π β (β€β₯βπ) β¦ (πΉβ(π΄ + (1 / π)))) = (π β (β€β₯βπ) β¦ (πΉβ(π
βπ)))) |
536 | 107, 535 | eqtrid 2789 |
. . . . . . . . . 10
β’ (π β π = (π β (β€β₯βπ) β¦ (πΉβ(π
βπ)))) |
537 | 536 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π β (lim supβπ) = (lim supβ(π β
(β€β₯βπ) β¦ (πΉβ(π
βπ))))) |
538 | 530, 536,
537 | 3brtr4d 5142 |
. . . . . . . . 9
β’ (π β π β (lim supβπ)) |
539 | 464 | mptex 7178 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β¦ (πΉβ(π΄ + (1 / π)))) β V |
540 | 107, 539 | eqeltri 2834 |
. . . . . . . . . . 11
β’ π β V |
541 | 540 | a1i 11 |
. . . . . . . . . 10
β’ (π β π β V) |
542 | | eqidd 2738 |
. . . . . . . . . 10
β’ ((π β§ π β β€) β (πβπ) = (πβπ)) |
543 | 541, 542 | clim 15383 |
. . . . . . . . 9
β’ (π β (π β (lim supβπ) β ((lim supβπ) β β β§ βπ β β+
βπ β β€
βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < π)))) |
544 | 538, 543 | mpbid 231 |
. . . . . . . 8
β’ (π β ((lim supβπ) β β β§
βπ β
β+ βπ β β€ βπ β (β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < π))) |
545 | 544 | simprd 497 |
. . . . . . 7
β’ (π β βπ β β+ βπ β β€ βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < π)) |
546 | 545 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
βπ β
β+ βπ β β€ βπ β (β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < π)) |
547 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
548 | 547 | rphalfcld 12976 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (π₯ / 2) β
β+) |
549 | | breq2 5114 |
. . . . . . . . 9
β’ (π = (π₯ / 2) β ((absβ((πβπ) β (lim supβπ))) < π β (absβ((πβπ) β (lim supβπ))) < (π₯ / 2))) |
550 | 549 | anbi2d 630 |
. . . . . . . 8
β’ (π = (π₯ / 2) β (((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < π) β ((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)))) |
551 | 550 | rexralbidv 3215 |
. . . . . . 7
β’ (π = (π₯ / 2) β (βπ β β€ βπ β (β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < π) β βπ β β€ βπ β (β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)))) |
552 | 551 | rspccva 3583 |
. . . . . 6
β’
((βπ β
β+ βπ β β€ βπ β (β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < π) β§ (π₯ / 2) β β+) β
βπ β β€
βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2))) |
553 | 546, 548,
552 | syl2anc 585 |
. . . . 5
β’ ((π β§ π₯ β β+) β
βπ β β€
βπ β
(β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2))) |
554 | 450, 553 | r19.29a 3160 |
. . . 4
β’ ((π β§ π₯ β β+) β
βπ β
(β€β₯βπ)(absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) |
555 | 404, 554 | r19.29a 3160 |
. . 3
β’ ((π β§ π₯ β β+) β
βπ¦ β
β+ βπ§ β (π΄(,)π΅)((π§ β π΄ β§ (absβ(π§ β π΄)) < π¦) β (absβ((πΉβπ§) β (lim supβπ))) < π₯)) |
556 | 555 | ralrimiva 3144 |
. 2
β’ (π β βπ₯ β β+ βπ¦ β β+
βπ§ β (π΄(,)π΅)((π§ β π΄ β§ (absβ(π§ β π΄)) < π¦) β (absβ((πΉβπ§) β (lim supβπ))) < π₯)) |
557 | | ioosscn 13333 |
. . . 4
β’ (π΄(,)π΅) β β |
558 | 557 | a1i 11 |
. . 3
β’ (π β (π΄(,)π΅) β β) |
559 | 453, 558,
98 | ellimc3 25259 |
. 2
β’ (π β ((lim supβπ) β (πΉ limβ π΄) β ((lim supβπ) β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β (π΄(,)π΅)((π§ β π΄ β§ (absβ(π§ β π΄)) < π¦) β (absβ((πΉβπ§) β (lim supβπ))) < π₯)))) |
560 | 136, 556,
559 | mpbir2and 712 |
1
β’ (π β (lim supβπ) β (πΉ limβ π΄)) |