Step | Hyp | Ref
| Expression |
1 | | 1nn 12171 |
. . . . 5
β’ 1 β
β |
2 | 1 | a1i 11 |
. . . 4
β’ ((π β§ π = β
) β 1 β
β) |
3 | | 0le0 12261 |
. . . . . 6
β’ 0 β€
0 |
4 | 3 | a1i 11 |
. . . . 5
β’ ((π β§ π = β
) β 0 β€
0) |
5 | | hoidmvlelem3.g |
. . . . . . . 8
β’ πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) |
6 | 5 | a1i 11 |
. . . . . . 7
β’ ((π β§ π = β
) β πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π))) |
7 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = β
β (πΏβπ) = (πΏββ
)) |
8 | | reseq2 5937 |
. . . . . . . . . 10
β’ (π = β
β (π΄ βΎ π) = (π΄ βΎ β
)) |
9 | | res0 5946 |
. . . . . . . . . . 11
β’ (π΄ βΎ β
) =
β
|
10 | 9 | a1i 11 |
. . . . . . . . . 10
β’ (π = β
β (π΄ βΎ β
) =
β
) |
11 | 8, 10 | eqtrd 2777 |
. . . . . . . . 9
β’ (π = β
β (π΄ βΎ π) = β
) |
12 | | reseq2 5937 |
. . . . . . . . . 10
β’ (π = β
β (π΅ βΎ π) = (π΅ βΎ β
)) |
13 | | res0 5946 |
. . . . . . . . . . 11
β’ (π΅ βΎ β
) =
β
|
14 | 13 | a1i 11 |
. . . . . . . . . 10
β’ (π = β
β (π΅ βΎ β
) =
β
) |
15 | 12, 14 | eqtrd 2777 |
. . . . . . . . 9
β’ (π = β
β (π΅ βΎ π) = β
) |
16 | 7, 11, 15 | oveq123d 7383 |
. . . . . . . 8
β’ (π = β
β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) = (β
(πΏββ
)β
)) |
17 | 16 | adantl 483 |
. . . . . . 7
β’ ((π β§ π = β
) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) = (β
(πΏββ
)β
)) |
18 | | hoidmvlelem3.l |
. . . . . . . 8
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
19 | | f0 6728 |
. . . . . . . . 9
β’
β
:β
βΆβ |
20 | 19 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π = β
) β
β
:β
βΆβ) |
21 | 18, 20, 20 | hoidmv0val 44898 |
. . . . . . 7
β’ ((π β§ π = β
) β (β
(πΏββ
)β
) =
0) |
22 | 6, 17, 21 | 3eqtrd 2781 |
. . . . . 6
β’ ((π β§ π = β
) β πΊ = 0) |
23 | | nfcvd 2909 |
. . . . . . . . . . 11
β’ (π β β²π(πβ1)) |
24 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²ππ |
25 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π = 1) β π = 1) |
26 | 25 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ π = 1) β (πβπ) = (πβ1)) |
27 | | 1red 11163 |
. . . . . . . . . . 11
β’ (π β 1 β
β) |
28 | | rge0ssre 13380 |
. . . . . . . . . . . . 13
β’
(0[,)+β) β β |
29 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π β π) |
30 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 1 β
β) |
31 | 1 | elexi 3467 |
. . . . . . . . . . . . . . 15
β’ 1 β
V |
32 | | eleq1 2826 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β (π β β β 1 β
β)) |
33 | 32 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β ((π β§ π β β) β (π β§ 1 β β))) |
34 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β (πβπ) = (πβ1)) |
35 | 34 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β ((πβπ) β (0[,)+β) β (πβ1) β
(0[,)+β))) |
36 | 33, 35 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β (((π β§ π β β) β (πβπ) β (0[,)+β)) β ((π β§ 1 β β) β
(πβ1) β
(0[,)+β)))) |
37 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β) |
38 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β ((π½βπ)(πΏβπ)(πΎβπ)) β V) |
39 | | hoidmvlelem3.p |
. . . . . . . . . . . . . . . . . . 19
β’ π = (π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ))) |
40 | 39 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ ((π½βπ)(πΏβπ)(πΎβπ)) β V) β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
41 | 37, 38, 40 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
42 | 41 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
43 | | hoidmvlelem3.x |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β Fin) |
44 | | hoidmvlelem3.w |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π = (π βͺ {π}) |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π = (π βͺ {π})) |
46 | | hoidmvlelem3.y |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β π) |
47 | | hoidmvlelem3.z |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β (π β π)) |
48 | 47 | eldifad 3927 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β π) |
49 | | snssi 4773 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β {π} β π) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β {π} β π) |
51 | 46, 50 | unssd 4151 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π βͺ {π}) β π) |
52 | 45, 51 | eqsstrd 3987 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β π) |
53 | 43, 52 | ssfid 9218 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β Fin) |
54 | | ssun1 4137 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π β (π βͺ {π}) |
55 | 44 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π βͺ {π}) = π |
56 | 54, 55 | sseqtri 3985 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β π |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β π) |
58 | 53, 57 | ssfid 9218 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β Fin) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β π β Fin) |
60 | | iftrue 4497 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = ((πΆβπ) βΎ π)) |
61 | 60 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = ((πΆβπ) βΎ π)) |
62 | | hoidmvlelem3.c |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β πΆ:ββΆ(β βm
π)) |
63 | 62 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β β) β (πΆβπ) β (β βm π)) |
64 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΆβπ) β (β βm π) β (πΆβπ):πβΆβ) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
66 | 54, 44 | sseqtrri 3986 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ π β π |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β π β π) |
68 | 65, 67 | fssresd 6714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β ((πΆβπ) βΎ π):πβΆβ) |
69 | | reex 11149 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ β
β V |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β β β
V) |
71 | 53, 57 | ssexd 5286 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β V) |
72 | 71 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β π β V) |
73 | 70, 72 | elmapd 8786 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β (((πΆβπ) βΎ π) β (β βm π) β ((πΆβπ) βΎ π):πβΆβ)) |
74 | 68, 73 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β ((πΆβπ) βΎ π) β (β βm π)) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((πΆβπ) βΎ π) β (β βm π)) |
76 | 61, 75 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β (β βm π)) |
77 | | iffalse 4500 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = πΉ) |
78 | 77 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = πΉ) |
79 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π¦ β π) β 0 β β) |
80 | | hoidmvlelem3.f |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ πΉ = (π¦ β π β¦ 0) |
81 | 79, 80 | fmptd 7067 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΉ:πβΆβ) |
82 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β
V) |
83 | 82, 58 | elmapd 8786 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (πΉ β (β βm π) β πΉ:πβΆβ)) |
84 | 81, 83 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΉ β (β βm π)) |
85 | 84 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β πΉ β (β βm π)) |
86 | 78, 85 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β (β βm π)) |
87 | 76, 86 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β (β βm π)) |
88 | | hoidmvlelem3.j |
. . . . . . . . . . . . . . . . . . . 20
β’ π½ = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
89 | 87, 88 | fmptd 7067 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π½:ββΆ(β βm
π)) |
90 | 89 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π½βπ) β (β βm π)) |
91 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½βπ) β (β βm π) β (π½βπ):πβΆβ) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (π½βπ):πβΆβ) |
93 | | iftrue 4497 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = ((π·βπ) βΎ π)) |
94 | 93 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = ((π·βπ) βΎ π)) |
95 | | hoidmvlelem3.d |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π·:ββΆ(β βm
π)) |
96 | 95 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β β) β (π·βπ) β (β βm π)) |
97 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π·βπ) β (β βm π) β (π·βπ):πβΆβ) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β (π·βπ):πβΆβ) |
99 | 98, 67 | fssresd 6714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β ((π·βπ) βΎ π):πβΆβ) |
100 | 70, 72 | elmapd 8786 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β (((π·βπ) βΎ π) β (β βm π) β ((π·βπ) βΎ π):πβΆβ)) |
101 | 99, 100 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β ((π·βπ) βΎ π) β (β βm π)) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((π·βπ) βΎ π) β (β βm π)) |
103 | 94, 102 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) β (β βm π)) |
104 | | iffalse 4500 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = πΉ) |
105 | 104 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = πΉ) |
106 | 105, 85 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) β (β βm π)) |
107 | 103, 106 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) β (β βm π)) |
108 | | hoidmvlelem3.k |
. . . . . . . . . . . . . . . . . . . 20
β’ πΎ = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
109 | 107, 108 | fmptd 7067 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΎ:ββΆ(β βm
π)) |
110 | 109 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (πΎβπ) β (β βm π)) |
111 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎβπ) β (β βm π) β (πΎβπ):πβΆβ) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (πΎβπ):πβΆβ) |
113 | 18, 59, 92, 112 | hoidmvcl 44897 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((π½βπ)(πΏβπ)(πΎβπ)) β (0[,)+β)) |
114 | 42, 113 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πβπ) β (0[,)+β)) |
115 | 31, 36, 114 | vtocl 3521 |
. . . . . . . . . . . . . 14
β’ ((π β§ 1 β β) β
(πβ1) β
(0[,)+β)) |
116 | 29, 30, 115 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (πβ1) β
(0[,)+β)) |
117 | 28, 116 | sselid 3947 |
. . . . . . . . . . . 12
β’ (π β (πβ1) β β) |
118 | 117 | recnd 11190 |
. . . . . . . . . . 11
β’ (π β (πβ1) β β) |
119 | 23, 24, 26, 27, 118 | sumsnd 43305 |
. . . . . . . . . 10
β’ (π β Ξ£π β {1} (πβπ) = (πβ1)) |
120 | 119 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π = β
) β Ξ£π β {1} (πβπ) = (πβ1)) |
121 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = 1 β (π½βπ) = (π½β1)) |
122 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = 1 β (πΎβπ) = (πΎβ1)) |
123 | 121, 122 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π = 1 β ((π½βπ)(πΏβπ)(πΎβπ)) = ((π½β1)(πΏβπ)(πΎβ1))) |
124 | | ovex 7395 |
. . . . . . . . . . . 12
β’ ((π½β1)(πΏβπ)(πΎβ1)) β V |
125 | 123, 39, 124 | fvmpt 6953 |
. . . . . . . . . . 11
β’ (1 β
β β (πβ1)
= ((π½β1)(πΏβπ)(πΎβ1))) |
126 | 1, 125 | ax-mp 5 |
. . . . . . . . . 10
β’ (πβ1) = ((π½β1)(πΏβπ)(πΎβ1)) |
127 | 126 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π = β
) β (πβ1) = ((π½β1)(πΏβπ)(πΎβ1))) |
128 | 7 | oveqd 7379 |
. . . . . . . . . . 11
β’ (π = β
β ((π½β1)(πΏβπ)(πΎβ1)) = ((π½β1)(πΏββ
)(πΎβ1))) |
129 | 128 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π = β
) β ((π½β1)(πΏβπ)(πΎβ1)) = ((π½β1)(πΏββ
)(πΎβ1))) |
130 | 121 | feq1d 6658 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β ((π½βπ):πβΆβ β (π½β1):πβΆβ)) |
131 | 33, 130 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β (((π β§ π β β) β (π½βπ):πβΆβ) β ((π β§ 1 β β) β (π½β1):πβΆβ))) |
132 | 68 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((πΆβπ) βΎ π):πβΆβ) |
133 | 61 | feq1d 6658 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ β ((πΆβπ) βΎ π):πβΆβ)) |
134 | 132, 133 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ) |
135 | 81 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β πΉ:πβΆβ) |
136 | 78 | feq1d 6658 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ β πΉ:πβΆβ)) |
137 | 135, 136 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ) |
138 | 134, 137 | pm2.61dan 812 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ) |
139 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π β β) |
140 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΆβπ) β V |
141 | 140 | resex 5990 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΆβπ) βΎ π) β V |
142 | 61, 141 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β V) |
143 | 84 | elexd 3468 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΉ β V) |
144 | 143 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β πΉ β V) |
145 | 144 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β πΉ β V) |
146 | 78, 145 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β V) |
147 | 142, 146 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β V) |
148 | 88 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β V) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
149 | 139, 147,
148 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
150 | 149 | feq1d 6658 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((π½βπ):πβΆβ β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ)) |
151 | 138, 150 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π½βπ):πβΆβ) |
152 | 31, 131, 151 | vtocl 3521 |
. . . . . . . . . . . . . 14
β’ ((π β§ 1 β β) β
(π½β1):πβΆβ) |
153 | 29, 30, 152 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (π½β1):πβΆβ) |
154 | 153 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π = β
) β (π½β1):πβΆβ) |
155 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π = β
β π = β
) |
156 | 155 | eqcomd 2743 |
. . . . . . . . . . . . . 14
β’ (π = β
β β
=
π) |
157 | 156 | feq2d 6659 |
. . . . . . . . . . . . 13
β’ (π = β
β ((π½β1):β
βΆβ
β (π½β1):πβΆβ)) |
158 | 157 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π = β
) β ((π½β1):β
βΆβ β
(π½β1):πβΆβ)) |
159 | 154, 158 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β§ π = β
) β (π½β1):β
βΆβ) |
160 | 122 | feq1d 6658 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β ((πΎβπ):πβΆβ β (πΎβ1):πβΆβ)) |
161 | 33, 160 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β (((π β§ π β β) β (πΎβπ):πβΆβ) β ((π β§ 1 β β) β (πΎβ1):πβΆβ))) |
162 | 31, 161, 112 | vtocl 3521 |
. . . . . . . . . . . . . 14
β’ ((π β§ 1 β β) β
(πΎβ1):πβΆβ) |
163 | 29, 30, 162 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (πΎβ1):πβΆβ) |
164 | 163 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π = β
) β (πΎβ1):πβΆβ) |
165 | 156 | feq2d 6659 |
. . . . . . . . . . . . 13
β’ (π = β
β ((πΎβ1):β
βΆβ
β (πΎβ1):πβΆβ)) |
166 | 165 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π = β
) β ((πΎβ1):β
βΆβ β
(πΎβ1):πβΆβ)) |
167 | 164, 166 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β§ π = β
) β (πΎβ1):β
βΆβ) |
168 | 18, 159, 167 | hoidmv0val 44898 |
. . . . . . . . . 10
β’ ((π β§ π = β
) β ((π½β1)(πΏββ
)(πΎβ1)) = 0) |
169 | 129, 168 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π = β
) β ((π½β1)(πΏβπ)(πΎβ1)) = 0) |
170 | 120, 127,
169 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((π β§ π = β
) β Ξ£π β {1} (πβπ) = 0) |
171 | 170 | oveq2d 7378 |
. . . . . . 7
β’ ((π β§ π = β
) β ((1 + πΈ) Β· Ξ£π β {1} (πβπ)) = ((1 + πΈ) Β· 0)) |
172 | | hoidmvlelem3.e |
. . . . . . . . . . . 12
β’ (π β πΈ β
β+) |
173 | 172 | rpred 12964 |
. . . . . . . . . . 11
β’ (π β πΈ β β) |
174 | 27, 173 | readdcld 11191 |
. . . . . . . . . 10
β’ (π β (1 + πΈ) β β) |
175 | 174 | recnd 11190 |
. . . . . . . . 9
β’ (π β (1 + πΈ) β β) |
176 | 175 | mul01d 11361 |
. . . . . . . 8
β’ (π β ((1 + πΈ) Β· 0) = 0) |
177 | 176 | adantr 482 |
. . . . . . 7
β’ ((π β§ π = β
) β ((1 + πΈ) Β· 0) = 0) |
178 | | eqidd 2738 |
. . . . . . 7
β’ ((π β§ π = β
) β 0 = 0) |
179 | 171, 177,
178 | 3eqtrd 2781 |
. . . . . 6
β’ ((π β§ π = β
) β ((1 + πΈ) Β· Ξ£π β {1} (πβπ)) = 0) |
180 | 22, 179 | breq12d 5123 |
. . . . 5
β’ ((π β§ π = β
) β (πΊ β€ ((1 + πΈ) Β· Ξ£π β {1} (πβπ)) β 0 β€ 0)) |
181 | 4, 180 | mpbird 257 |
. . . 4
β’ ((π β§ π = β
) β πΊ β€ ((1 + πΈ) Β· Ξ£π β {1} (πβπ))) |
182 | | oveq2 7370 |
. . . . . . . . 9
β’ (π = 1 β (1...π) = (1...1)) |
183 | 1 | nnzi 12534 |
. . . . . . . . . . 11
β’ 1 β
β€ |
184 | | fzsn 13490 |
. . . . . . . . . . 11
β’ (1 β
β€ β (1...1) = {1}) |
185 | 183, 184 | ax-mp 5 |
. . . . . . . . . 10
β’ (1...1) =
{1} |
186 | 185 | a1i 11 |
. . . . . . . . 9
β’ (π = 1 β (1...1) =
{1}) |
187 | 182, 186 | eqtrd 2777 |
. . . . . . . 8
β’ (π = 1 β (1...π) = {1}) |
188 | 187 | sumeq1d 15593 |
. . . . . . 7
β’ (π = 1 β Ξ£π β (1...π)(πβπ) = Ξ£π β {1} (πβπ)) |
189 | 188 | oveq2d 7378 |
. . . . . 6
β’ (π = 1 β ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) = ((1 + πΈ) Β· Ξ£π β {1} (πβπ))) |
190 | 189 | breq2d 5122 |
. . . . 5
β’ (π = 1 β (πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) β πΊ β€ ((1 + πΈ) Β· Ξ£π β {1} (πβπ)))) |
191 | 190 | rspcev 3584 |
. . . 4
β’ ((1
β β β§ πΊ β€
((1 + πΈ) Β·
Ξ£π β {1} (πβπ))) β βπ β β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
192 | 2, 181, 191 | syl2anc 585 |
. . 3
β’ ((π β§ π = β
) β βπ β β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
193 | | simpl 484 |
. . . 4
β’ ((π β§ Β¬ π = β
) β π) |
194 | | neqne 2952 |
. . . . 5
β’ (Β¬
π = β
β π β β
) |
195 | 194 | adantl 483 |
. . . 4
β’ ((π β§ Β¬ π = β
) β π β β
) |
196 | | nfv 1918 |
. . . . . 6
β’
β²π(π β§ π β β
) |
197 | 183 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β
) β 1 β
β€) |
198 | | nnuz 12813 |
. . . . . 6
β’ β =
(β€β₯β1) |
199 | 114 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β β) β (πβπ) β (0[,)+β)) |
200 | | hoidmvlelem3.a |
. . . . . . . . . . . 12
β’ (π β π΄:πβΆβ) |
201 | 66 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β π β π) |
202 | 200, 201 | fssresd 6714 |
. . . . . . . . . . 11
β’ (π β (π΄ βΎ π):πβΆβ) |
203 | | hoidmvlelem3.b |
. . . . . . . . . . . 12
β’ (π β π΅:πβΆβ) |
204 | 203, 201 | fssresd 6714 |
. . . . . . . . . . 11
β’ (π β (π΅ βΎ π):πβΆβ) |
205 | 18, 58, 202, 204 | hoidmvcl 44897 |
. . . . . . . . . 10
β’ (π β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β (0[,)+β)) |
206 | 28, 205 | sselid 3947 |
. . . . . . . . 9
β’ (π β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β β) |
207 | 5, 206 | eqeltrid 2842 |
. . . . . . . 8
β’ (π β πΊ β β) |
208 | | 0red 11165 |
. . . . . . . . 9
β’ (π β 0 β
β) |
209 | | 1rp 12926 |
. . . . . . . . . . . . 13
β’ 1 β
β+ |
210 | 209 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 1 β
β+) |
211 | 210, 172 | jca 513 |
. . . . . . . . . . 11
β’ (π β (1 β
β+ β§ πΈ
β β+)) |
212 | | rpaddcl 12944 |
. . . . . . . . . . 11
β’ ((1
β β+ β§ πΈ β β+) β (1 +
πΈ) β
β+) |
213 | 211, 212 | syl 17 |
. . . . . . . . . 10
β’ (π β (1 + πΈ) β
β+) |
214 | | rpgt0 12934 |
. . . . . . . . . 10
β’ ((1 +
πΈ) β
β+ β 0 < (1 + πΈ)) |
215 | 213, 214 | syl 17 |
. . . . . . . . 9
β’ (π β 0 < (1 + πΈ)) |
216 | 208, 215 | gtned 11297 |
. . . . . . . 8
β’ (π β (1 + πΈ) β 0) |
217 | 207, 174,
216 | redivcld 11990 |
. . . . . . 7
β’ (π β (πΊ / (1 + πΈ)) β β) |
218 | 217 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β
) β (πΊ / (1 + πΈ)) β β) |
219 | 217 | ltpnfd 13049 |
. . . . . . . . . 10
β’ (π β (πΊ / (1 + πΈ)) < +β) |
220 | 219 | adantr 482 |
. . . . . . . . 9
β’ ((π β§
(Ξ£^β(π β β β¦ (πβπ))) = +β) β (πΊ / (1 + πΈ)) < +β) |
221 | | id 22 |
. . . . . . . . . . 11
β’
((Ξ£^β(π β β β¦ (πβπ))) = +β β
(Ξ£^β(π β β β¦ (πβπ))) = +β) |
222 | 221 | eqcomd 2743 |
. . . . . . . . . 10
β’
((Ξ£^β(π β β β¦ (πβπ))) = +β β +β =
(Ξ£^β(π β β β¦ (πβπ)))) |
223 | 222 | adantl 483 |
. . . . . . . . 9
β’ ((π β§
(Ξ£^β(π β β β¦ (πβπ))) = +β) β +β =
(Ξ£^β(π β β β¦ (πβπ)))) |
224 | 220, 223 | breqtrd 5136 |
. . . . . . . 8
β’ ((π β§
(Ξ£^β(π β β β¦ (πβπ))) = +β) β (πΊ / (1 + πΈ)) <
(Ξ£^β(π β β β¦ (πβπ)))) |
225 | 224 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β β
) β§
(Ξ£^β(π β β β¦ (πβπ))) = +β) β (πΊ / (1 + πΈ)) <
(Ξ£^β(π β β β¦ (πβπ)))) |
226 | | simpl 484 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ Β¬
(Ξ£^β(π β β β¦ (πβπ))) = +β) β (π β§ π β β
)) |
227 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ Β¬
(Ξ£^β(π β β β¦ (πβπ))) = +β) β Β¬
(Ξ£^β(π β β β¦ (πβπ))) = +β) |
228 | | nnex 12166 |
. . . . . . . . . . . 12
β’ β
β V |
229 | 228 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ Β¬
(Ξ£^β(π β β β¦ (πβπ))) = +β) β β β
V) |
230 | | icossicc 13360 |
. . . . . . . . . . . . . 14
β’
(0[,)+β) β (0[,]+β) |
231 | 230, 114 | sselid 3947 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πβπ) β (0[,]+β)) |
232 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π β β β¦ (πβπ)) = (π β β β¦ (πβπ)) |
233 | 231, 232 | fmptd 7067 |
. . . . . . . . . . . 12
β’ (π β (π β β β¦ (πβπ)):ββΆ(0[,]+β)) |
234 | 233 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ Β¬
(Ξ£^β(π β β β¦ (πβπ))) = +β) β (π β β β¦ (πβπ)):ββΆ(0[,]+β)) |
235 | 229, 234 | sge0repnf 44701 |
. . . . . . . . . 10
β’ ((π β§ Β¬
(Ξ£^β(π β β β¦ (πβπ))) = +β) β
((Ξ£^β(π β β β¦ (πβπ))) β β β Β¬
(Ξ£^β(π β β β¦ (πβπ))) = +β)) |
236 | 227, 235 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ Β¬
(Ξ£^β(π β β β¦ (πβπ))) = +β) β
(Ξ£^β(π β β β¦ (πβπ))) β β) |
237 | 236 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ Β¬
(Ξ£^β(π β β β¦ (πβπ))) = +β) β
(Ξ£^β(π β β β¦ (πβπ))) β β) |
238 | 218 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§
(Ξ£^β(π β β β¦ (πβπ))) β β) β (πΊ / (1 + πΈ)) β β) |
239 | 207 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§
(Ξ£^β(π β β β¦ (πβπ))) β β) β πΊ β β) |
240 | 239 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§
(Ξ£^β(π β β β¦ (πβπ))) β β) β πΊ β β) |
241 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§
(Ξ£^β(π β β β¦ (πβπ))) β β) β
(Ξ£^β(π β β β¦ (πβπ))) β β) |
242 | 27, 172 | ltaddrpd 12997 |
. . . . . . . . . . . 12
β’ (π β 1 < (1 + πΈ)) |
243 | 242 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β
) β 1 < (1 + πΈ)) |
244 | 58 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β
) β π β Fin) |
245 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β
) β π β β
) |
246 | 202 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β
) β (π΄ βΎ π):πβΆβ) |
247 | 204 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β
) β (π΅ βΎ π):πβΆβ) |
248 | 18, 244, 245, 246, 247 | hoidmvn0val 44899 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β
) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) = βπ β π (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ)))) |
249 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β
) β πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π))) |
250 | | fvres 6866 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β ((π΄ βΎ π)βπ) = (π΄βπ)) |
251 | | fvres 6866 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β ((π΅ βΎ π)βπ) = (π΅βπ)) |
252 | 250, 251 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β (((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ)) = ((π΄βπ)[,)(π΅βπ))) |
253 | 252 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
254 | 253 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
255 | 200 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β π΄:πβΆβ) |
256 | | elun1 4141 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β π β (π βͺ {π})) |
257 | 256, 44 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β π β π) |
258 | 257 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β π β π) |
259 | 255, 258 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β (π΄βπ) β β) |
260 | 203 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β π΅:πβΆβ) |
261 | 260, 258 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β (π΅βπ) β β) |
262 | | volico 44298 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) = if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0)) |
263 | 259, 261,
262 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) = if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0)) |
264 | | hoidmvlelem3.lt |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β (π΄βπ) < (π΅βπ)) |
265 | 258, 264 | syldan 592 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β (π΄βπ) < (π΅βπ)) |
266 | 265 | iftrued 4499 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0) = ((π΅βπ) β (π΄βπ))) |
267 | 254, 263,
266 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ))) = ((π΅βπ) β (π΄βπ))) |
268 | 267 | prodeq2dv 15813 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β π (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ))) = βπ β π ((π΅βπ) β (π΄βπ))) |
269 | 268 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β π ((π΅βπ) β (π΄βπ)) = βπ β π (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ)))) |
270 | 269 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β
) β βπ β π ((π΅βπ) β (π΄βπ)) = βπ β π (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ)))) |
271 | 248, 249,
270 | 3eqtr4d 2787 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β
) β πΊ = βπ β π ((π΅βπ) β (π΄βπ))) |
272 | | difrp 12960 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β ((π΄βπ) < (π΅βπ) β ((π΅βπ) β (π΄βπ)) β
β+)) |
273 | 259, 261,
272 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β ((π΄βπ) < (π΅βπ) β ((π΅βπ) β (π΄βπ)) β
β+)) |
274 | 265, 273 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ((π΅βπ) β (π΄βπ)) β
β+) |
275 | 58, 274 | fprodrpcl 15846 |
. . . . . . . . . . . . . 14
β’ (π β βπ β π ((π΅βπ) β (π΄βπ)) β
β+) |
276 | 275 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β
) β βπ β π ((π΅βπ) β (π΄βπ)) β
β+) |
277 | 271, 276 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ ((π β§ π β β
) β πΊ β
β+) |
278 | 213 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β
) β (1 + πΈ) β
β+) |
279 | 277, 278 | ltdivgt1 43664 |
. . . . . . . . . . 11
β’ ((π β§ π β β
) β (1 < (1 + πΈ) β (πΊ / (1 + πΈ)) < πΊ)) |
280 | 243, 279 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π β β
) β (πΊ / (1 + πΈ)) < πΊ) |
281 | 280 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§
(Ξ£^β(π β β β¦ (πβπ))) β β) β (πΊ / (1 + πΈ)) < πΊ) |
282 | | hoidmvlelem3.i2 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
283 | 282 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
284 | | fvexd 6862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (π₯βπ) β V) |
285 | | hoidmvlelem3.s |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β π) |
286 | 285 | elexd 3468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π β V) |
287 | 284, 286 | ifcld 4537 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β if(π β π, (π₯βπ), π) β V) |
288 | 287 | ralrimivw 3148 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β βπ β π if(π β π, (π₯βπ), π) β V) |
289 | 288 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β βπ β π if(π β π, (π₯βπ), π) β V) |
290 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β¦ if(π β π, (π₯βπ), π)) = (π β π β¦ if(π β π, (π₯βπ), π)) |
291 | 290 | fnmpt 6646 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ β
π if(π β π, (π₯βπ), π) β V β (π β π β¦ if(π β π, (π₯βπ), π)) Fn π) |
292 | 289, 291 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β (π β π β¦ if(π β π, (π₯βπ), π)) Fn π) |
293 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) |
294 | | mptexg 7176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β Fin β (π β π β¦ if(π β π, (π₯βπ), π)) β V) |
295 | 53, 294 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π β π β¦ if(π β π, (π₯βπ), π)) β V) |
296 | 295 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β (π β π β¦ if(π β π, (π₯βπ), π)) β V) |
297 | | hoidmvlelem3.o |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ π = (π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ)) β¦ (π β π β¦ if(π β π, (π₯βπ), π))) |
298 | 297 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β§ (π β π β¦ if(π β π, (π₯βπ), π)) β V) β (πβπ₯) = (π β π β¦ if(π β π, (π₯βπ), π))) |
299 | 293, 296,
298 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β (πβπ₯) = (π β π β¦ if(π β π, (π₯βπ), π))) |
300 | 299 | fneq1d 6600 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β ((πβπ₯) Fn π β (π β π β¦ if(π β π, (π₯βπ), π)) Fn π)) |
301 | 292, 300 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β (πβπ₯) Fn π) |
302 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²ππ |
303 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²ππ₯ |
304 | | nfixp1 8863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²πXπ β
π ((π΄βπ)[,)(π΅βπ)) |
305 | 303, 304 | nfel 2922 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ)) |
306 | 302, 305 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) |
307 | 299 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β ((πβπ₯)βπ) = ((π β π β¦ if(π β π, (π₯βπ), π))βπ)) |
308 | 307 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β ((πβπ₯)βπ) = ((π β π β¦ if(π β π, (π₯βπ), π))βπ)) |
309 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β π) β π β π) |
310 | 287 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β π) β if(π β π, (π₯βπ), π) β V) |
311 | 290 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β π β§ if(π β π, (π₯βπ), π) β V) β ((π β π β¦ if(π β π, (π₯βπ), π))βπ) = if(π β π, (π₯βπ), π)) |
312 | 309, 310,
311 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β π) β ((π β π β¦ if(π β π, (π₯βπ), π))βπ) = if(π β π, (π₯βπ), π)) |
313 | 312 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β ((π β π β¦ if(π β π, (π₯βπ), π))βπ) = if(π β π, (π₯βπ), π)) |
314 | 308, 313 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β ((πβπ₯)βπ) = if(π β π, (π₯βπ), π)) |
315 | | iftrue 4497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β if(π β π, (π₯βπ), π) = (π₯βπ)) |
316 | 315 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β§ π β π) β if(π β π, (π₯βπ), π) = (π₯βπ)) |
317 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ π₯ β V |
318 | 317 | elixp 8849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β (π₯ Fn π β§ βπ β π (π₯βπ) β ((π΄βπ)[,)(π΅βπ)))) |
319 | 318 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βπ β π (π₯βπ) β ((π΄βπ)[,)(π΅βπ))) |
320 | 319 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β βπ β π (π₯βπ) β ((π΄βπ)[,)(π΅βπ))) |
321 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β π β π) |
322 | | rspa 3234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((βπ β
π (π₯βπ) β ((π΄βπ)[,)(π΅βπ)) β§ π β π) β (π₯βπ) β ((π΄βπ)[,)(π΅βπ))) |
323 | 320, 321,
322 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β (π₯βπ) β ((π΄βπ)[,)(π΅βπ))) |
324 | 323 | ad4ant24 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β§ π β π) β (π₯βπ) β ((π΄βπ)[,)(π΅βπ))) |
325 | 316, 324 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β§ π β π) β if(π β π, (π₯βπ), π) β ((π΄βπ)[,)(π΅βπ))) |
326 | | snidg 4625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β (π β π) β π β {π}) |
327 | 47, 326 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β π β {π}) |
328 | | elun2 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β {π} β π β (π βͺ {π})) |
329 | 327, 328 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β π β (π βͺ {π})) |
330 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β (π βͺ {π}) = π) |
331 | 329, 330 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β π β π) |
332 | 200, 331 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (π΄βπ) β β) |
333 | 332 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (π΄βπ) β
β*) |
334 | 203, 331 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (π΅βπ) β β) |
335 | 334 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (π΅βπ) β
β*) |
336 | | iccssxr 13354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π΄βπ)[,](π΅βπ)) β
β* |
337 | | hoidmvlelem3.u |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ π = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} |
338 | | ssrab2 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β ((π΄βπ)[,](π΅βπ)) |
339 | 337, 338 | eqsstri 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ π β ((π΄βπ)[,](π΅βπ)) |
340 | 339, 285 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β π β ((π΄βπ)[,](π΅βπ))) |
341 | 336, 340 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β π β
β*) |
342 | | iccgelb 13327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π΄βπ) β β* β§ (π΅βπ) β β* β§ π β ((π΄βπ)[,](π΅βπ))) β (π΄βπ) β€ π) |
343 | 333, 335,
340, 342 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (π΄βπ) β€ π) |
344 | | hoidmvlelem3.sb |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β π < (π΅βπ)) |
345 | 333, 335,
341, 343, 344 | elicod 13321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β ((π΄βπ)[,)(π΅βπ))) |
346 | 345 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β π) β§ Β¬ π β π) β π β ((π΄βπ)[,)(π΅βπ))) |
347 | | iffalse 4500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (Β¬
π β π β if(π β π, (π₯βπ), π) = π) |
348 | 347 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β π) β§ Β¬ π β π) β if(π β π, (π₯βπ), π) = π) |
349 | 44 | eleq2i 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β π β π β (π βͺ {π})) |
350 | 349 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β π β π β (π βͺ {π})) |
351 | 350 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β π β§ Β¬ π β π) β π β (π βͺ {π})) |
352 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β π β§ Β¬ π β π) β Β¬ π β π) |
353 | | elunnel1 4114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β (π βͺ {π}) β§ Β¬ π β π) β π β {π}) |
354 | 351, 352,
353 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β π β§ Β¬ π β π) β π β {π}) |
355 | | elsni 4608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β {π} β π = π) |
356 | 354, 355 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β π β§ Β¬ π β π) β π = π) |
357 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = π β (π΄βπ) = (π΄βπ)) |
358 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = π β (π΅βπ) = (π΅βπ)) |
359 | 357, 358 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π β ((π΄βπ)[,)(π΅βπ)) = ((π΄βπ)[,)(π΅βπ))) |
360 | 356, 359 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β π β§ Β¬ π β π) β ((π΄βπ)[,)(π΅βπ)) = ((π΄βπ)[,)(π΅βπ))) |
361 | 360 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β π) β§ Β¬ π β π) β ((π΄βπ)[,)(π΅βπ)) = ((π΄βπ)[,)(π΅βπ))) |
362 | 348, 361 | eleq12d 2832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β π) β§ Β¬ π β π) β (if(π β π, (π₯βπ), π) β ((π΄βπ)[,)(π΅βπ)) β π β ((π΄βπ)[,)(π΅βπ)))) |
363 | 346, 362 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β π) β§ Β¬ π β π) β if(π β π, (π₯βπ), π) β ((π΄βπ)[,)(π΅βπ))) |
364 | 363 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β§ Β¬ π β π) β if(π β π, (π₯βπ), π) β ((π΄βπ)[,)(π΅βπ))) |
365 | 325, 364 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β if(π β π, (π₯βπ), π) β ((π΄βπ)[,)(π΅βπ))) |
366 | 314, 365 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β ((πβπ₯)βπ) β ((π΄βπ)[,)(π΅βπ))) |
367 | 366 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β (π β π β ((πβπ₯)βπ) β ((π΄βπ)[,)(π΅βπ)))) |
368 | 306, 367 | ralrimi 3243 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β βπ β π ((πβπ₯)βπ) β ((π΄βπ)[,)(π΅βπ))) |
369 | 301, 368 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β ((πβπ₯) Fn π β§ βπ β π ((πβπ₯)βπ) β ((π΄βπ)[,)(π΅βπ)))) |
370 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πβπ₯) β V |
371 | 370 | elixp 8849 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβπ₯) β Xπ β π ((π΄βπ)[,)(π΅βπ)) β ((πβπ₯) Fn π β§ βπ β π ((πβπ₯)βπ) β ((π΄βπ)[,)(π΅βπ)))) |
372 | 369, 371 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β (πβπ₯) β Xπ β π ((π΄βπ)[,)(π΅βπ))) |
373 | 283, 372 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β (πβπ₯) β βͺ
π β β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
374 | | eliun 4963 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ₯) β βͺ
π β β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β βπ β β (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
375 | 373, 374 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β βπ β β (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
376 | | ixpfn 8848 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β π₯ Fn π) |
377 | 376 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β π₯ Fn π) |
378 | 377 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π₯ Fn π) |
379 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π π β β |
380 | 306, 379 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) |
381 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π(πβπ₯) |
382 | | nfixp1 8863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²πXπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) |
383 | 381, 382 | nfel 2922 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) |
384 | 380, 383 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
385 | 307 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β ((πβπ₯)βπ) = ((π β π β¦ if(π β π, (π₯βπ), π))βπ)) |
386 | 287 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β π) β if(π β π, (π₯βπ), π) β V) |
387 | 258, 386,
311 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π β π) β ((π β π β¦ if(π β π, (π₯βπ), π))βπ) = if(π β π, (π₯βπ), π)) |
388 | 387 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β ((π β π β¦ if(π β π, (π₯βπ), π))βπ) = if(π β π, (π₯βπ), π)) |
389 | 315 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β if(π β π, (π₯βπ), π) = (π₯βπ)) |
390 | 385, 388,
389 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β (π₯βπ) = ((πβπ₯)βπ)) |
391 | 390 | ad5ant125 1367 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (π₯βπ) = ((πβπ₯)βπ)) |
392 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β§ π β π) β (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
393 | 370 | elixp 8849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β ((πβπ₯) Fn π β§ βπ β π ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
394 | 392, 393 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β§ π β π) β ((πβπ₯) Fn π β§ βπ β π ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
395 | 394 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β§ π β π) β βπ β π ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
396 | 257 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β§ π β π) β π β π) |
397 | | rspa 3234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((βπ β
π ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β§ π β π) β ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
398 | 395, 396,
397 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β§ π β π) β ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
399 | 398 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
400 | 391, 399 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (π₯βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
401 | 29 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π) |
402 | 37 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π β β) |
403 | 299 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β ((πβπ₯)βπ) = ((π β π β¦ if(π β π, (π₯βπ), π))βπ)) |
404 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β (π β π β¦ if(π β π, (π₯βπ), π)) = (π β π β¦ if(π β π, (π₯βπ), π))) |
405 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π = π β (π β π β π β π)) |
406 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π = π β (π₯βπ) = (π₯βπ)) |
407 | 405, 406 | ifbieq1d 4515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π = π β if(π β π, (π₯βπ), π) = if(π β π, (π₯βπ), π)) |
408 | 407 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β§ π = π) β if(π β π, (π₯βπ), π) = if(π β π, (π₯βπ), π)) |
409 | | fvexd 6862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β (π₯βπ) β V) |
410 | 409, 286 | ifcld 4537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β if(π β π, (π₯βπ), π) β V) |
411 | 404, 408,
331, 410 | fvmptd 6960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β ((π β π β¦ if(π β π, (π₯βπ), π))βπ) = if(π β π, (π₯βπ), π)) |
412 | 411 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β ((π β π β¦ if(π β π, (π₯βπ), π))βπ) = if(π β π, (π₯βπ), π)) |
413 | 47 | eldifbd 3928 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β Β¬ π β π) |
414 | 413 | iffalsed 4502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β if(π β π, (π₯βπ), π) = π) |
415 | 414 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β if(π β π, (π₯βπ), π) = π) |
416 | 403, 412,
415 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β π = ((πβπ₯)βπ)) |
417 | 416 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π = ((πβπ₯)βπ)) |
418 | 401, 331 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π β π) |
419 | 393 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β βπ β π ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
420 | 419 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β βπ β π ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
421 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π β ((πβπ₯)βπ) = ((πβπ₯)βπ)) |
422 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π β ((πΆβπ)βπ) = ((πΆβπ)βπ)) |
423 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π β ((π·βπ)βπ) = ((π·βπ)βπ)) |
424 | 422, 423 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
425 | 421, 424 | eleq12d 2832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = π β (((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
426 | 425 | rspcva 3582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β π β§ βπ β π ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
427 | 418, 420,
426 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((πβπ₯)βπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
428 | 417, 427 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
429 | 149 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β β β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
430 | 60 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β β β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = ((πΆβπ) βΎ π)) |
431 | 429, 430 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π β β β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π½βπ) = ((πΆβπ) βΎ π)) |
432 | 431 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β β β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((π½βπ)βπ) = (((πΆβπ) βΎ π)βπ)) |
433 | 401, 402,
428, 432 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((π½βπ)βπ) = (((πΆβπ) βΎ π)βπ)) |
434 | 433 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((π½βπ)βπ) = (((πΆβπ) βΎ π)βπ)) |
435 | | fvres 6866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β (((πΆβπ) βΎ π)βπ) = ((πΆβπ)βπ)) |
436 | 435 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (((πΆβπ) βΎ π)βπ) = ((πΆβπ)βπ)) |
437 | 434, 436 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((π½βπ)βπ) = ((πΆβπ)βπ)) |
438 | 107 | elexd 3468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) β V) |
439 | 108 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β β β§ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) β V) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
440 | 139, 438,
439 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π β β) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
441 | 440 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β β β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
442 | 93 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β β β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = ((π·βπ) βΎ π)) |
443 | 441, 442 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π β β β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (πΎβπ) = ((π·βπ) βΎ π)) |
444 | 443 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β β β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((πΎβπ)βπ) = (((π·βπ) βΎ π)βπ)) |
445 | 401, 402,
428, 444 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((πΎβπ)βπ) = (((π·βπ) βΎ π)βπ)) |
446 | 445 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((πΎβπ)βπ) = (((π·βπ) βΎ π)βπ)) |
447 | | fvres 6866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β (((π·βπ) βΎ π)βπ) = ((π·βπ)βπ)) |
448 | 447 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (((π·βπ) βΎ π)βπ) = ((π·βπ)βπ)) |
449 | 446, 448 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((πΎβπ)βπ) = ((π·βπ)βπ)) |
450 | 437, 449 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (((π½βπ)βπ)[,)((πΎβπ)βπ)) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
451 | 450 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (((πΆβπ)βπ)[,)((π·βπ)βπ)) = (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
452 | 400, 451 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π₯ β Xπ β
π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (π₯βπ) β (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
453 | 452 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π β π β (π₯βπ) β (((π½βπ)βπ)[,)((πΎβπ)βπ)))) |
454 | 384, 453 | ralrimi 3243 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β βπ β π (π₯βπ) β (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
455 | 378, 454 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π₯ Fn π β§ βπ β π (π₯βπ) β (((π½βπ)βπ)[,)((πΎβπ)βπ)))) |
456 | 317 | elixp 8849 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β Xπ β
π (((π½βπ)βπ)[,)((πΎβπ)βπ)) β (π₯ Fn π β§ βπ β π (π₯βπ) β (((π½βπ)βπ)[,)((πΎβπ)βπ)))) |
457 | 455, 456 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β§ (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π₯ β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
458 | 457 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β β) β ((πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β π₯ β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ)))) |
459 | 458 | reximdva 3166 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β (βπ β β (πβπ₯) β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β βπ β β π₯ β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ)))) |
460 | 375, 459 | mpd 15 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β βπ β β π₯ β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
461 | | eliun 4963 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ)) β βπ β β π₯ β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
462 | 460, 461 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ))) β π₯ β βͺ
π β β Xπ β
π (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
463 | 462 | ralrimiva 3144 |
. . . . . . . . . . . . . . 15
β’ (π β βπ₯ β X π β π ((π΄βπ)[,)(π΅βπ))π₯ β βͺ
π β β Xπ β
π (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
464 | | dfss3 3937 |
. . . . . . . . . . . . . . 15
β’ (Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ)) β βπ₯ β X π β π ((π΄βπ)[,)(π΅βπ))π₯ β βͺ
π β β Xπ β
π (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
465 | 463, 464 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
466 | | ovexd 7397 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β
βm π)
β V) |
467 | 228 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β
V) |
468 | 466, 467 | elmapd 8786 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΎ β ((β βm π) βm β)
β πΎ:ββΆ(β βm
π))) |
469 | 109, 468 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (π β πΎ β ((β βm π) βm
β)) |
470 | 466, 467 | elmapd 8786 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π½ β ((β βm π) βm β)
β π½:ββΆ(β βm
π))) |
471 | 89, 470 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (π β π½ β ((β βm π) βm
β)) |
472 | 82, 71 | elmapd 8786 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π΅ βΎ π) β (β βm π) β (π΅ βΎ π):πβΆβ)) |
473 | 204, 472 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΅ βΎ π) β (β βm π)) |
474 | 82, 71 | elmapd 8786 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π΄ βΎ π) β (β βm π) β (π΄ βΎ π):πβΆβ)) |
475 | 202, 474 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ βΎ π) β (β βm π)) |
476 | | hoidmvlelem3.i |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ β (β βm π)βπ β (β βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
477 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = (π΄ βΎ π) β (πβπ) = ((π΄ βΎ π)βπ)) |
478 | 477 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π = (π΄ βΎ π) β§ π β π) β (πβπ) = ((π΄ βΎ π)βπ)) |
479 | 250 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π = (π΄ βΎ π) β§ π β π) β ((π΄ βΎ π)βπ) = (π΄βπ)) |
480 | 478, 479 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π = (π΄ βΎ π) β§ π β π) β (πβπ) = (π΄βπ)) |
481 | 480 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π = (π΄ βΎ π) β§ π β π) β ((πβπ)[,)(πβπ)) = ((π΄βπ)[,)(πβπ))) |
482 | 481 | ixpeq2dva 8857 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π΄ βΎ π) β Xπ β π ((πβπ)[,)(πβπ)) = Xπ β π ((π΄βπ)[,)(πβπ))) |
483 | 482 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π΄ βΎ π) β (Xπ β π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β Xπ β π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)))) |
484 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π΄ βΎ π) β (π(πΏβπ)π) = ((π΄ βΎ π)(πΏβπ)π)) |
485 | 484 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π΄ βΎ π) β ((π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
486 | 483, 485 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π΄ βΎ π) β ((Xπ β π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))) β (Xπ β π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))))) |
487 | 486 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π΄ βΎ π) β (ββ β ((β βm π) βm
β)(Xπ β π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))) β ββ β ((β βm π) βm
β)(Xπ β π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))))) |
488 | 487 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π΄ βΎ π) β (βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))) β βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))))) |
489 | 488 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π΄ βΎ π) β (βπ β (β βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))) β βπ β (β βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))))) |
490 | 489 | rspcva 3582 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ βΎ π) β (β βm π) β§ βπ β (β
βm π)βπ β (β βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) β βπ β (β βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
491 | 475, 476,
490 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ β (β βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
492 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (π΅ βΎ π) β (πβπ) = ((π΅ βΎ π)βπ)) |
493 | 492 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π = (π΅ βΎ π) β§ π β π) β (πβπ) = ((π΅ βΎ π)βπ)) |
494 | 251 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π = (π΅ βΎ π) β§ π β π) β ((π΅ βΎ π)βπ) = (π΅βπ)) |
495 | 493, 494 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π = (π΅ βΎ π) β§ π β π) β (πβπ) = (π΅βπ)) |
496 | 495 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π = (π΅ βΎ π) β§ π β π) β ((π΄βπ)[,)(πβπ)) = ((π΄βπ)[,)(π΅βπ))) |
497 | 496 | ixpeq2dva 8857 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π΅ βΎ π) β Xπ β π ((π΄βπ)[,)(πβπ)) = Xπ β π ((π΄βπ)[,)(π΅βπ))) |
498 | 497 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π΅ βΎ π) β (Xπ β π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)))) |
499 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π΅ βΎ π) β ((π΄ βΎ π)(πΏβπ)π) = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π))) |
500 | 499 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π΅ βΎ π) β (((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
501 | 498, 500 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π΅ βΎ π) β ((Xπ β π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))) β (Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))))) |
502 | 501 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π΅ βΎ π) β (ββ β ((β βm π) βm
β)(Xπ β π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))) β ββ β ((β βm π) βm
β)(Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))))) |
503 | 502 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π΅ βΎ π) β (βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))) β βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))))) |
504 | 503 | rspcva 3582 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅ βΎ π) β (β βm π) β§ βπ β (β
βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((π΄βπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) β βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
505 | 473, 491,
504 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
506 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π½ β (πβπ) = (π½βπ)) |
507 | 506 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π½ β ((πβπ)βπ) = ((π½βπ)βπ)) |
508 | 507 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π½ β (((πβπ)βπ)[,)((ββπ)βπ)) = (((π½βπ)βπ)[,)((ββπ)βπ))) |
509 | 508 | ixpeq2dv 8858 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π½ β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) = Xπ β π (((π½βπ)βπ)[,)((ββπ)βπ))) |
510 | 509 | iuneq2d 4988 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π½ β βͺ
π β β Xπ β
π (((πβπ)βπ)[,)((ββπ)βπ)) = βͺ
π β β Xπ β
π (((π½βπ)βπ)[,)((ββπ)βπ))) |
511 | 510 | sseq2d 3981 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π½ β (Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((ββπ)βπ)))) |
512 | 506 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π½ β ((πβπ)(πΏβπ)(ββπ)) = ((π½βπ)(πΏβπ)(ββπ))) |
513 | 512 | mpteq2dv 5212 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π½ β (π β β β¦ ((πβπ)(πΏβπ)(ββπ))) = (π β β β¦ ((π½βπ)(πΏβπ)(ββπ)))) |
514 | 513 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π½ β
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))) =
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(ββπ))))) |
515 | 514 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π½ β (((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(ββπ)))))) |
516 | 511, 515 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π½ β ((Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))) β (Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(ββπ))))))) |
517 | 516 | ralbidv 3175 |
. . . . . . . . . . . . . . . . 17
β’ (π = π½ β (ββ β ((β βm π) βm
β)(Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ))))) β ββ β ((β βm π) βm
β)(Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(ββπ))))))) |
518 | 517 | rspcva 3582 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β ((β
βm π)
βm β) β§ βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) β ββ β ((β βm π) βm
β)(Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(ββπ)))))) |
519 | 471, 505,
518 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β ββ β ((β βm π) βm
β)(Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(ββπ)))))) |
520 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β = πΎ β (ββπ) = (πΎβπ)) |
521 | 520 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β = πΎ β ((ββπ)βπ) = ((πΎβπ)βπ)) |
522 | 521 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = πΎ β (((π½βπ)βπ)[,)((ββπ)βπ)) = (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
523 | 522 | ixpeq2dv 8858 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = πΎ β Xπ β π (((π½βπ)βπ)[,)((ββπ)βπ)) = Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
524 | 523 | iuneq2d 4988 |
. . . . . . . . . . . . . . . . . 18
β’ (β = πΎ β βͺ
π β β Xπ β
π (((π½βπ)βπ)[,)((ββπ)βπ)) = βͺ
π β β Xπ β
π (((π½βπ)βπ)[,)((πΎβπ)βπ))) |
525 | 524 | sseq2d 3981 |
. . . . . . . . . . . . . . . . 17
β’ (β = πΎ β (Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((ββπ)βπ)) β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ)))) |
526 | 520 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = πΎ β ((π½βπ)(πΏβπ)(ββπ)) = ((π½βπ)(πΏβπ)(πΎβπ))) |
527 | 526 | mpteq2dv 5212 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = πΎ β (π β β β¦ ((π½βπ)(πΏβπ)(ββπ))) = (π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ)))) |
528 | 527 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ (β = πΎ β
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(ββπ)))) =
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ))))) |
529 | 528 | breq2d 5122 |
. . . . . . . . . . . . . . . . 17
β’ (β = πΎ β (((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(ββπ)))) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ)))))) |
530 | 525, 529 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (β = πΎ β ((Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(ββπ))))) β (Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ))))))) |
531 | 530 | rspcva 3582 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β ((β
βm π)
βm β) β§ ββ β ((β βm π) βm
β)(Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((ββπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(ββπ)))))) β (Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ)))))) |
532 | 469, 519,
531 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((π½βπ)βπ)[,)((πΎβπ)βπ)) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ)))))) |
533 | 465, 532 | mpd 15 |
. . . . . . . . . . . . 13
β’ (π β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ))))) |
534 | | idd 24 |
. . . . . . . . . . . . 13
β’ (π β (((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ)))) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ)))))) |
535 | 533, 534 | mpd 15 |
. . . . . . . . . . . 12
β’ (π β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ))))) |
536 | 535 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β
) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ))))) |
537 | 41 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β
) β§ π β β) β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
538 | 537 | mpteq2dva 5210 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β
) β (π β β β¦ (πβπ)) = (π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ)))) |
539 | 538 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ ((π β§ π β β
) β
(Ξ£^β(π β β β¦ (πβπ))) =
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ))))) |
540 | 249, 539 | breq12d 5123 |
. . . . . . . . . . 11
β’ ((π β§ π β β
) β (πΊ β€
(Ξ£^β(π β β β¦ (πβπ))) β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β€
(Ξ£^β(π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ)))))) |
541 | 536, 540 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ π β β
) β πΊ β€
(Ξ£^β(π β β β¦ (πβπ)))) |
542 | 541 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§
(Ξ£^β(π β β β¦ (πβπ))) β β) β πΊ β€
(Ξ£^β(π β β β¦ (πβπ)))) |
543 | 238, 240,
241, 281, 542 | ltletrd 11322 |
. . . . . . . 8
β’ (((π β§ π β β
) β§
(Ξ£^β(π β β β¦ (πβπ))) β β) β (πΊ / (1 + πΈ)) <
(Ξ£^β(π β β β¦ (πβπ)))) |
544 | 226, 237,
543 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β β
) β§ Β¬
(Ξ£^β(π β β β¦ (πβπ))) = +β) β (πΊ / (1 + πΈ)) <
(Ξ£^β(π β β β¦ (πβπ)))) |
545 | 225, 544 | pm2.61dan 812 |
. . . . . 6
β’ ((π β§ π β β
) β (πΊ / (1 + πΈ)) <
(Ξ£^β(π β β β¦ (πβπ)))) |
546 | 196, 197,
198, 199, 218, 545 | sge0uzfsumgt 44759 |
. . . . 5
β’ ((π β§ π β β
) β βπ β β (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ)) |
547 | 217 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ)) β (πΊ / (1 + πΈ)) β β) |
548 | | fzfid 13885 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β Fin) |
549 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β π) |
550 | | elfznn 13477 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β π β β) |
551 | 550 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β π β β) |
552 | 28, 114 | sselid 3947 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πβπ) β β) |
553 | 549, 551,
552 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (πβπ) β β) |
554 | 548, 553 | fsumrecl 15626 |
. . . . . . . . . . . 12
β’ (π β Ξ£π β (1...π)(πβπ) β β) |
555 | 554 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ)) β Ξ£π β (1...π)(πβπ) β β) |
556 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ)) β (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ)) |
557 | 547, 555,
556 | ltled 11310 |
. . . . . . . . . 10
β’ ((π β§ (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ)) β (πΊ / (1 + πΈ)) β€ Ξ£π β (1...π)(πβπ)) |
558 | 207 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ)) β πΊ β β) |
559 | 213 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ)) β (1 + πΈ) β
β+) |
560 | 558, 555,
559 | ledivmuld 13017 |
. . . . . . . . . 10
β’ ((π β§ (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ)) β ((πΊ / (1 + πΈ)) β€ Ξ£π β (1...π)(πβπ) β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)))) |
561 | 557, 560 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ)) β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
562 | 561 | ex 414 |
. . . . . . . 8
β’ (π β ((πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ) β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)))) |
563 | 562 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ) β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)))) |
564 | 563 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β β) β ((πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ) β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)))) |
565 | 564 | reximdva 3166 |
. . . . 5
β’ ((π β§ π β β
) β (βπ β β (πΊ / (1 + πΈ)) < Ξ£π β (1...π)(πβπ) β βπ β β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)))) |
566 | 546, 565 | mpd 15 |
. . . 4
β’ ((π β§ π β β
) β βπ β β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
567 | 193, 195,
566 | syl2anc 585 |
. . 3
β’ ((π β§ Β¬ π = β
) β βπ β β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
568 | 192, 567 | pm2.61dan 812 |
. 2
β’ (π β βπ β β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
569 | 43 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β π β Fin) |
570 | 46 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β π β π) |
571 | 47 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β π β (π β π)) |
572 | 200 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β π΄:πβΆβ) |
573 | 203 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β π΅:πβΆβ) |
574 | 62 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β πΆ:ββΆ(β βm
π)) |
575 | | eqid 2737 |
. . . . 5
β’ (π¦ β π β¦ 0) = (π¦ β π β¦ 0) |
576 | | eqid 2737 |
. . . . 5
β’ (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0))) = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0))) |
577 | 95 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β π·:ββΆ(β βm
π)) |
578 | | eqid 2737 |
. . . . 5
β’ (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0))) = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0))) |
579 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β (πΆβπ) = (πΆβπ)) |
580 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β (π·βπ) = (π·βπ)) |
581 | 579, 580 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β ((πΆβπ)(πΏβπ)(π·βπ)) = ((πΆβπ)(πΏβπ)(π·βπ))) |
582 | 581 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))) = (π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))) |
583 | 582 | fveq2i 6850 |
. . . . . . 7
β’
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) |
584 | | hoidmvlelem3.r |
. . . . . . 7
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
585 | 583, 584 | eqeltrid 2842 |
. . . . . 6
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
586 | 585 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
587 | | hoidmvlelem3.h |
. . . . . 6
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
588 | | eleq1w 2821 |
. . . . . . . . . 10
β’ (π = π β (π β π β π β π)) |
589 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
590 | 589 | breq1d 5120 |
. . . . . . . . . . 11
β’ (π = π β ((πβπ) β€ π₯ β (πβπ) β€ π₯)) |
591 | 590, 589 | ifbieq1d 4515 |
. . . . . . . . . 10
β’ (π = π β if((πβπ) β€ π₯, (πβπ), π₯) = if((πβπ) β€ π₯, (πβπ), π₯)) |
592 | 588, 589,
591 | ifbieq12d 4519 |
. . . . . . . . 9
β’ (π = π β if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)) = if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) |
593 | 592 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) = (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) |
594 | 593 | mpteq2i 5215 |
. . . . . . 7
β’ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) = (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) |
595 | 594 | mpteq2i 5215 |
. . . . . 6
β’ (π₯ β β β¦ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
596 | 587, 595 | eqtri 2765 |
. . . . 5
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
597 | 172 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β πΈ β
β+) |
598 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πΆβπ) = (πΆβπ)) |
599 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (π·βπ) = (π·βπ)) |
600 | 599 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = π β ((π»βπ§)β(π·βπ)) = ((π»βπ§)β(π·βπ))) |
601 | 598, 600 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))) = ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))) |
602 | 601 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))) |
603 | 602 | fveq2i 6850 |
. . . . . . . . 9
β’
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))) |
604 | 603 | oveq2i 7373 |
. . . . . . . 8
β’ ((1 +
πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) = ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) |
605 | 604 | breq2i 5118 |
. . . . . . 7
β’ ((πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) β (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))) |
606 | 605 | rabbii 3416 |
. . . . . 6
β’ {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} |
607 | 337, 606 | eqtri 2765 |
. . . . 5
β’ π = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} |
608 | 285 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β π β π) |
609 | 344 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β π < (π΅βπ)) |
610 | | eqid 2737 |
. . . . 5
β’ (π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ))) = (π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ))) |
611 | | simp2 1138 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β π β β) |
612 | | id 22 |
. . . . . . . 8
β’ (πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
613 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
614 | 613 | cbvsumv 15588 |
. . . . . . . . . 10
β’
Ξ£π β
(1...π)(πβπ) = Ξ£π β (1...π)(πβπ) |
615 | 614 | oveq2i 7373 |
. . . . . . . . 9
β’ ((1 +
πΈ) Β· Ξ£π β (1...π)(πβπ)) = ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) |
616 | 615 | a1i 11 |
. . . . . . . 8
β’ (πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) β ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) = ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
617 | 612, 616 | breqtrd 5136 |
. . . . . . 7
β’ (πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
618 | 617 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
619 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β π) |
620 | | elfznn 13477 |
. . . . . . . . . . 11
β’ (π β (1...π) β π β β) |
621 | 620 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β π β β) |
622 | | eleq1w 2821 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π β β β π β β)) |
623 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π½βπ) = (π½βπ)) |
624 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΎβπ) = (πΎβπ)) |
625 | 623, 624 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π½βπ)(πΏβπ)(πΎβπ)) = ((π½βπ)(πΏβπ)(πΎβπ))) |
626 | 613, 625 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πβπ) = ((π½βπ)(πΏβπ)(πΎβπ)) β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ)))) |
627 | 622, 626 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π β β β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) β (π β β β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))))) |
628 | 627, 41 | chvarvv 2003 |
. . . . . . . . . . . . 13
β’ (π β β β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
629 | 628 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
630 | 622 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π β§ π β β) β (π β§ π β β))) |
631 | 598 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((πΆβπ)βπ) = ((πΆβπ)βπ)) |
632 | 599 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π·βπ)βπ) = ((π·βπ)βπ)) |
633 | 631, 632 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
634 | 633 | eleq2d 2824 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β π β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
635 | 598 | reseq1d 5941 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((πΆβπ) βΎ π) = ((πΆβπ) βΎ π)) |
636 | 634, 635 | ifbieq1d 4515 |
. . . . . . . . . . . . . . . 16
β’ (π = π β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
637 | 623, 636 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ))) |
638 | 630, 637 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π = π β (((π β§ π β β) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) β ((π β§ π β β) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)))) |
639 | 638, 149 | chvarvv 2003 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
640 | 599 | reseq1d 5941 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((π·βπ) βΎ π) = ((π·βπ) βΎ π)) |
641 | 634, 640 | ifbieq1d 4515 |
. . . . . . . . . . . . . . . 16
β’ (π = π β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
642 | 624, 641 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ))) |
643 | 630, 642 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π = π β (((π β§ π β β) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) β ((π β§ π β β) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)))) |
644 | 643, 440 | chvarvv 2003 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
645 | 639, 644 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π½βπ)(πΏβπ)(πΎβπ)) = (if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)(πΏβπ)if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ))) |
646 | 629, 645 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβπ) = (if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)(πΏβπ)if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ))) |
647 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β) |
648 | | ovexd 7397 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)) β V) |
649 | 610 | fvmpt2 6964 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)) β V) β ((π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)))βπ) = (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ))) |
650 | 647, 648,
649 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)))βπ) = (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ))) |
651 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΆβπ) β V |
652 | 651 | resex 5990 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΆβπ) βΎ π) β V |
653 | 652 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((πΆβπ) βΎ π) β V) |
654 | 80, 143 | eqeltrrid 2843 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π¦ β π β¦ 0) β V) |
655 | 653, 654 | ifcld 4537 |
. . . . . . . . . . . . . . . 16
β’ (π β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)) β V) |
656 | 655 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)) β V) |
657 | 576 | fvmpt2 6964 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)) β V) β ((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0))) |
658 | 647, 656,
657 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0))) |
659 | 80 | eqcomi 2746 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π β¦ 0) = πΉ |
660 | | ifeq2 4496 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β π β¦ 0) = πΉ β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
661 | 659, 660 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) |
662 | 661 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
663 | 658, 662 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
664 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . 19
β’ (π·βπ) β V |
665 | 664 | resex 5990 |
. . . . . . . . . . . . . . . . . 18
β’ ((π·βπ) βΎ π) β V |
666 | 665 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π·βπ) βΎ π) β V) |
667 | 666, 654 | ifcld 4537 |
. . . . . . . . . . . . . . . 16
β’ (π β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)) β V) |
668 | 667 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)) β V) |
669 | 578 | fvmpt2 6964 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)) β V) β ((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0))) |
670 | 647, 668,
669 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0))) |
671 | | biid 261 |
. . . . . . . . . . . . . . . 16
β’ (π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
672 | 671, 659 | ifbieq2i 4516 |
. . . . . . . . . . . . . . 15
β’ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) |
673 | 672 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
674 | 670, 673 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
675 | 663, 674 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)) = (if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)(πΏβπ)if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ))) |
676 | 650, 675 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)))βπ) = (if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)(πΏβπ)if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ))) |
677 | 646, 676 | eqtr4d 2780 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ) = ((π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)))βπ)) |
678 | 619, 621,
677 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (πβπ) = ((π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)))βπ)) |
679 | 678 | 3ad2antl1 1186 |
. . . . . . . 8
β’ (((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β§ π β (1...π)) β (πβπ) = ((π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)))βπ)) |
680 | 679 | sumeq2dv 15595 |
. . . . . . 7
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β Ξ£π β (1...π)(πβπ) = Ξ£π β (1...π)((π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)))βπ)) |
681 | 680 | oveq2d 7378 |
. . . . . 6
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) = ((1 + πΈ) Β· Ξ£π β (1...π)((π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)))βπ))) |
682 | 618, 681 | breqtrd 5136 |
. . . . 5
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)((π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)))βπ))) |
683 | | fveq2 6847 |
. . . . . . . 8
β’ (π = β β (π·βπ) = (π·ββ)) |
684 | 683 | fveq1d 6849 |
. . . . . . 7
β’ (π = β β ((π·βπ)βπ) = ((π·ββ)βπ)) |
685 | 684 | cbvmptv 5223 |
. . . . . 6
β’ (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) = (β β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·ββ)βπ)) |
686 | 685 | rneqi 5897 |
. . . . 5
β’ ran
(π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) = ran (β β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·ββ)βπ)) |
687 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (β = π β (πΆββ) = (πΆβπ)) |
688 | 687 | fveq1d 6849 |
. . . . . . . . . . 11
β’ (β = π β ((πΆββ)βπ) = ((πΆβπ)βπ)) |
689 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (β = π β (π·ββ) = (π·βπ)) |
690 | 689 | fveq1d 6849 |
. . . . . . . . . . 11
β’ (β = π β ((π·ββ)βπ) = ((π·βπ)βπ)) |
691 | 688, 690 | oveq12d 7380 |
. . . . . . . . . 10
β’ (β = π β (((πΆββ)βπ)[,)((π·ββ)βπ)) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
692 | 691 | eleq2d 2824 |
. . . . . . . . 9
β’ (β = π β (π β (((πΆββ)βπ)[,)((π·ββ)βπ)) β π β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
693 | 692 | cbvrabv 3420 |
. . . . . . . 8
β’ {β β (1...π) β£ π β (((πΆββ)βπ)[,)((π·ββ)βπ))} = {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} |
694 | 693 | mpteq1i 5206 |
. . . . . . 7
β’ (π β {β β (1...π) β£ π β (((πΆββ)βπ)[,)((π·ββ)βπ))} β¦ ((π·βπ)βπ)) = (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) |
695 | 694 | rneqi 5897 |
. . . . . 6
β’ ran
(π β {β β (1...π) β£ π β (((πΆββ)βπ)[,)((π·ββ)βπ))} β¦ ((π·βπ)βπ)) = ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) |
696 | 695 | uneq2i 4125 |
. . . . 5
β’ ({(π΅βπ)} βͺ ran (π β {β β (1...π) β£ π β (((πΆββ)βπ)[,)((π·ββ)βπ))} β¦ ((π·βπ)βπ))) = ({(π΅βπ)} βͺ ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ))) |
697 | | eqid 2737 |
. . . . 5
β’
inf(({(π΅βπ)} βͺ ran (π β {β β (1...π) β£ π β (((πΆββ)βπ)[,)((π·ββ)βπ))} β¦ ((π·βπ)βπ))), β, < ) = inf(({(π΅βπ)} βͺ ran (π β {β β (1...π) β£ π β (((πΆββ)βπ)[,)((π·ββ)βπ))} β¦ ((π·βπ)βπ))), β, < ) |
698 | 18, 569, 570, 571, 44, 572, 573, 574, 575, 576, 577, 578, 586, 596, 5, 597, 607, 608, 609, 610, 611, 682, 686, 696, 697 | hoidmvlelem2 44911 |
. . . 4
β’ ((π β§ π β β β§ πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) β βπ’ β π π < π’) |
699 | 698 | 3exp 1120 |
. . 3
β’ (π β (π β β β (πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) β βπ’ β π π < π’))) |
700 | 699 | rexlimdv 3151 |
. 2
β’ (π β (βπ β β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) β βπ’ β π π < π’)) |
701 | 568, 700 | mpd 15 |
1
β’ (π β βπ’ β π π < π’) |