Step | Hyp | Ref
| Expression |
1 | | hoidmvlelem1.s |
. . . . . 6
β’ π = sup(π, β, < ) |
2 | 1 | a1i 11 |
. . . . 5
β’ (π β π = sup(π, β, < )) |
3 | | hoidmvlelem1.a |
. . . . . . 7
β’ (π β π΄:πβΆβ) |
4 | | hoidmvlelem1.z |
. . . . . . . . . 10
β’ (π β π β (π β π)) |
5 | | snidg 4618 |
. . . . . . . . . 10
β’ (π β (π β π) β π β {π}) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
β’ (π β π β {π}) |
7 | | elun2 4135 |
. . . . . . . . 9
β’ (π β {π} β π β (π βͺ {π})) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
β’ (π β π β (π βͺ {π})) |
9 | | hoidmvlelem1.w |
. . . . . . . 8
β’ π = (π βͺ {π}) |
10 | 8, 9 | eleqtrrdi 2849 |
. . . . . . 7
β’ (π β π β π) |
11 | 3, 10 | ffvelcdmd 7032 |
. . . . . 6
β’ (π β (π΄βπ) β β) |
12 | | hoidmvlelem1.b |
. . . . . . 7
β’ (π β π΅:πβΆβ) |
13 | 12, 10 | ffvelcdmd 7032 |
. . . . . 6
β’ (π β (π΅βπ) β β) |
14 | | hoidmvlelem1.u |
. . . . . . . 8
β’ π = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} |
15 | | ssrab2 4035 |
. . . . . . . 8
β’ {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β ((π΄βπ)[,](π΅βπ)) |
16 | 14, 15 | eqsstri 3976 |
. . . . . . 7
β’ π β ((π΄βπ)[,](π΅βπ)) |
17 | 16 | a1i 11 |
. . . . . 6
β’ (π β π β ((π΄βπ)[,](π΅βπ))) |
18 | 11 | leidd 11679 |
. . . . . . . . . . 11
β’ (π β (π΄βπ) β€ (π΄βπ)) |
19 | | hoidmvlelem1.ab |
. . . . . . . . . . . 12
β’ (π β (π΄βπ) < (π΅βπ)) |
20 | 11, 13, 19 | ltled 11261 |
. . . . . . . . . . 11
β’ (π β (π΄βπ) β€ (π΅βπ)) |
21 | 11, 13, 11, 18, 20 | eliccd 43643 |
. . . . . . . . . 10
β’ (π β (π΄βπ) β ((π΄βπ)[,](π΅βπ))) |
22 | 11 | recnd 11141 |
. . . . . . . . . . . . . 14
β’ (π β (π΄βπ) β β) |
23 | 22 | subidd 11458 |
. . . . . . . . . . . . 13
β’ (π β ((π΄βπ) β (π΄βπ)) = 0) |
24 | 23 | oveq2d 7367 |
. . . . . . . . . . . 12
β’ (π β (πΊ Β· ((π΄βπ) β (π΄βπ))) = (πΊ Β· 0)) |
25 | | rge0ssre 13327 |
. . . . . . . . . . . . . . 15
β’
(0[,)+β) β β |
26 | | hoidmvlelem1.g |
. . . . . . . . . . . . . . . 16
β’ πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) |
27 | | hoidmvlelem1.l |
. . . . . . . . . . . . . . . . 17
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
28 | | hoidmvlelem1.x |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β Fin) |
29 | | hoidmvlelem1.y |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β π) |
30 | 28, 29 | ssfid 9169 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β Fin) |
31 | | ssun1 4130 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β (π βͺ {π}) |
32 | 31, 9 | sseqtrri 3979 |
. . . . . . . . . . . . . . . . . . 19
β’ π β π |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β π) |
34 | 3, 33 | fssresd 6706 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΄ βΎ π):πβΆβ) |
35 | 12, 33 | fssresd 6706 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΅ βΎ π):πβΆβ) |
36 | 27, 30, 34, 35 | hoidmvcl 44724 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β (0[,)+β)) |
37 | 26, 36 | eqeltrid 2842 |
. . . . . . . . . . . . . . 15
β’ (π β πΊ β (0[,)+β)) |
38 | 25, 37 | sselid 3940 |
. . . . . . . . . . . . . 14
β’ (π β πΊ β β) |
39 | 38 | recnd 11141 |
. . . . . . . . . . . . 13
β’ (π β πΊ β β) |
40 | 39 | mul01d 11312 |
. . . . . . . . . . . 12
β’ (π β (πΊ Β· 0) = 0) |
41 | 24, 40 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β (πΊ Β· ((π΄βπ) β (π΄βπ))) = 0) |
42 | | 1red 11114 |
. . . . . . . . . . . . 13
β’ (π β 1 β
β) |
43 | | hoidmvlelem1.e |
. . . . . . . . . . . . . 14
β’ (π β πΈ β
β+) |
44 | 43 | rpred 12911 |
. . . . . . . . . . . . 13
β’ (π β πΈ β β) |
45 | 42, 44 | readdcld 11142 |
. . . . . . . . . . . 12
β’ (π β (1 + πΈ) β β) |
46 | | 0red 11116 |
. . . . . . . . . . . . 13
β’ (π β 0 β
β) |
47 | | 0lt1 11635 |
. . . . . . . . . . . . . . 15
β’ 0 <
1 |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 0 < 1) |
49 | 42, 43 | ltaddrpd 12944 |
. . . . . . . . . . . . . 14
β’ (π β 1 < (1 + πΈ)) |
50 | 46, 42, 45, 48, 49 | lttrd 11274 |
. . . . . . . . . . . . 13
β’ (π β 0 < (1 + πΈ)) |
51 | 46, 45, 50 | ltled 11261 |
. . . . . . . . . . . 12
β’ (π β 0 β€ (1 + πΈ)) |
52 | | nnex 12117 |
. . . . . . . . . . . . . . 15
β’ β
β V |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β β
V) |
54 | | icossicc 13307 |
. . . . . . . . . . . . . . . 16
β’
(0[,)+β) β (0[,]+β) |
55 | | snfi 8946 |
. . . . . . . . . . . . . . . . . . . . 21
β’ {π} β Fin |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {π} β Fin) |
57 | | unfi 9074 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Fin β§ {π} β Fin) β (π βͺ {π}) β Fin) |
58 | 30, 56, 57 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π βͺ {π}) β Fin) |
59 | 9, 58 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β Fin) |
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β π β Fin) |
61 | | hoidmvlelem1.c |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΆ:ββΆ(β βm
π)) |
62 | 61 | ffvelcdmda 7031 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (πΆβπ) β (β βm π)) |
63 | | elmapi 8745 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΆβπ) β (β βm π) β (πΆβπ):πβΆβ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
65 | | hoidmvlelem1.h |
. . . . . . . . . . . . . . . . . . 19
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
66 | | eleq1w 2820 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = β β (π β π β β β π)) |
67 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = β β (πβπ) = (πββ)) |
68 | 67 | breq1d 5113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = β β ((πβπ) β€ π₯ β (πββ) β€ π₯)) |
69 | 68, 67 | ifbieq1d 4508 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = β β if((πβπ) β€ π₯, (πβπ), π₯) = if((πββ) β€ π₯, (πββ), π₯)) |
70 | 66, 67, 69 | ifbieq12d 4512 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = β β if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)) = if(β β π, (πββ), if((πββ) β€ π₯, (πββ), π₯))) |
71 | 70 | cbvmptv 5216 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) = (β β π β¦ if(β β π, (πββ), if((πββ) β€ π₯, (πββ), π₯))) |
72 | 71 | mpteq2i 5208 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) = (π β (β βm π) β¦ (β β π β¦ if(β β π, (πββ), if((πββ) β€ π₯, (πββ), π₯)))) |
73 | 72 | mpteq2i 5208 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β¦ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) = (π₯ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β β π, (πββ), if((πββ) β€ π₯, (πββ), π₯))))) |
74 | 65, 73 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β β π, (πββ), if((πββ) β€ π₯, (πββ), π₯))))) |
75 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π΄βπ) β β) |
76 | | hoidmvlelem1.d |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π·:ββΆ(β βm
π)) |
77 | 76 | ffvelcdmda 7031 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (π·βπ) β (β βm π)) |
78 | | elmapi 8745 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π·βπ) β (β βm π) β (π·βπ):πβΆβ) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π·βπ):πβΆβ) |
80 | 74, 75, 60, 79 | hsphoif 44718 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β ((π»β(π΄βπ))β(π·βπ)):πβΆβ) |
81 | 27, 60, 64, 80 | hoidmvcl 44724 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))) β (0[,)+β)) |
82 | 54, 81 | sselid 3940 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))) β (0[,]+β)) |
83 | 82 | fmpttd 7059 |
. . . . . . . . . . . . . 14
β’ (π β (π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ)))):ββΆ(0[,]+β)) |
84 | 53, 83 | sge0cl 44523 |
. . . . . . . . . . . . 13
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) β (0[,]+β)) |
85 | 53, 83 | sge0xrcl 44527 |
. . . . . . . . . . . . . 14
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) β
β*) |
86 | | pnfxr 11167 |
. . . . . . . . . . . . . . 15
β’ +β
β β* |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β +β β
β*) |
88 | | hoidmvlelem1.r |
. . . . . . . . . . . . . . . 16
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
89 | 88 | rexrd 11163 |
. . . . . . . . . . . . . . 15
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β
β*) |
90 | | nfv 1917 |
. . . . . . . . . . . . . . . 16
β’
β²ππ |
91 | 27, 60, 64, 79 | hoidmvcl 44724 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,)+β)) |
92 | 54, 91 | sselid 3940 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,]+β)) |
93 | 4 | eldifbd 3921 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Β¬ π β π) |
94 | 10, 93 | eldifd 3919 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (π β π)) |
95 | 94 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β π β (π β π)) |
96 | 27, 60, 95, 9, 75, 74, 64, 79 | hsphoidmvle 44728 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))) β€ ((πΆβπ)(πΏβπ)(π·βπ))) |
97 | 90, 53, 82, 92, 96 | sge0lempt 44552 |
. . . . . . . . . . . . . . 15
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
98 | 88 | ltpnfd 12996 |
. . . . . . . . . . . . . . 15
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) < +β) |
99 | 85, 89, 87, 97, 98 | xrlelttrd 13033 |
. . . . . . . . . . . . . 14
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) < +β) |
100 | 85, 87, 99 | xrltned 43496 |
. . . . . . . . . . . . 13
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) β +β) |
101 | | ge0xrre 43670 |
. . . . . . . . . . . . 13
β’
(((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) β (0[,]+β) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) β +β) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) β β) |
102 | 84, 100, 101 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) β β) |
103 | 53, 83 | sge0ge0 44526 |
. . . . . . . . . . . 12
β’ (π β 0 β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ)))))) |
104 | | mulge0 11631 |
. . . . . . . . . . . 12
β’ ((((1 +
πΈ) β β β§ 0
β€ (1 + πΈ)) β§
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) β β β§ 0 β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))))) β 0 β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))))) |
105 | 45, 51, 102, 103, 104 | syl22anc 837 |
. . . . . . . . . . 11
β’ (π β 0 β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))))) |
106 | 41, 105 | eqbrtrd 5125 |
. . . . . . . . . 10
β’ (π β (πΊ Β· ((π΄βπ) β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))))) |
107 | 21, 106 | jca 512 |
. . . . . . . . 9
β’ (π β ((π΄βπ) β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· ((π΄βπ) β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ)))))))) |
108 | | oveq1 7358 |
. . . . . . . . . . . 12
β’ (π§ = (π΄βπ) β (π§ β (π΄βπ)) = ((π΄βπ) β (π΄βπ))) |
109 | 108 | oveq2d 7367 |
. . . . . . . . . . 11
β’ (π§ = (π΄βπ) β (πΊ Β· (π§ β (π΄βπ))) = (πΊ Β· ((π΄βπ) β (π΄βπ)))) |
110 | | fveq2 6839 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π΄βπ) β (π»βπ§) = (π»β(π΄βπ))) |
111 | 110 | fveq1d 6841 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π΄βπ) β ((π»βπ§)β(π·βπ)) = ((π»β(π΄βπ))β(π·βπ))) |
112 | 111 | oveq2d 7367 |
. . . . . . . . . . . . . 14
β’ (π§ = (π΄βπ) β ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))) = ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ)))) |
113 | 112 | mpteq2dv 5205 |
. . . . . . . . . . . . 13
β’ (π§ = (π΄βπ) β (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))) |
114 | 113 | fveq2d 6843 |
. . . . . . . . . . . 12
β’ (π§ = (π΄βπ) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ)))))) |
115 | 114 | oveq2d 7367 |
. . . . . . . . . . 11
β’ (π§ = (π΄βπ) β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) = ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ))))))) |
116 | 109, 115 | breq12d 5116 |
. . . . . . . . . 10
β’ (π§ = (π΄βπ) β ((πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) β (πΊ Β· ((π΄βπ) β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ)))))))) |
117 | 116 | elrab 3643 |
. . . . . . . . 9
β’ ((π΄βπ) β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β ((π΄βπ) β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· ((π΄βπ) β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΄βπ))β(π·βπ)))))))) |
118 | 107, 117 | sylibr 233 |
. . . . . . . 8
β’ (π β (π΄βπ) β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))}) |
119 | 118, 14 | eleqtrrdi 2849 |
. . . . . . 7
β’ (π β (π΄βπ) β π) |
120 | | ne0i 4292 |
. . . . . . 7
β’ ((π΄βπ) β π β π β β
) |
121 | 119, 120 | syl 17 |
. . . . . 6
β’ (π β π β β
) |
122 | 11, 13, 17, 121 | supicc 13372 |
. . . . 5
β’ (π β sup(π, β, < ) β ((π΄βπ)[,](π΅βπ))) |
123 | 2, 122 | eqeltrd 2838 |
. . . 4
β’ (π β π β ((π΄βπ)[,](π΅βπ))) |
124 | 2 | oveq1d 7366 |
. . . . . . 7
β’ (π β (π β (π΄βπ)) = (sup(π, β, < ) β (π΄βπ))) |
125 | 124 | oveq2d 7367 |
. . . . . 6
β’ (π β (πΊ Β· (π β (π΄βπ))) = (πΊ Β· (sup(π, β, < ) β (π΄βπ)))) |
126 | 11, 13 | iccssred 13305 |
. . . . . . . . 9
β’ (π β ((π΄βπ)[,](π΅βπ)) β β) |
127 | 17, 126 | sstrd 3952 |
. . . . . . . 8
β’ (π β π β β) |
128 | 11, 13 | jca 512 |
. . . . . . . . . 10
β’ (π β ((π΄βπ) β β β§ (π΅βπ) β β)) |
129 | | iccsupr 13313 |
. . . . . . . . . 10
β’ ((((π΄βπ) β β β§ (π΅βπ) β β) β§ π β ((π΄βπ)[,](π΅βπ)) β§ (π΄βπ) β π) β (π β β β§ π β β
β§ βπ¦ β β βπ§ β π π§ β€ π¦)) |
130 | 128, 17, 119, 129 | syl3anc 1371 |
. . . . . . . . 9
β’ (π β (π β β β§ π β β
β§ βπ¦ β β βπ§ β π π§ β€ π¦)) |
131 | 130 | simp3d 1144 |
. . . . . . . 8
β’ (π β βπ¦ β β βπ§ β π π§ β€ π¦) |
132 | | eqid 2737 |
. . . . . . . 8
β’ {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} = {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} |
133 | 127, 121,
131, 11, 132 | supsubc 43492 |
. . . . . . 7
β’ (π β (sup(π, β, < ) β (π΄βπ)) = sup({π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}, β, < )) |
134 | 133 | oveq2d 7367 |
. . . . . 6
β’ (π β (πΊ Β· (sup(π, β, < ) β (π΄βπ))) = (πΊ Β· sup({π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}, β, < ))) |
135 | 46 | rexrd 11163 |
. . . . . . . 8
β’ (π β 0 β
β*) |
136 | | icogelb 13269 |
. . . . . . . 8
β’ ((0
β β* β§ +β β β* β§
πΊ β (0[,)+β))
β 0 β€ πΊ) |
137 | 135, 87, 37, 136 | syl3anc 1371 |
. . . . . . 7
β’ (π β 0 β€ πΊ) |
138 | | vex 3447 |
. . . . . . . . . . . 12
β’ π β V |
139 | | eqeq1 2741 |
. . . . . . . . . . . . 13
β’ (π€ = π β (π€ = (π’ β (π΄βπ)) β π = (π’ β (π΄βπ)))) |
140 | 139 | rexbidv 3173 |
. . . . . . . . . . . 12
β’ (π€ = π β (βπ’ β π π€ = (π’ β (π΄βπ)) β βπ’ β π π = (π’ β (π΄βπ)))) |
141 | 138, 140 | elab 3628 |
. . . . . . . . . . 11
β’ (π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β βπ’ β π π = (π’ β (π΄βπ))) |
142 | 141 | biimpi 215 |
. . . . . . . . . 10
β’ (π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β βπ’ β π π = (π’ β (π΄βπ))) |
143 | 142 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β βπ’ β π π = (π’ β (π΄βπ))) |
144 | | nfv 1917 |
. . . . . . . . . . 11
β’
β²π’π |
145 | | nfcv 2905 |
. . . . . . . . . . . 12
β’
β²π’π |
146 | | nfre1 3266 |
. . . . . . . . . . . . 13
β’
β²π’βπ’ β π π€ = (π’ β (π΄βπ)) |
147 | 146 | nfab 2911 |
. . . . . . . . . . . 12
β’
β²π’{π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} |
148 | 145, 147 | nfel 2919 |
. . . . . . . . . . 11
β’
β²π’ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} |
149 | 144, 148 | nfan 1902 |
. . . . . . . . . 10
β’
β²π’(π β§ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) |
150 | | nfv 1917 |
. . . . . . . . . 10
β’
β²π’0 β€ π |
151 | 11 | rexrd 11163 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΄βπ) β
β*) |
152 | 151 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β (π΄βπ) β
β*) |
153 | 13 | rexrd 11163 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΅βπ) β
β*) |
154 | 153 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β (π΅βπ) β
β*) |
155 | 17 | sselda 3942 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β π’ β ((π΄βπ)[,](π΅βπ))) |
156 | | iccgelb 13274 |
. . . . . . . . . . . . . . . 16
β’ (((π΄βπ) β β* β§ (π΅βπ) β β* β§ π’ β ((π΄βπ)[,](π΅βπ))) β (π΄βπ) β€ π’) |
157 | 152, 154,
155, 156 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β (π΄βπ) β€ π’) |
158 | 127 | sselda 3942 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β π’ β β) |
159 | 11 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β (π΄βπ) β β) |
160 | 158, 159 | subge0d 11703 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β (0 β€ (π’ β (π΄βπ)) β (π΄βπ) β€ π’)) |
161 | 157, 160 | mpbird 256 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π) β 0 β€ (π’ β (π΄βπ))) |
162 | 161 | 3adant3 1132 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β π β§ π = (π’ β (π΄βπ))) β 0 β€ (π’ β (π΄βπ))) |
163 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π = (π’ β (π΄βπ)) β π = (π’ β (π΄βπ))) |
164 | 163 | eqcomd 2743 |
. . . . . . . . . . . . . 14
β’ (π = (π’ β (π΄βπ)) β (π’ β (π΄βπ)) = π) |
165 | 164 | 3ad2ant3 1135 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β π β§ π = (π’ β (π΄βπ))) β (π’ β (π΄βπ)) = π) |
166 | 162, 165 | breqtrd 5129 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β π β§ π = (π’ β (π΄βπ))) β 0 β€ π) |
167 | 166 | 3exp 1119 |
. . . . . . . . . . 11
β’ (π β (π’ β π β (π = (π’ β (π΄βπ)) β 0 β€ π))) |
168 | 167 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β (π’ β π β (π = (π’ β (π΄βπ)) β 0 β€ π))) |
169 | 149, 150,
168 | rexlimd 3247 |
. . . . . . . . 9
β’ ((π β§ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β (βπ’ β π π = (π’ β (π΄βπ)) β 0 β€ π)) |
170 | 143, 169 | mpd 15 |
. . . . . . . 8
β’ ((π β§ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β 0 β€ π) |
171 | 170 | ralrimiva 3141 |
. . . . . . 7
β’ (π β βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}0 β€ π) |
172 | | simp3 1138 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β π β§ π€ = (π’ β (π΄βπ))) β π€ = (π’ β (π΄βπ))) |
173 | 158, 159 | resubcld 11541 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β π) β (π’ β (π΄βπ)) β β) |
174 | 173 | 3adant3 1132 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β π β§ π€ = (π’ β (π΄βπ))) β (π’ β (π΄βπ)) β β) |
175 | 172, 174 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ ((π β§ π’ β π β§ π€ = (π’ β (π΄βπ))) β π€ β β) |
176 | 175 | 3exp 1119 |
. . . . . . . . . 10
β’ (π β (π’ β π β (π€ = (π’ β (π΄βπ)) β π€ β β))) |
177 | 176 | rexlimdv 3148 |
. . . . . . . . 9
β’ (π β (βπ’ β π π€ = (π’ β (π΄βπ)) β π€ β β)) |
178 | 177 | alrimiv 1930 |
. . . . . . . 8
β’ (π β βπ€(βπ’ β π π€ = (π’ β (π΄βπ)) β π€ β β)) |
179 | | abss 4015 |
. . . . . . . 8
β’ ({π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β β β βπ€(βπ’ β π π€ = (π’ β (π΄βπ)) β π€ β β)) |
180 | 178, 179 | sylibr 233 |
. . . . . . 7
β’ (π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β β) |
181 | 23 | eqcomd 2743 |
. . . . . . . . . 10
β’ (π β 0 = ((π΄βπ) β (π΄βπ))) |
182 | | oveq1 7358 |
. . . . . . . . . . 11
β’ (π’ = (π΄βπ) β (π’ β (π΄βπ)) = ((π΄βπ) β (π΄βπ))) |
183 | 182 | rspceeqv 3593 |
. . . . . . . . . 10
β’ (((π΄βπ) β π β§ 0 = ((π΄βπ) β (π΄βπ))) β βπ’ β π 0 = (π’ β (π΄βπ))) |
184 | 119, 181,
183 | syl2anc 584 |
. . . . . . . . 9
β’ (π β βπ’ β π 0 = (π’ β (π΄βπ))) |
185 | | eqeq1 2741 |
. . . . . . . . . 10
β’ (π€ = 0 β (π€ = (π’ β (π΄βπ)) β 0 = (π’ β (π΄βπ)))) |
186 | 185 | rexbidv 3173 |
. . . . . . . . 9
β’ (π€ = 0 β (βπ’ β π π€ = (π’ β (π΄βπ)) β βπ’ β π 0 = (π’ β (π΄βπ)))) |
187 | 46, 184, 186 | elabd 3631 |
. . . . . . . 8
β’ (π β 0 β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) |
188 | | ne0i 4292 |
. . . . . . . 8
β’ (0 β
{π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β β
) |
189 | 187, 188 | syl 17 |
. . . . . . 7
β’ (π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β β
) |
190 | 13, 11 | resubcld 11541 |
. . . . . . . 8
β’ (π β ((π΅βπ) β (π΄βπ)) β β) |
191 | | vex 3447 |
. . . . . . . . . . . . 13
β’ π β V |
192 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
β’ (π€ = π β (π€ = (π’ β (π΄βπ)) β π = (π’ β (π΄βπ)))) |
193 | 192 | rexbidv 3173 |
. . . . . . . . . . . . 13
β’ (π€ = π β (βπ’ β π π€ = (π’ β (π΄βπ)) β βπ’ β π π = (π’ β (π΄βπ)))) |
194 | 191, 193 | elab 3628 |
. . . . . . . . . . . 12
β’ (π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β βπ’ β π π = (π’ β (π΄βπ))) |
195 | 194 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β βπ’ β π π = (π’ β (π΄βπ))) |
196 | 195 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β βπ’ β π π = (π’ β (π΄βπ))) |
197 | | nfcv 2905 |
. . . . . . . . . . . . 13
β’
β²π’π |
198 | 197, 147 | nfel 2919 |
. . . . . . . . . . . 12
β’
β²π’ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} |
199 | 144, 198 | nfan 1902 |
. . . . . . . . . . 11
β’
β²π’(π β§ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) |
200 | | nfv 1917 |
. . . . . . . . . . 11
β’
β²π’ π β€ ((π΅βπ) β (π΄βπ)) |
201 | | simp3 1138 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π β§ π = (π’ β (π΄βπ))) β π = (π’ β (π΄βπ))) |
202 | 159 | 3adant3 1132 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π β§ π = (π’ β (π΄βπ))) β (π΄βπ) β β) |
203 | 13 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π β§ π = (π’ β (π΄βπ))) β (π΅βπ) β β) |
204 | 155 | 3adant3 1132 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π β§ π = (π’ β (π΄βπ))) β π’ β ((π΄βπ)[,](π΅βπ))) |
205 | 21 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π β§ π = (π’ β (π΄βπ))) β (π΄βπ) β ((π΄βπ)[,](π΅βπ))) |
206 | 202, 203,
204, 205 | iccsuble 43658 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π β§ π = (π’ β (π΄βπ))) β (π’ β (π΄βπ)) β€ ((π΅βπ) β (π΄βπ))) |
207 | 201, 206 | eqbrtrd 5125 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β π β§ π = (π’ β (π΄βπ))) β π β€ ((π΅βπ) β (π΄βπ))) |
208 | 207 | 3exp 1119 |
. . . . . . . . . . . 12
β’ (π β (π’ β π β (π = (π’ β (π΄βπ)) β π β€ ((π΅βπ) β (π΄βπ))))) |
209 | 208 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β (π’ β π β (π = (π’ β (π΄βπ)) β π β€ ((π΅βπ) β (π΄βπ))))) |
210 | 199, 200,
209 | rexlimd 3247 |
. . . . . . . . . 10
β’ ((π β§ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β (βπ’ β π π = (π’ β (π΄βπ)) β π β€ ((π΅βπ) β (π΄βπ)))) |
211 | 196, 210 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β π β€ ((π΅βπ) β (π΄βπ))) |
212 | 211 | ralrimiva 3141 |
. . . . . . . 8
β’ (π β βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π β€ ((π΅βπ) β (π΄βπ))) |
213 | | brralrspcev 5163 |
. . . . . . . 8
β’ ((((π΅βπ) β (π΄βπ)) β β β§ βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π β€ ((π΅βπ) β (π΄βπ))) β βπ β β βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π β€ π) |
214 | 190, 212,
213 | syl2anc 584 |
. . . . . . 7
β’ (π β βπ β β βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π β€ π) |
215 | | eqid 2737 |
. . . . . . . 8
β’ {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} = {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} |
216 | | biid 260 |
. . . . . . . 8
β’ (((πΊ β β β§ 0 β€
πΊ β§ βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}0 β€ π) β§ ({π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β β β§ {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β β
β§ βπ β β βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π β€ π)) β ((πΊ β β β§ 0 β€ πΊ β§ βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}0 β€ π) β§ ({π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β β β§ {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β β
β§ βπ β β βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π β€ π))) |
217 | 215, 216 | supmul1 12082 |
. . . . . . 7
β’ (((πΊ β β β§ 0 β€
πΊ β§ βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}0 β€ π) β§ ({π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β β β§ {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β β
β§ βπ β β βπ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π β€ π)) β (πΊ Β· sup({π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}, β, < )) = sup({π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}, β, < )) |
218 | 38, 137, 171, 180, 189, 214, 217 | syl33anc 1385 |
. . . . . 6
β’ (π β (πΊ Β· sup({π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}, β, < )) = sup({π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}, β, < )) |
219 | 125, 134,
218 | 3eqtrd 2781 |
. . . . 5
β’ (π β (πΊ Β· (π β (π΄βπ))) = sup({π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}, β, < )) |
220 | | vex 3447 |
. . . . . . . . . . . 12
β’ π β V |
221 | | eqeq1 2741 |
. . . . . . . . . . . . 13
β’ (π£ = π β (π£ = (πΊ Β· π‘) β π = (πΊ Β· π‘))) |
222 | 221 | rexbidv 3173 |
. . . . . . . . . . . 12
β’ (π£ = π β (βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘) β βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π = (πΊ Β· π‘))) |
223 | 220, 222 | elab 3628 |
. . . . . . . . . . 11
β’ (π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π = (πΊ Β· π‘)) |
224 | 223 | biimpi 215 |
. . . . . . . . . 10
β’ (π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π = (πΊ Β· π‘)) |
225 | | nfv 1917 |
. . . . . . . . . . . 12
β’
β²π‘βπ’ β π π = (πΊ Β· (π’ β (π΄βπ))) |
226 | | vex 3447 |
. . . . . . . . . . . . . . . . 17
β’ π‘ β V |
227 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = π‘ β (π€ = (π’ β (π΄βπ)) β π‘ = (π’ β (π΄βπ)))) |
228 | 227 | rexbidv 3173 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π‘ β (βπ’ β π π€ = (π’ β (π΄βπ)) β βπ’ β π π‘ = (π’ β (π΄βπ)))) |
229 | 226, 228 | elab 3628 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β βπ’ β π π‘ = (π’ β (π΄βπ))) |
230 | 229 | biimpi 215 |
. . . . . . . . . . . . . . 15
β’ (π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β βπ’ β π π‘ = (π’ β (π΄βπ))) |
231 | 230 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β§ π = (πΊ Β· π‘)) β βπ’ β π π‘ = (π’ β (π΄βπ))) |
232 | | simpl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = (πΊ Β· π‘) β§ π‘ = (π’ β (π΄βπ))) β π = (πΊ Β· π‘)) |
233 | | oveq2 7359 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = (π’ β (π΄βπ)) β (πΊ Β· π‘) = (πΊ Β· (π’ β (π΄βπ)))) |
234 | 233 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = (πΊ Β· π‘) β§ π‘ = (π’ β (π΄βπ))) β (πΊ Β· π‘) = (πΊ Β· (π’ β (π΄βπ)))) |
235 | 232, 234 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (πΊ Β· π‘) β§ π‘ = (π’ β (π΄βπ))) β π = (πΊ Β· (π’ β (π΄βπ)))) |
236 | 235 | ex 413 |
. . . . . . . . . . . . . . . 16
β’ (π = (πΊ Β· π‘) β (π‘ = (π’ β (π΄βπ)) β π = (πΊ Β· (π’ β (π΄βπ))))) |
237 | 236 | reximdv 3165 |
. . . . . . . . . . . . . . 15
β’ (π = (πΊ Β· π‘) β (βπ’ β π π‘ = (π’ β (π΄βπ)) β βπ’ β π π = (πΊ Β· (π’ β (π΄βπ))))) |
238 | 237 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β§ π = (πΊ Β· π‘)) β (βπ’ β π π‘ = (π’ β (π΄βπ)) β βπ’ β π π = (πΊ Β· (π’ β (π΄βπ))))) |
239 | 231, 238 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β§ π = (πΊ Β· π‘)) β βπ’ β π π = (πΊ Β· (π’ β (π΄βπ)))) |
240 | 239 | ex 413 |
. . . . . . . . . . . 12
β’ (π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β (π = (πΊ Β· π‘) β βπ’ β π π = (πΊ Β· (π’ β (π΄βπ))))) |
241 | 225, 240 | rexlimi 3240 |
. . . . . . . . . . 11
β’
(βπ‘ β
{π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π = (πΊ Β· π‘) β βπ’ β π π = (πΊ Β· (π’ β (π΄βπ)))) |
242 | 241 | a1i 11 |
. . . . . . . . . 10
β’ (π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β (βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π = (πΊ Β· π‘) β βπ’ β π π = (πΊ Β· (π’ β (π΄βπ))))) |
243 | 224, 242 | mpd 15 |
. . . . . . . . 9
β’ (π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β βπ’ β π π = (πΊ Β· (π’ β (π΄βπ)))) |
244 | 243 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) β βπ’ β π π = (πΊ Β· (π’ β (π΄βπ)))) |
245 | | simp3 1138 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β π β§ π = (πΊ Β· (π’ β (π΄βπ)))) β π = (πΊ Β· (π’ β (π΄βπ)))) |
246 | 38 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β πΊ β β) |
247 | 246, 173 | remulcld 11143 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π) β (πΊ Β· (π’ β (π΄βπ))) β β) |
248 | 45 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β (1 + πΈ) β β) |
249 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β π) β β β V) |
250 | 60 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π’ β π) β§ π β β) β π β Fin) |
251 | 64 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π’ β π) β§ π β β) β (πΆβπ):πβΆβ) |
252 | 158 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π’ β π) β§ π β β) β π’ β β) |
253 | 79 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π’ β π) β§ π β β) β (π·βπ):πβΆβ) |
254 | 74, 252, 250, 253 | hsphoif 44718 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π’ β π) β§ π β β) β ((π»βπ’)β(π·βπ)):πβΆβ) |
255 | 27, 250, 251, 254 | hoidmvcl 44724 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π’ β π) β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))) β (0[,)+β)) |
256 | 54, 255 | sselid 3940 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π’ β π) β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))) β (0[,]+β)) |
257 | 256 | fmpttd 7059 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β π) β (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ)))):ββΆ(0[,]+β)) |
258 | 249, 257 | sge0cl 44523 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) β (0[,]+β)) |
259 | 249, 257 | sge0xrcl 44527 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β π) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) β
β*) |
260 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β π) β +β β
β*) |
261 | 89 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β π) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β
β*) |
262 | | nfv 1917 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(π β§ π’ β π) |
263 | 92 | adantlr 713 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π’ β π) β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,]+β)) |
264 | 95 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π’ β π) β§ π β β) β π β (π β π)) |
265 | 27, 250, 264, 9, 252, 74, 251, 253 | hsphoidmvle 44728 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π’ β π) β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))) β€ ((πΆβπ)(πΏβπ)(π·βπ))) |
266 | 262, 249,
256, 263, 265 | sge0lempt 44552 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β π) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
267 | 98 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β π) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) < +β) |
268 | 259, 261,
260, 266, 267 | xrlelttrd 13033 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β π) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) < +β) |
269 | 259, 260,
268 | xrltned 43496 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) β +β) |
270 | | ge0xrre 43670 |
. . . . . . . . . . . . . . . 16
β’
(((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) β (0[,]+β) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) β +β) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) β β) |
271 | 258, 269,
270 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) β β) |
272 | 248, 271 | remulcld 11143 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π) β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ)))))) β β) |
273 | 126, 123 | sseldd 3943 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
274 | 27, 30, 94, 9, 61, 76, 88, 65, 273 | sge0hsphoire 44731 |
. . . . . . . . . . . . . . . 16
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) |
275 | 45, 274 | remulcld 11143 |
. . . . . . . . . . . . . . 15
β’ (π β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) β β) |
276 | 275 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π) β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) β β) |
277 | 14 | eleq2i 2829 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β π β π’ β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))}) |
278 | 277 | biimpi 215 |
. . . . . . . . . . . . . . . . 17
β’ (π’ β π β π’ β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))}) |
279 | | oveq1 7358 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = π’ β (π§ β (π΄βπ)) = (π’ β (π΄βπ))) |
280 | 279 | oveq2d 7367 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = π’ β (πΊ Β· (π§ β (π΄βπ))) = (πΊ Β· (π’ β (π΄βπ)))) |
281 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π§ = π’ β (π»βπ§) = (π»βπ’)) |
282 | 281 | fveq1d 6841 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ = π’ β ((π»βπ§)β(π·βπ)) = ((π»βπ’)β(π·βπ))) |
283 | 282 | oveq2d 7367 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ = π’ β ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))) = ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ)))) |
284 | 283 | mpteq2dv 5205 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ = π’ β (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) |
285 | 284 | fveq2d 6843 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = π’ β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ)))))) |
286 | 285 | oveq2d 7367 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = π’ β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) = ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))))) |
287 | 280, 286 | breq12d 5116 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = π’ β ((πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) β (πΊ Β· (π’ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ)))))))) |
288 | 287 | elrab 3643 |
. . . . . . . . . . . . . . . . 17
β’ (π’ β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β (π’ β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· (π’ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ)))))))) |
289 | 278, 288 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (π’ β π β (π’ β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· (π’ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ)))))))) |
290 | 289 | simprd 496 |
. . . . . . . . . . . . . . 15
β’ (π’ β π β (πΊ Β· (π’ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))))) |
291 | 290 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π) β (πΊ Β· (π’ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))))) |
292 | 274 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) |
293 | 51 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β 0 β€ (1 + πΈ)) |
294 | 273 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β π β β) |
295 | 74, 294, 60, 79 | hsphoif 44718 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β ((π»βπ)β(π·βπ)):πβΆβ) |
296 | 27, 60, 64, 295 | hoidmvcl 44724 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,)+β)) |
297 | 54, 296 | sselid 3940 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,]+β)) |
298 | 297 | adantlr 713 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π’ β π) β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,]+β)) |
299 | 294 | adantlr 713 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π’ β π) β§ π β β) β π β β) |
300 | 127 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β π) β π β β) |
301 | 121 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β π) β π β β
) |
302 | 131 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β π) β βπ¦ β β βπ§ β π π§ β€ π¦) |
303 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β π) β π’ β π) |
304 | | suprub 12074 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π β β
β§ βπ¦ β β βπ§ β π π§ β€ π¦) β§ π’ β π) β π’ β€ sup(π, β, < )) |
305 | 300, 301,
302, 303, 304 | syl31anc 1373 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β π) β π’ β€ sup(π, β, < )) |
306 | 305, 1 | breqtrrdi 5145 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β π) β π’ β€ π) |
307 | 306 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π’ β π) β§ π β β) β π’ β€ π) |
308 | 27, 250, 264, 9, 252, 299, 307, 74, 251, 253 | hsphoidmvle2 44727 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π’ β π) β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))) β€ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
309 | 262, 249,
256, 298, 308 | sge0lempt 44552 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ))))) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) |
310 | 271, 292,
248, 293, 309 | lemul2ad 12053 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π) β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ’)β(π·βπ)))))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
311 | 247, 272,
276, 291, 310 | letrd 11270 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β π) β (πΊ Β· (π’ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
312 | 311 | 3adant3 1132 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β π β§ π = (πΊ Β· (π’ β (π΄βπ)))) β (πΊ Β· (π’ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
313 | 245, 312 | eqbrtrd 5125 |
. . . . . . . . . . 11
β’ ((π β§ π’ β π β§ π = (πΊ Β· (π’ β (π΄βπ)))) β π β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
314 | 313 | 3exp 1119 |
. . . . . . . . . 10
β’ (π β (π’ β π β (π = (πΊ Β· (π’ β (π΄βπ))) β π β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))))) |
315 | 314 | rexlimdv 3148 |
. . . . . . . . 9
β’ (π β (βπ’ β π π = (πΊ Β· (π’ β (π΄βπ))) β π β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
316 | 315 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) β (βπ’ β π π = (πΊ Β· (π’ β (π΄βπ))) β π β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
317 | 244, 316 | mpd 15 |
. . . . . . 7
β’ ((π β§ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) β π β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
318 | 317 | ralrimiva 3141 |
. . . . . 6
β’ (π β βπ β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}π β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
319 | 224 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) β βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π = (πΊ Β· π‘)) |
320 | | nfv 1917 |
. . . . . . . . . . . 12
β’
β²π‘π |
321 | | nfcv 2905 |
. . . . . . . . . . . . 13
β’
β²π‘π |
322 | | nfre1 3266 |
. . . . . . . . . . . . . 14
β’
β²π‘βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘) |
323 | 322 | nfab 2911 |
. . . . . . . . . . . . 13
β’
β²π‘{π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} |
324 | 321, 323 | nfel 2919 |
. . . . . . . . . . . 12
β’
β²π‘ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} |
325 | 320, 324 | nfan 1902 |
. . . . . . . . . . 11
β’
β²π‘(π β§ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) |
326 | | nfv 1917 |
. . . . . . . . . . 11
β’
β²π‘ π β β |
327 | 230 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β βπ’ β π π‘ = (π’ β (π΄βπ))) |
328 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π’ β π β§ π‘ = (π’ β (π΄βπ))) β§ π = (πΊ Β· π‘)) β π = (πΊ Β· π‘)) |
329 | 246 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π’ β π β§ π‘ = (π’ β (π΄βπ))) β πΊ β β) |
330 | | simp3 1138 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π’ β π β§ π‘ = (π’ β (π΄βπ))) β π‘ = (π’ β (π΄βπ))) |
331 | 173 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π’ β π β§ π‘ = (π’ β (π΄βπ))) β (π’ β (π΄βπ)) β β) |
332 | 330, 331 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π’ β π β§ π‘ = (π’ β (π΄βπ))) β π‘ β β) |
333 | 329, 332 | remulcld 11143 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β π β§ π‘ = (π’ β (π΄βπ))) β (πΊ Β· π‘) β β) |
334 | 333 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π’ β π β§ π‘ = (π’ β (π΄βπ))) β§ π = (πΊ Β· π‘)) β (πΊ Β· π‘) β β) |
335 | 328, 334 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π’ β π β§ π‘ = (π’ β (π΄βπ))) β§ π = (πΊ Β· π‘)) β π β β) |
336 | 335 | ex 413 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β π β§ π‘ = (π’ β (π΄βπ))) β (π = (πΊ Β· π‘) β π β β)) |
337 | 336 | 3exp 1119 |
. . . . . . . . . . . . . . . 16
β’ (π β (π’ β π β (π‘ = (π’ β (π΄βπ)) β (π = (πΊ Β· π‘) β π β β)))) |
338 | 337 | rexlimdv 3148 |
. . . . . . . . . . . . . . 15
β’ (π β (βπ’ β π π‘ = (π’ β (π΄βπ)) β (π = (πΊ Β· π‘) β π β β))) |
339 | 338 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β (βπ’ β π π‘ = (π’ β (π΄βπ)) β (π = (πΊ Β· π‘) β π β β))) |
340 | 327, 339 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}) β (π = (πΊ Β· π‘) β π β β)) |
341 | 340 | ex 413 |
. . . . . . . . . . . 12
β’ (π β (π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β (π = (πΊ Β· π‘) β π β β))) |
342 | 341 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) β (π‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))} β (π = (πΊ Β· π‘) β π β β))) |
343 | 325, 326,
342 | rexlimd 3247 |
. . . . . . . . . 10
β’ ((π β§ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) β (βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π = (πΊ Β· π‘) β π β β)) |
344 | 319, 343 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) β π β β) |
345 | 344 | ralrimiva 3141 |
. . . . . . . 8
β’ (π β βπ β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}π β β) |
346 | | dfss3 3930 |
. . . . . . . 8
β’ ({π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β β β βπ β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}π β β) |
347 | 345, 346 | sylibr 233 |
. . . . . . 7
β’ (π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β β) |
348 | 40 | eqcomd 2743 |
. . . . . . . . . 10
β’ (π β 0 = (πΊ Β· 0)) |
349 | | oveq2 7359 |
. . . . . . . . . . 11
β’ (π‘ = 0 β (πΊ Β· π‘) = (πΊ Β· 0)) |
350 | 349 | rspceeqv 3593 |
. . . . . . . . . 10
β’ ((0
β {π€ β£
βπ’ β π π€ = (π’ β (π΄βπ))} β§ 0 = (πΊ Β· 0)) β βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}0 = (πΊ Β· π‘)) |
351 | 187, 348,
350 | syl2anc 584 |
. . . . . . . . 9
β’ (π β βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}0 = (πΊ Β· π‘)) |
352 | | eqeq1 2741 |
. . . . . . . . . 10
β’ (π£ = 0 β (π£ = (πΊ Β· π‘) β 0 = (πΊ Β· π‘))) |
353 | 352 | rexbidv 3173 |
. . . . . . . . 9
β’ (π£ = 0 β (βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘) β βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}0 = (πΊ Β· π‘))) |
354 | 46, 351, 353 | elabd 3631 |
. . . . . . . 8
β’ (π β 0 β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) |
355 | | ne0i 4292 |
. . . . . . . 8
β’ (0 β
{π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β β
) |
356 | 354, 355 | syl 17 |
. . . . . . 7
β’ (π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β β
) |
357 | 38, 190 | remulcld 11143 |
. . . . . . . 8
β’ (π β (πΊ Β· ((π΅βπ) β (π΄βπ))) β β) |
358 | 190 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β ((π΅βπ) β (π΄βπ)) β β) |
359 | 137 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β 0 β€ πΊ) |
360 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β π) β (π΅βπ) β β) |
361 | | iccleub 13273 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄βπ) β β* β§ (π΅βπ) β β* β§ π’ β ((π΄βπ)[,](π΅βπ))) β π’ β€ (π΅βπ)) |
362 | 152, 154,
155, 361 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β π) β π’ β€ (π΅βπ)) |
363 | 158, 360,
159, 362 | lesub1dd 11729 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β (π’ β (π΄βπ)) β€ ((π΅βπ) β (π΄βπ))) |
364 | 173, 358,
246, 359, 363 | lemul2ad 12053 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β (πΊ Β· (π’ β (π΄βπ))) β€ (πΊ Β· ((π΅βπ) β (π΄βπ)))) |
365 | 364 | 3adant3 1132 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π β§ π = (πΊ Β· (π’ β (π΄βπ)))) β (πΊ Β· (π’ β (π΄βπ))) β€ (πΊ Β· ((π΅βπ) β (π΄βπ)))) |
366 | 245, 365 | eqbrtrd 5125 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β π β§ π = (πΊ Β· (π’ β (π΄βπ)))) β π β€ (πΊ Β· ((π΅βπ) β (π΄βπ)))) |
367 | 366 | 3exp 1119 |
. . . . . . . . . . . 12
β’ (π β (π’ β π β (π = (πΊ Β· (π’ β (π΄βπ))) β π β€ (πΊ Β· ((π΅βπ) β (π΄βπ)))))) |
368 | 367 | rexlimdv 3148 |
. . . . . . . . . . 11
β’ (π β (βπ’ β π π = (πΊ Β· (π’ β (π΄βπ))) β π β€ (πΊ Β· ((π΅βπ) β (π΄βπ))))) |
369 | 368 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) β (βπ’ β π π = (πΊ Β· (π’ β (π΄βπ))) β π β€ (πΊ Β· ((π΅βπ) β (π΄βπ))))) |
370 | 244, 369 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}) β π β€ (πΊ Β· ((π΅βπ) β (π΄βπ)))) |
371 | 370 | ralrimiva 3141 |
. . . . . . . 8
β’ (π β βπ β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}π β€ (πΊ Β· ((π΅βπ) β (π΄βπ)))) |
372 | | brralrspcev 5163 |
. . . . . . . 8
β’ (((πΊ Β· ((π΅βπ) β (π΄βπ))) β β β§ βπ β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}π β€ (πΊ Β· ((π΅βπ) β (π΄βπ)))) β βπ¦ β β βπ β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}π β€ π¦) |
373 | 357, 371,
372 | syl2anc 584 |
. . . . . . 7
β’ (π β βπ¦ β β βπ β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}π β€ π¦) |
374 | | suprleub 12079 |
. . . . . . 7
β’ ((({π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β β β§ {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)} β β
β§ βπ¦ β β βπ β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}π β€ π¦) β§ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) β β) β (sup({π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}, β, < ) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) β βπ β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}π β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
375 | 347, 356,
373, 275, 374 | syl31anc 1373 |
. . . . . 6
β’ (π β (sup({π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}, β, < ) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) β βπ β {π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}π β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
376 | 318, 375 | mpbird 256 |
. . . . 5
β’ (π β sup({π£ β£ βπ‘ β {π€ β£ βπ’ β π π€ = (π’ β (π΄βπ))}π£ = (πΊ Β· π‘)}, β, < ) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
377 | 219, 376 | eqbrtrd 5125 |
. . . 4
β’ (π β (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
378 | 123, 377 | jca 512 |
. . 3
β’ (π β (π β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
379 | | oveq1 7358 |
. . . . . 6
β’ (π§ = π β (π§ β (π΄βπ)) = (π β (π΄βπ))) |
380 | 379 | oveq2d 7367 |
. . . . 5
β’ (π§ = π β (πΊ Β· (π§ β (π΄βπ))) = (πΊ Β· (π β (π΄βπ)))) |
381 | | fveq2 6839 |
. . . . . . . . . 10
β’ (π§ = π β (π»βπ§) = (π»βπ)) |
382 | 381 | fveq1d 6841 |
. . . . . . . . 9
β’ (π§ = π β ((π»βπ§)β(π·βπ)) = ((π»βπ)β(π·βπ))) |
383 | 382 | oveq2d 7367 |
. . . . . . . 8
β’ (π§ = π β ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))) = ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
384 | 383 | mpteq2dv 5205 |
. . . . . . 7
β’ (π§ = π β (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) |
385 | 384 | fveq2d 6843 |
. . . . . 6
β’ (π§ = π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) |
386 | 385 | oveq2d 7367 |
. . . . 5
β’ (π§ = π β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) = ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
387 | 380, 386 | breq12d 5116 |
. . . 4
β’ (π§ = π β ((πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) β (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
388 | 387 | elrab 3643 |
. . 3
β’ (π β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β (π β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
389 | 378, 388 | sylibr 233 |
. 2
β’ (π β π β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))}) |
390 | 389, 14 | eleqtrrdi 2849 |
1
β’ (π β π β π) |