Step | Hyp | Ref
| Expression |
1 | | hoidmvlelem2.a |
. . . . . . 7
β’ (π β π΄:πβΆβ) |
2 | | hoidmvlelem2.z |
. . . . . . . . . 10
β’ (π β π β (π β π)) |
3 | | snidg 4661 |
. . . . . . . . . 10
β’ (π β (π β π) β π β {π}) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
β’ (π β π β {π}) |
5 | | elun2 4176 |
. . . . . . . . 9
β’ (π β {π} β π β (π βͺ {π})) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
β’ (π β π β (π βͺ {π})) |
7 | | hoidmvlelem2.w |
. . . . . . . 8
β’ π = (π βͺ {π}) |
8 | 6, 7 | eleqtrrdi 2845 |
. . . . . . 7
β’ (π β π β π) |
9 | 1, 8 | ffvelcdmd 7083 |
. . . . . 6
β’ (π β (π΄βπ) β β) |
10 | | hoidmvlelem2.b |
. . . . . . 7
β’ (π β π΅:πβΆβ) |
11 | 10, 8 | ffvelcdmd 7083 |
. . . . . 6
β’ (π β (π΅βπ) β β) |
12 | | hoidmvlelem2.v |
. . . . . . . 8
β’ π = ({(π΅βπ)} βͺ π) |
13 | 11 | snssd 4811 |
. . . . . . . . 9
β’ (π β {(π΅βπ)} β β) |
14 | | hoidmvlelem2.O |
. . . . . . . . . 10
β’ π = ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) |
15 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²ππ |
16 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) = (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) |
17 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}) β π) |
18 | | fz1ssnn 13528 |
. . . . . . . . . . . . . 14
β’
(1...π) β
β |
19 | | elrabi 3676 |
. . . . . . . . . . . . . 14
β’ (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β π β (1...π)) |
20 | 18, 19 | sselid 3979 |
. . . . . . . . . . . . 13
β’ (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β π β β) |
21 | 20 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}) β π β β) |
22 | | eleq1w 2817 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π β β β π β β)) |
23 | 22 | anbi2d 630 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π β§ π β β) β (π β§ π β β))) |
24 | | fveq2 6888 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π·βπ) = (π·βπ)) |
25 | 24 | fveq1d 6890 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π·βπ)βπ) = ((π·βπ)βπ)) |
26 | 25 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π = π β (((π·βπ)βπ) β β β ((π·βπ)βπ) β β)) |
27 | 23, 26 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = π β (((π β§ π β β) β ((π·βπ)βπ) β β) β ((π β§ π β β) β ((π·βπ)βπ) β β))) |
28 | | hoidmvlelem2.d |
. . . . . . . . . . . . . . . 16
β’ (π β π·:ββΆ(β βm
π)) |
29 | 28 | ffvelcdmda 7082 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π·βπ) β (β βm π)) |
30 | | elmapi 8839 |
. . . . . . . . . . . . . . 15
β’ ((π·βπ) β (β βm π) β (π·βπ):πβΆβ) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π·βπ):πβΆβ) |
32 | 8 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β π) |
33 | 31, 32 | ffvelcdmd 7083 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((π·βπ)βπ) β β) |
34 | 27, 33 | chvarvv 2003 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π·βπ)βπ) β β) |
35 | 17, 21, 34 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}) β ((π·βπ)βπ) β β) |
36 | 15, 16, 35 | rnmptssd 43828 |
. . . . . . . . . 10
β’ (π β ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) β β) |
37 | 14, 36 | eqsstrid 4029 |
. . . . . . . . 9
β’ (π β π β β) |
38 | 13, 37 | unssd 4185 |
. . . . . . . 8
β’ (π β ({(π΅βπ)} βͺ π) β β) |
39 | 12, 38 | eqsstrid 4029 |
. . . . . . 7
β’ (π β π β β) |
40 | | hoidmvlelem2.q |
. . . . . . . 8
β’ π = inf(π, β, < ) |
41 | | ltso 11290 |
. . . . . . . . . 10
β’ < Or
β |
42 | 41 | a1i 11 |
. . . . . . . . 9
β’ (π β < Or
β) |
43 | | snfi 9040 |
. . . . . . . . . . . 12
β’ {(π΅βπ)} β Fin |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
β’ (π β {(π΅βπ)} β Fin) |
45 | | fzfi 13933 |
. . . . . . . . . . . . . . 15
β’
(1...π) β
Fin |
46 | | rabfi 9265 |
. . . . . . . . . . . . . . 15
β’
((1...π) β Fin
β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β Fin) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β Fin |
48 | 47 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β Fin) |
49 | 16 | rnmptfi 43800 |
. . . . . . . . . . . . 13
β’ ({π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β Fin β ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) β Fin) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) β Fin) |
51 | 14, 50 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (π β π β Fin) |
52 | | unfi 9168 |
. . . . . . . . . . 11
β’ (({(π΅βπ)} β Fin β§ π β Fin) β ({(π΅βπ)} βͺ π) β Fin) |
53 | 44, 51, 52 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β ({(π΅βπ)} βͺ π) β Fin) |
54 | 12, 53 | eqeltrid 2838 |
. . . . . . . . 9
β’ (π β π β Fin) |
55 | | fvex 6901 |
. . . . . . . . . . . . . 14
β’ (π΅βπ) β V |
56 | 55 | snid 4663 |
. . . . . . . . . . . . 13
β’ (π΅βπ) β {(π΅βπ)} |
57 | | elun1 4175 |
. . . . . . . . . . . . 13
β’ ((π΅βπ) β {(π΅βπ)} β (π΅βπ) β ({(π΅βπ)} βͺ π)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (π΅βπ) β ({(π΅βπ)} βͺ π) |
59 | 12 | eqcomi 2742 |
. . . . . . . . . . . 12
β’ ({(π΅βπ)} βͺ π) = π |
60 | 58, 59 | eleqtri 2832 |
. . . . . . . . . . 11
β’ (π΅βπ) β π |
61 | 60 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π΅βπ) β π) |
62 | | ne0i 4333 |
. . . . . . . . . 10
β’ ((π΅βπ) β π β π β β
) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
β’ (π β π β β
) |
64 | | fiinfcl 9492 |
. . . . . . . . 9
β’ (( <
Or β β§ (π β
Fin β§ π β β
β§ π β β))
β inf(π, β, <
) β π) |
65 | 42, 54, 63, 39, 64 | syl13anc 1373 |
. . . . . . . 8
β’ (π β inf(π, β, < ) β π) |
66 | 40, 65 | eqeltrid 2838 |
. . . . . . 7
β’ (π β π β π) |
67 | 39, 66 | sseldd 3982 |
. . . . . 6
β’ (π β π β β) |
68 | | hoidmvlelem2.u |
. . . . . . . . . . . 12
β’ π = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} |
69 | | ssrab2 4076 |
. . . . . . . . . . . 12
β’ {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β ((π΄βπ)[,](π΅βπ)) |
70 | 68, 69 | eqsstri 4015 |
. . . . . . . . . . 11
β’ π β ((π΄βπ)[,](π΅βπ)) |
71 | 70 | a1i 11 |
. . . . . . . . . 10
β’ (π β π β ((π΄βπ)[,](π΅βπ))) |
72 | 9, 11 | iccssred 13407 |
. . . . . . . . . 10
β’ (π β ((π΄βπ)[,](π΅βπ)) β β) |
73 | 71, 72 | sstrd 3991 |
. . . . . . . . 9
β’ (π β π β β) |
74 | | hoidmvlelem2.su |
. . . . . . . . 9
β’ (π β π β π) |
75 | 73, 74 | sseldd 3982 |
. . . . . . . 8
β’ (π β π β β) |
76 | 9 | rexrd 11260 |
. . . . . . . . 9
β’ (π β (π΄βπ) β
β*) |
77 | 11 | rexrd 11260 |
. . . . . . . . 9
β’ (π β (π΅βπ) β
β*) |
78 | 70, 74 | sselid 3979 |
. . . . . . . . 9
β’ (π β π β ((π΄βπ)[,](π΅βπ))) |
79 | | iccgelb 13376 |
. . . . . . . . 9
β’ (((π΄βπ) β β* β§ (π΅βπ) β β* β§ π β ((π΄βπ)[,](π΅βπ))) β (π΄βπ) β€ π) |
80 | 76, 77, 78, 79 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π΄βπ) β€ π) |
81 | | hoidmvlelem2.sb |
. . . . . . . . . . . . . . 15
β’ (π β π < (π΅βπ)) |
82 | 81 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ = (π΅βπ)) β π < (π΅βπ)) |
83 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (π΅βπ) β π₯ = (π΅βπ)) |
84 | 83 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π΅βπ) β (π΅βπ) = π₯) |
85 | 84 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ = (π΅βπ)) β (π΅βπ) = π₯) |
86 | 82, 85 | breqtrd 5173 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ = (π΅βπ)) β π < π₯) |
87 | 86 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π₯ = (π΅βπ)) β π < π₯) |
88 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ Β¬ π₯ = (π΅βπ)) β π) |
89 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β π₯ β π) |
90 | 89, 12 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π β π₯ β ({(π΅βπ)} βͺ π)) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π β§ Β¬ π₯ = (π΅βπ)) β π₯ β ({(π΅βπ)} βͺ π)) |
92 | | elsni 4644 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β {(π΅βπ)} β π₯ = (π΅βπ)) |
93 | 92 | con3i 154 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π₯ = (π΅βπ) β Β¬ π₯ β {(π΅βπ)}) |
94 | 93 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π β§ Β¬ π₯ = (π΅βπ)) β Β¬ π₯ β {(π΅βπ)}) |
95 | | elunnel1 4148 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β ({(π΅βπ)} βͺ π) β§ Β¬ π₯ β {(π΅βπ)}) β π₯ β π) |
96 | 91, 94, 95 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π β§ Β¬ π₯ = (π΅βπ)) β π₯ β π) |
97 | 96 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ Β¬ π₯ = (π΅βπ)) β π₯ β π) |
98 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β π₯ β π) |
99 | 98, 14 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π β π₯ β ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ))) |
100 | | vex 3479 |
. . . . . . . . . . . . . . . . 17
β’ π₯ β V |
101 | 16 | elrnmpt 5953 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β V β (π₯ β ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) β βπ β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}π₯ = ((π·βπ)βπ))) |
102 | 100, 101 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ)) β βπ β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}π₯ = ((π·βπ)βπ)) |
103 | 99, 102 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π β βπ β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}π₯ = ((π·βπ)βπ)) |
104 | 103 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β βπ β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}π₯ = ((π·βπ)βπ)) |
105 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π β (πΆβπ) = (πΆβπ)) |
106 | 105 | fveq1d 6890 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β ((πΆβπ)βπ) = ((πΆβπ)βπ)) |
107 | 106 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (((πΆβπ)βπ) β β β ((πΆβπ)βπ) β β)) |
108 | 23, 107 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (((π β§ π β β) β ((πΆβπ)βπ) β β) β ((π β§ π β β) β ((πΆβπ)βπ) β β))) |
109 | | hoidmvlelem2.c |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β πΆ:ββΆ(β βm
π)) |
110 | 109 | ffvelcdmda 7082 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β (πΆβπ) β (β βm π)) |
111 | | elmapi 8839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΆβπ) β (β βm π) β (πΆβπ):πβΆβ) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
113 | 112, 32 | ffvelcdmd 7083 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β ((πΆβπ)βπ) β β) |
114 | 108, 113 | chvarvv 2003 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β ((πΆβπ)βπ) β β) |
115 | 114 | rexrd 11260 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β ((πΆβπ)βπ) β
β*) |
116 | 17, 21, 115 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}) β ((πΆβπ)βπ) β
β*) |
117 | 34 | rexrd 11260 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β ((π·βπ)βπ) β
β*) |
118 | 17, 21, 117 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}) β ((π·βπ)βπ) β
β*) |
119 | 106, 25 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
120 | 119 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β π β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
121 | 120 | elrab 3682 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β (π β (1...π) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
122 | 121 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β (π β (1...π) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
123 | 122 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
124 | 123 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}) β π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
125 | | icoltub 44156 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΆβπ)βπ) β β* β§ ((π·βπ)βπ) β β* β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π < ((π·βπ)βπ)) |
126 | 116, 118,
124, 125 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}) β π < ((π·βπ)βπ)) |
127 | 126 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β§ π₯ = ((π·βπ)βπ)) β π < ((π·βπ)βπ)) |
128 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = ((π·βπ)βπ) β π₯ = ((π·βπ)βπ)) |
129 | 128 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = ((π·βπ)βπ) β ((π·βπ)βπ) = π₯) |
130 | 129 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β§ π₯ = ((π·βπ)βπ)) β ((π·βπ)βπ) = π₯) |
131 | 127, 130 | breqtrd 5173 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β§ π₯ = ((π·βπ)βπ)) β π < π₯) |
132 | 131 | 3exp 1120 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β (π₯ = ((π·βπ)βπ) β π < π₯))) |
133 | 132 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π) β (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β (π₯ = ((π·βπ)βπ) β π < π₯))) |
134 | 133 | rexlimdv 3154 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β (βπ β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}π₯ = ((π·βπ)βπ) β π < π₯)) |
135 | 104, 134 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π) β π < π₯) |
136 | 88, 97, 135 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ Β¬ π₯ = (π΅βπ)) β π < π₯) |
137 | 87, 136 | pm2.61dan 812 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β π < π₯) |
138 | 137 | ralrimiva 3147 |
. . . . . . . . . 10
β’ (π β βπ₯ β π π < π₯) |
139 | | breq2 5151 |
. . . . . . . . . . 11
β’ (π₯ = inf(π, β, < ) β (π < π₯ β π < inf(π, β, < ))) |
140 | 139 | rspcva 3610 |
. . . . . . . . . 10
β’
((inf(π, β,
< ) β π β§
βπ₯ β π π < π₯) β π < inf(π, β, < )) |
141 | 65, 138, 140 | syl2anc 585 |
. . . . . . . . 9
β’ (π β π < inf(π, β, < )) |
142 | 40 | eqcomi 2742 |
. . . . . . . . . 10
β’ inf(π, β, < ) = π |
143 | 142 | a1i 11 |
. . . . . . . . 9
β’ (π β inf(π, β, < ) = π) |
144 | 141, 143 | breqtrd 5173 |
. . . . . . . 8
β’ (π β π < π) |
145 | 9, 75, 67, 80, 144 | lelttrd 11368 |
. . . . . . 7
β’ (π β (π΄βπ) < π) |
146 | 9, 67, 145 | ltled 11358 |
. . . . . 6
β’ (π β (π΄βπ) β€ π) |
147 | | fiminre 12157 |
. . . . . . . . 9
β’ ((π β β β§ π β Fin β§ π β β
) β
βπ₯ β π βπ¦ β π π₯ β€ π¦) |
148 | 39, 54, 63, 147 | syl3anc 1372 |
. . . . . . . 8
β’ (π β βπ₯ β π βπ¦ β π π₯ β€ π¦) |
149 | | lbinfle 12165 |
. . . . . . . 8
β’ ((π β β β§
βπ₯ β π βπ¦ β π π₯ β€ π¦ β§ (π΅βπ) β π) β inf(π, β, < ) β€ (π΅βπ)) |
150 | 39, 148, 61, 149 | syl3anc 1372 |
. . . . . . 7
β’ (π β inf(π, β, < ) β€ (π΅βπ)) |
151 | 40, 150 | eqbrtrid 5182 |
. . . . . 6
β’ (π β π β€ (π΅βπ)) |
152 | 9, 11, 67, 146, 151 | eliccd 44152 |
. . . . 5
β’ (π β π β ((π΄βπ)[,](π΅βπ))) |
153 | 67 | recnd 11238 |
. . . . . . . . . 10
β’ (π β π β β) |
154 | 75 | recnd 11238 |
. . . . . . . . . 10
β’ (π β π β β) |
155 | 9 | recnd 11238 |
. . . . . . . . . 10
β’ (π β (π΄βπ) β β) |
156 | 153, 154,
155 | npncand 11591 |
. . . . . . . . 9
β’ (π β ((π β π) + (π β (π΄βπ))) = (π β (π΄βπ))) |
157 | 156 | eqcomd 2739 |
. . . . . . . 8
β’ (π β (π β (π΄βπ)) = ((π β π) + (π β (π΄βπ)))) |
158 | 157 | oveq2d 7420 |
. . . . . . 7
β’ (π β (πΊ Β· (π β (π΄βπ))) = (πΊ Β· ((π β π) + (π β (π΄βπ))))) |
159 | | rge0ssre 13429 |
. . . . . . . . . 10
β’
(0[,)+β) β β |
160 | | hoidmvlelem2.g |
. . . . . . . . . . 11
β’ πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) |
161 | | hoidmvlelem2.l |
. . . . . . . . . . . 12
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
162 | | hoidmvlelem2.x |
. . . . . . . . . . . . 13
β’ (π β π β Fin) |
163 | | hoidmvlelem2.y |
. . . . . . . . . . . . 13
β’ (π β π β π) |
164 | 162, 163 | ssfid 9263 |
. . . . . . . . . . . 12
β’ (π β π β Fin) |
165 | | ssun1 4171 |
. . . . . . . . . . . . . . 15
β’ π β (π βͺ {π}) |
166 | 165, 7 | sseqtrri 4018 |
. . . . . . . . . . . . . 14
β’ π β π |
167 | 166 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β π β π) |
168 | 1, 167 | fssresd 6755 |
. . . . . . . . . . . 12
β’ (π β (π΄ βΎ π):πβΆβ) |
169 | 10, 167 | fssresd 6755 |
. . . . . . . . . . . 12
β’ (π β (π΅ βΎ π):πβΆβ) |
170 | 161, 164,
168, 169 | hoidmvcl 45233 |
. . . . . . . . . . 11
β’ (π β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) β (0[,)+β)) |
171 | 160, 170 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (π β πΊ β (0[,)+β)) |
172 | 159, 171 | sselid 3979 |
. . . . . . . . 9
β’ (π β πΊ β β) |
173 | 172 | recnd 11238 |
. . . . . . . 8
β’ (π β πΊ β β) |
174 | 153, 154 | subcld 11567 |
. . . . . . . 8
β’ (π β (π β π) β β) |
175 | 154, 155 | subcld 11567 |
. . . . . . . 8
β’ (π β (π β (π΄βπ)) β β) |
176 | 173, 174,
175 | adddid 11234 |
. . . . . . 7
β’ (π β (πΊ Β· ((π β π) + (π β (π΄βπ)))) = ((πΊ Β· (π β π)) + (πΊ Β· (π β (π΄βπ))))) |
177 | 173, 174 | mulcld 11230 |
. . . . . . . 8
β’ (π β (πΊ Β· (π β π)) β β) |
178 | 173, 175 | mulcld 11230 |
. . . . . . . 8
β’ (π β (πΊ Β· (π β (π΄βπ))) β β) |
179 | 177, 178 | addcomd 11412 |
. . . . . . 7
β’ (π β ((πΊ Β· (π β π)) + (πΊ Β· (π β (π΄βπ)))) = ((πΊ Β· (π β (π΄βπ))) + (πΊ Β· (π β π)))) |
180 | 158, 176,
179 | 3eqtrd 2777 |
. . . . . 6
β’ (π β (πΊ Β· (π β (π΄βπ))) = ((πΊ Β· (π β (π΄βπ))) + (πΊ Β· (π β π)))) |
181 | 67, 75 | jca 513 |
. . . . . . . . . . . . 13
β’ (π β (π β β β§ π β β)) |
182 | | resubcl 11520 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β (π β π) β β) |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β π) β β) |
184 | 172, 183 | jca 513 |
. . . . . . . . . . 11
β’ (π β (πΊ β β β§ (π β π) β β)) |
185 | | remulcl 11191 |
. . . . . . . . . . 11
β’ ((πΊ β β β§ (π β π) β β) β (πΊ Β· (π β π)) β β) |
186 | 184, 185 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΊ Β· (π β π)) β β) |
187 | 75, 9 | jca 513 |
. . . . . . . . . . . . 13
β’ (π β (π β β β§ (π΄βπ) β β)) |
188 | | resubcl 11520 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π΄βπ) β β) β (π β (π΄βπ)) β β) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β (π΄βπ)) β β) |
190 | 172, 189 | jca 513 |
. . . . . . . . . . 11
β’ (π β (πΊ β β β§ (π β (π΄βπ)) β β)) |
191 | | remulcl 11191 |
. . . . . . . . . . 11
β’ ((πΊ β β β§ (π β (π΄βπ)) β β) β (πΊ Β· (π β (π΄βπ))) β β) |
192 | 190, 191 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΊ Β· (π β (π΄βπ))) β β) |
193 | 186, 192 | jca 513 |
. . . . . . . . 9
β’ (π β ((πΊ Β· (π β π)) β β β§ (πΊ Β· (π β (π΄βπ))) β β)) |
194 | | readdcl 11189 |
. . . . . . . . 9
β’ (((πΊ Β· (π β π)) β β β§ (πΊ Β· (π β (π΄βπ))) β β) β ((πΊ Β· (π β π)) + (πΊ Β· (π β (π΄βπ)))) β β) |
195 | 193, 194 | syl 17 |
. . . . . . . 8
β’ (π β ((πΊ Β· (π β π)) + (πΊ Β· (π β (π΄βπ)))) β β) |
196 | 179, 195 | eqeltrrd 2835 |
. . . . . . 7
β’ (π β ((πΊ Β· (π β (π΄βπ))) + (πΊ Β· (π β π))) β β) |
197 | | 1red 11211 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
198 | | hoidmvlelem2.e |
. . . . . . . . . . 11
β’ (π β πΈ β
β+) |
199 | 198 | rpred 13012 |
. . . . . . . . . 10
β’ (π β πΈ β β) |
200 | 197, 199 | readdcld 11239 |
. . . . . . . . 9
β’ (π β (1 + πΈ) β β) |
201 | 2 | eldifbd 3960 |
. . . . . . . . . . 11
β’ (π β Β¬ π β π) |
202 | 8, 201 | eldifd 3958 |
. . . . . . . . . 10
β’ (π β π β (π β π)) |
203 | | hoidmvlelem2.r |
. . . . . . . . . 10
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
204 | | hoidmvlelem2.h |
. . . . . . . . . 10
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
205 | 161, 164,
202, 7, 109, 28, 203, 204, 75 | sge0hsphoire 45240 |
. . . . . . . . 9
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) |
206 | 200, 205 | remulcld 11240 |
. . . . . . . 8
β’ (π β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) β β) |
207 | | fzfid 13934 |
. . . . . . . . . 10
β’ (π β (1...π) β Fin) |
208 | 183 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (π β π) β β) |
209 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β π) |
210 | | elfznn 13526 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β π β β) |
211 | 210 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β π β β) |
212 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
213 | | ovexd 7439 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((π½βπ)(πΏβπ)(πΎβπ)) β V) |
214 | | hoidmvlelem2.p |
. . . . . . . . . . . . . . . . 17
β’ π = (π β β β¦ ((π½βπ)(πΏβπ)(πΎβπ))) |
215 | 214 | fvmpt2 7005 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ ((π½βπ)(πΏβπ)(πΎβπ)) β V) β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
216 | 212, 213,
215 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β β β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
217 | 216 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
218 | 164 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β Fin) |
219 | 166 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β π β π) |
220 | 112, 219 | fssresd 6755 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β ((πΆβπ) βΎ π):πβΆβ) |
221 | 220 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((πΆβπ) βΎ π):πβΆβ) |
222 | | iftrue 4533 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = ((πΆβπ) βΎ π)) |
223 | 222 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = ((πΆβπ) βΎ π)) |
224 | 223 | feq1d 6699 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ β ((πΆβπ) βΎ π):πβΆβ)) |
225 | 221, 224 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ) |
226 | | 0red 11213 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β π) β 0 β β) |
227 | | hoidmvlelem2.f |
. . . . . . . . . . . . . . . . . . . 20
β’ πΉ = (π¦ β π β¦ 0) |
228 | 226, 227 | fmptd 7109 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ:πβΆβ) |
229 | 228 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β πΉ:πβΆβ) |
230 | | iffalse 4536 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = πΉ) |
231 | 230 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = πΉ) |
232 | 231 | feq1d 6699 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ β πΉ:πβΆβ)) |
233 | 229, 232 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ) |
234 | 225, 233 | pm2.61dan 812 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ) |
235 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π β β) |
236 | | fvex 6901 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΆβπ) β V |
237 | 236 | resex 6027 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΆβπ) βΎ π) β V |
238 | 237 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((πΆβπ) βΎ π) β V) |
239 | 162, 163 | ssexd 5323 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β V) |
240 | | mptexg 7218 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β V β (π¦ β π β¦ 0) β V) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π¦ β π β¦ 0) β V) |
242 | 227, 241 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΉ β V) |
243 | 238, 242 | ifcld 4573 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β V) |
244 | 243 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β V) |
245 | | hoidmvlelem2.j |
. . . . . . . . . . . . . . . . . . 19
β’ π½ = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
246 | 245 | fvmpt2 7005 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) β V) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
247 | 235, 244,
246 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
248 | 247 | feq1d 6699 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((π½βπ):πβΆβ β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ):πβΆβ)) |
249 | 234, 248 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π½βπ):πβΆβ) |
250 | 31, 219 | fssresd 6755 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β ((π·βπ) βΎ π):πβΆβ) |
251 | 250 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((π·βπ) βΎ π):πβΆβ) |
252 | | iftrue 4533 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = ((π·βπ) βΎ π)) |
253 | 252 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = ((π·βπ) βΎ π)) |
254 | 253 | feq1d 6699 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ):πβΆβ β ((π·βπ) βΎ π):πβΆβ)) |
255 | 251, 254 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ):πβΆβ) |
256 | | iffalse 4536 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = πΉ) |
257 | 256 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = πΉ) |
258 | 257 | feq1d 6699 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ):πβΆβ β πΉ:πβΆβ)) |
259 | 229, 258 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ):πβΆβ) |
260 | 255, 259 | pm2.61dan 812 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ):πβΆβ) |
261 | | fvex 6901 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π·βπ) β V |
262 | 261 | resex 6027 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π·βπ) βΎ π) β V |
263 | 262 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π·βπ) βΎ π) β V) |
264 | 263, 242 | ifcld 4573 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) β V) |
265 | 264 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) β V) |
266 | | hoidmvlelem2.k |
. . . . . . . . . . . . . . . . . . 19
β’ πΎ = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
267 | 266 | fvmpt2 7005 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) β V) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
268 | 235, 265,
267 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
269 | 268 | feq1d 6699 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((πΎβπ):πβΆβ β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ):πβΆβ)) |
270 | 260, 269 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΎβπ):πβΆβ) |
271 | 161, 218,
249, 270 | hoidmvcl 45233 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((π½βπ)(πΏβπ)(πΎβπ)) β (0[,)+β)) |
272 | 217, 271 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πβπ) β (0[,)+β)) |
273 | 159, 272 | sselid 3979 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβπ) β β) |
274 | 209, 211,
273 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (πβπ) β β) |
275 | 208, 274 | remulcld 11240 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β ((π β π) Β· (πβπ)) β β) |
276 | 207, 275 | fsumrecl 15676 |
. . . . . . . . 9
β’ (π β Ξ£π β (1...π)((π β π) Β· (πβπ)) β β) |
277 | 200, 276 | remulcld 11240 |
. . . . . . . 8
β’ (π β ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ))) β β) |
278 | 206, 277 | readdcld 11239 |
. . . . . . 7
β’ (π β (((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) + ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ)))) β β) |
279 | 161, 164,
202, 7, 109, 28, 203, 204, 67 | sge0hsphoire 45240 |
. . . . . . . 8
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) |
280 | 200, 279 | remulcld 11240 |
. . . . . . 7
β’ (π β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) β β) |
281 | 74, 68 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ (π β π β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))}) |
282 | | oveq1 7411 |
. . . . . . . . . . . . 13
β’ (π§ = π β (π§ β (π΄βπ)) = (π β (π΄βπ))) |
283 | 282 | oveq2d 7420 |
. . . . . . . . . . . 12
β’ (π§ = π β (πΊ Β· (π§ β (π΄βπ))) = (πΊ Β· (π β (π΄βπ)))) |
284 | | fveq2 6888 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β (π»βπ§) = (π»βπ)) |
285 | 284 | fveq1d 6890 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β ((π»βπ§)β(π·βπ)) = ((π»βπ)β(π·βπ))) |
286 | 285 | oveq2d 7420 |
. . . . . . . . . . . . . . 15
β’ (π§ = π β ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))) = ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
287 | 286 | mpteq2dv 5249 |
. . . . . . . . . . . . . 14
β’ (π§ = π β (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) |
288 | 287 | fveq2d 6892 |
. . . . . . . . . . . . 13
β’ (π§ = π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) |
289 | 288 | oveq2d 7420 |
. . . . . . . . . . . 12
β’ (π§ = π β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) = ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
290 | 283, 289 | breq12d 5160 |
. . . . . . . . . . 11
β’ (π§ = π β ((πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) β (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
291 | 290 | elrab 3682 |
. . . . . . . . . 10
β’ (π β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β (π β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
292 | 281, 291 | sylib 217 |
. . . . . . . . 9
β’ (π β (π β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
293 | 292 | simprd 497 |
. . . . . . . 8
β’ (π β (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
294 | 207, 274 | fsumrecl 15676 |
. . . . . . . . . . 11
β’ (π β Ξ£π β (1...π)(πβπ) β β) |
295 | 200, 294 | remulcld 11240 |
. . . . . . . . . 10
β’ (π β ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) β β) |
296 | | 0red 11213 |
. . . . . . . . . . 11
β’ (π β 0 β
β) |
297 | 75, 67 | posdifd 11797 |
. . . . . . . . . . . 12
β’ (π β (π < π β 0 < (π β π))) |
298 | 144, 297 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β 0 < (π β π)) |
299 | 296, 183,
298 | ltled 11358 |
. . . . . . . . . 10
β’ (π β 0 β€ (π β π)) |
300 | | hoidmvlelem2.le |
. . . . . . . . . 10
β’ (π β πΊ β€ ((1 + πΈ) Β· Ξ£π β (1...π)(πβπ))) |
301 | 172, 295,
183, 299, 300 | lemul1ad 12149 |
. . . . . . . . 9
β’ (π β (πΊ Β· (π β π)) β€ (((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) Β· (π β π))) |
302 | 200 | recnd 11238 |
. . . . . . . . . . 11
β’ (π β (1 + πΈ) β β) |
303 | 294 | recnd 11238 |
. . . . . . . . . . 11
β’ (π β Ξ£π β (1...π)(πβπ) β β) |
304 | 302, 303,
174 | mulassd 11233 |
. . . . . . . . . 10
β’ (π β (((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) Β· (π β π)) = ((1 + πΈ) Β· (Ξ£π β (1...π)(πβπ) Β· (π β π)))) |
305 | 274 | recnd 11238 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (πβπ) β β) |
306 | 207, 174,
305 | fsummulc1 15727 |
. . . . . . . . . . . 12
β’ (π β (Ξ£π β (1...π)(πβπ) Β· (π β π)) = Ξ£π β (1...π)((πβπ) Β· (π β π))) |
307 | 174 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (π β π) β β) |
308 | 305, 307 | mulcomd 11231 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β ((πβπ) Β· (π β π)) = ((π β π) Β· (πβπ))) |
309 | 308 | sumeq2dv 15645 |
. . . . . . . . . . . 12
β’ (π β Ξ£π β (1...π)((πβπ) Β· (π β π)) = Ξ£π β (1...π)((π β π) Β· (πβπ))) |
310 | 306, 309 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β (Ξ£π β (1...π)(πβπ) Β· (π β π)) = Ξ£π β (1...π)((π β π) Β· (πβπ))) |
311 | 310 | oveq2d 7420 |
. . . . . . . . . 10
β’ (π β ((1 + πΈ) Β· (Ξ£π β (1...π)(πβπ) Β· (π β π))) = ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ)))) |
312 | 304, 311 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β (((1 + πΈ) Β· Ξ£π β (1...π)(πβπ)) Β· (π β π)) = ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ)))) |
313 | 301, 312 | breqtrd 5173 |
. . . . . . . 8
β’ (π β (πΊ Β· (π β π)) β€ ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ)))) |
314 | 192, 186,
206, 277, 293, 313 | leadd12dd 43961 |
. . . . . . 7
β’ (π β ((πΊ Β· (π β (π΄βπ))) + (πΊ Β· (π β π))) β€ (((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) + ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ))))) |
315 | | hoidmvlelem2.m |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
316 | | nnsplit 44003 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β β =
((1...π) βͺ
(β€β₯β(π + 1)))) |
317 | 315, 316 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β β = ((1...π) βͺ
(β€β₯β(π + 1)))) |
318 | | uncom 4152 |
. . . . . . . . . . . . . . . . 17
β’
((1...π) βͺ
(β€β₯β(π + 1))) =
((β€β₯β(π + 1)) βͺ (1...π)) |
319 | 318 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β ((1...π) βͺ (β€β₯β(π + 1))) =
((β€β₯β(π + 1)) βͺ (1...π))) |
320 | 317, 319 | eqtr2d 2774 |
. . . . . . . . . . . . . . 15
β’ (π β
((β€β₯β(π + 1)) βͺ (1...π)) = β) |
321 | 320 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ (π β β =
((β€β₯β(π + 1)) βͺ (1...π))) |
322 | 321 | mpteq1d 5242 |
. . . . . . . . . . . . 13
β’ (π β (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) = (π β ((β€β₯β(π + 1)) βͺ (1...π)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) |
323 | 322 | fveq2d 6892 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) =
(Ξ£^β(π β ((β€β₯β(π + 1)) βͺ (1...π)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) |
324 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²ππ |
325 | | fvexd 6903 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β(π + 1)) β V) |
326 | | ovexd 7439 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β V) |
327 | | incom 4200 |
. . . . . . . . . . . . . . 15
β’
((β€β₯β(π + 1)) β© (1...π)) = ((1...π) β© (β€β₯β(π + 1))) |
328 | | nnuzdisj 44000 |
. . . . . . . . . . . . . . 15
β’
((1...π) β©
(β€β₯β(π + 1))) = β
|
329 | 327, 328 | eqtri 2761 |
. . . . . . . . . . . . . 14
β’
((β€β₯β(π + 1)) β© (1...π)) = β
|
330 | 329 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β
((β€β₯β(π + 1)) β© (1...π)) = β
) |
331 | | icossicc 13409 |
. . . . . . . . . . . . . 14
β’
(0[,)+β) β (0[,]+β) |
332 | | ssid 4003 |
. . . . . . . . . . . . . . 15
β’
(0[,)+β) β (0[,)+β) |
333 | | simpl 484 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯β(π + 1))) β π) |
334 | 315 | peano2nnd 12225 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π + 1) β β) |
335 | | uznnssnn 12875 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π + 1) β β β
(β€β₯β(π + 1)) β β) |
336 | 334, 335 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β(π + 1)) β β) |
337 | 336 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (β€β₯β(π + 1))) β
(β€β₯β(π + 1)) β β) |
338 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (β€β₯β(π + 1))) β π β
(β€β₯β(π + 1))) |
339 | 337, 338 | sseldd 3982 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯β(π + 1))) β π β
β) |
340 | | snfi 9040 |
. . . . . . . . . . . . . . . . . . . . 21
β’ {π} β Fin |
341 | 340 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {π} β Fin) |
342 | | unfi 9168 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Fin β§ {π} β Fin) β (π βͺ {π}) β Fin) |
343 | 164, 341,
342 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π βͺ {π}) β Fin) |
344 | 7, 343 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β Fin) |
345 | 344 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β π β Fin) |
346 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (π β π β π β π)) |
347 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πβπ) = (πβπ)) |
348 | 347 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β ((πβπ) β€ π₯ β (πβπ) β€ π₯)) |
349 | 348, 347 | ifbieq1d 4551 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β if((πβπ) β€ π₯, (πβπ), π₯) = if((πβπ) β€ π₯, (πβπ), π₯)) |
350 | 346, 347,
349 | ifbieq12d 4555 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)) = if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) |
351 | 350 | cbvmptv 5260 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) = (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) |
352 | 351 | mpteq2i 5252 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) = (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) |
353 | 352 | mpteq2i 5252 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β¦ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
354 | 204, 353 | eqtri 2761 |
. . . . . . . . . . . . . . . . . 18
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
355 | 75 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π β β) |
356 | 354, 355,
345, 31 | hsphoif 45227 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β ((π»βπ)β(π·βπ)):πβΆβ) |
357 | 161, 345,
112, 356 | hoidmvcl 45233 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,)+β)) |
358 | 333, 339,
357 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯β(π + 1))) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,)+β)) |
359 | 332, 358 | sselid 3979 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯β(π + 1))) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,)+β)) |
360 | 331, 359 | sselid 3979 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯β(π + 1))) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,]+β)) |
361 | 209, 211,
357 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,)+β)) |
362 | 331, 361 | sselid 3979 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,]+β)) |
363 | 324, 325,
326, 330, 360, 362 | sge0splitmpt 45062 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β ((β€β₯β(π + 1)) βͺ (1...π)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +π
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
364 | | nnex 12214 |
. . . . . . . . . . . . . . 15
β’ β
β V |
365 | 364 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β β
V) |
366 | 331, 357 | sselid 3979 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,]+β)) |
367 | 324, 365,
366, 205, 336 | sge0ssrempt 45056 |
. . . . . . . . . . . . 13
β’ (π β
(Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) |
368 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β β) |
369 | 324, 365,
366, 205, 368 | sge0ssrempt 45056 |
. . . . . . . . . . . . 13
β’ (π β
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) |
370 | | rexadd 13207 |
. . . . . . . . . . . . 13
β’
(((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β β§
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +π
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
371 | 367, 369,
370 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +π
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
372 | 323, 363,
371 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
373 | 372 | oveq2d 7420 |
. . . . . . . . . 10
β’ (π β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) = ((1 + πΈ) Β·
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
374 | 373 | oveq1d 7419 |
. . . . . . . . 9
β’ (π β (((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) + ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ)))) = (((1 + πΈ) Β·
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) + ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ))))) |
375 | 372, 205 | eqeltrrd 2835 |
. . . . . . . . . . . 12
β’ (π β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) β β) |
376 | 375 | recnd 11238 |
. . . . . . . . . . 11
β’ (π β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) β β) |
377 | 276 | recnd 11238 |
. . . . . . . . . . 11
β’ (π β Ξ£π β (1...π)((π β π) Β· (πβπ)) β β) |
378 | 302, 376,
377 | adddid 11234 |
. . . . . . . . . 10
β’ (π β ((1 + πΈ) Β·
(((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) + Ξ£π β (1...π)((π β π) Β· (πβπ)))) = (((1 + πΈ) Β·
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) + ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ))))) |
379 | 378 | eqcomd 2739 |
. . . . . . . . 9
β’ (π β (((1 + πΈ) Β·
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) + ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ)))) = ((1 + πΈ) Β·
(((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) + Ξ£π β (1...π)((π β π) Β· (πβπ))))) |
380 | 367 | recnd 11238 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) |
381 | 369 | recnd 11238 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) |
382 | 380, 381,
377 | addassd 11232 |
. . . . . . . . . . 11
β’ (π β
(((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) + Ξ£π β (1...π)((π β π) Β· (πβπ))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
((Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)((π β π) Β· (πβπ))))) |
383 | 207, 361 | sge0fsummpt 45041 |
. . . . . . . . . . . . . 14
β’ (π β
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) = Ξ£π β (1...π)((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
384 | 383 | oveq1d 7419 |
. . . . . . . . . . . . 13
β’ (π β
((Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)((π β π) Β· (πβπ))) = (Ξ£π β (1...π)((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + Ξ£π β (1...π)((π β π) Β· (πβπ)))) |
385 | | ax-resscn 11163 |
. . . . . . . . . . . . . . . . . 18
β’ β
β β |
386 | 159, 385 | sstri 3990 |
. . . . . . . . . . . . . . . . 17
β’
(0[,)+β) β β |
387 | 386, 357 | sselid 3979 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β β) |
388 | 209, 211,
387 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β β) |
389 | 183 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π β π) β β) |
390 | 389, 273 | remulcld 11240 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β ((π β π) Β· (πβπ)) β β) |
391 | 390 | recnd 11238 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((π β π) Β· (πβπ)) β β) |
392 | 211, 391 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((π β π) Β· (πβπ)) β β) |
393 | 207, 388,
392 | fsumadd 15682 |
. . . . . . . . . . . . . 14
β’ (π β Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) = (Ξ£π β (1...π)((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + Ξ£π β (1...π)((π β π) Β· (πβπ)))) |
394 | 393 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ (π β (Ξ£π β (1...π)((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + Ξ£π β (1...π)((π β π) Β· (πβπ))) = Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ)))) |
395 | 384, 394 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β
((Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)((π β π) Β· (πβπ))) = Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ)))) |
396 | 395 | oveq2d 7420 |
. . . . . . . . . . 11
β’ (π β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
((Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)((π β π) Β· (πβπ)))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))))) |
397 | 382, 396 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β
(((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) + Ξ£π β (1...π)((π β π) Β· (πβπ))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))))) |
398 | 397 | oveq2d 7420 |
. . . . . . . . 9
β’ (π β ((1 + πΈ) Β·
(((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) + Ξ£π β (1...π)((π β π) Β· (πβπ)))) = ((1 + πΈ) Β·
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ)))))) |
399 | 374, 379,
398 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β (((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) + ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ)))) = ((1 + πΈ) Β·
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ)))))) |
400 | 159, 357 | sselid 3979 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β β) |
401 | 400, 390 | readdcld 11239 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) β β) |
402 | 209, 211,
401 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) β β) |
403 | 207, 402 | fsumrecl 15676 |
. . . . . . . . . 10
β’ (π β Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) β β) |
404 | 367, 403 | readdcld 11239 |
. . . . . . . . 9
β’ (π β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ)))) β β) |
405 | | 0le1 11733 |
. . . . . . . . . . 11
β’ 0 β€
1 |
406 | 405 | a1i 11 |
. . . . . . . . . 10
β’ (π β 0 β€ 1) |
407 | 198 | rpge0d 13016 |
. . . . . . . . . 10
β’ (π β 0 β€ πΈ) |
408 | 197, 199,
406, 407 | addge0d 11786 |
. . . . . . . . 9
β’ (π β 0 β€ (1 + πΈ)) |
409 | 67 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β β) |
410 | 354, 409,
345, 31 | hsphoif 45227 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((π»βπ)β(π·βπ)):πβΆβ) |
411 | 161, 345,
112, 410 | hoidmvcl 45233 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,)+β)) |
412 | 331, 411 | sselid 3979 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,]+β)) |
413 | 324, 365,
412, 279, 336 | sge0ssrempt 45056 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) |
414 | 159, 411 | sselid 3979 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β β) |
415 | 209, 211,
414 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β β) |
416 | 207, 415 | fsumrecl 15676 |
. . . . . . . . . . 11
β’ (π β Ξ£π β (1...π)((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β β) |
417 | 333, 339,
412 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯β(π + 1))) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,]+β)) |
418 | 202 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β (π β π)) |
419 | 75, 67, 144 | ltled 11358 |
. . . . . . . . . . . . . . 15
β’ (π β π β€ π) |
420 | 419 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β€ π) |
421 | 161, 345,
418, 7, 355, 409, 420, 354, 112, 31 | hsphoidmvle2 45236 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β€ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
422 | 333, 339,
421 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯β(π + 1))) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β€ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
423 | 324, 325,
360, 417, 422 | sge0lempt 45061 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β€
(Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) |
424 | 209 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...π)) β§ (πβπ) = 0) β π) |
425 | 211 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...π)) β§ (πβπ) = 0) β π β β) |
426 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...π)) β§ (πβπ) = 0) β (πβπ) = 0) |
427 | | oveq2 7412 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ) = 0 β ((π β π) Β· (πβπ)) = ((π β π) Β· 0)) |
428 | 427 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (πβπ) = 0) β ((π β π) Β· (πβπ)) = ((π β π) Β· 0)) |
429 | 174 | mul01d 11409 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π β π) Β· 0) = 0) |
430 | 429 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (πβπ) = 0) β ((π β π) Β· 0) = 0) |
431 | 428, 430 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (πβπ) = 0) β ((π β π) Β· (πβπ)) = 0) |
432 | 431 | oveq2d 7420 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (πβπ) = 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) = (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + 0)) |
433 | 387 | addridd 11410 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + 0) = ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
434 | 433 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (πβπ) = 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + 0) = ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
435 | 432, 434 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (πβπ) = 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) = ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
436 | 421 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (πβπ) = 0) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β€ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
437 | 435, 436 | eqbrtrd 5169 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ (πβπ) = 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) β€ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
438 | 424, 425,
426, 437 | syl21anc 837 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ (πβπ) = 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) β€ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
439 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...π)) β§ Β¬ (πβπ) = 0) β (π β§ π β (1...π))) |
440 | | neqne 2949 |
. . . . . . . . . . . . . . 15
β’ (Β¬
(πβπ) = 0 β (πβπ) β 0) |
441 | 440 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...π)) β§ Β¬ (πβπ) = 0) β (πβπ) β 0) |
442 | 402 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) β β) |
443 | 209 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π) |
444 | 211 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π β β) |
445 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (πβπ) β 0) |
446 | 2 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β π β (π β π)) |
447 | 201 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β Β¬ π β π) |
448 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
βπ β
π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) |
449 | 161, 218,
446, 447, 7, 112, 356, 448 | hoiprodp1 45239 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) = (βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) Β· (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))))) |
450 | 449 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) = (βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) Β· (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))))) |
451 | 217 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ (πβπ) β 0) β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
452 | 218 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ (πβπ) β 0) β π β Fin) |
453 | 217 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ π = β
) β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
454 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = β
β (πΏβπ) = (πΏββ
)) |
455 | 454 | oveqd 7421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = β
β ((π½βπ)(πΏβπ)(πΎβπ)) = ((π½βπ)(πΏββ
)(πΎβπ))) |
456 | 455 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ π = β
) β ((π½βπ)(πΏβπ)(πΎβπ)) = ((π½βπ)(πΏββ
)(πΎβπ))) |
457 | 249 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ π = β
) β (π½βπ):πβΆβ) |
458 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = β
β π = β
) |
459 | 458 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = β
β β
=
π) |
460 | 459 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π β β) β§ π = β
) β β
= π) |
461 | 460 | feq2d 6700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ π = β
) β ((π½βπ):β
βΆβ β (π½βπ):πβΆβ)) |
462 | 457, 461 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ π = β
) β (π½βπ):β
βΆβ) |
463 | 270 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ π = β
) β (πΎβπ):πβΆβ) |
464 | 460 | feq2d 6700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ π = β
) β ((πΎβπ):β
βΆβ β (πΎβπ):πβΆβ)) |
465 | 463, 464 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ π = β
) β (πΎβπ):β
βΆβ) |
466 | 161, 462,
465 | hoidmv0val 45234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ π = β
) β ((π½βπ)(πΏββ
)(πΎβπ)) = 0) |
467 | 453, 456,
466 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β β) β§ π = β
) β (πβπ) = 0) |
468 | 467 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ π = β
) β (πβπ) = 0) |
469 | | neneq 2947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πβπ) β 0 β Β¬ (πβπ) = 0) |
470 | 469 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ π = β
) β Β¬ (πβπ) = 0) |
471 | 468, 470 | pm2.65da 816 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ (πβπ) β 0) β Β¬ π = β
) |
472 | 471 | neqned 2948 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ (πβπ) β 0) β π β β
) |
473 | 249 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ (πβπ) β 0) β (π½βπ):πβΆβ) |
474 | 270 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ (πβπ) β 0) β (πΎβπ):πβΆβ) |
475 | 161, 452,
472, 473, 474 | hoidmvn0val 45235 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((π½βπ)(πΏβπ)(πΎβπ)) = βπ β π (volβ(((π½βπ)βπ)[,)((πΎβπ)βπ)))) |
476 | 247 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ (πβπ) β 0) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
477 | 217 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (πβπ) = ((π½βπ)(πΏβπ)(πΎβπ))) |
478 | 247 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π½βπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ)) |
479 | 478, 231 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π½βπ) = πΉ) |
480 | 268 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
481 | 480, 257 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (πΎβπ) = πΉ) |
482 | 479, 481 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((π½βπ)(πΏβπ)(πΎβπ)) = (πΉ(πΏβπ)πΉ)) |
483 | 161, 164,
228 | hoidmvval0b 45241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β (πΉ(πΏβπ)πΉ) = 0) |
484 | 483 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (πΉ(πΏβπ)πΉ) = 0) |
485 | 477, 482,
484 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π β β) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (πβπ) = 0) |
486 | 485 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (πβπ) = 0) |
487 | 469 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β Β¬ (πβπ) = 0) |
488 | 486, 487 | condan 817 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π β β) β§ (πβπ) β 0) β π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
489 | 488 | iftrued 4535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ (πβπ) β 0) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), πΉ) = ((πΆβπ) βΎ π)) |
490 | 476, 489 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ (πβπ) β 0) β (π½βπ) = ((πΆβπ) βΎ π)) |
491 | 490 | fveq1d 6890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((π½βπ)βπ) = (((πΆβπ) βΎ π)βπ)) |
492 | 491 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ π β π) β ((π½βπ)βπ) = (((πΆβπ) βΎ π)βπ)) |
493 | | fvres 6907 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β (((πΆβπ) βΎ π)βπ) = ((πΆβπ)βπ)) |
494 | 493 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ π β π) β (((πΆβπ) βΎ π)βπ) = ((πΆβπ)βπ)) |
495 | 492, 494 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ π β π) β ((π½βπ)βπ) = ((πΆβπ)βπ)) |
496 | 268 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ (πβπ) β 0) β (πΎβπ) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ)) |
497 | 488, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ (πβπ) β 0) β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), πΉ) = ((π·βπ) βΎ π)) |
498 | 496, 497 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ (πβπ) β 0) β (πΎβπ) = ((π·βπ) βΎ π)) |
499 | 498 | fveq1d 6890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((πΎβπ)βπ) = (((π·βπ) βΎ π)βπ)) |
500 | 499 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ π β π) β ((πΎβπ)βπ) = (((π·βπ) βΎ π)βπ)) |
501 | | fvres 6907 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β (((π·βπ) βΎ π)βπ) = ((π·βπ)βπ)) |
502 | 501 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ π β π) β (((π·βπ) βΎ π)βπ) = ((π·βπ)βπ)) |
503 | 500, 502 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ π β π) β ((πΎβπ)βπ) = ((π·βπ)βπ)) |
504 | 495, 503 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ π β π) β (((π½βπ)βπ)[,)((πΎβπ)βπ)) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
505 | 504 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ π β π) β (volβ(((π½βπ)βπ)[,)((πΎβπ)βπ))) = (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
506 | 505 | prodeq2dv 15863 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β) β§ (πβπ) β 0) β βπ β π (volβ(((π½βπ)βπ)[,)((πΎβπ)βπ))) = βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
507 | 475, 506 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((π½βπ)(πΏβπ)(πΎβπ)) = βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
508 | 355 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ π β π) β π β β) |
509 | 345 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ π β π) β π β Fin) |
510 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ π β π) β (π·βπ):πβΆβ) |
511 | | elun1 4175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β π β π β (π βͺ {π})) |
512 | 511, 7 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β π β π β π) |
513 | 512 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ π β π) β π β π) |
514 | 354, 508,
509, 510, 513 | hsphoival 45230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ π β π) β (((π»βπ)β(π·βπ))βπ) = if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
515 | | iftrue 4533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = ((π·βπ)βπ)) |
516 | 515 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ π β π) β if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = ((π·βπ)βπ)) |
517 | 514, 516 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β β) β§ π β π) β (((π»βπ)β(π·βπ))βπ) = ((π·βπ)βπ)) |
518 | 517 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ π β π) β (((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ)) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
519 | 518 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π β π) β (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
520 | 519 | prodeq2dv 15863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
521 | 520 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ))) = βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ)))) |
522 | 521 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ (πβπ) β 0) β βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ))) = βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ)))) |
523 | 451, 507,
522 | 3eqtrrd 2778 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ (πβπ) β 0) β βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = (πβπ)) |
524 | 354, 355,
345, 31, 32 | hsphoival 45230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β β) β (((π»βπ)β(π·βπ))βπ) = if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
525 | 201 | iffalsed 4538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) |
526 | 525 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β β) β if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) |
527 | 524, 526 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β β) β (((π»βπ)β(π·βπ))βπ) = if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) |
528 | 527 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β (((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ)) = (((πΆβπ)βπ)[,)if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
529 | 528 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ (πβπ) β 0) β (((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ)) = (((πΆβπ)βπ)[,)if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
530 | 113 | rexrd 11260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π β β) β ((πΆβπ)βπ) β
β*) |
531 | 530 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((πΆβπ)βπ) β
β*) |
532 | 33 | rexrd 11260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π β β) β ((π·βπ)βπ) β
β*) |
533 | 532 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((π·βπ)βπ) β
β*) |
534 | | icoltub 44156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((πΆβπ)βπ) β β* β§ ((π·βπ)βπ) β β* β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π < ((π·βπ)βπ)) |
535 | 531, 533,
488, 534 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β β) β§ (πβπ) β 0) β π < ((π·βπ)βπ)) |
536 | 355 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ (πβπ) β 0) β π β β) |
537 | 33 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((π·βπ)βπ) β β) |
538 | 536, 537 | ltnled 11357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β β) β§ (πβπ) β 0) β (π < ((π·βπ)βπ) β Β¬ ((π·βπ)βπ) β€ π)) |
539 | 535, 538 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ (πβπ) β 0) β Β¬ ((π·βπ)βπ) β€ π) |
540 | 539 | iffalsed 4538 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ (πβπ) β 0) β if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π) = π) |
541 | 540 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ (πβπ) β 0) β (((πΆβπ)βπ)[,)if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = (((πΆβπ)βπ)[,)π)) |
542 | 529, 541 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β) β§ (πβπ) β 0) β (((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ)) = (((πΆβπ)βπ)[,)π)) |
543 | 542 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ (πβπ) β 0) β (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = (volβ(((πΆβπ)βπ)[,)π))) |
544 | | volico 44634 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΆβπ)βπ) β β β§ π β β) β (volβ(((πΆβπ)βπ)[,)π)) = if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0)) |
545 | 113, 536,
544 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β) β§ ((π β§ π β β) β§ (πβπ) β 0)) β (volβ(((πΆβπ)βπ)[,)π)) = if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0)) |
546 | 545 | anabss5 667 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ (πβπ) β 0) β (volβ(((πΆβπ)βπ)[,)π)) = if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0)) |
547 | | iftrue 4533 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΆβπ)βπ) < π β if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0) = (π β ((πΆβπ)βπ))) |
548 | 547 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ ((πΆβπ)βπ) < π) β if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0) = (π β ((πΆβπ)βπ))) |
549 | | iffalse 4536 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (Β¬
((πΆβπ)βπ) < π β if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0) = 0) |
550 | 549 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0) = 0) |
551 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β (π β§ π β β)) |
552 | | icogelb 13371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((πΆβπ)βπ) β β* β§ ((π·βπ)βπ) β β* β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((πΆβπ)βπ) β€ π) |
553 | 531, 533,
488, 552 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((πΆβπ)βπ) β€ π) |
554 | 553 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β ((πΆβπ)βπ) β€ π) |
555 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β Β¬ ((πΆβπ)βπ) < π) |
556 | 554, 555 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β (((πΆβπ)βπ) β€ π β§ Β¬ ((πΆβπ)βπ) < π)) |
557 | 551, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β ((πΆβπ)βπ) β β) |
558 | 551, 355 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β π β β) |
559 | 557, 558 | eqleltd 11354 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β (((πΆβπ)βπ) = π β (((πΆβπ)βπ) β€ π β§ Β¬ ((πΆβπ)βπ) < π))) |
560 | 556, 559 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β ((πΆβπ)βπ) = π) |
561 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((πΆβπ)βπ) = π β ((πΆβπ)βπ) = π) |
562 | 561 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πΆβπ)βπ) = π β π = ((πΆβπ)βπ)) |
563 | 562 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΆβπ)βπ) = π β (π β ((πΆβπ)βπ)) = (((πΆβπ)βπ) β ((πΆβπ)βπ))) |
564 | 563 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ ((πΆβπ)βπ) = π) β (π β ((πΆβπ)βπ)) = (((πΆβπ)βπ) β ((πΆβπ)βπ))) |
565 | 385, 113 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β β) β ((πΆβπ)βπ) β β) |
566 | 565 | subidd 11555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β β) β (((πΆβπ)βπ) β ((πΆβπ)βπ)) = 0) |
567 | 566 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ ((πΆβπ)βπ) = π) β (((πΆβπ)βπ) β ((πΆβπ)βπ)) = 0) |
568 | 564, 567 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ ((πΆβπ)βπ) = π) β 0 = (π β ((πΆβπ)βπ))) |
569 | 551, 560,
568 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β 0 = (π β ((πΆβπ)βπ))) |
570 | 550, 569 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ (πβπ) β 0) β§ Β¬ ((πΆβπ)βπ) < π) β if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0) = (π β ((πΆβπ)βπ))) |
571 | 548, 570 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ (πβπ) β 0) β if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0) = (π β ((πΆβπ)βπ))) |
572 | 543, 546,
571 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ (πβπ) β 0) β (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = (π β ((πΆβπ)βπ))) |
573 | 523, 572 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (πβπ) β 0) β (βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) Β· (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ)))) = ((πβπ) Β· (π β ((πΆβπ)βπ)))) |
574 | 386, 272 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β (πβπ) β β) |
575 | 355, 113 | resubcld 11638 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β (π β ((πΆβπ)βπ)) β β) |
576 | 575 | recnd 11238 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β (π β ((πΆβπ)βπ)) β β) |
577 | 574, 576 | mulcomd 11231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β ((πβπ) Β· (π β ((πΆβπ)βπ))) = ((π β ((πΆβπ)βπ)) Β· (πβπ))) |
578 | 577 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((πβπ) Β· (π β ((πΆβπ)βπ))) = ((π β ((πΆβπ)βπ)) Β· (πβπ))) |
579 | 450, 573,
578 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (πβπ) β 0) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) = ((π β ((πΆβπ)βπ)) Β· (πβπ))) |
580 | 579 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (πβπ) β 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) = (((π β ((πΆβπ)βπ)) Β· (πβπ)) + ((π β π) Β· (πβπ)))) |
581 | 174 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β (π β π) β β) |
582 | 576, 581,
574 | adddird 11235 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β (((π β ((πΆβπ)βπ)) + (π β π)) Β· (πβπ)) = (((π β ((πΆβπ)βπ)) Β· (πβπ)) + ((π β π) Β· (πβπ)))) |
583 | 582 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (((π β ((πΆβπ)βπ)) Β· (πβπ)) + ((π β π) Β· (πβπ))) = (((π β ((πΆβπ)βπ)) + (π β π)) Β· (πβπ))) |
584 | 583 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (πβπ) β 0) β (((π β ((πΆβπ)βπ)) Β· (πβπ)) + ((π β π) Β· (πβπ))) = (((π β ((πΆβπ)βπ)) + (π β π)) Β· (πβπ))) |
585 | 576, 581 | addcomd 11412 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β ((π β ((πΆβπ)βπ)) + (π β π)) = ((π β π) + (π β ((πΆβπ)βπ)))) |
586 | 153 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β π β β) |
587 | 154 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β π β β) |
588 | 586, 587,
565 | npncand 11591 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β ((π β π) + (π β ((πΆβπ)βπ))) = (π β ((πΆβπ)βπ))) |
589 | 585, 588 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β ((π β ((πΆβπ)βπ)) + (π β π)) = (π β ((πΆβπ)βπ))) |
590 | 589 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (((π β ((πΆβπ)βπ)) + (π β π)) Β· (πβπ)) = ((π β ((πΆβπ)βπ)) Β· (πβπ))) |
591 | 590 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (πβπ) β 0) β (((π β ((πΆβπ)βπ)) + (π β π)) Β· (πβπ)) = ((π β ((πΆβπ)βπ)) Β· (πβπ))) |
592 | 580, 584,
591 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (πβπ) β 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) = ((π β ((πΆβπ)βπ)) Β· (πβπ))) |
593 | 443, 444,
445, 592 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) = ((π β ((πΆβπ)βπ)) Β· (πβπ))) |
594 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’
βπ β
π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) |
595 | 161, 218,
32, 447, 7, 112, 410, 594 | hoiprodp1 45239 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) = (βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) Β· (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))))) |
596 | 209, 211,
595 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) = (βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) Β· (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))))) |
597 | 596 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) = (βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) Β· (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))))) |
598 | 507 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (πβπ) β 0) β βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ))) = ((π½βπ)(πΏβπ)(πΎβπ))) |
599 | 409 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ π β π) β π β β) |
600 | 354, 599,
509, 510, 513 | hsphoival 45230 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π β π) β (((π»βπ)β(π·βπ))βπ) = if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
601 | | iftrue 4533 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = ((π·βπ)βπ)) |
602 | 601 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π β π) β if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = ((π·βπ)βπ)) |
603 | 600, 602 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ π β π) β (((π»βπ)β(π·βπ))βπ) = ((π·βπ)βπ)) |
604 | 603 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β) β§ π β π) β (((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ)) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
605 | 604 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β π) β (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
606 | 605 | prodeq2dv 15863 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
607 | 606 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (πβπ) β 0) β βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
608 | 598, 607,
451 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (πβπ) β 0) β βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = (πβπ)) |
609 | 443, 444,
445, 608 | syl21anc 837 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = (πβπ)) |
610 | 354, 409,
345, 31, 32 | hsphoival 45230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β (((π»βπ)β(π·βπ))βπ) = if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
611 | 211, 610 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (1...π)) β (((π»βπ)β(π·βπ))βπ) = if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
612 | 611 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (((π»βπ)β(π·βπ))βπ) = if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
613 | 201 | iffalsed 4538 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) |
614 | 613 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β if(π β π, ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) |
615 | 211, 33 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β (1...π)) β ((π·βπ)βπ) β β) |
616 | 615 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (1...π)) β§ ((π·βπ)βπ) = π) β ((π·βπ)βπ) β β) |
617 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (1...π)) β§ ((π·βπ)βπ) = π) β ((π·βπ)βπ) = π) |
618 | 616, 617 | eqled 11313 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (1...π)) β§ ((π·βπ)βπ) = π) β ((π·βπ)βπ) β€ π) |
619 | 618 | iftrued 4535 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (1...π)) β§ ((π·βπ)βπ) = π) β if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π) = ((π·βπ)βπ)) |
620 | 619, 617 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β (1...π)) β§ ((π·βπ)βπ) = π) β if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π) = π) |
621 | 620 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (1...π)) β§ (πβπ) β 0) β§ ((π·βπ)βπ) = π) β if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π) = π) |
622 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β (1...π)) β π β β) |
623 | 622 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (1...π)) β§ Β¬ ((π·βπ)βπ) = π) β π β β) |
624 | 623 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β (1...π)) β§ (πβπ) β 0) β§ Β¬ ((π·βπ)βπ) = π) β π β β) |
625 | 615 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (1...π)) β§ Β¬ ((π·βπ)βπ) = π) β ((π·βπ)βπ) β β) |
626 | 625 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β (1...π)) β§ (πβπ) β 0) β§ Β¬ ((π·βπ)βπ) = π) β ((π·βπ)βπ) β β) |
627 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π = inf(π, β, < )) |
628 | 443, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π β β) |
629 | 148 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β βπ₯ β π βπ¦ β π π₯ β€ π¦) |
630 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π β (1...π)) |
631 | 210, 488 | sylanl2 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
632 | 630, 631 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (π β (1...π) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
633 | | rabid 3453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β (π β (1...π) β§ π β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
634 | 632, 633 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))}) |
635 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((π·βπ)βπ) = ((π·βπ)βπ)) |
636 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π = π β (π·βπ) = (π·βπ)) |
637 | 636 | fveq1d 6890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π = π β ((π·βπ)βπ) = ((π·βπ)βπ)) |
638 | 637 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π β (((π·βπ)βπ) = ((π·βπ)βπ) β ((π·βπ)βπ) = ((π·βπ)βπ))) |
639 | 638 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β§ ((π·βπ)βπ) = ((π·βπ)βπ)) β βπ β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} ((π·βπ)βπ) = ((π·βπ)βπ)) |
640 | 634, 635,
639 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β βπ β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} ((π·βπ)βπ) = ((π·βπ)βπ)) |
641 | | fvexd 6903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((π·βπ)βπ) β V) |
642 | 16, 640, 641 | elrnmptd 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((π·βπ)βπ) β ran (π β {π β (1...π) β£ π β (((πΆβπ)βπ)[,)((π·βπ)βπ))} β¦ ((π·βπ)βπ))) |
643 | 642, 14 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((π·βπ)βπ) β π) |
644 | | elun2 4176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π·βπ)βπ) β π β ((π·βπ)βπ) β ({(π΅βπ)} βͺ π)) |
645 | 643, 644 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((π·βπ)βπ) β ({(π΅βπ)} βͺ π)) |
646 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ({(π΅βπ)} βͺ π) = π) |
647 | 645, 646 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((π·βπ)βπ) β π) |
648 | | lbinfle 12165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β β§
βπ₯ β π βπ¦ β π π₯ β€ π¦ β§ ((π·βπ)βπ) β π) β inf(π, β, < ) β€ ((π·βπ)βπ)) |
649 | 628, 629,
647, 648 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β inf(π, β, < ) β€ ((π·βπ)βπ)) |
650 | 627, 649 | eqbrtrd 5169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π β€ ((π·βπ)βπ)) |
651 | 650 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β (1...π)) β§ (πβπ) β 0) β§ Β¬ ((π·βπ)βπ) = π) β π β€ ((π·βπ)βπ)) |
652 | | neqne 2949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (Β¬
((π·βπ)βπ) = π β ((π·βπ)βπ) β π) |
653 | 652 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β (1...π)) β§ (πβπ) β 0) β§ Β¬ ((π·βπ)βπ) = π) β ((π·βπ)βπ) β π) |
654 | 624, 626,
651, 653 | leneltd 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β (1...π)) β§ (πβπ) β 0) β§ Β¬ ((π·βπ)βπ) = π) β π < ((π·βπ)βπ)) |
655 | 624, 626 | ltnled 11357 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β (1...π)) β§ (πβπ) β 0) β§ Β¬ ((π·βπ)βπ) = π) β (π < ((π·βπ)βπ) β Β¬ ((π·βπ)βπ) β€ π)) |
656 | 654, 655 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (1...π)) β§ (πβπ) β 0) β§ Β¬ ((π·βπ)βπ) = π) β Β¬ ((π·βπ)βπ) β€ π) |
657 | 656 | iffalsed 4538 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (1...π)) β§ (πβπ) β 0) β§ Β¬ ((π·βπ)βπ) = π) β if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π) = π) |
658 | 621, 657 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π) = π) |
659 | 612, 614,
658 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (((π»βπ)β(π·βπ))βπ) = π) |
660 | 659 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ)) = (((πΆβπ)βπ)[,)π)) |
661 | 660 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = (volβ(((πΆβπ)βπ)[,)π))) |
662 | 209, 211,
113 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (1...π)) β ((πΆβπ)βπ) β β) |
663 | 662 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((πΆβπ)βπ) β β) |
664 | 443, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π β β) |
665 | | volico 44634 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΆβπ)βπ) β β β§ π β β) β (volβ(((πΆβπ)βπ)[,)π)) = if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0)) |
666 | 663, 664,
665 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (volβ(((πΆβπ)βπ)[,)π)) = if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0)) |
667 | 443, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π β β) |
668 | 443, 444,
445, 553 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((πΆβπ)βπ) β€ π) |
669 | 443, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β π < π) |
670 | 663, 667,
664, 668, 669 | lelttrd 11368 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((πΆβπ)βπ) < π) |
671 | 670 | iftrued 4535 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β if(((πΆβπ)βπ) < π, (π β ((πΆβπ)βπ)), 0) = (π β ((πΆβπ)βπ))) |
672 | 661, 666,
671 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) = (π β ((πΆβπ)βπ))) |
673 | 609, 672 | oveq12d 7422 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (βπ β π (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ))) Β· (volβ(((πΆβπ)βπ)[,)(((π»βπ)β(π·βπ))βπ)))) = ((πβπ) Β· (π β ((πΆβπ)βπ)))) |
674 | 209, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (1...π)) β π β β) |
675 | 385, 662 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (1...π)) β ((πΆβπ)βπ) β β) |
676 | 674, 675 | subcld 11567 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (1...π)) β (π β ((πΆβπ)βπ)) β β) |
677 | 305, 676 | mulcomd 11231 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β ((πβπ) Β· (π β ((πΆβπ)βπ))) = ((π β ((πΆβπ)βπ)) Β· (πβπ))) |
678 | 677 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((πβπ) Β· (π β ((πΆβπ)βπ))) = ((π β ((πΆβπ)βπ)) Β· (πβπ))) |
679 | 597, 673,
678 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) = ((π β ((πΆβπ)βπ)) Β· (πβπ))) |
680 | 593, 679 | eqtr4d 2776 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) = ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
681 | 442, 680 | eqled 11313 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...π)) β§ (πβπ) β 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) β€ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
682 | 439, 441,
681 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ Β¬ (πβπ) = 0) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) β€ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
683 | 438, 682 | pm2.61dan 812 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) β€ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
684 | 207, 402,
415, 683 | fsumle 15741 |
. . . . . . . . . . 11
β’ (π β Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))) β€ Ξ£π β (1...π)((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
685 | 367, 403,
413, 416, 423, 684 | leadd12dd 43961 |
. . . . . . . . . 10
β’ (π β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ)))) β€
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) |
686 | 321 | mpteq1d 5242 |
. . . . . . . . . . . . 13
β’ (π β (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) = (π β ((β€β₯β(π + 1)) βͺ (1...π)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) |
687 | 686 | fveq2d 6892 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) =
(Ξ£^β(π β ((β€β₯β(π + 1)) βͺ (1...π)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) |
688 | 211, 412 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,]+β)) |
689 | 324, 325,
326, 330, 417, 688 | sge0splitmpt 45062 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β ((β€β₯β(π + 1)) βͺ (1...π)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +π
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
690 | 687, 689 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +π
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
691 | 209, 211,
411 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) β (0[,)+β)) |
692 | 207, 691 | sge0fsummpt 45041 |
. . . . . . . . . . . . 13
β’ (π β
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) = Ξ£π β (1...π)((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
693 | 692, 416 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) |
694 | | rexadd 13207 |
. . . . . . . . . . . 12
β’
(((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β β§
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) β β) β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +π
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
695 | 413, 693,
694 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +π
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
696 | 692 | oveq2d 7420 |
. . . . . . . . . . 11
β’ (π β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) +
(Ξ£^β(π β (1...π) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) =
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) |
697 | 690, 695,
696 | 3eqtrrd 2778 |
. . . . . . . . . 10
β’ (π β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) |
698 | 685, 697 | breqtrd 5173 |
. . . . . . . . 9
β’ (π β
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ)))) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) |
699 | 404, 279,
200, 408, 698 | lemul2ad 12150 |
. . . . . . . 8
β’ (π β ((1 + πΈ) Β·
((Ξ£^β(π β (β€β₯β(π + 1)) β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) + Ξ£π β (1...π)(((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))) + ((π β π) Β· (πβπ))))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
700 | 399, 699 | eqbrtrd 5169 |
. . . . . . 7
β’ (π β (((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) + ((1 + πΈ) Β· Ξ£π β (1...π)((π β π) Β· (πβπ)))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
701 | 196, 278,
280, 314, 700 | letrd 11367 |
. . . . . 6
β’ (π β ((πΊ Β· (π β (π΄βπ))) + (πΊ Β· (π β π))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
702 | 180, 701 | eqbrtrd 5169 |
. . . . 5
β’ (π β (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
703 | 152, 702 | jca 513 |
. . . 4
β’ (π β (π β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
704 | | oveq1 7411 |
. . . . . . 7
β’ (π§ = π β (π§ β (π΄βπ)) = (π β (π΄βπ))) |
705 | 704 | oveq2d 7420 |
. . . . . 6
β’ (π§ = π β (πΊ Β· (π§ β (π΄βπ))) = (πΊ Β· (π β (π΄βπ)))) |
706 | | fveq2 6888 |
. . . . . . . . . . 11
β’ (π§ = π β (π»βπ§) = (π»βπ)) |
707 | 706 | fveq1d 6890 |
. . . . . . . . . 10
β’ (π§ = π β ((π»βπ§)β(π·βπ)) = ((π»βπ)β(π·βπ))) |
708 | 707 | oveq2d 7420 |
. . . . . . . . 9
β’ (π§ = π β ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))) = ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))) |
709 | 708 | mpteq2dv 5249 |
. . . . . . . 8
β’ (π§ = π β (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))) |
710 | 709 | fveq2d 6892 |
. . . . . . 7
β’ (π§ = π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))) |
711 | 710 | oveq2d 7420 |
. . . . . 6
β’ (π§ = π β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) = ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ))))))) |
712 | 705, 711 | breq12d 5160 |
. . . . 5
β’ (π§ = π β ((πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) β (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
713 | 712 | elrab 3682 |
. . . 4
β’ (π β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β (π β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· (π β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ)β(π·βπ)))))))) |
714 | 703, 713 | sylibr 233 |
. . 3
β’ (π β π β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))}) |
715 | 714, 68 | eleqtrrdi 2845 |
. 2
β’ (π β π β π) |
716 | | breq2 5151 |
. . 3
β’ (π’ = π β (π < π’ β π < π)) |
717 | 716 | rspcev 3612 |
. 2
β’ ((π β π β§ π < π) β βπ’ β π π < π’) |
718 | 715, 144,
717 | syl2anc 585 |
1
β’ (π β βπ’ β π π < π’) |