Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . 5
β’
β²π π |
2 | | nfre1 3267 |
. . . . 5
β’
β²π βπ β π (π΅βπ ) β€ (π΄βπ ) |
3 | 1, 2 | nfan 1903 |
. . . 4
β’
β²π (π β§ βπ β π (π΅βπ ) β€ (π΄βπ )) |
4 | | hoidmvlelem5.l |
. . . 4
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
5 | | hoidmvlelem5.w |
. . . . . 6
β’ π = (π βͺ {π}) |
6 | | hoidmvlelem5.f |
. . . . . . . 8
β’ (π β π β Fin) |
7 | | hoidmvlelem5.y |
. . . . . . . 8
β’ (π β π β π) |
8 | | ssfi 9123 |
. . . . . . . 8
β’ ((π β Fin β§ π β π) β π β Fin) |
9 | 6, 7, 8 | syl2anc 585 |
. . . . . . 7
β’ (π β π β Fin) |
10 | | snfi 8994 |
. . . . . . . 8
β’ {π} β Fin |
11 | 10 | a1i 11 |
. . . . . . 7
β’ (π β {π} β Fin) |
12 | | unfi 9122 |
. . . . . . 7
β’ ((π β Fin β§ {π} β Fin) β (π βͺ {π}) β Fin) |
13 | 9, 11, 12 | syl2anc 585 |
. . . . . 6
β’ (π β (π βͺ {π}) β Fin) |
14 | 5, 13 | eqeltrid 2838 |
. . . . 5
β’ (π β π β Fin) |
15 | 14 | adantr 482 |
. . . 4
β’ ((π β§ βπ β π (π΅βπ ) β€ (π΄βπ )) β π β Fin) |
16 | | hoidmvlelem5.a |
. . . . 5
β’ (π β π΄:πβΆβ) |
17 | 16 | adantr 482 |
. . . 4
β’ ((π β§ βπ β π (π΅βπ ) β€ (π΄βπ )) β π΄:πβΆβ) |
18 | | hoidmvlelem5.b |
. . . . 5
β’ (π β π΅:πβΆβ) |
19 | 18 | adantr 482 |
. . . 4
β’ ((π β§ βπ β π (π΅βπ ) β€ (π΄βπ )) β π΅:πβΆβ) |
20 | | simpr 486 |
. . . 4
β’ ((π β§ βπ β π (π΅βπ ) β€ (π΄βπ )) β βπ β π (π΅βπ ) β€ (π΄βπ )) |
21 | 3, 4, 15, 17, 19, 20 | hoidmvval0 44918 |
. . 3
β’ ((π β§ βπ β π (π΅βπ ) β€ (π΄βπ )) β (π΄(πΏβπ)π΅) = 0) |
22 | | nnex 12167 |
. . . . . 6
β’ β
β V |
23 | 22 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
24 | | icossicc 13362 |
. . . . . . 7
β’
(0[,)+β) β (0[,]+β) |
25 | 14 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π β Fin) |
26 | | hoidmvlelem5.c |
. . . . . . . . . 10
β’ (π β πΆ:ββΆ(β βm
π)) |
27 | 26 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΆβπ) β (β βm π)) |
28 | | elmapi 8793 |
. . . . . . . . 9
β’ ((πΆβπ) β (β βm π) β (πΆβπ):πβΆβ) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
30 | | hoidmvlelem5.d |
. . . . . . . . . 10
β’ (π β π·:ββΆ(β βm
π)) |
31 | 30 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π·βπ) β (β βm π)) |
32 | | elmapi 8793 |
. . . . . . . . 9
β’ ((π·βπ) β (β βm π) β (π·βπ):πβΆβ) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β (π·βπ):πβΆβ) |
34 | 4, 25, 29, 33 | hoidmvcl 44913 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,)+β)) |
35 | 24, 34 | sselid 3946 |
. . . . . 6
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,]+β)) |
36 | 35 | fmpttd 7067 |
. . . . 5
β’ (π β (π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))):ββΆ(0[,]+β)) |
37 | 23, 36 | sge0ge0 44715 |
. . . 4
β’ (π β 0 β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
38 | 37 | adantr 482 |
. . 3
β’ ((π β§ βπ β π (π΅βπ ) β€ (π΄βπ )) β 0 β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
39 | 21, 38 | eqbrtrd 5131 |
. 2
β’ ((π β§ βπ β π (π΅βπ ) β€ (π΄βπ )) β (π΄(πΏβπ)π΅) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
40 | | icossxr 13358 |
. . . . . . 7
β’
(0[,)+β) β β* |
41 | 4, 14, 16, 18 | hoidmvcl 44913 |
. . . . . . 7
β’ (π β (π΄(πΏβπ)π΅) β (0[,)+β)) |
42 | 40, 41 | sselid 3946 |
. . . . . 6
β’ (π β (π΄(πΏβπ)π΅) β
β*) |
43 | 42 | adantr 482 |
. . . . 5
β’ ((π β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β (π΄(πΏβπ)π΅) β
β*) |
44 | 23, 36 | sge0xrcl 44716 |
. . . . . 6
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β
β*) |
45 | 44 | adantr 482 |
. . . . 5
β’ ((π β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β
β*) |
46 | | rge0ssre 13382 |
. . . . . . . . 9
β’
(0[,)+β) β β |
47 | 46, 41 | sselid 3946 |
. . . . . . . 8
β’ (π β (π΄(πΏβπ)π΅) β β) |
48 | | ltpnf 13049 |
. . . . . . . 8
β’ ((π΄(πΏβπ)π΅) β β β (π΄(πΏβπ)π΅) < +β) |
49 | 47, 48 | syl 17 |
. . . . . . 7
β’ (π β (π΄(πΏβπ)π΅) < +β) |
50 | 49 | adantr 482 |
. . . . . 6
β’ ((π β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β (π΄(πΏβπ)π΅) < +β) |
51 | | id 22 |
. . . . . . . 8
β’
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) |
52 | 51 | eqcomd 2739 |
. . . . . . 7
β’
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β β +β =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
53 | 52 | adantl 483 |
. . . . . 6
β’ ((π β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β +β =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
54 | 50, 53 | breqtrd 5135 |
. . . . 5
β’ ((π β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β (π΄(πΏβπ)π΅) <
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
55 | 43, 45, 54 | xrltled 13078 |
. . . 4
β’ ((π β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β (π΄(πΏβπ)π΅) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
56 | 55 | adantlr 714 |
. . 3
β’ (((π β§ Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β (π΄(πΏβπ)π΅) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
57 | | simpll 766 |
. . . 4
β’ (((π β§ Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) β§ Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β π) |
58 | | simpr 486 |
. . . . . 6
β’ ((π β§ Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) β Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) |
59 | 16 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π΄βπ ) β β) |
60 | 18 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π΅βπ ) β β) |
61 | 59, 60 | ltnled 11310 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((π΄βπ ) < (π΅βπ ) β Β¬ (π΅βπ ) β€ (π΄βπ ))) |
62 | 61 | ralbidva 3169 |
. . . . . . . 8
β’ (π β (βπ β π (π΄βπ ) < (π΅βπ ) β βπ β π Β¬ (π΅βπ ) β€ (π΄βπ ))) |
63 | | ralnex 3072 |
. . . . . . . . 9
β’
(βπ β
π Β¬ (π΅βπ ) β€ (π΄βπ ) β Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) |
64 | 63 | a1i 11 |
. . . . . . . 8
β’ (π β (βπ β π Β¬ (π΅βπ ) β€ (π΄βπ ) β Β¬ βπ β π (π΅βπ ) β€ (π΄βπ ))) |
65 | 62, 64 | bitrd 279 |
. . . . . . 7
β’ (π β (βπ β π (π΄βπ ) < (π΅βπ ) β Β¬ βπ β π (π΅βπ ) β€ (π΄βπ ))) |
66 | 65 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) β (βπ β π (π΄βπ ) < (π΅βπ ) β Β¬ βπ β π (π΅βπ ) β€ (π΄βπ ))) |
67 | 58, 66 | mpbird 257 |
. . . . 5
β’ ((π β§ Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) β βπ β π (π΄βπ ) < (π΅βπ )) |
68 | 67 | adantr 482 |
. . . 4
β’ (((π β§ Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) β§ Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β βπ β π (π΄βπ ) < (π΅βπ )) |
69 | | simpr 486 |
. . . . . 6
β’ ((π β§ Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) |
70 | 22 | a1i 11 |
. . . . . . 7
β’ ((π β§ Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β β β
V) |
71 | 36 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β (π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))):ββΆ(0[,]+β)) |
72 | 70, 71 | sge0repnf 44717 |
. . . . . 6
β’ ((π β§ Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β β Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β)) |
73 | 69, 72 | mpbird 257 |
. . . . 5
β’ ((π β§ Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
74 | 73 | adantlr 714 |
. . . 4
β’ (((π β§ Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) β§ Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
75 | | simpll 766 |
. . . . . . 7
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β (π β§ βπ β π (π΄βπ ) < (π΅βπ ))) |
76 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π = π β (πΆβπ) = (πΆβπ)) |
77 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π = π β (π·βπ) = (π·βπ)) |
78 | 76, 77 | oveq12d 7379 |
. . . . . . . . . . . 12
β’ (π = π β ((πΆβπ)(πΏβπ)(π·βπ)) = ((πΆβπ)(πΏβπ)(π·βπ))) |
79 | 78 | cbvmptv 5222 |
. . . . . . . . . . 11
β’ (π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))) = (π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))) |
80 | 79 | fveq2i 6849 |
. . . . . . . . . 10
β’
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) |
81 | 80 | eleq1i 2825 |
. . . . . . . . 9
β’
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
82 | 81 | biimpi 215 |
. . . . . . . 8
β’
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
83 | 82 | ad2antlr 726 |
. . . . . . 7
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
84 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β π β
β+) |
85 | 6 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β π β Fin) |
86 | 7 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β π β π) |
87 | | hoidmvlelem5.n |
. . . . . . . . 9
β’ (π β π β β
) |
88 | 87 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β π β β
) |
89 | | hoidmvlelem5.z |
. . . . . . . . 9
β’ (π β π β (π β π)) |
90 | 89 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β π β (π β π)) |
91 | 16 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β π΄:πβΆβ) |
92 | 18 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β π΅:πβΆβ) |
93 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄βπ ) = (π΄βπ)) |
94 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΅βπ ) = (π΅βπ)) |
95 | 93, 94 | breq12d 5122 |
. . . . . . . . . . . . 13
β’ (π = π β ((π΄βπ ) < (π΅βπ ) β (π΄βπ) < (π΅βπ))) |
96 | 95 | cbvralvw 3224 |
. . . . . . . . . . . 12
β’
(βπ β
π (π΄βπ ) < (π΅βπ ) β βπ β π (π΄βπ) < (π΅βπ)) |
97 | 96 | biimpi 215 |
. . . . . . . . . . 11
β’
(βπ β
π (π΄βπ ) < (π΅βπ ) β βπ β π (π΄βπ) < (π΅βπ)) |
98 | 97 | adantr 482 |
. . . . . . . . . 10
β’
((βπ β
π (π΄βπ ) < (π΅βπ ) β§ π β π) β βπ β π (π΄βπ) < (π΅βπ)) |
99 | | simpr 486 |
. . . . . . . . . 10
β’
((βπ β
π (π΄βπ ) < (π΅βπ ) β§ π β π) β π β π) |
100 | | rspa 3230 |
. . . . . . . . . 10
β’
((βπ β
π (π΄βπ) < (π΅βπ) β§ π β π) β (π΄βπ) < (π΅βπ)) |
101 | 98, 99, 100 | syl2anc 585 |
. . . . . . . . 9
β’
((βπ β
π (π΄βπ ) < (π΅βπ ) β§ π β π) β (π΄βπ) < (π΅βπ)) |
102 | 101 | ad5ant25 761 |
. . . . . . . 8
β’
(((((π β§
βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β§ π β π) β (π΄βπ) < (π΅βπ)) |
103 | 26 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β πΆ:ββΆ(β
βm π)) |
104 | 30 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β π·:ββΆ(β
βm π)) |
105 | 81 | biimpri 227 |
. . . . . . . . 9
β’
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
106 | 105 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
107 | | fveq1 6845 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
108 | 107 | breq1d 5119 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβπ) β€ π₯ β (πβπ) β€ π₯)) |
109 | 108, 107 | ifbieq1d 4514 |
. . . . . . . . . . . . 13
β’ (π = π β if((πβπ) β€ π₯, (πβπ), π₯) = if((πβπ) β€ π₯, (πβπ), π₯)) |
110 | 107, 109 | ifeq12d 4511 |
. . . . . . . . . . . 12
β’ (π = π β if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)) = if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) |
111 | 110 | mpteq2dv 5211 |
. . . . . . . . . . 11
β’ (π = π β (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) = (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) |
112 | | eleq1w 2817 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π β π β π)) |
113 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
114 | 113 | breq1d 5119 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πβπ) β€ π₯ β (πβπ) β€ π₯)) |
115 | 114, 113 | ifbieq1d 4514 |
. . . . . . . . . . . . . 14
β’ (π = π β if((πβπ) β€ π₯, (πβπ), π₯) = if((πβπ) β€ π₯, (πβπ), π₯)) |
116 | 112, 113,
115 | ifbieq12d 4518 |
. . . . . . . . . . . . 13
β’ (π = π β if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)) = if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) |
117 | 116 | cbvmptv 5222 |
. . . . . . . . . . . 12
β’ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) = (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) |
118 | 117 | a1i 11 |
. . . . . . . . . . 11
β’ (π = π β (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) = (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) |
119 | 111, 118 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π = π β (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) = (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) |
120 | 119 | cbvmptv 5222 |
. . . . . . . . 9
β’ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) = (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) |
121 | 120 | mpteq2i 5214 |
. . . . . . . 8
β’ (π₯ β β β¦ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
122 | | eqid 2733 |
. . . . . . . 8
β’ ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) |
123 | | simpr 486 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β π β
β+) |
124 | | oveq1 7368 |
. . . . . . . . . . 11
β’ (π€ = π§ β (π€ β (π΄βπ)) = (π§ β (π΄βπ))) |
125 | 124 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π€ = π§ β (((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) Β· (π€ β (π΄βπ))) = (((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) Β· (π§ β (π΄βπ)))) |
126 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ = π₯ β ((πβπ) β€ π€ β (πβπ) β€ π₯)) |
127 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ = π₯ β (πβπ) = (πβπ)) |
128 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ = π₯ β π€ = π₯) |
129 | 126, 127,
128 | ifbieq12d 4518 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ = π₯ β if((πβπ) β€ π€, (πβπ), π€) = if((πβπ) β€ π₯, (πβπ), π₯)) |
130 | 129 | ifeq2d 4510 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ = π₯ β if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)) = if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) |
131 | 130 | mpteq2dv 5211 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = π₯ β (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€))) = (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) |
132 | 131 | mpteq2dv 5211 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ = π₯ β (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))) = (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
133 | 132 | cbvmptv 5222 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β β β¦ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€))))) = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π§ β (π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€))))) = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))) |
135 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π§ β π€ = π§) |
136 | 134, 135 | fveq12d 6853 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π§ β ((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€) = ((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)) |
137 | 136 | fveq1d 6848 |
. . . . . . . . . . . . . . 15
β’ (π€ = π§ β (((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€)β(π·βπ)) = (((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ))) |
138 | 137 | oveq2d 7377 |
. . . . . . . . . . . . . 14
β’ (π€ = π§ β ((πΆβπ)(πΏβπ)(((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€)β(π·βπ))) = ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ)))) |
139 | 138 | mpteq2dv 5211 |
. . . . . . . . . . . . 13
β’ (π€ = π§ β (π β β β¦ ((πΆβπ)(πΏβπ)(((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ))))) |
140 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΆβπ) = (πΆβπ)) |
141 | | 2fveq3 6851 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ)) = (((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ))) |
142 | 140, 141 | oveq12d 7379 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ))) = ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ)))) |
143 | 142 | cbvmptv 5222 |
. . . . . . . . . . . . . 14
β’ (π β β β¦ ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ)))) |
144 | 143 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π€ = π§ β (π β β β¦ ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ))))) |
145 | 139, 144 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π€ = π§ β (π β β β¦ ((πΆβπ)(πΏβπ)(((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ))))) |
146 | 145 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (π€ = π§ β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€)β(π·βπ))))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ)))))) |
147 | 146 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π€ = π§ β ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€)β(π·βπ)))))) = ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ))))))) |
148 | 125, 147 | breq12d 5122 |
. . . . . . . . 9
β’ (π€ = π§ β ((((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) Β· (π€ β (π΄βπ))) β€ ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€)β(π·βπ)))))) β (((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) Β· (π§ β (π΄βπ))) β€ ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ)))))))) |
149 | 148 | cbvrabv 3416 |
. . . . . . . 8
β’ {π€ β ((π΄βπ)[,](π΅βπ)) β£ (((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) Β· (π€ β (π΄βπ))) β€ ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€)β(π·βπ))))))} = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) Β· (π§ β (π΄βπ))) β€ ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(((π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))))βπ§)β(π·βπ))))))} |
150 | | eqid 2733 |
. . . . . . . 8
β’
sup({π€ β
((π΄βπ)[,](π΅βπ)) β£ (((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) Β· (π€ β (π΄βπ))) β€ ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€)β(π·βπ))))))}, β, < ) = sup({π€ β ((π΄βπ)[,](π΅βπ)) β£ (((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) Β· (π€ β (π΄βπ))) β€ ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(((π€ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π€, (πβπ), π€)))))βπ€)β(π·βπ))))))}, β, < ) |
151 | | hoidmvlelem5.i |
. . . . . . . . 9
β’ (π β βπ β (β βm π)βπ β (β βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
152 | 151 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β
βπ β (β
βm π)βπ β (β βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
153 | | hoidmvlelem5.s |
. . . . . . . . 9
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
154 | 153 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
155 | 4, 85, 86, 88, 90, 5, 91, 92, 102, 103, 104, 106, 121, 122, 123, 149, 150, 152, 154 | hoidmvlelem4 44929 |
. . . . . . 7
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β (π΄(πΏβπ)π΅) β€ ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))))) |
156 | 75, 83, 84, 155 | syl21anc 837 |
. . . . . 6
β’ ((((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β§ π β β+) β (π΄(πΏβπ)π΅) β€ ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))))) |
157 | 156 | ralrimiva 3140 |
. . . . 5
β’ (((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β βπ β β+
(π΄(πΏβπ)π΅) β€ ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))))) |
158 | | nfv 1918 |
. . . . . 6
β’
β²π((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
159 | 42 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β (π΄(πΏβπ)π΅) β
β*) |
160 | | 0xr 11210 |
. . . . . . . 8
β’ 0 β
β* |
161 | 160 | a1i 11 |
. . . . . . 7
β’ (((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β 0 β
β*) |
162 | | pnfxr 11217 |
. . . . . . . 8
β’ +β
β β* |
163 | 162 | a1i 11 |
. . . . . . 7
β’ (((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β +β β
β*) |
164 | 44 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β
β*) |
165 | 37 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β 0 β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
166 | | ltpnf 13049 |
. . . . . . . 8
β’
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) < +β) |
167 | 166 | adantl 483 |
. . . . . . 7
β’ (((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) < +β) |
168 | 161, 163,
164, 165, 167 | elicod 13323 |
. . . . . 6
β’ (((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β (0[,)+β)) |
169 | 158, 159,
168 | xralrple2 43679 |
. . . . 5
β’ (((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β ((π΄(πΏβπ)π΅) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β βπ β β+ (π΄(πΏβπ)π΅) β€ ((1 + π) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))))) |
170 | 157, 169 | mpbird 257 |
. . . 4
β’ (((π β§ βπ β π (π΄βπ ) < (π΅βπ )) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) β (π΄(πΏβπ)π΅) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
171 | 57, 68, 74, 170 | syl21anc 837 |
. . 3
β’ (((π β§ Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) β§ Β¬
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) = +β) β (π΄(πΏβπ)π΅) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
172 | 56, 171 | pm2.61dan 812 |
. 2
β’ ((π β§ Β¬ βπ β π (π΅βπ ) β€ (π΄βπ )) β (π΄(πΏβπ)π΅) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
173 | 39, 172 | pm2.61dan 812 |
1
β’ (π β (π΄(πΏβπ)π΅) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |