Step | Hyp | Ref
| Expression |
1 | | omssubadd.b |
. . . . . 6
β’ (π β π βΌ Ο) |
2 | | nnenom 13941 |
. . . . . . 7
β’ β
β Ο |
3 | 2 | ensymi 8996 |
. . . . . 6
β’ Ο
β β |
4 | | domentr 9005 |
. . . . . 6
β’ ((π βΌ Ο β§ Ο
β β) β π
βΌ β) |
5 | 1, 3, 4 | sylancl 587 |
. . . . 5
β’ (π β π βΌ β) |
6 | | brdomi 8950 |
. . . . 5
β’ (π βΌ β β
βπ π:πβ1-1ββ) |
7 | 5, 6 | syl 17 |
. . . 4
β’ (π β βπ π:πβ1-1ββ) |
8 | 7 | adantr 482 |
. . 3
β’ ((π β§ Ξ£*π¦ β π(πβπ΄) β β) β βπ π:πβ1-1ββ) |
9 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β π) |
10 | | ctex 8955 |
. . . . . . . . . . 11
β’ (π βΌ Ο β π β V) |
11 | 1, 10 | syl 17 |
. . . . . . . . . 10
β’ (π β π β V) |
12 | 9, 11 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β π β V) |
13 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π¦π |
14 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²π¦π |
15 | 14 | nfesum1 32976 |
. . . . . . . . . . . . . 14
β’
β²π¦Ξ£*π¦ β π(πβπ΄) |
16 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π¦β |
17 | 15, 16 | nfel 2918 |
. . . . . . . . . . . . 13
β’
β²π¦Ξ£*π¦ β π(πβπ΄) β β |
18 | 13, 17 | nfan 1903 |
. . . . . . . . . . . 12
β’
β²π¦(π β§ Ξ£*π¦ β π(πβπ΄) β β) |
19 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π¦ π:πβ1-1ββ |
20 | 18, 19 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π¦((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) |
21 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π¦ π β
β+ |
22 | 20, 21 | nfan 1903 |
. . . . . . . . . 10
β’
β²π¦(((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) |
23 | 9 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β π) |
24 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β π¦ β π) |
25 | 11 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ Ξ£*π¦ β π(πβπ΄) β β) β π β V) |
26 | | oms.o |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β π) |
27 | | oms.r |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π
:πβΆ(0[,]+β)) |
28 | | omsf 33233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π β§ π
:πβΆ(0[,]+β)) β
(toOMeasβπ
):π«
βͺ dom π
βΆ(0[,]+β)) |
29 | | oms.m |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ π = (toOMeasβπ
) |
30 | 29 | feq1i 6705 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π:π« βͺ dom π
βΆ(0[,]+β) β
(toOMeasβπ
):π«
βͺ dom π
βΆ(0[,]+β)) |
31 | 28, 30 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π β§ π
:πβΆ(0[,]+β)) β π:π« βͺ dom π
βΆ(0[,]+β)) |
32 | 26, 27, 31 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π:π« βͺ dom
π
βΆ(0[,]+β)) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β π) β π:π« βͺ dom
π
βΆ(0[,]+β)) |
34 | | omssubadd.a |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π¦ β π) β π΄ β βͺ π) |
35 | 27 | fdmd 6725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β dom π
= π) |
36 | 35 | unieqd 4921 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β βͺ dom π
= βͺ π) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π¦ β π) β βͺ dom
π
= βͺ π) |
38 | 34, 37 | sseqtrrd 4022 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π¦ β π) β π΄ β βͺ dom
π
) |
39 | 26 | uniexd 7727 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β βͺ π
β V) |
40 | 39 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π¦ β π) β βͺ π β V) |
41 | | ssexg 5322 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π΄ β βͺ π
β§ βͺ π β V) β π΄ β V) |
42 | 34, 40, 41 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π¦ β π) β π΄ β V) |
43 | | elpwg 4604 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π΄ β V β (π΄ β π« βͺ dom π
β π΄ β βͺ dom
π
)) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π¦ β π) β (π΄ β π« βͺ dom π
β π΄ β βͺ dom
π
)) |
45 | 38, 44 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β π) β π΄ β π« βͺ dom π
) |
46 | 33, 45 | ffvelcdmd 7083 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β π) β (πβπ΄) β (0[,]+β)) |
47 | 46 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π¦ β π) β (πβπ΄) β (0[,]+β)) |
48 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ Ξ£*π¦ β π(πβπ΄) β β) β
Ξ£*π¦ β
π(πβπ΄) β β) |
49 | 18, 25, 47, 48 | esumcvgre 33027 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π¦ β π) β (πβπ΄) β β) |
50 | 49 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π¦ β π) β (πβπ΄) β β) |
51 | 50 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (πβπ΄) β β) |
52 | | rpssre 12977 |
. . . . . . . . . . . . . . . . . . 19
β’
β+ β β |
53 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β π β β+) |
54 | | 2rp 12975 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 2 β
β+ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β 2 β
β+) |
56 | | df-f1 6545 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π:πβ1-1ββ β (π:πβΆβ β§ Fun β‘π)) |
57 | 56 | simplbi 499 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π:πβ1-1ββ β π:πβΆβ) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π:πβ1-1ββ) β π:πβΆβ) |
59 | 58 | ffvelcdmda 7082 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β (πβπ¦) β β) |
60 | 59 | nnzd 12581 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β (πβπ¦) β β€) |
61 | 55, 60 | rpexpcld 14206 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β (2β(πβπ¦)) β
β+) |
62 | 61 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (2β(πβπ¦)) β
β+) |
63 | 53, 62 | rpdivcld 13029 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (π / (2β(πβπ¦))) β
β+) |
64 | 52, 63 | sselid 3979 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (π / (2β(πβπ¦))) β β) |
65 | 64 | adantl3r 749 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (π / (2β(πβπ¦))) β β) |
66 | | rexadd 13207 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ΄) β β β§ (π / (2β(πβπ¦))) β β) β ((πβπ΄) +π (π / (2β(πβπ¦)))) = ((πβπ΄) + (π / (2β(πβπ¦))))) |
67 | 51, 65, 66 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β ((πβπ΄) +π (π / (2β(πβπ¦)))) = ((πβπ΄) + (π / (2β(πβπ¦))))) |
68 | 9, 46 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (πβπ΄) β (0[,]+β)) |
69 | | dfrp2 13369 |
. . . . . . . . . . . . . . . . . . . 20
β’
β+ = (0(,)+β) |
70 | | ioossicc 13406 |
. . . . . . . . . . . . . . . . . . . 20
β’
(0(,)+β) β (0[,]+β) |
71 | 69, 70 | eqsstri 4015 |
. . . . . . . . . . . . . . . . . . 19
β’
β+ β (0[,]+β) |
72 | 71, 63 | sselid 3979 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (π / (2β(πβπ¦))) β (0[,]+β)) |
73 | 72 | adantl3r 749 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (π / (2β(πβπ¦))) β (0[,]+β)) |
74 | 68, 73 | xrge0addcld 31953 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β ((πβπ΄) +π (π / (2β(πβπ¦)))) β (0[,]+β)) |
75 | 67, 74 | eqeltrrd 2835 |
. . . . . . . . . . . . . . 15
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β ((πβπ΄) + (π / (2β(πβπ¦)))) β (0[,]+β)) |
76 | 52, 53 | sselid 3979 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β π β β) |
77 | 76 | adantl3r 749 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β π β β) |
78 | 52, 61 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β (2β(πβπ¦)) β β) |
79 | 78 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (2β(πβπ¦)) β β) |
80 | 79 | adantl3r 749 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (2β(πβπ¦)) β β) |
81 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β π β β+) |
82 | 81 | rpgt0d 13015 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β 0 < π) |
83 | | 2re 12282 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β 2 β β) |
85 | 60 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π¦ β π) β (πβπ¦) β β€) |
86 | 85 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (πβπ¦) β β€) |
87 | | 2pos 12311 |
. . . . . . . . . . . . . . . . . . . 20
β’ 0 <
2 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β 0 < 2) |
89 | | expgt0 14057 |
. . . . . . . . . . . . . . . . . . 19
β’ ((2
β β β§ (πβπ¦) β β€ β§ 0 < 2) β 0
< (2β(πβπ¦))) |
90 | 84, 86, 88, 89 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β 0 < (2β(πβπ¦))) |
91 | 77, 80, 82, 90 | divgt0d 12145 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β 0 < (π / (2β(πβπ¦)))) |
92 | 65, 51 | ltaddposd 11794 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (0 < (π / (2β(πβπ¦))) β (πβπ΄) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
93 | 91, 92 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (πβπ΄) < ((πβπ΄) + (π / (2β(πβπ¦))))) |
94 | 29 | fveq1i 6889 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πβπ΄) = ((toOMeasβπ
)βπ΄) |
95 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β π) β π β π) |
96 | 27 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β π) β π
:πβΆ(0[,]+β)) |
97 | | omsfval 33231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β π β§ π
:πβΆ(0[,]+β) β§ π΄ β βͺ π)
β ((toOMeasβπ
)βπ΄) = inf(ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < )) |
98 | 95, 96, 34, 97 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β π) β ((toOMeasβπ
)βπ΄) = inf(ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < )) |
99 | 94, 98 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β π) β (πβπ΄) = inf(ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < )) |
100 | 9, 99 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (πβπ΄) = inf(ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < )) |
101 | 100 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β inf(ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < ) = (πβπ΄)) |
102 | 101 | breq1d 5157 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (inf(ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < ) < ((πβπ΄) + (π / (2β(πβπ¦)))) β (πβπ΄) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
103 | 93, 102 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β inf(ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < ) < ((πβπ΄) + (π / (2β(πβπ¦))))) |
104 | 75, 103 | jca 513 |
. . . . . . . . . . . . . 14
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (((πβπ΄) + (π / (2β(πβπ¦)))) β (0[,]+β) β§ inf(ran
(π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < ) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
105 | | iccssxr 13403 |
. . . . . . . . . . . . . . . . . . 19
β’
(0[,]+β) β β* |
106 | | xrltso 13116 |
. . . . . . . . . . . . . . . . . . 19
β’ < Or
β* |
107 | | soss 5607 |
. . . . . . . . . . . . . . . . . . 19
β’
((0[,]+β) β β* β ( < Or
β* β < Or (0[,]+β))) |
108 | 105, 106,
107 | mp2 9 |
. . . . . . . . . . . . . . . . . 18
β’ < Or
(0[,]+β) |
109 | | biid 261 |
. . . . . . . . . . . . . . . . . 18
β’ ( < Or
(0[,]+β) β < Or (0[,]+β)) |
110 | 108, 109 | mpbi 229 |
. . . . . . . . . . . . . . . . 17
β’ < Or
(0[,]+β) |
111 | 110 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β π) β < Or
(0[,]+β)) |
112 | | omscl 33232 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ π
:πβΆ(0[,]+β) β§ π΄ β π« βͺ dom π
) β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β (0[,]+β)) |
113 | 95, 96, 45, 112 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β π) β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β (0[,]+β)) |
114 | | xrge0infss 31951 |
. . . . . . . . . . . . . . . . 17
β’ (ran
(π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β (0[,]+β) β βπ£ β
(0[,]+β)(ββ
β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) Β¬ β < π£ β§ ββ β (0[,]+β)(π£ < β β βπ’ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))π’ < β))) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β π) β βπ£ β (0[,]+β)(ββ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) Β¬ β < π£ β§ ββ β (0[,]+β)(π£ < β β βπ’ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))π’ < β))) |
116 | 111, 115 | infglb 9481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β π) β ((((πβπ΄) + (π / (2β(πβπ¦)))) β (0[,]+β) β§ inf(ran
(π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < ) < ((πβπ΄) + (π / (2β(πβπ¦))))) β βπ’ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))π’ < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
117 | 116 | imp 408 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β π) β§ (((πβπ΄) + (π / (2β(πβπ¦)))) β (0[,]+β) β§ inf(ran
(π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < ) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βπ’ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))π’ < ((πβπ΄) + (π / (2β(πβπ¦))))) |
118 | 23, 24, 104, 117 | syl21anc 837 |
. . . . . . . . . . . . 13
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β βπ’ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))π’ < ((πβπ΄) + (π / (2β(πβπ¦))))) |
119 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) = (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) |
120 | | esumex 32965 |
. . . . . . . . . . . . . . . . . . 19
β’
Ξ£*π€
β π₯(π
βπ€) β V |
121 | 119, 120 | elrnmpti 5957 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}π’ = Ξ£*π€ β π₯(π
βπ€)) |
122 | 121 | anbi1i 625 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦))))) β (βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}π’ = Ξ£*π€ β π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
123 | | r19.41v 3189 |
. . . . . . . . . . . . . . . . 17
β’
(βπ₯ β
{π§ β π« dom
π
β£ (π΄ β βͺ π§
β§ π§ βΌ Ο)}
(π’ =
Ξ£*π€ β
π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦))))) β (βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}π’ = Ξ£*π€ β π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
124 | 122, 123 | bitr4i 278 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦))))) β βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} (π’ = Ξ£*π€ β π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
125 | 124 | exbii 1851 |
. . . . . . . . . . . . . . 15
β’
(βπ’(π’ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦))))) β βπ’βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} (π’ = Ξ£*π€ β π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
126 | | df-rex 3072 |
. . . . . . . . . . . . . . 15
β’
(βπ’ β ran
(π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))π’ < ((πβπ΄) + (π / (2β(πβπ¦)))) β βπ’(π’ β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
127 | | rexcom4 3286 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
{π§ β π« dom
π
β£ (π΄ β βͺ π§
β§ π§ βΌ
Ο)}βπ’(π’ = Ξ£*π€ β π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦))))) β βπ’βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} (π’ = Ξ£*π€ β π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
128 | 125, 126,
127 | 3bitr4i 303 |
. . . . . . . . . . . . . 14
β’
(βπ’ β ran
(π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))π’ < ((πβπ΄) + (π / (2β(πβπ¦)))) β βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}βπ’(π’ = Ξ£*π€ β π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
129 | | breq1 5150 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = Ξ£*π€ β π₯(π
βπ€) β (π’ < ((πβπ΄) + (π / (2β(πβπ¦)))) β Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
130 | | idd 24 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = Ξ£*π€ β π₯(π
βπ€) β (Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))) β Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
131 | 129, 130 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = Ξ£*π€ β π₯(π
βπ€) β (π’ < ((πβπ΄) + (π / (2β(πβπ¦)))) β Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
132 | 131 | imp 408 |
. . . . . . . . . . . . . . . 16
β’ ((π’ = Ξ£*π€ β π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦))))) β Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) |
133 | 132 | exlimiv 1934 |
. . . . . . . . . . . . . . 15
β’
(βπ’(π’ = Ξ£*π€ β π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦))))) β Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) |
134 | 133 | reximi 3085 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
{π§ β π« dom
π
β£ (π΄ β βͺ π§
β§ π§ βΌ
Ο)}βπ’(π’ = Ξ£*π€ β π₯(π
βπ€) β§ π’ < ((πβπ΄) + (π / (2β(πβπ¦))))) β βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) |
135 | 128, 134 | sylbi 216 |
. . . . . . . . . . . . 13
β’
(βπ’ β ran
(π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))π’ < ((πβπ΄) + (π / (2β(πβπ¦)))) β βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) |
136 | 118, 135 | syl 17 |
. . . . . . . . . . . 12
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) |
137 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β βͺ π§
β§ π§ βΌ Ο)
β π§ βΌ
Ο) |
138 | 137 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π§ β π« dom π
β ((π΄ β βͺ π§ β§ π§ βΌ Ο) β π§ βΌ Ο)) |
139 | 138 | ss2rabi 4073 |
. . . . . . . . . . . . . 14
β’ {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β {π§ β π« dom π
β£ π§ βΌ Ο} |
140 | | rexss 4054 |
. . . . . . . . . . . . . 14
β’ ({π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β {π§ β π« dom π
β£ π§ βΌ Ο} β (βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))) β βπ₯ β {π§ β π« dom π
β£ π§ βΌ Ο} (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β§
Ξ£*π€ β
π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))))) |
141 | 139, 140 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
{π§ β π« dom
π
β£ (π΄ β βͺ π§
β§ π§ βΌ
Ο)}Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))) β βπ₯ β {π§ β π« dom π
β£ π§ βΌ Ο} (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β§
Ξ£*π€ β
π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
142 | | unieq 4918 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ = π₯ β βͺ π§ = βͺ
π₯) |
143 | 142 | sseq2d 4013 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = π₯ β (π΄ β βͺ π§ β π΄ β βͺ π₯)) |
144 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = π₯ β (π§ βΌ Ο β π₯ βΌ Ο)) |
145 | 143, 144 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = π₯ β ((π΄ β βͺ π§ β§ π§ βΌ Ο) β (π΄ β βͺ π₯ β§ π₯ βΌ Ο))) |
146 | 145 | elrab 3682 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β (π₯ β π« dom π
β§ (π΄ β βͺ π₯ β§ π₯ βΌ Ο))) |
147 | 146 | simprbi 498 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β (π΄ β βͺ π₯ β§ π₯ βΌ Ο)) |
148 | 147 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β π΄ β βͺ π₯) |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . 15
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β π΄ β βͺ π₯)) |
150 | 149 | anim1d 612 |
. . . . . . . . . . . . . 14
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β ((π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β§
Ξ£*π€ β
π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β (π΄ β βͺ π₯ β§ Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))))) |
151 | 150 | reximdv 3171 |
. . . . . . . . . . . . 13
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (βπ₯ β {π§ β π« dom π
β£ π§ βΌ Ο} (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β§
Ξ£*π€ β
π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β βπ₯ β {π§ β π« dom π
β£ π§ βΌ Ο} (π΄ β βͺ π₯ β§ Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))))) |
152 | 141, 151 | biimtrid 241 |
. . . . . . . . . . . 12
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))) β βπ₯ β {π§ β π« dom π
β£ π§ βΌ Ο} (π΄ β βͺ π₯ β§ Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))))) |
153 | 136, 152 | mpd 15 |
. . . . . . . . . . 11
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β βπ₯ β {π§ β π« dom π
β£ π§ βΌ Ο} (π΄ β βͺ π₯ β§ Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
154 | 153 | ex 414 |
. . . . . . . . . 10
β’ ((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β (π¦ β π β βπ₯ β {π§ β π« dom π
β£ π§ βΌ Ο} (π΄ β βͺ π₯ β§ Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))))) |
155 | 22, 154 | ralrimi 3255 |
. . . . . . . . 9
β’ ((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β
βπ¦ β π βπ₯ β {π§ β π« dom π
β£ π§ βΌ Ο} (π΄ β βͺ π₯ β§ Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
156 | | unieq 4918 |
. . . . . . . . . . . . 13
β’ (π₯ = (πβπ¦) β βͺ π₯ = βͺ
(πβπ¦)) |
157 | 156 | sseq2d 4013 |
. . . . . . . . . . . 12
β’ (π₯ = (πβπ¦) β (π΄ β βͺ π₯ β π΄ β βͺ (πβπ¦))) |
158 | | esumeq1 32970 |
. . . . . . . . . . . . 13
β’ (π₯ = (πβπ¦) β Ξ£*π€ β π₯(π
βπ€) = Ξ£*π€ β (πβπ¦)(π
βπ€)) |
159 | 158 | breq1d 5157 |
. . . . . . . . . . . 12
β’ (π₯ = (πβπ¦) β (Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))) β Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
160 | 157, 159 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π₯ = (πβπ¦) β ((π΄ β βͺ π₯ β§ Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))))) |
161 | 160 | ac6sg 10479 |
. . . . . . . . . 10
β’ (π β V β (βπ¦ β π βπ₯ β {π§ β π« dom π
β£ π§ βΌ Ο} (π΄ β βͺ π₯ β§ Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β βπ(π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))))) |
162 | 161 | imp 408 |
. . . . . . . . 9
β’ ((π β V β§ βπ¦ β π βπ₯ β {π§ β π« dom π
β£ π§ βΌ Ο} (π΄ β βͺ π₯ β§ Ξ£*π€ β π₯(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βπ(π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))))) |
163 | 12, 155, 162 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β
βπ(π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))))) |
164 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π) |
165 | 38 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ¦ β π π΄ β βͺ dom
π
) |
166 | | iunss 5047 |
. . . . . . . . . . . . . . . . . 18
β’ (βͺ π¦ β π π΄ β βͺ dom
π
β βπ¦ β π π΄ β βͺ dom
π
) |
167 | 165, 166 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (π β βͺ π¦ β π π΄ β βͺ dom
π
) |
168 | 42 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ¦ β π π΄ β V) |
169 | | iunexg 7945 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β V β§ βπ¦ β π π΄ β V) β βͺ π¦ β π π΄ β V) |
170 | 11, 168, 169 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βͺ π¦ β π π΄ β V) |
171 | | elpwg 4604 |
. . . . . . . . . . . . . . . . . 18
β’ (βͺ π¦ β π π΄ β V β (βͺ π¦ β π π΄ β π« βͺ dom π
β βͺ
π¦ β π π΄ β βͺ dom
π
)) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (βͺ π¦ β π π΄ β π« βͺ dom π
β βͺ
π¦ β π π΄ β βͺ dom
π
)) |
173 | 167, 172 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (π β βͺ π¦ β π π΄ β π« βͺ dom π
) |
174 | 32, 173 | ffvelcdmd 7083 |
. . . . . . . . . . . . . . 15
β’ (π β (πββͺ
π¦ β π π΄) β (0[,]+β)) |
175 | 105, 174 | sselid 3979 |
. . . . . . . . . . . . . 14
β’ (π β (πββͺ
π¦ β π π΄) β
β*) |
176 | 164, 175 | syl 17 |
. . . . . . . . . . . . 13
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (πββͺ
π¦ β π π΄) β
β*) |
177 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) |
178 | 25 | ad4antr 731 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π β V) |
179 | 177, 178 | fexd 7224 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π β V) |
180 | | rnexg 7890 |
. . . . . . . . . . . . . . . 16
β’ (π β V β ran π β V) |
181 | | uniexg 7725 |
. . . . . . . . . . . . . . . 16
β’ (ran
π β V β βͺ ran π β V) |
182 | 179, 180,
181 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βͺ
ran π β
V) |
183 | | simp-5l 784 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π) |
184 | 27 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π β βͺ ran
π) β π
:πβΆ(0[,]+β)) |
185 | | frn 6721 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β ran π β {π§ β π« dom π
β£ π§ βΌ Ο}) |
186 | | ssrab2 4076 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ {π§ β π« dom π
β£ π§ βΌ Ο} β π« dom π
|
187 | 185, 186 | sstrdi 3993 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β ran π β π« dom π
) |
188 | 187 | unissd 4917 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β βͺ ran π β βͺ
π« dom π
) |
189 | | unipw 5449 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ βͺ π« dom π
= dom π
|
190 | 188, 189 | sseqtrdi 4031 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β βͺ ran π β dom π
) |
191 | 190 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β βͺ ran π β dom π
) |
192 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β dom π
= π) |
193 | 191, 192 | sseqtrd 4021 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β βͺ ran π β π) |
194 | 193 | sselda 3981 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π β βͺ ran
π) β π β π) |
195 | 184, 194 | ffvelcdmd 7083 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π β βͺ ran
π) β (π
βπ) β (0[,]+β)) |
196 | 195 | ralrimiva 3147 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β βπ β βͺ ran π(π
βπ) β (0[,]+β)) |
197 | 183, 177,
196 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βπ β βͺ ran
π(π
βπ) β (0[,]+β)) |
198 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
β’
β²πβͺ ran π |
199 | 198 | esumcl 32966 |
. . . . . . . . . . . . . . 15
β’ ((βͺ ran π β V β§ βπ β βͺ ran
π(π
βπ) β (0[,]+β)) β
Ξ£*π β
βͺ ran π(π
βπ) β (0[,]+β)) |
200 | 182, 197,
199 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π β βͺ ran π(π
βπ) β (0[,]+β)) |
201 | 105, 200 | sselid 3979 |
. . . . . . . . . . . . 13
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π β βͺ ran π(π
βπ) β
β*) |
202 | | simp-5r 785 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β π(πβπ΄) β β) |
203 | 202 | rexrd 11260 |
. . . . . . . . . . . . . 14
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β π(πβπ΄) β
β*) |
204 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π β β+) |
205 | 204 | rpxrd 13013 |
. . . . . . . . . . . . . 14
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π β β*) |
206 | 203, 205 | xaddcld 13276 |
. . . . . . . . . . . . 13
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (Ξ£*π¦ β π(πβπ΄) +π π) β
β*) |
207 | 185 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β ran π β {π§ β π« dom π
β£ π§ βΌ Ο}) |
208 | | sstr 3989 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((ran
π β {π§ β π« dom π
β£ π§ βΌ Ο} β§ {π§ β π« dom π
β£ π§ βΌ Ο} β π« dom π
) β ran π β π« dom π
) |
209 | 186, 208 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (ran
π β {π§ β π« dom π
β£ π§ βΌ Ο} β ran π β π« dom π
) |
210 | | sspwuni 5102 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (ran
π β π« dom
π
β βͺ ran π β dom π
) |
211 | 209, 210 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (ran
π β {π§ β π« dom π
β£ π§ βΌ Ο} β βͺ ran π β dom π
) |
212 | 207, 211 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βͺ
ran π β dom π
) |
213 | | ffn 6714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β π Fn π) |
214 | 213 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π Fn π) |
215 | 164, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π βΌ Ο) |
216 | | fnct 10528 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π Fn π β§ π βΌ Ο) β π βΌ Ο) |
217 | | rnct 10516 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π βΌ Ο β ran
π βΌ
Ο) |
218 | 216, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π Fn π β§ π βΌ Ο) β ran π βΌ
Ο) |
219 | | dfss3 3969 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (ran
π β {π§ β π« dom π
β£ π§ βΌ Ο} β βπ€ β ran π π€ β {π§ β π« dom π
β£ π§ βΌ Ο}) |
220 | 219 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (ran
π β {π§ β π« dom π
β£ π§ βΌ Ο} β βπ€ β ran π π€ β {π§ β π« dom π
β£ π§ βΌ Ο}) |
221 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π§ = π€ β (π§ βΌ Ο β π€ βΌ Ο)) |
222 | 221 | elrab 3682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ β {π§ β π« dom π
β£ π§ βΌ Ο} β (π€ β π« dom π
β§ π€ βΌ Ο)) |
223 | 222 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π€ β {π§ β π« dom π
β£ π§ βΌ Ο} β π€ βΌ Ο) |
224 | 223 | ralimi 3084 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ€ β
ran π π€ β {π§ β π« dom π
β£ π§ βΌ Ο} β βπ€ β ran π π€ βΌ Ο) |
225 | 220, 224 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (ran
π β {π§ β π« dom π
β£ π§ βΌ Ο} β βπ€ β ran π π€ βΌ Ο) |
226 | | unictb 10566 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((ran
π βΌ Ο β§
βπ€ β ran π π€ βΌ Ο) β βͺ ran π βΌ Ο) |
227 | 218, 225,
226 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π Fn π β§ π βΌ Ο) β§ ran π β {π§ β π« dom π
β£ π§ βΌ Ο}) β βͺ ran π βΌ Ο) |
228 | 214, 215,
207, 227 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βͺ
ran π βΌ
Ο) |
229 | | ctex 8955 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (βͺ ran π βΌ Ο β βͺ ran π β V) |
230 | | elpwg 4604 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (βͺ ran π β V β (βͺ ran π β π« dom π
β βͺ ran
π β dom π
)) |
231 | 228, 229,
230 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (βͺ
ran π β π« dom
π
β βͺ ran π β dom π
)) |
232 | 212, 231 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βͺ
ran π β π« dom
π
) |
233 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β π΄ β βͺ (πβπ¦)) |
234 | 233 | ralimi 3084 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ¦ β
π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β βπ¦ β π π΄ β βͺ (πβπ¦)) |
235 | | fvssunirn 6921 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πβπ¦) β βͺ ran
π |
236 | 235 | unissi 4916 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ βͺ (πβπ¦) β βͺ βͺ ran π |
237 | | sstr 3989 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π΄ β βͺ (πβπ¦) β§ βͺ (πβπ¦) β βͺ βͺ ran π) β π΄ β βͺ βͺ ran π) |
238 | 236, 237 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π΄ β βͺ (πβπ¦) β π΄ β βͺ βͺ ran π) |
239 | 238 | ralimi 3084 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ¦ β
π π΄ β βͺ (πβπ¦) β βπ¦ β π π΄ β βͺ βͺ ran π) |
240 | | iunss 5047 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (βͺ π¦ β π π΄ β βͺ βͺ ran π β βπ¦ β π π΄ β βͺ βͺ ran π) |
241 | 239, 240 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ¦ β
π π΄ β βͺ (πβπ¦) β βͺ
π¦ β π π΄ β βͺ βͺ ran π) |
242 | 234, 241 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ¦ β
π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β βͺ π¦ β π π΄ β βͺ βͺ ran π) |
243 | 242 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βͺ π¦ β π π΄ β βͺ βͺ ran π) |
244 | 232, 243,
228 | jca32 517 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (βͺ
ran π β π« dom
π
β§ (βͺ π¦ β π π΄ β βͺ βͺ ran π β§ βͺ ran π βΌ
Ο))) |
245 | | unieq 4918 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ = βͺ
ran π β βͺ π§ =
βͺ βͺ ran π) |
246 | 245 | sseq2d 4013 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ = βͺ
ran π β (βͺ π¦ β π π΄ β βͺ π§ β βͺ π¦ β π π΄ β βͺ βͺ ran π)) |
247 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ = βͺ
ran π β (π§ βΌ Ο β βͺ ran π βΌ Ο)) |
248 | 246, 247 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = βͺ
ran π β ((βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο) β (βͺ π¦ β π π΄ β βͺ βͺ ran π β§ βͺ ran π βΌ
Ο))) |
249 | 248 | elrab 3682 |
. . . . . . . . . . . . . . . . . . 19
β’ (βͺ ran π β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β (βͺ ran π β π« dom π
β§ (βͺ
π¦ β π π΄ β βͺ βͺ ran π β§ βͺ ran π βΌ
Ο))) |
250 | 244, 249 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βͺ
ran π β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)}) |
251 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π€ β (π
βπ) = (π
βπ€)) |
252 | 251 | cbvesumv 32979 |
. . . . . . . . . . . . . . . . . 18
β’
Ξ£*π
β βͺ ran π(π
βπ) = Ξ£*π€ β βͺ ran
π(π
βπ€) |
253 | | esumeq1 32970 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = βͺ
ran π β
Ξ£*π€ β
π₯(π
βπ€) = Ξ£*π€ β βͺ ran
π(π
βπ€)) |
254 | 253 | rspceeqv 3632 |
. . . . . . . . . . . . . . . . . 18
β’ ((βͺ ran π β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β§
Ξ£*π β
βͺ ran π(π
βπ) = Ξ£*π€ β βͺ ran
π(π
βπ€)) β βπ₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)}Ξ£*π β βͺ ran π(π
βπ) = Ξ£*π€ β π₯(π
βπ€)) |
255 | 250, 252,
254 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βπ₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)}Ξ£*π β βͺ ran π(π
βπ) = Ξ£*π€ β π₯(π
βπ€)) |
256 | | esumex 32965 |
. . . . . . . . . . . . . . . . . 18
β’
Ξ£*π
β βͺ ran π(π
βπ) β V |
257 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) = (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) |
258 | 257 | elrnmpt 5953 |
. . . . . . . . . . . . . . . . . 18
β’
(Ξ£*π β βͺ ran
π(π
βπ) β V β (Ξ£*π β βͺ ran π(π
βπ) β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β βπ₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)}Ξ£*π β βͺ ran π(π
βπ) = Ξ£*π€ β π₯(π
βπ€))) |
259 | 256, 258 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
(Ξ£*π β βͺ ran
π(π
βπ) β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β βπ₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)}Ξ£*π β βͺ ran π(π
βπ) = Ξ£*π€ β π₯(π
βπ€)) |
260 | 255, 259 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π β βͺ ran π(π
βπ) β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))) |
261 | 110 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β < Or
(0[,]+β)) |
262 | | omscl 33232 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π β§ π
:πβΆ(0[,]+β) β§ βͺ π¦ β π π΄ β π« βͺ dom π
) β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β (0[,]+β)) |
263 | 26, 27, 173, 262 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β (0[,]+β)) |
264 | | xrge0infss 31951 |
. . . . . . . . . . . . . . . . . . 19
β’ (ran
(π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β (0[,]+β) β βπ β
(0[,]+β)(βπ‘
β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) Β¬ π‘ < π β§ βπ‘ β (0[,]+β)(π < π‘ β βπ’ β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))π’ < π‘))) |
265 | 263, 264 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ β (0[,]+β)(βπ‘ β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) Β¬ π‘ < π β§ βπ‘ β (0[,]+β)(π < π‘ β βπ’ β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€))π’ < π‘))) |
266 | 261, 265 | inflb 9480 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Ξ£*π β βͺ ran π(π
βπ) β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β Β¬ Ξ£*π β βͺ ran π(π
βπ) < inf(ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < ))) |
267 | 29 | fveq1i 6889 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πββͺ π¦ β π π΄) = ((toOMeasβπ
)ββͺ
π¦ β π π΄) |
268 | 167, 36 | sseqtrd 4021 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β βͺ π¦ β π π΄ β βͺ π) |
269 | | omsfval 33231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β π β§ π
:πβΆ(0[,]+β) β§ βͺ π¦ β π π΄ β βͺ π) β ((toOMeasβπ
)ββͺ π¦ β π π΄) = inf(ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < )) |
270 | 26, 27, 268, 269 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((toOMeasβπ
)ββͺ π¦ β π π΄) = inf(ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < )) |
271 | 267, 270 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πββͺ
π¦ β π π΄) = inf(ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < )) |
272 | 271 | breq2d 5159 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (Ξ£*π β βͺ ran π(π
βπ) < (πββͺ
π¦ β π π΄) β Ξ£*π β βͺ ran π(π
βπ) < inf(ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < ))) |
273 | 272 | notbid 318 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Β¬
Ξ£*π β
βͺ ran π(π
βπ) < (πββͺ
π¦ β π π΄) β Β¬ Ξ£*π β βͺ ran π(π
βπ) < inf(ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)), (0[,]+β), < ))) |
274 | 266, 273 | sylibrd 259 |
. . . . . . . . . . . . . . . 16
β’ (π β (Ξ£*π β βͺ ran π(π
βπ) β ran (π₯ β {π§ β π« dom π
β£ (βͺ π¦ β π π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π€ β
π₯(π
βπ€)) β Β¬ Ξ£*π β βͺ ran π(π
βπ) < (πββͺ
π¦ β π π΄))) |
275 | 164, 260,
274 | sylc 65 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Β¬ Ξ£*π β βͺ ran π(π
βπ) < (πββͺ
π¦ β π π΄)) |
276 | | biid 261 |
. . . . . . . . . . . . . . 15
β’ (Β¬
Ξ£*π β
βͺ ran π(π
βπ) < (πββͺ
π¦ β π π΄) β Β¬ Ξ£*π β βͺ ran π(π
βπ) < (πββͺ
π¦ β π π΄)) |
277 | 275, 276 | sylib 217 |
. . . . . . . . . . . . . 14
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Β¬ Ξ£*π β βͺ ran π(π
βπ) < (πββͺ
π¦ β π π΄)) |
278 | | xrlenlt 11275 |
. . . . . . . . . . . . . . 15
β’ (((πββͺ π¦ β π π΄) β β* β§
Ξ£*π β
βͺ ran π(π
βπ) β β*) β ((πββͺ π¦ β π π΄) β€ Ξ£*π β βͺ ran
π(π
βπ) β Β¬ Ξ£*π β βͺ ran π(π
βπ) < (πββͺ
π¦ β π π΄))) |
279 | 176, 201,
278 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β ((πββͺ
π¦ β π π΄) β€ Ξ£*π β βͺ ran
π(π
βπ) β Β¬ Ξ£*π β βͺ ran π(π
βπ) < (πββͺ
π¦ β π π΄))) |
280 | 277, 279 | mpbird 257 |
. . . . . . . . . . . . 13
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (πββͺ
π¦ β π π΄) β€ Ξ£*π β βͺ ran
π(π
βπ)) |
281 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π¦ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} |
282 | 22, 281 | nfan 1903 |
. . . . . . . . . . . . . . . . . 18
β’
β²π¦((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) |
283 | | nfra1 3282 |
. . . . . . . . . . . . . . . . . 18
β’
β²π¦βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) |
284 | 282, 283 | nfan 1903 |
. . . . . . . . . . . . . . . . 17
β’
β²π¦(((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
285 | | simp-6l 786 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β§ π¦ β π) β π) |
286 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β§ π¦ β π) β π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) |
287 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β§ π¦ β π) β π¦ β π) |
288 | 27 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ π€ β (πβπ¦)) β π
:πβΆ(0[,]+β)) |
289 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ π€ β (πβπ¦)) β π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) |
290 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ π€ β (πβπ¦)) β π¦ β π) |
291 | 289, 290 | ffvelcdmd 7083 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ π€ β (πβπ¦)) β (πβπ¦) β {π§ β π« dom π
β£ π§ βΌ Ο}) |
292 | 186, 291 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ π€ β (πβπ¦)) β (πβπ¦) β π« dom π
) |
293 | 292 | elpwid 4610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ π€ β (πβπ¦)) β (πβπ¦) β dom π
) |
294 | 288, 293 | fssdmd 6733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ π€ β (πβπ¦)) β (πβπ¦) β π) |
295 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ π€ β (πβπ¦)) β π€ β (πβπ¦)) |
296 | 294, 295 | sseldd 3982 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ π€ β (πβπ¦)) β π€ β π) |
297 | 288, 296 | ffvelcdmd 7083 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ π€ β (πβπ¦)) β (π
βπ€) β (0[,]+β)) |
298 | 297 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β βπ€ β (πβπ¦)(π
βπ€) β (0[,]+β)) |
299 | | fvex 6901 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πβπ¦) β V |
300 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π€(πβπ¦) |
301 | 300 | esumcl 32966 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβπ¦) β V β§ βπ€ β (πβπ¦)(π
βπ€) β (0[,]+β)) β
Ξ£*π€ β
(πβπ¦)(π
βπ€) β (0[,]+β)) |
302 | 299, 301 | mpan 689 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ€ β
(πβπ¦)(π
βπ€) β (0[,]+β) β
Ξ£*π€ β
(πβπ¦)(π
βπ€) β (0[,]+β)) |
303 | 298, 302 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β Ξ£*π€ β (πβπ¦)(π
βπ€) β (0[,]+β)) |
304 | 285, 286,
287, 303 | syl21anc 837 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β§ π¦ β π) β Ξ£*π€ β (πβπ¦)(π
βπ€) β (0[,]+β)) |
305 | 304 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (π¦ β π β Ξ£*π€ β (πβπ¦)(π
βπ€) β (0[,]+β))) |
306 | 284, 305 | ralrimi 3255 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βπ¦ β π Ξ£*π€ β (πβπ¦)(π
βπ€) β (0[,]+β)) |
307 | 14 | esumcl 32966 |
. . . . . . . . . . . . . . . 16
β’ ((π β V β§ βπ¦ β π Ξ£*π€ β (πβπ¦)(π
βπ€) β (0[,]+β)) β
Ξ£*π¦ β
πΞ£*π€ β (πβπ¦)(π
βπ€) β (0[,]+β)) |
308 | 178, 306,
307 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β πΞ£*π€ β (πβπ¦)(π
βπ€) β (0[,]+β)) |
309 | 105, 308 | sselid 3979 |
. . . . . . . . . . . . . 14
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β πΞ£*π€ β (πβπ¦)(π
βπ€) β
β*) |
310 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π€(π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) |
311 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) |
312 | | fniunfv 7241 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π Fn π β βͺ
π¦ β π (πβπ¦) = βͺ ran π) |
313 | 311, 213,
312 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β βͺ π¦ β π (πβπ¦) = βͺ ran π) |
314 | 310, 313 | esumeq1d 32971 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β
Ξ£*π€ β
βͺ π¦ β π (πβπ¦)(π
βπ€) = Ξ£*π€ β βͺ ran
π(π
βπ€)) |
315 | 11 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β π β V) |
316 | 299 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β (πβπ¦) β V) |
317 | 315, 316,
297 | esumiun 33030 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β
Ξ£*π€ β
βͺ π¦ β π (πβπ¦)(π
βπ€) β€ Ξ£*π¦ β πΞ£*π€ β (πβπ¦)(π
βπ€)) |
318 | 314, 317 | eqbrtrrd 5171 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β
Ξ£*π€ β
βͺ ran π(π
βπ€) β€ Ξ£*π¦ β πΞ£*π€ β (πβπ¦)(π
βπ€)) |
319 | 9, 318 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β
Ξ£*π€ β
βͺ ran π(π
βπ€) β€ Ξ£*π¦ β πΞ£*π€ β (πβπ¦)(π
βπ€)) |
320 | 319 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π€ β βͺ ran π(π
βπ€) β€ Ξ£*π¦ β πΞ£*π€ β (πβπ¦)(π
βπ€)) |
321 | 252, 320 | eqbrtrid 5182 |
. . . . . . . . . . . . . 14
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π β βͺ ran π(π
βπ) β€ Ξ£*π¦ β πΞ£*π€ β (πβπ¦)(π
βπ€)) |
322 | 285, 287,
46 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β§ π¦ β π) β (πβπ΄) β (0[,]+β)) |
323 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β§ π¦ β π) β (((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β
β+)) |
324 | 323, 287,
73 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β§ π¦ β π) β (π / (2β(πβπ¦))) β (0[,]+β)) |
325 | 322, 324 | xrge0addcld 31953 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β§ π¦ β π) β ((πβπ΄) +π (π / (2β(πβπ¦)))) β (0[,]+β)) |
326 | 325 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (π¦ β π β ((πβπ΄) +π (π / (2β(πβπ¦)))) β (0[,]+β))) |
327 | 284, 326 | ralrimi 3255 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βπ¦ β π ((πβπ΄) +π (π / (2β(πβπ¦)))) β (0[,]+β)) |
328 | 14 | esumcl 32966 |
. . . . . . . . . . . . . . . . 17
β’ ((π β V β§ βπ¦ β π ((πβπ΄) +π (π / (2β(πβπ¦)))) β (0[,]+β)) β
Ξ£*π¦ β
π((πβπ΄) +π (π / (2β(πβπ¦)))) β (0[,]+β)) |
329 | 178, 327,
328 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β π((πβπ΄) +π (π / (2β(πβπ¦)))) β (0[,]+β)) |
330 | 105, 329 | sselid 3979 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β π((πβπ΄) +π (π / (2β(πβπ¦)))) β
β*) |
331 | 215, 10 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π β V) |
332 | | simp-4l 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β (π β§ Ξ£*π¦ β π(πβπ΄) β β)) |
333 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β π¦ β π) |
334 | 332, 333,
49 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β (πβπ΄) β β) |
335 | 334 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β (πβπ΄) β β) |
336 | 65 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β (π / (2β(πβπ¦))) β β) |
337 | 336 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β (π / (2β(πβπ¦))) β β) |
338 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))) β Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) |
339 | 338 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) |
340 | 66 | breq2d 5159 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πβπ΄) β β β§ (π / (2β(πβπ¦))) β β) β
(Ξ£*π€
β (πβπ¦)(π
βπ€) < ((πβπ΄) +π (π / (2β(πβπ¦)))) β Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) |
341 | 340 | biimpar 479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πβπ΄) β β β§ (π / (2β(πβπ¦))) β β) β§
Ξ£*π€ β
(πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) +π (π / (2β(πβπ¦))))) |
342 | 335, 337,
339, 341 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) +π (π / (2β(πβπ¦))))) |
343 | 342 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β (Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))) β Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) +π (π / (2β(πβπ¦)))))) |
344 | 332 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β π) |
345 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) |
346 | 344, 345,
333, 303 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β Ξ£*π€ β (πβπ¦)(π
βπ€) β (0[,]+β)) |
347 | 105, 346 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β Ξ£*π€ β (πβπ¦)(π
βπ€) β
β*) |
348 | 334 | rexrd 11260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β (πβπ΄) β
β*) |
349 | 336 | rexrd 11260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β (π / (2β(πβπ¦))) β
β*) |
350 | 348, 349 | xaddcld 13276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β ((πβπ΄) +π (π / (2β(πβπ¦)))) β
β*) |
351 | | xrltle 13124 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((Ξ£*π€ β (πβπ¦)(π
βπ€) β β* β§ ((πβπ΄) +π (π / (2β(πβπ¦)))) β β*) β
(Ξ£*π€
β (πβπ¦)(π
βπ€) < ((πβπ΄) +π (π / (2β(πβπ¦)))) β Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦)))))) |
352 | 347, 350,
351 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β (Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) +π (π / (2β(πβπ¦)))) β Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦)))))) |
353 | 343, 352 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β (Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))) β Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦)))))) |
354 | 353 | adantld 492 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ π¦ β π) β ((π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦)))))) |
355 | 354 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β (π¦ β π β ((π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦))))))) |
356 | 282, 355 | ralrimi 3255 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β βπ¦ β π ((π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦)))))) |
357 | | ralim 3087 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ¦ β
π ((π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦))))) β (βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β βπ¦ β π Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦)))))) |
358 | 356, 357 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β (βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))) β βπ¦ β π Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦)))))) |
359 | 358 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βπ¦ β π Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦))))) |
360 | 359 | r19.21bi 3249 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β§ π¦ β π) β Ξ£*π€ β (πβπ¦)(π
βπ€) β€ ((πβπ΄) +π (π / (2β(πβπ¦))))) |
361 | 284, 14, 331, 304, 325, 360 | esumlef 32998 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β πΞ£*π€ β (πβπ¦)(π
βπ€) β€ Ξ£*π¦ β π((πβπ΄) +π (π / (2β(πβπ¦))))) |
362 | 164, 46 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β§ π¦ β π) β (πβπ΄) β (0[,]+β)) |
363 | 284, 14, 331, 362, 324 | esumaddf 32997 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β π((πβπ΄) +π (π / (2β(πβπ¦)))) = (Ξ£*π¦ β π(πβπ΄) +π
Ξ£*π¦ β
π(π / (2β(πβπ¦))))) |
364 | 324 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (π¦ β π β (π / (2β(πβπ¦))) β (0[,]+β))) |
365 | 284, 364 | ralrimi 3255 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β βπ¦ β π (π / (2β(πβπ¦))) β (0[,]+β)) |
366 | 14 | esumcl 32966 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β V β§ βπ¦ β π (π / (2β(πβπ¦))) β (0[,]+β)) β
Ξ£*π¦ β
π(π / (2β(πβπ¦))) β (0[,]+β)) |
367 | 178, 365,
366 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β π(π / (2β(πβπ¦))) β (0[,]+β)) |
368 | 105, 367 | sselid 3979 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β π(π / (2β(πβπ¦))) β
β*) |
369 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π:πβ1-1ββ) |
370 | | vex 3479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ π β V |
371 | 370 | rnex 7898 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ran π β V |
372 | 371 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β ran π β V) |
373 | 58 | frnd 6722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π:πβ1-1ββ) β ran π β β) |
374 | 373 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β ran π β
β) |
375 | 374 | sselda 3981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π§ β ran π) β π§ β β) |
376 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π:πβ1-1ββ) β§ π§ β β) β 2 β
β+) |
377 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π:πβ1-1ββ) β§ π§ β β) β π§ β β) |
378 | 377 | nnzd 12581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π:πβ1-1ββ) β§ π§ β β) β π§ β β€) |
379 | 376, 378 | rpexpcld 14206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π:πβ1-1ββ) β§ π§ β β) β (2βπ§) β
β+) |
380 | 379 | rpreccld 13022 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π:πβ1-1ββ) β§ π§ β β) β (1 / (2βπ§)) β
β+) |
381 | 71, 380 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π:πβ1-1ββ) β§ π§ β β) β (1 / (2βπ§)) β
(0[,]+β)) |
382 | 381 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π§ β β) β (1 /
(2βπ§)) β
(0[,]+β)) |
383 | 375, 382 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π§ β ran π) β (1 / (2βπ§)) β (0[,]+β)) |
384 | 383 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β
βπ§ β ran π(1 / (2βπ§)) β (0[,]+β)) |
385 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π§ran
π |
386 | 385 | esumcl 32966 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((ran
π β V β§
βπ§ β ran π(1 / (2βπ§)) β (0[,]+β)) β
Ξ£*π§ β
ran π(1 / (2βπ§)) β
(0[,]+β)) |
387 | 372, 384,
386 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β
Ξ£*π§ β
ran π(1 / (2βπ§)) β
(0[,]+β)) |
388 | 105, 387 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β
Ξ£*π§ β
ran π(1 / (2βπ§)) β
β*) |
389 | | 1xr 11269 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 1 β
β* |
390 | 389 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β 1 β
β*) |
391 | 71 | sseli 3977 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β+
β π β
(0[,]+β)) |
392 | 391 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β π β
(0[,]+β)) |
393 | | elxrge0 13430 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0[,]+β) β
(π β
β* β§ 0 β€ π)) |
394 | 392, 393 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β (π β β*
β§ 0 β€ π)) |
395 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π§(π β§ π:πβ1-1ββ) |
396 | | nnex 12214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ β
β V |
397 | 396 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π:πβ1-1ββ) β β β
V) |
398 | 395, 397,
381, 373 | esummono 32990 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π:πβ1-1ββ) β Ξ£*π§ β ran π(1 / (2βπ§)) β€ Ξ£*π§ β β(1 / (2βπ§))) |
399 | | oveq2 7412 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ = π€ β (2βπ§) = (2βπ€)) |
400 | 399 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π§ = π€ β (1 / (2βπ§)) = (1 / (2βπ€))) |
401 | | ioossico 13411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(0(,)+β) β (0[,)+β) |
402 | 69, 401 | eqsstri 4015 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β+ β (0[,)+β) |
403 | 402, 380 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π:πβ1-1ββ) β§ π§ β β) β (1 / (2βπ§)) β
(0[,)+β)) |
404 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ β β β (π€ β β β¦ (1 /
(2βπ€))) = (π€ β β β¦ (1 /
(2βπ€)))) |
405 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π§ β β β§ π€ = π§) β π€ = π§) |
406 | 405 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π§ β β β§ π€ = π§) β (2βπ€) = (2βπ§)) |
407 | 406 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π§ β β β§ π€ = π§) β (1 / (2βπ€)) = (1 / (2βπ§))) |
408 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ β β β π§ β
β) |
409 | | ovexd 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ β β β (1 /
(2βπ§)) β
V) |
410 | 404, 407,
408, 409 | fvmptd 7001 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ β β β ((π€ β β β¦ (1 /
(2βπ€)))βπ§) = (1 / (2βπ§))) |
411 | 410 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π:πβ1-1ββ) β§ π§ β β) β ((π€ β β β¦ (1 / (2βπ€)))βπ§) = (1 / (2βπ§))) |
412 | | ax-1cn 11164 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 1 β
β |
413 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ β β β¦ (1 /
(2βπ€))) = (π€ β β β¦ (1 /
(2βπ€))) |
414 | 413 | geo2lim 15817 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (1 β
β β seq1( + , (π€
β β β¦ (1 / (2βπ€)))) β 1) |
415 | 412, 414 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ seq1( + ,
(π€ β β β¦
(1 / (2βπ€)))) β
1 |
416 | 415 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π:πβ1-1ββ) β seq1( + , (π€ β β β¦ (1 / (2βπ€)))) β 1) |
417 | | 1re 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 1 β
β |
418 | 417 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π:πβ1-1ββ) β 1 β
β) |
419 | 400, 403,
411, 416, 418 | esumcvgsum 33024 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π:πβ1-1ββ) β Ξ£*π§ β β(1 /
(2βπ§)) = Ξ£π§ β β (1 /
(2βπ§))) |
420 | | geoihalfsum 15824 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
Ξ£π§ β
β (1 / (2βπ§)) =
1 |
421 | 419, 420 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π:πβ1-1ββ) β Ξ£*π§ β β(1 /
(2βπ§)) =
1) |
422 | 398, 421 | breqtrd 5173 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π:πβ1-1ββ) β Ξ£*π§ β ran π(1 / (2βπ§)) β€ 1) |
423 | 422 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β
Ξ£*π§ β
ran π(1 / (2βπ§)) β€ 1) |
424 | | xlemul2a 13264 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((Ξ£*π§ β ran π(1 / (2βπ§)) β β* β§ 1 β
β* β§ (π β β* β§ 0 β€
π)) β§
Ξ£*π§ β
ran π(1 / (2βπ§)) β€ 1) β (π Β·e
Ξ£*π§ β
ran π(1 / (2βπ§))) β€ (π Β·e 1)) |
425 | 388, 390,
394, 423, 424 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β (π Β·e
Ξ£*π§ β
ran π(1 / (2βπ§))) β€ (π Β·e 1)) |
426 | 13, 19 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π¦(π β§ π:πβ1-1ββ) |
427 | 426, 21 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π¦((π β§ π:πβ1-1ββ) β§ π β β+) |
428 | 76 | recnd 11238 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β π β β) |
429 | 78 | recnd 11238 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β (2β(πβπ¦)) β β) |
430 | 429 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (2β(πβπ¦)) β β) |
431 | | 2cn 12283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 2 β
β |
432 | 431 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β 2 β β) |
433 | | 2ne0 12312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 2 β
0 |
434 | 433 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β 2 β 0) |
435 | 432, 434,
60 | expne0d 14113 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β (2β(πβπ¦)) β 0) |
436 | 435 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (2β(πβπ¦)) β 0) |
437 | 428, 430,
436 | divrecd 11989 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (π / (2β(πβπ¦))) = (π Β· (1 / (2β(πβπ¦))))) |
438 | | 1rp 12974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 1 β
β+ |
439 | 438 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β 1 β
β+) |
440 | 439, 61 | rpdivcld 13029 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β (1 / (2β(πβπ¦))) β
β+) |
441 | 52, 440 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β (1 / (2β(πβπ¦))) β β) |
442 | 441 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (1 / (2β(πβπ¦))) β β) |
443 | | rexmul 13246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ (1 /
(2β(πβπ¦))) β β) β
(π Β·e (1
/ (2β(πβπ¦)))) = (π Β· (1 / (2β(πβπ¦))))) |
444 | 76, 442, 443 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (π Β·e (1 / (2β(πβπ¦)))) = (π Β· (1 / (2β(πβπ¦))))) |
445 | 437, 444 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (π / (2β(πβπ¦))) = (π Β·e (1 / (2β(πβπ¦))))) |
446 | 445 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β
βπ¦ β π (π / (2β(πβπ¦))) = (π Β·e (1 / (2β(πβπ¦))))) |
447 | 427, 446 | esumeq2d 32973 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β
Ξ£*π¦ β
π(π / (2β(πβπ¦))) = Ξ£*π¦ β π(π Β·e (1 / (2β(πβπ¦))))) |
448 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β π β V) |
449 | 71, 440 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π:πβ1-1ββ) β§ π¦ β π) β (1 / (2β(πβπ¦))) β (0[,]+β)) |
450 | 449 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π:πβ1-1ββ) β§ π β β+) β§ π¦ β π) β (1 / (2β(πβπ¦))) β (0[,]+β)) |
451 | 402 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π:πβ1-1ββ) β β+ β
(0[,)+β)) |
452 | 451 | sselda 3981 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β π β
(0[,)+β)) |
453 | 448, 450,
452 | esummulc2 33018 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β (π Β·e
Ξ£*π¦ β
π(1 / (2β(πβπ¦)))) = Ξ£*π¦ β π(π Β·e (1 / (2β(πβπ¦))))) |
454 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π¦(1 /
(2βπ§)) |
455 | | oveq2 7412 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ = (πβπ¦) β (2βπ§) = (2β(πβπ¦))) |
456 | 455 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π§ = (πβπ¦) β (1 / (2βπ§)) = (1 / (2β(πβπ¦)))) |
457 | 11 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π:πβ1-1ββ) β π β V) |
458 | 56 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π:πβ1-1ββ β Fun β‘π) |
459 | 57 | feqmptd 6956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π:πβ1-1ββ β π = (π¦ β π β¦ (πβπ¦))) |
460 | 459 | cnveqd 5873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π:πβ1-1ββ β β‘π = β‘(π¦ β π β¦ (πβπ¦))) |
461 | 460 | funeqd 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π:πβ1-1ββ β (Fun β‘π β Fun β‘(π¦ β π β¦ (πβπ¦)))) |
462 | 458, 461 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π:πβ1-1ββ β Fun β‘(π¦ β π β¦ (πβπ¦))) |
463 | 462 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π:πβ1-1ββ) β Fun β‘(π¦ β π β¦ (πβπ¦))) |
464 | 454, 426,
14, 456, 457, 463, 449, 59 | esumc 32987 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π:πβ1-1ββ) β Ξ£*π¦ β π(1 / (2β(πβπ¦))) = Ξ£*π§ β {π₯ β£ βπ¦ β π π₯ = (πβπ¦)} (1 / (2βπ§))) |
465 | | ffn 6714 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π:πβΆβ β π Fn π) |
466 | | fnrnfv 6948 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π Fn π β ran π = {π₯ β£ βπ¦ β π π₯ = (πβπ¦)}) |
467 | 58, 465, 466 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π:πβ1-1ββ) β ran π = {π₯ β£ βπ¦ β π π₯ = (πβπ¦)}) |
468 | 395, 467 | esumeq1d 32971 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π:πβ1-1ββ) β Ξ£*π§ β ran π(1 / (2βπ§)) = Ξ£*π§ β {π₯ β£ βπ¦ β π π₯ = (πβπ¦)} (1 / (2βπ§))) |
469 | 464, 468 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π:πβ1-1ββ) β Ξ£*π¦ β π(1 / (2β(πβπ¦))) = Ξ£*π§ β ran π(1 / (2βπ§))) |
470 | 469 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β
Ξ£*π¦ β
π(1 / (2β(πβπ¦))) = Ξ£*π§ β ran π(1 / (2βπ§))) |
471 | 470 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β (π Β·e
Ξ£*π¦ β
π(1 / (2β(πβπ¦)))) = (π Β·e
Ξ£*π§ β
ran π(1 / (2βπ§)))) |
472 | 447, 453,
471 | 3eqtr2rd 2780 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β (π Β·e
Ξ£*π§ β
ran π(1 / (2βπ§))) = Ξ£*π¦ β π(π / (2β(πβπ¦)))) |
473 | 394 | simpld 496 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β π β
β*) |
474 | | xmulrid 13254 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β*
β (π
Β·e 1) = π) |
475 | 473, 474 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β (π Β·e 1) = π) |
476 | 425, 472,
475 | 3brtr3d 5178 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π:πβ1-1ββ) β§ π β β+) β
Ξ£*π¦ β
π(π / (2β(πβπ¦))) β€ π) |
477 | 164, 369,
204, 476 | syl21anc 837 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β π(π / (2β(πβπ¦))) β€ π) |
478 | | xleadd2a 13229 |
. . . . . . . . . . . . . . . . 17
β’
(((Ξ£*π¦ β π(π / (2β(πβπ¦))) β β* β§ π β β*
β§ Ξ£*π¦
β π(πβπ΄) β β*) β§
Ξ£*π¦ β
π(π / (2β(πβπ¦))) β€ π) β (Ξ£*π¦ β π(πβπ΄) +π
Ξ£*π¦ β
π(π / (2β(πβπ¦)))) β€ (Ξ£*π¦ β π(πβπ΄) +π π)) |
479 | 368, 205,
203, 477, 478 | syl31anc 1374 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (Ξ£*π¦ β π(πβπ΄) +π
Ξ£*π¦ β
π(π / (2β(πβπ¦)))) β€ (Ξ£*π¦ β π(πβπ΄) +π π)) |
480 | 363, 479 | eqbrtrd 5169 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β π((πβπ΄) +π (π / (2β(πβπ¦)))) β€ (Ξ£*π¦ β π(πβπ΄) +π π)) |
481 | 309, 330,
206, 361, 480 | xrletrd 13137 |
. . . . . . . . . . . . . 14
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π¦ β πΞ£*π€ β (πβπ¦)(π
βπ€) β€ (Ξ£*π¦ β π(πβπ΄) +π π)) |
482 | 201, 309,
206, 321, 481 | xrletrd 13137 |
. . . . . . . . . . . . 13
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β Ξ£*π β βͺ ran π(π
βπ) β€ (Ξ£*π¦ β π(πβπ΄) +π π)) |
483 | 176, 201,
206, 280, 482 | xrletrd 13137 |
. . . . . . . . . . . 12
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (πββͺ
π¦ β π π΄) β€ (Ξ£*π¦ β π(πβπ΄) +π π)) |
484 | 204 | rpred 13012 |
. . . . . . . . . . . . 13
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β π β β) |
485 | | rexadd 13207 |
. . . . . . . . . . . . 13
β’
((Ξ£*π¦ β π(πβπ΄) β β β§ π β β) β
(Ξ£*π¦
β π(πβπ΄) +π π) = (Ξ£*π¦ β π(πβπ΄) + π)) |
486 | 202, 484,
485 | syl2anc 585 |
. . . . . . . . . . . 12
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (Ξ£*π¦ β π(πβπ΄) +π π) = (Ξ£*π¦ β π(πβπ΄) + π)) |
487 | 483, 486 | breqtrd 5173 |
. . . . . . . . . . 11
β’
((((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο}) β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (πββͺ
π¦ β π π΄) β€ (Ξ£*π¦ β π(πβπ΄) + π)) |
488 | 487 | anasss 468 |
. . . . . . . . . 10
β’
(((((π β§
Ξ£*π¦ β
π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β§ (π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦))))))) β (πββͺ
π¦ β π π΄) β€ (Ξ£*π¦ β π(πβπ΄) + π)) |
489 | 488 | ex 414 |
. . . . . . . . 9
β’ ((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β ((π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (πββͺ
π¦ β π π΄) β€ (Ξ£*π¦ β π(πβπ΄) + π))) |
490 | 489 | exlimdv 1937 |
. . . . . . . 8
β’ ((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β
(βπ(π:πβΆ{π§ β π« dom π
β£ π§ βΌ Ο} β§ βπ¦ β π (π΄ β βͺ (πβπ¦) β§ Ξ£*π€ β (πβπ¦)(π
βπ€) < ((πβπ΄) + (π / (2β(πβπ¦)))))) β (πββͺ
π¦ β π π΄) β€ (Ξ£*π¦ β π(πβπ΄) + π))) |
491 | 163, 490 | mpd 15 |
. . . . . . 7
β’ ((((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β§ π β β+) β (πββͺ π¦ β π π΄) β€ (Ξ£*π¦ β π(πβπ΄) + π)) |
492 | 491 | ralrimiva 3147 |
. . . . . 6
β’ (((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β βπ β β+ (πββͺ π¦ β π π΄) β€ (Ξ£*π¦ β π(πβπ΄) + π)) |
493 | | xralrple 13180 |
. . . . . . . 8
β’ (((πββͺ π¦ β π π΄) β β* β§
Ξ£*π¦ β
π(πβπ΄) β β) β ((πββͺ
π¦ β π π΄) β€ Ξ£*π¦ β π(πβπ΄) β βπ β β+ (πββͺ π¦ β π π΄) β€ (Ξ£*π¦ β π(πβπ΄) + π))) |
494 | 175, 493 | sylan 581 |
. . . . . . 7
β’ ((π β§ Ξ£*π¦ β π(πβπ΄) β β) β ((πββͺ
π¦ β π π΄) β€ Ξ£*π¦ β π(πβπ΄) β βπ β β+ (πββͺ π¦ β π π΄) β€ (Ξ£*π¦ β π(πβπ΄) + π))) |
495 | 494 | adantr 482 |
. . . . . 6
β’ (((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β ((πββͺ
π¦ β π π΄) β€ Ξ£*π¦ β π(πβπ΄) β βπ β β+ (πββͺ π¦ β π π΄) β€ (Ξ£*π¦ β π(πβπ΄) + π))) |
496 | 492, 495 | mpbird 257 |
. . . . 5
β’ (((π β§ Ξ£*π¦ β π(πβπ΄) β β) β§ π:πβ1-1ββ) β (πββͺ
π¦ β π π΄) β€ Ξ£*π¦ β π(πβπ΄)) |
497 | 496 | ex 414 |
. . . 4
β’ ((π β§ Ξ£*π¦ β π(πβπ΄) β β) β (π:πβ1-1ββ β (πββͺ
π¦ β π π΄) β€ Ξ£*π¦ β π(πβπ΄))) |
498 | 497 | exlimdv 1937 |
. . 3
β’ ((π β§ Ξ£*π¦ β π(πβπ΄) β β) β (βπ π:πβ1-1ββ β (πββͺ
π¦ β π π΄) β€ Ξ£*π¦ β π(πβπ΄))) |
499 | 8, 498 | mpd 15 |
. 2
β’ ((π β§ Ξ£*π¦ β π(πβπ΄) β β) β (πββͺ
π¦ β π π΄) β€ Ξ£*π¦ β π(πβπ΄)) |
500 | 175 | adantr 482 |
. . . 4
β’ ((π β§ Β¬
Ξ£*π¦ β
π(πβπ΄) β β) β (πββͺ
π¦ β π π΄) β
β*) |
501 | | pnfge 13106 |
. . . 4
β’ ((πββͺ π¦ β π π΄) β β* β (πββͺ π¦ β π π΄) β€ +β) |
502 | 500, 501 | syl 17 |
. . 3
β’ ((π β§ Β¬
Ξ£*π¦ β
π(πβπ΄) β β) β (πββͺ
π¦ β π π΄) β€ +β) |
503 | 46 | ralrimiva 3147 |
. . . . 5
β’ (π β βπ¦ β π (πβπ΄) β (0[,]+β)) |
504 | 14 | esumcl 32966 |
. . . . 5
β’ ((π β V β§ βπ¦ β π (πβπ΄) β (0[,]+β)) β
Ξ£*π¦ β
π(πβπ΄) β (0[,]+β)) |
505 | 11, 503, 504 | syl2anc 585 |
. . . 4
β’ (π β Ξ£*π¦ β π(πβπ΄) β (0[,]+β)) |
506 | | xrge0nre 13426 |
. . . 4
β’
((Ξ£*π¦ β π(πβπ΄) β (0[,]+β) β§ Β¬
Ξ£*π¦ β
π(πβπ΄) β β) β
Ξ£*π¦ β
π(πβπ΄) = +β) |
507 | 505, 506 | sylan 581 |
. . 3
β’ ((π β§ Β¬
Ξ£*π¦ β
π(πβπ΄) β β) β
Ξ£*π¦ β
π(πβπ΄) = +β) |
508 | 502, 507 | breqtrrd 5175 |
. 2
β’ ((π β§ Β¬
Ξ£*π¦ β
π(πβπ΄) β β) β (πββͺ
π¦ β π π΄) β€ Ξ£*π¦ β π(πβπ΄)) |
509 | 499, 508 | pm2.61dan 812 |
1
β’ (π β (πββͺ
π¦ β π π΄) β€ Ξ£*π¦ β π(πβπ΄)) |