Step | Hyp | Ref
| Expression |
1 | | areaquad.1 |
. . . . . . . . . 10
β’ π΄ β β |
2 | | areaquad.2 |
. . . . . . . . . 10
β’ π΅ β β |
3 | | iccssre 13353 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
4 | 1, 2, 3 | mp2an 691 |
. . . . . . . . 9
β’ (π΄[,]π΅) β β |
5 | 4 | sseli 3945 |
. . . . . . . 8
β’ (π₯ β (π΄[,]π΅) β π₯ β β) |
6 | 5 | adantr 482 |
. . . . . . 7
β’ ((π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π)) β π₯ β β) |
7 | | areaquad.3 |
. . . . . . . . . . . . . . . 16
β’ πΆ β β |
8 | 7 | recni 11176 |
. . . . . . . . . . . . . . 15
β’ πΆ β β |
9 | 8 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β πΆ β
β) |
10 | | resubcl 11472 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ π΄ β β) β (π₯ β π΄) β β) |
11 | 1, 10 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β (π₯ β π΄) β β) |
12 | 2, 1 | resubcli 11470 |
. . . . . . . . . . . . . . . . . 18
β’ (π΅ β π΄) β β |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β (π΅ β π΄) β β) |
14 | 2 | recni 11176 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π΅ β β |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β β β π΅ β
β) |
16 | | recn 11148 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β β β π΄ β
β) |
17 | | areaquad.7 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π΄ < π΅ |
18 | 1, 17 | gtneii 11274 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π΅ β π΄ |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β β β π΅ β π΄) |
20 | 15, 16, 19 | subne0d 11528 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β β (π΅ β π΄) β 0) |
21 | 1, 20 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’ (π΅ β π΄) β 0 |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β (π΅ β π΄) β 0) |
23 | 11, 13, 22 | redivcld 11990 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β ((π₯ β π΄) / (π΅ β π΄)) β β) |
24 | 23 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β ((π₯ β π΄) / (π΅ β π΄)) β β) |
25 | | areaquad.4 |
. . . . . . . . . . . . . . . . 17
β’ π· β β |
26 | 25 | recni 11176 |
. . . . . . . . . . . . . . . 16
β’ π· β β |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β π· β
β) |
28 | 24, 27 | mulcld 11182 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (((π₯ β π΄) / (π΅ β π΄)) Β· π·) β β) |
29 | 24, 9 | mulcld 11182 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (((π₯ β π΄) / (π΅ β π΄)) Β· πΆ) β β) |
30 | 9, 28, 29 | addsub12d 11542 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (πΆ + ((((π₯ β π΄) / (π΅ β π΄)) Β· π·) β (((π₯ β π΄) / (π΅ β π΄)) Β· πΆ))) = ((((π₯ β π΄) / (π΅ β π΄)) Β· π·) + (πΆ β (((π₯ β π΄) / (π΅ β π΄)) Β· πΆ)))) |
31 | | areaquad.10 |
. . . . . . . . . . . . . 14
β’ π = (πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) |
32 | 24, 27, 9 | subdid 11618 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)) = ((((π₯ β π΄) / (π΅ β π΄)) Β· π·) β (((π₯ β π΄) / (π΅ β π΄)) Β· πΆ))) |
33 | 32 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) = (πΆ + ((((π₯ β π΄) / (π΅ β π΄)) Β· π·) β (((π₯ β π΄) / (π΅ β π΄)) Β· πΆ)))) |
34 | 31, 33 | eqtrid 2789 |
. . . . . . . . . . . . 13
β’ (π₯ β β β π = (πΆ + ((((π₯ β π΄) / (π΅ β π΄)) Β· π·) β (((π₯ β π΄) / (π΅ β π΄)) Β· πΆ)))) |
35 | | 1cnd 11157 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β 1 β
β) |
36 | 35, 24, 9 | subdird 11619 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β ((1
β ((π₯ β π΄) / (π΅ β π΄))) Β· πΆ) = ((1 Β· πΆ) β (((π₯ β π΄) / (π΅ β π΄)) Β· πΆ))) |
37 | 8 | mulid2i 11167 |
. . . . . . . . . . . . . . . 16
β’ (1
Β· πΆ) = πΆ |
38 | 37 | oveq1i 7372 |
. . . . . . . . . . . . . . 15
β’ ((1
Β· πΆ) β
(((π₯ β π΄) / (π΅ β π΄)) Β· πΆ)) = (πΆ β (((π₯ β π΄) / (π΅ β π΄)) Β· πΆ)) |
39 | 36, 38 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β ((1
β ((π₯ β π΄) / (π΅ β π΄))) Β· πΆ) = (πΆ β (((π₯ β π΄) / (π΅ β π΄)) Β· πΆ))) |
40 | 39 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((((π₯ β π΄) / (π΅ β π΄)) Β· π·) + ((1 β ((π₯ β π΄) / (π΅ β π΄))) Β· πΆ)) = ((((π₯ β π΄) / (π΅ β π΄)) Β· π·) + (πΆ β (((π₯ β π΄) / (π΅ β π΄)) Β· πΆ)))) |
41 | 30, 34, 40 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
β’ (π₯ β β β π = ((((π₯ β π΄) / (π΅ β π΄)) Β· π·) + ((1 β ((π₯ β π΄) / (π΅ β π΄))) Β· πΆ))) |
42 | | 1red 11163 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β 1 β
β) |
43 | 42, 23 | resubcld 11590 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (1
β ((π₯ β π΄) / (π΅ β π΄))) β β) |
44 | 43 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (1
β ((π₯ β π΄) / (π΅ β π΄))) β β) |
45 | 44, 9 | mulcld 11182 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((1
β ((π₯ β π΄) / (π΅ β π΄))) Β· πΆ) β β) |
46 | 28, 45 | addcomd 11364 |
. . . . . . . . . . . 12
β’ (π₯ β β β ((((π₯ β π΄) / (π΅ β π΄)) Β· π·) + ((1 β ((π₯ β π΄) / (π΅ β π΄))) Β· πΆ)) = (((1 β ((π₯ β π΄) / (π΅ β π΄))) Β· πΆ) + (((π₯ β π΄) / (π΅ β π΄)) Β· π·))) |
47 | 44, 9 | mulcomd 11183 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((1
β ((π₯ β π΄) / (π΅ β π΄))) Β· πΆ) = (πΆ Β· (1 β ((π₯ β π΄) / (π΅ β π΄))))) |
48 | 24, 27 | mulcomd 11183 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (((π₯ β π΄) / (π΅ β π΄)) Β· π·) = (π· Β· ((π₯ β π΄) / (π΅ β π΄)))) |
49 | 47, 48 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π₯ β β β (((1
β ((π₯ β π΄) / (π΅ β π΄))) Β· πΆ) + (((π₯ β π΄) / (π΅ β π΄)) Β· π·)) = ((πΆ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) + (π· Β· ((π₯ β π΄) / (π΅ β π΄))))) |
50 | 41, 46, 49 | 3eqtrd 2781 |
. . . . . . . . . . 11
β’ (π₯ β β β π = ((πΆ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) + (π· Β· ((π₯ β π΄) / (π΅ β π΄))))) |
51 | 7 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β β β πΆ β
β) |
52 | 51, 43 | remulcld 11192 |
. . . . . . . . . . . 12
β’ (π₯ β β β (πΆ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) β β) |
53 | 25 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β β β π· β
β) |
54 | 53, 23 | remulcld 11192 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π· Β· ((π₯ β π΄) / (π΅ β π΄))) β β) |
55 | 52, 54 | readdcld 11191 |
. . . . . . . . . . 11
β’ (π₯ β β β ((πΆ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) + (π· Β· ((π₯ β π΄) / (π΅ β π΄)))) β β) |
56 | 50, 55 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (π₯ β β β π β
β) |
57 | | areaquad.5 |
. . . . . . . . . . . . . . . 16
β’ πΈ β β |
58 | 57 | recni 11176 |
. . . . . . . . . . . . . . 15
β’ πΈ β β |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β πΈ β
β) |
60 | | areaquad.6 |
. . . . . . . . . . . . . . . . 17
β’ πΉ β β |
61 | 60 | recni 11176 |
. . . . . . . . . . . . . . . 16
β’ πΉ β β |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β πΉ β
β) |
63 | 24, 62 | mulcld 11182 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) β β) |
64 | 24, 59 | mulcld 11182 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (((π₯ β π΄) / (π΅ β π΄)) Β· πΈ) β β) |
65 | 59, 63, 64 | addsub12d 11542 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (πΈ + ((((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) β (((π₯ β π΄) / (π΅ β π΄)) Β· πΈ))) = ((((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) + (πΈ β (((π₯ β π΄) / (π΅ β π΄)) Β· πΈ)))) |
66 | | areaquad.11 |
. . . . . . . . . . . . . 14
β’ π = (πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) |
67 | 24, 62, 59 | subdid 11618 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)) = ((((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) β (((π₯ β π΄) / (π΅ β π΄)) Β· πΈ))) |
68 | 67 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) = (πΈ + ((((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) β (((π₯ β π΄) / (π΅ β π΄)) Β· πΈ)))) |
69 | 66, 68 | eqtrid 2789 |
. . . . . . . . . . . . 13
β’ (π₯ β β β π = (πΈ + ((((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) β (((π₯ β π΄) / (π΅ β π΄)) Β· πΈ)))) |
70 | 35, 24, 59 | subdird 11619 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β ((1
β ((π₯ β π΄) / (π΅ β π΄))) Β· πΈ) = ((1 Β· πΈ) β (((π₯ β π΄) / (π΅ β π΄)) Β· πΈ))) |
71 | 58 | mulid2i 11167 |
. . . . . . . . . . . . . . . 16
β’ (1
Β· πΈ) = πΈ |
72 | 71 | oveq1i 7372 |
. . . . . . . . . . . . . . 15
β’ ((1
Β· πΈ) β
(((π₯ β π΄) / (π΅ β π΄)) Β· πΈ)) = (πΈ β (((π₯ β π΄) / (π΅ β π΄)) Β· πΈ)) |
73 | 70, 72 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β ((1
β ((π₯ β π΄) / (π΅ β π΄))) Β· πΈ) = (πΈ β (((π₯ β π΄) / (π΅ β π΄)) Β· πΈ))) |
74 | 73 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) + ((1 β ((π₯ β π΄) / (π΅ β π΄))) Β· πΈ)) = ((((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) + (πΈ β (((π₯ β π΄) / (π΅ β π΄)) Β· πΈ)))) |
75 | 65, 69, 74 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
β’ (π₯ β β β π = ((((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) + ((1 β ((π₯ β π΄) / (π΅ β π΄))) Β· πΈ))) |
76 | 44, 59 | mulcld 11182 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((1
β ((π₯ β π΄) / (π΅ β π΄))) Β· πΈ) β β) |
77 | 63, 76 | addcomd 11364 |
. . . . . . . . . . . 12
β’ (π₯ β β β ((((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) + ((1 β ((π₯ β π΄) / (π΅ β π΄))) Β· πΈ)) = (((1 β ((π₯ β π΄) / (π΅ β π΄))) Β· πΈ) + (((π₯ β π΄) / (π΅ β π΄)) Β· πΉ))) |
78 | 44, 59 | mulcomd 11183 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((1
β ((π₯ β π΄) / (π΅ β π΄))) Β· πΈ) = (πΈ Β· (1 β ((π₯ β π΄) / (π΅ β π΄))))) |
79 | 24, 62 | mulcomd 11183 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (((π₯ β π΄) / (π΅ β π΄)) Β· πΉ) = (πΉ Β· ((π₯ β π΄) / (π΅ β π΄)))) |
80 | 78, 79 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π₯ β β β (((1
β ((π₯ β π΄) / (π΅ β π΄))) Β· πΈ) + (((π₯ β π΄) / (π΅ β π΄)) Β· πΉ)) = ((πΈ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) + (πΉ Β· ((π₯ β π΄) / (π΅ β π΄))))) |
81 | 75, 77, 80 | 3eqtrd 2781 |
. . . . . . . . . . 11
β’ (π₯ β β β π = ((πΈ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) + (πΉ Β· ((π₯ β π΄) / (π΅ β π΄))))) |
82 | 57 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β β β πΈ β
β) |
83 | 82, 43 | remulcld 11192 |
. . . . . . . . . . . 12
β’ (π₯ β β β (πΈ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) β β) |
84 | 60 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β β β πΉ β
β) |
85 | 84, 23 | remulcld 11192 |
. . . . . . . . . . . 12
β’ (π₯ β β β (πΉ Β· ((π₯ β π΄) / (π΅ β π΄))) β β) |
86 | 83, 85 | readdcld 11191 |
. . . . . . . . . . 11
β’ (π₯ β β β ((πΈ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) + (πΉ Β· ((π₯ β π΄) / (π΅ β π΄)))) β β) |
87 | 81, 86 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (π₯ β β β π β
β) |
88 | | iccssre 13353 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (π[,]π) β β) |
89 | 56, 87, 88 | syl2anc 585 |
. . . . . . . . 9
β’ (π₯ β β β (π[,]π) β β) |
90 | 5, 89 | syl 17 |
. . . . . . . 8
β’ (π₯ β (π΄[,]π΅) β (π[,]π) β β) |
91 | 90 | sselda 3949 |
. . . . . . 7
β’ ((π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π)) β π¦ β β) |
92 | 6, 91 | jca 513 |
. . . . . 6
β’ ((π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π)) β (π₯ β β β§ π¦ β β)) |
93 | 92 | ssopab2i 5512 |
. . . . 5
β’
{β¨π₯, π¦β© β£ (π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π))} β {β¨π₯, π¦β© β£ (π₯ β β β§ π¦ β β)} |
94 | | areaquad.12 |
. . . . 5
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π))} |
95 | | df-xp 5644 |
. . . . 5
β’ (β
Γ β) = {β¨π₯, π¦β© β£ (π₯ β β β§ π¦ β β)} |
96 | 93, 94, 95 | 3sstr4i 3992 |
. . . 4
β’ π β (β Γ
β) |
97 | | iftrue 4497 |
. . . . . . . . . 10
β’ (π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (π β π), 0) = (π β π)) |
98 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π¦ π₯ β (π΄[,]π΅) |
99 | | nfopab2 5181 |
. . . . . . . . . . . . . . 15
β’
β²π¦{β¨π₯, π¦β© β£ (π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π))} |
100 | 94, 99 | nfcxfr 2906 |
. . . . . . . . . . . . . 14
β’
β²π¦π |
101 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π¦{π₯} |
102 | 100, 101 | nfima 6026 |
. . . . . . . . . . . . 13
β’
β²π¦(π β {π₯}) |
103 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π¦(π[,]π) |
104 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π₯ β V |
105 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π¦ β V |
106 | 104, 105 | elimasn 6046 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (π β {π₯}) β β¨π₯, π¦β© β π) |
107 | 94 | eleq2i 2830 |
. . . . . . . . . . . . . . 15
β’
(β¨π₯, π¦β© β π β β¨π₯, π¦β© β {β¨π₯, π¦β© β£ (π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π))}) |
108 | | opabidw 5486 |
. . . . . . . . . . . . . . 15
β’
(β¨π₯, π¦β© β {β¨π₯, π¦β© β£ (π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π))} β (π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π))) |
109 | 106, 107,
108 | 3bitri 297 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π β {π₯}) β (π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π))) |
110 | 109 | baib 537 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β (π¦ β (π β {π₯}) β π¦ β (π[,]π))) |
111 | 98, 102, 103, 110 | eqrd 3968 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β (π β {π₯}) = (π[,]π)) |
112 | 111 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (π₯ β (π΄[,]π΅) β (volβ(π β {π₯})) = (volβ(π[,]π))) |
113 | 5, 56 | syl 17 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β π β β) |
114 | 5, 87 | syl 17 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β π β β) |
115 | | iccmbl 24946 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β (π[,]π) β dom vol) |
116 | 113, 114,
115 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β (π[,]π) β dom vol) |
117 | | mblvol 24910 |
. . . . . . . . . . . 12
β’ ((π[,]π) β dom vol β (volβ(π[,]π)) = (vol*β(π[,]π))) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . 11
β’ (π₯ β (π΄[,]π΅) β (volβ(π[,]π)) = (vol*β(π[,]π))) |
119 | 5, 52 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄[,]π΅) β (πΆ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) β β) |
120 | 5, 54 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄[,]π΅) β (π· Β· ((π₯ β π΄) / (π΅ β π΄))) β β) |
121 | 5, 83 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄[,]π΅) β (πΈ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) β β) |
122 | 5, 85 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄[,]π΅) β (πΉ Β· ((π₯ β π΄) / (π΅ β π΄))) β β) |
123 | 7 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β πΆ β β) |
124 | 57 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β πΈ β β) |
125 | 5, 43 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β (1 β ((π₯ β π΄) / (π΅ β π΄))) β β) |
126 | 5, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π΄[,]π΅) β ((π₯ β π΄) / (π΅ β π΄)) β β) |
127 | 126 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄[,]π΅) β ((π₯ β π΄) / (π΅ β π΄)) β β) |
128 | 127 | subidd 11507 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π΄[,]π΅) β (((π₯ β π΄) / (π΅ β π΄)) β ((π₯ β π΄) / (π΅ β π΄))) = 0) |
129 | | 1red 11163 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄[,]π΅) β 1 β β) |
130 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (π΄[,]π΅) β π΅ β β) |
131 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (π΄[,]π΅) β π΄ β β) |
132 | 1 | rexri 11220 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π΄ β
β* |
133 | 2 | rexri 11220 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π΅ β
β* |
134 | | iccleub 13326 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β β*
β§ π΅ β
β* β§ π₯
β (π΄[,]π΅)) β π₯ β€ π΅) |
135 | 132, 133,
134 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (π΄[,]π΅) β π₯ β€ π΅) |
136 | 5, 130, 131, 135 | lesub1dd 11778 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (π΄[,]π΅) β (π₯ β π΄) β€ (π΅ β π΄)) |
137 | 5, 1, 10 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (π΄[,]π΅) β (π₯ β π΄) β β) |
138 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (π΄[,]π΅) β (π΅ β π΄) β β) |
139 | 1 | recni 11176 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π΄ β β |
140 | 139 | subidi 11479 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄ β π΄) = 0 |
141 | 131, 130,
131 | ltsub1d 11771 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (π΄[,]π΅) β (π΄ < π΅ β (π΄ β π΄) < (π΅ β π΄))) |
142 | 17, 141 | mpbii 232 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β (π΄[,]π΅) β (π΄ β π΄) < (π΅ β π΄)) |
143 | 140, 142 | eqbrtrrid 5146 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (π΄[,]π΅) β 0 < (π΅ β π΄)) |
144 | | lediv1 12027 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β π΄) β β β§ (π΅ β π΄) β β β§ ((π΅ β π΄) β β β§ 0 < (π΅ β π΄))) β ((π₯ β π΄) β€ (π΅ β π΄) β ((π₯ β π΄) / (π΅ β π΄)) β€ ((π΅ β π΄) / (π΅ β π΄)))) |
145 | 137, 138,
138, 143, 144 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (π΄[,]π΅) β ((π₯ β π΄) β€ (π΅ β π΄) β ((π₯ β π΄) / (π΅ β π΄)) β€ ((π΅ β π΄) / (π΅ β π΄)))) |
146 | 136, 145 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π΄[,]π΅) β ((π₯ β π΄) / (π΅ β π΄)) β€ ((π΅ β π΄) / (π΅ β π΄))) |
147 | 12 | recni 11176 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΅ β π΄) β β |
148 | 147, 21 | dividi 11895 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΅ β π΄) / (π΅ β π΄)) = 1 |
149 | 146, 148 | breqtrdi 5151 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄[,]π΅) β ((π₯ β π΄) / (π΅ β π΄)) β€ 1) |
150 | 126, 129,
126, 149 | lesub1dd 11778 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π΄[,]π΅) β (((π₯ β π΄) / (π΅ β π΄)) β ((π₯ β π΄) / (π΅ β π΄))) β€ (1 β ((π₯ β π΄) / (π΅ β π΄)))) |
151 | 128, 150 | eqbrtrrd 5134 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β 0 β€ (1 β ((π₯ β π΄) / (π΅ β π΄)))) |
152 | | areaquad.8 |
. . . . . . . . . . . . . . . 16
β’ πΆ β€ πΈ |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β πΆ β€ πΈ) |
154 | 123, 124,
125, 151, 153 | lemul1ad 12101 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄[,]π΅) β (πΆ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) β€ (πΈ Β· (1 β ((π₯ β π΄) / (π΅ β π΄))))) |
155 | 25 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β π· β β) |
156 | 60 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β πΉ β β) |
157 | 138, 143 | elrpd 12961 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π΄[,]π΅) β (π΅ β π΄) β
β+) |
158 | | iccgelb 13327 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β β*
β§ π΅ β
β* β§ π₯
β (π΄[,]π΅)) β π΄ β€ π₯) |
159 | 132, 133,
158 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π΄[,]π΅) β π΄ β€ π₯) |
160 | 131, 5, 131, 159 | lesub1dd 11778 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄[,]π΅) β (π΄ β π΄) β€ (π₯ β π΄)) |
161 | 140, 160 | eqbrtrrid 5146 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π΄[,]π΅) β 0 β€ (π₯ β π΄)) |
162 | 137, 157,
161 | divge0d 13004 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β 0 β€ ((π₯ β π΄) / (π΅ β π΄))) |
163 | | areaquad.9 |
. . . . . . . . . . . . . . . 16
β’ π· β€ πΉ |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β π· β€ πΉ) |
165 | 155, 156,
126, 162, 164 | lemul1ad 12101 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄[,]π΅) β (π· Β· ((π₯ β π΄) / (π΅ β π΄))) β€ (πΉ Β· ((π₯ β π΄) / (π΅ β π΄)))) |
166 | 119, 120,
121, 122, 154, 165 | le2addd 11781 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β ((πΆ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) + (π· Β· ((π₯ β π΄) / (π΅ β π΄)))) β€ ((πΈ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) + (πΉ Β· ((π₯ β π΄) / (π΅ β π΄))))) |
167 | 5, 50 | syl 17 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β π = ((πΆ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) + (π· Β· ((π₯ β π΄) / (π΅ β π΄))))) |
168 | 5, 81 | syl 17 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β π = ((πΈ Β· (1 β ((π₯ β π΄) / (π΅ β π΄)))) + (πΉ Β· ((π₯ β π΄) / (π΅ β π΄))))) |
169 | 166, 167,
168 | 3brtr4d 5142 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β π β€ π) |
170 | | ovolicc 24903 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β β§ π β€ π) β (vol*β(π[,]π)) = (π β π)) |
171 | 113, 114,
169, 170 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π₯ β (π΄[,]π΅) β (vol*β(π[,]π)) = (π β π)) |
172 | 112, 118,
171 | 3eqtrd 2781 |
. . . . . . . . . 10
β’ (π₯ β (π΄[,]π΅) β (volβ(π β {π₯})) = (π β π)) |
173 | 97, 172 | eqtr4d 2780 |
. . . . . . . . 9
β’ (π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (π β π), 0) = (volβ(π β {π₯}))) |
174 | | iffalse 4500 |
. . . . . . . . . 10
β’ (Β¬
π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (π β π), 0) = 0) |
175 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π¦ Β¬ π₯ β (π΄[,]π΅) |
176 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π¦β
|
177 | 109 | simplbi 499 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π β {π₯}) β π₯ β (π΄[,]π΅)) |
178 | | noel 4295 |
. . . . . . . . . . . . . . 15
β’ Β¬
π¦ β
β
|
179 | 178 | pm2.21i 119 |
. . . . . . . . . . . . . 14
β’ (π¦ β β
β π₯ β (π΄[,]π΅)) |
180 | 177, 179 | pm5.21ni 379 |
. . . . . . . . . . . . 13
β’ (Β¬
π₯ β (π΄[,]π΅) β (π¦ β (π β {π₯}) β π¦ β β
)) |
181 | 175, 102,
176, 180 | eqrd 3968 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β (π΄[,]π΅) β (π β {π₯}) = β
) |
182 | 181 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β (π΄[,]π΅) β (volβ(π β {π₯})) = (volββ
)) |
183 | | 0mbl 24919 |
. . . . . . . . . . . . 13
β’ β
β dom vol |
184 | | mblvol 24910 |
. . . . . . . . . . . . 13
β’ (β
β dom vol β (volββ
) =
(vol*ββ
)) |
185 | 183, 184 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(volββ
) = (vol*ββ
) |
186 | | ovol0 24873 |
. . . . . . . . . . . 12
β’
(vol*ββ
) = 0 |
187 | 185, 186 | eqtri 2765 |
. . . . . . . . . . 11
β’
(volββ
) = 0 |
188 | 182, 187 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (Β¬
π₯ β (π΄[,]π΅) β (volβ(π β {π₯})) = 0) |
189 | 174, 188 | eqtr4d 2780 |
. . . . . . . . 9
β’ (Β¬
π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (π β π), 0) = (volβ(π β {π₯}))) |
190 | 173, 189 | pm2.61i 182 |
. . . . . . . 8
β’ if(π₯ β (π΄[,]π΅), (π β π), 0) = (volβ(π β {π₯})) |
191 | 190 | eqcomi 2746 |
. . . . . . 7
β’
(volβ(π
β {π₯})) = if(π₯ β (π΄[,]π΅), (π β π), 0) |
192 | 87, 56 | resubcld 11590 |
. . . . . . . 8
β’ (π₯ β β β (π β π) β β) |
193 | | 0re 11164 |
. . . . . . . 8
β’ 0 β
β |
194 | | ifcl 4536 |
. . . . . . . 8
β’ (((π β π) β β β§ 0 β β)
β if(π₯ β (π΄[,]π΅), (π β π), 0) β β) |
195 | 192, 193,
194 | sylancl 587 |
. . . . . . 7
β’ (π₯ β β β if(π₯ β (π΄[,]π΅), (π β π), 0) β β) |
196 | 191, 195 | eqeltrid 2842 |
. . . . . 6
β’ (π₯ β β β
(volβ(π β
{π₯})) β
β) |
197 | | volf 24909 |
. . . . . . . 8
β’ vol:dom
volβΆ(0[,]+β) |
198 | | ffun 6676 |
. . . . . . . 8
β’ (vol:dom
volβΆ(0[,]+β) β Fun vol) |
199 | 197, 198 | ax-mp 5 |
. . . . . . 7
β’ Fun
vol |
200 | | iftrue 4497 |
. . . . . . . . . 10
β’ (π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (π[,]π), β
) = (π[,]π)) |
201 | 111, 200 | eqtr4d 2780 |
. . . . . . . . 9
β’ (π₯ β (π΄[,]π΅) β (π β {π₯}) = if(π₯ β (π΄[,]π΅), (π[,]π), β
)) |
202 | | iffalse 4500 |
. . . . . . . . . 10
β’ (Β¬
π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (π[,]π), β
) = β
) |
203 | 181, 202 | eqtr4d 2780 |
. . . . . . . . 9
β’ (Β¬
π₯ β (π΄[,]π΅) β (π β {π₯}) = if(π₯ β (π΄[,]π΅), (π[,]π), β
)) |
204 | 201, 203 | pm2.61i 182 |
. . . . . . . 8
β’ (π β {π₯}) = if(π₯ β (π΄[,]π΅), (π[,]π), β
) |
205 | 56, 87, 115 | syl2anc 585 |
. . . . . . . . 9
β’ (π₯ β β β (π[,]π) β dom vol) |
206 | 183 | a1i 11 |
. . . . . . . . 9
β’ (π₯ β β β β
β dom vol) |
207 | 205, 206 | ifcld 4537 |
. . . . . . . 8
β’ (π₯ β β β if(π₯ β (π΄[,]π΅), (π[,]π), β
) β dom vol) |
208 | 204, 207 | eqeltrid 2842 |
. . . . . . 7
β’ (π₯ β β β (π β {π₯}) β dom vol) |
209 | | fvimacnv 7008 |
. . . . . . 7
β’ ((Fun vol
β§ (π β {π₯}) β dom vol) β
((volβ(π β
{π₯})) β β β
(π β {π₯}) β (β‘vol β β))) |
210 | 199, 208,
209 | sylancr 588 |
. . . . . 6
β’ (π₯ β β β
((volβ(π β
{π₯})) β β β
(π β {π₯}) β (β‘vol β β))) |
211 | 196, 210 | mpbid 231 |
. . . . 5
β’ (π₯ β β β (π β {π₯}) β (β‘vol β β)) |
212 | 211 | rgen 3067 |
. . . 4
β’
βπ₯ β
β (π β {π₯}) β (β‘vol β β) |
213 | 4 | a1i 11 |
. . . . . 6
β’ (0 β
β β (π΄[,]π΅) β
β) |
214 | | rembl 24920 |
. . . . . . 7
β’ β
β dom vol |
215 | 214 | a1i 11 |
. . . . . 6
β’ (0 β
β β β β dom vol) |
216 | 114, 113 | resubcld 11590 |
. . . . . . . 8
β’ (π₯ β (π΄[,]π΅) β (π β π) β β) |
217 | 172, 216 | eqeltrd 2838 |
. . . . . . 7
β’ (π₯ β (π΄[,]π΅) β (volβ(π β {π₯})) β β) |
218 | 217 | adantl 483 |
. . . . . 6
β’ ((0
β β β§ π₯
β (π΄[,]π΅)) β (volβ(π β {π₯})) β β) |
219 | | eldifn 4092 |
. . . . . . . 8
β’ (π₯ β (β β (π΄[,]π΅)) β Β¬ π₯ β (π΄[,]π΅)) |
220 | 219, 188 | syl 17 |
. . . . . . 7
β’ (π₯ β (β β (π΄[,]π΅)) β (volβ(π β {π₯})) = 0) |
221 | 220 | adantl 483 |
. . . . . 6
β’ ((0
β β β§ π₯
β (β β (π΄[,]π΅))) β (volβ(π β {π₯})) = 0) |
222 | 172 | mpteq2ia 5213 |
. . . . . . . 8
β’ (π₯ β (π΄[,]π΅) β¦ (volβ(π β {π₯}))) = (π₯ β (π΄[,]π΅) β¦ (π β π)) |
223 | | eqid 2737 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
224 | 223 | subcn 24245 |
. . . . . . . . . . . 12
β’ β
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
225 | 224 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β β β (((TopOpenββfld)
Γt (TopOpenββfld)) Cn
(TopOpenββfld))) |
226 | 66 | mpteq2i 5215 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β¦ π) = (π₯ β (π΄[,]π΅) β¦ (πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)))) |
227 | 223 | addcn 24244 |
. . . . . . . . . . . . . 14
β’ + β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
228 | 227 | a1i 11 |
. . . . . . . . . . . . 13
β’ (β€
β + β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
229 | | ax-resscn 11115 |
. . . . . . . . . . . . . . . 16
β’ β
β β |
230 | 4, 229 | sstri 3958 |
. . . . . . . . . . . . . . 15
β’ (π΄[,]π΅) β β |
231 | | ssid 3971 |
. . . . . . . . . . . . . . 15
β’ β
β β |
232 | | cncfmptc 24291 |
. . . . . . . . . . . . . . 15
β’ ((πΈ β β β§ (π΄[,]π΅) β β β§ β β
β) β (π₯ β
(π΄[,]π΅) β¦ πΈ) β ((π΄[,]π΅)βcnββ)) |
233 | 58, 230, 231, 232 | mp3an 1462 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄[,]π΅) β¦ πΈ) β ((π΄[,]π΅)βcnββ) |
234 | 233 | a1i 11 |
. . . . . . . . . . . . 13
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ πΈ) β ((π΄[,]π΅)βcnββ)) |
235 | 230 | sseli 3945 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π΄[,]π΅) β π₯ β β) |
236 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π΄[,]π΅) β π΄ β β) |
237 | 147 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π΄[,]π΅) β (π΅ β π΄) β β) |
238 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π΄[,]π΅) β (π΅ β π΄) β 0) |
239 | 235, 236,
237, 238 | divsubdird 11977 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄[,]π΅) β ((π₯ β π΄) / (π΅ β π΄)) = ((π₯ / (π΅ β π΄)) β (π΄ / (π΅ β π΄)))) |
240 | 239 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (π΄[,]π΅)) β ((π₯ β π΄) / (π΅ β π΄)) = ((π₯ / (π΅ β π΄)) β (π΄ / (π΅ β π΄)))) |
241 | 240 | mpteq2dva 5210 |
. . . . . . . . . . . . . . 15
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ ((π₯ β π΄) / (π΅ β π΄))) = (π₯ β (π΄[,]π΅) β¦ ((π₯ / (π΅ β π΄)) β (π΄ / (π΅ β π΄))))) |
242 | | resmpt 5996 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄[,]π΅) β β β ((π₯ β β β¦ (π₯ / (π΅ β π΄))) βΎ (π΄[,]π΅)) = (π₯ β (π΄[,]π΅) β¦ (π₯ / (π΅ β π΄)))) |
243 | 230, 242 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β¦ (π₯ / (π΅ β π΄))) βΎ (π΄[,]π΅)) = (π₯ β (π΄[,]π΅) β¦ (π₯ / (π΅ β π΄))) |
244 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β¦ (π₯ / (π΅ β π΄))) = (π₯ β β β¦ (π₯ / (π΅ β π΄))) |
245 | 244 | divccncf 24285 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΅ β π΄) β β β§ (π΅ β π΄) β 0) β (π₯ β β β¦ (π₯ / (π΅ β π΄))) β (ββcnββ)) |
246 | 147, 21, 245 | mp2an 691 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β¦ (π₯ / (π΅ β π΄))) β (ββcnββ) |
247 | | rescncf 24276 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄[,]π΅) β β β ((π₯ β β β¦ (π₯ / (π΅ β π΄))) β (ββcnββ) β ((π₯ β β β¦ (π₯ / (π΅ β π΄))) βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ))) |
248 | 230, 246,
247 | mp2 9 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β¦ (π₯ / (π΅ β π΄))) βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ) |
249 | 243, 248 | eqeltrri 2835 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄[,]π΅) β¦ (π₯ / (π΅ β π΄))) β ((π΄[,]π΅)βcnββ) |
250 | 249 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (π₯ / (π΅ β π΄))) β ((π΄[,]π΅)βcnββ)) |
251 | 139, 147,
21 | divcli 11904 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ / (π΅ β π΄)) β β |
252 | | cncfmptc 24291 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ / (π΅ β π΄)) β β β§ (π΄[,]π΅) β β β§ β β
β) β (π₯ β
(π΄[,]π΅) β¦ (π΄ / (π΅ β π΄))) β ((π΄[,]π΅)βcnββ)) |
253 | 251, 230,
231, 252 | mp3an 1462 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄[,]π΅) β¦ (π΄ / (π΅ β π΄))) β ((π΄[,]π΅)βcnββ) |
254 | 253 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (π΄ / (π΅ β π΄))) β ((π΄[,]π΅)βcnββ)) |
255 | 223, 225,
250, 254 | cncfmpt2f 24294 |
. . . . . . . . . . . . . . 15
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ ((π₯ / (π΅ β π΄)) β (π΄ / (π΅ β π΄)))) β ((π΄[,]π΅)βcnββ)) |
256 | 241, 255 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ ((π₯ β π΄) / (π΅ β π΄))) β ((π΄[,]π΅)βcnββ)) |
257 | | cncfmptc 24291 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β β β§ (π΄[,]π΅) β β β§ β β
β) β (π₯ β
(π΄[,]π΅) β¦ πΉ) β ((π΄[,]π΅)βcnββ)) |
258 | 61, 230, 231, 257 | mp3an 1462 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π΄[,]π΅) β¦ πΉ) β ((π΄[,]π΅)βcnββ) |
259 | 258 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ πΉ) β ((π΄[,]π΅)βcnββ)) |
260 | 223, 225,
259, 234 | cncfmpt2f 24294 |
. . . . . . . . . . . . . 14
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (πΉ β πΈ)) β ((π΄[,]π΅)βcnββ)) |
261 | 256, 260 | mulcncf 24826 |
. . . . . . . . . . . . 13
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) β ((π΄[,]π΅)βcnββ)) |
262 | 223, 228,
234, 261 | cncfmpt2f 24294 |
. . . . . . . . . . . 12
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)))) β ((π΄[,]π΅)βcnββ)) |
263 | 226, 262 | eqeltrid 2842 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ π) β ((π΄[,]π΅)βcnββ)) |
264 | 31 | mpteq2i 5215 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β¦ π) = (π₯ β (π΄[,]π΅) β¦ (πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)))) |
265 | | cncfmptc 24291 |
. . . . . . . . . . . . . . 15
β’ ((πΆ β β β§ (π΄[,]π΅) β β β§ β β
β) β (π₯ β
(π΄[,]π΅) β¦ πΆ) β ((π΄[,]π΅)βcnββ)) |
266 | 8, 230, 231, 265 | mp3an 1462 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄[,]π΅) β¦ πΆ) β ((π΄[,]π΅)βcnββ) |
267 | 266 | a1i 11 |
. . . . . . . . . . . . 13
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ πΆ) β ((π΄[,]π΅)βcnββ)) |
268 | | cncfmptc 24291 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β β β§ (π΄[,]π΅) β β β§ β β
β) β (π₯ β
(π΄[,]π΅) β¦ π·) β ((π΄[,]π΅)βcnββ)) |
269 | 26, 230, 231, 268 | mp3an 1462 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π΄[,]π΅) β¦ π·) β ((π΄[,]π΅)βcnββ) |
270 | 269 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ π·) β ((π΄[,]π΅)βcnββ)) |
271 | 223, 225,
270, 267 | cncfmpt2f 24294 |
. . . . . . . . . . . . . 14
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (π· β πΆ)) β ((π΄[,]π΅)βcnββ)) |
272 | 256, 271 | mulcncf 24826 |
. . . . . . . . . . . . 13
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) β ((π΄[,]π΅)βcnββ)) |
273 | 223, 228,
267, 272 | cncfmpt2f 24294 |
. . . . . . . . . . . 12
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)))) β ((π΄[,]π΅)βcnββ)) |
274 | 264, 273 | eqeltrid 2842 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ π) β ((π΄[,]π΅)βcnββ)) |
275 | 223, 225,
263, 274 | cncfmpt2f 24294 |
. . . . . . . . . 10
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (π β π)) β ((π΄[,]π΅)βcnββ)) |
276 | 275 | mptru 1549 |
. . . . . . . . 9
β’ (π₯ β (π΄[,]π΅) β¦ (π β π)) β ((π΄[,]π΅)βcnββ) |
277 | | cniccibl 25221 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ (π β π)) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ (π β π)) β
πΏ1) |
278 | 1, 2, 276, 277 | mp3an 1462 |
. . . . . . . 8
β’ (π₯ β (π΄[,]π΅) β¦ (π β π)) β
πΏ1 |
279 | 222, 278 | eqeltri 2834 |
. . . . . . 7
β’ (π₯ β (π΄[,]π΅) β¦ (volβ(π β {π₯}))) β
πΏ1 |
280 | 279 | a1i 11 |
. . . . . 6
β’ (0 β
β β (π₯ β
(π΄[,]π΅) β¦ (volβ(π β {π₯}))) β
πΏ1) |
281 | 213, 215,
218, 221, 280 | iblss2 25186 |
. . . . 5
β’ (0 β
β β (π₯ β
β β¦ (volβ(π β {π₯}))) β
πΏ1) |
282 | 193, 281 | ax-mp 5 |
. . . 4
β’ (π₯ β β β¦
(volβ(π β
{π₯}))) β
πΏ1 |
283 | | dmarea 26323 |
. . . 4
β’ (π β dom area β (π β (β Γ
β) β§ βπ₯
β β (π β
{π₯}) β (β‘vol β β) β§ (π₯ β β β¦
(volβ(π β
{π₯}))) β
πΏ1)) |
284 | 96, 212, 282, 283 | mpbir3an 1342 |
. . 3
β’ π β dom
area |
285 | | areaval 26330 |
. . 3
β’ (π β dom area β
(areaβπ) =
β«β(volβ(π
β {π₯})) dπ₯) |
286 | 284, 285 | ax-mp 5 |
. 2
β’
(areaβπ) =
β«β(volβ(π
β {π₯})) dπ₯ |
287 | | itgeq2 25158 |
. . . 4
β’
(βπ₯ β
β (volβ(π
β {π₯})) = if(π₯ β (π΄[,]π΅), (π β π), 0) β β«β(volβ(π β {π₯})) dπ₯ = β«βif(π₯ β (π΄[,]π΅), (π β π), 0) dπ₯) |
288 | 191 | a1i 11 |
. . . 4
β’ (π₯ β β β
(volβ(π β
{π₯})) = if(π₯ β (π΄[,]π΅), (π β π), 0)) |
289 | 287, 288 | mprg 3071 |
. . 3
β’
β«β(volβ(π β {π₯})) dπ₯ = β«βif(π₯ β (π΄[,]π΅), (π β π), 0) dπ₯ |
290 | | itgss2 25193 |
. . . 4
β’ ((π΄[,]π΅) β β β β«(π΄[,]π΅)(π β π) dπ₯ = β«βif(π₯ β (π΄[,]π΅), (π β π), 0) dπ₯) |
291 | 4, 290 | ax-mp 5 |
. . 3
β’
β«(π΄[,]π΅)(π β π) dπ₯ = β«βif(π₯ β (π΄[,]π΅), (π β π), 0) dπ₯ |
292 | 61, 58 | addcli 11168 |
. . . . . 6
β’ (πΉ + πΈ) β β |
293 | | 2cnne0 12370 |
. . . . . 6
β’ (2 β
β β§ 2 β 0) |
294 | | div32 11840 |
. . . . . 6
β’ (((πΉ + πΈ) β β β§ (2 β β
β§ 2 β 0) β§ (π΅
β π΄) β β)
β (((πΉ + πΈ) / 2) Β· (π΅ β π΄)) = ((πΉ + πΈ) Β· ((π΅ β π΄) / 2))) |
295 | 292, 293,
147, 294 | mp3an 1462 |
. . . . 5
β’ (((πΉ + πΈ) / 2) Β· (π΅ β π΄)) = ((πΉ + πΈ) Β· ((π΅ β π΄) / 2)) |
296 | 26, 8 | addcli 11168 |
. . . . . 6
β’ (π· + πΆ) β β |
297 | | div32 11840 |
. . . . . 6
β’ (((π· + πΆ) β β β§ (2 β β
β§ 2 β 0) β§ (π΅
β π΄) β β)
β (((π· + πΆ) / 2) Β· (π΅ β π΄)) = ((π· + πΆ) Β· ((π΅ β π΄) / 2))) |
298 | 296, 293,
147, 297 | mp3an 1462 |
. . . . 5
β’ (((π· + πΆ) / 2) Β· (π΅ β π΄)) = ((π· + πΆ) Β· ((π΅ β π΄) / 2)) |
299 | 295, 298 | oveq12i 7374 |
. . . 4
β’ ((((πΉ + πΈ) / 2) Β· (π΅ β π΄)) β (((π· + πΆ) / 2) Β· (π΅ β π΄))) = (((πΉ + πΈ) Β· ((π΅ β π΄) / 2)) β ((π· + πΆ) Β· ((π΅ β π΄) / 2))) |
300 | | 2cn 12235 |
. . . . . 6
β’ 2 β
β |
301 | | 2ne0 12264 |
. . . . . 6
β’ 2 β
0 |
302 | 292, 300,
301 | divcli 11904 |
. . . . 5
β’ ((πΉ + πΈ) / 2) β β |
303 | 296, 300,
301 | divcli 11904 |
. . . . 5
β’ ((π· + πΆ) / 2) β β |
304 | 302, 303,
147 | subdiri 11612 |
. . . 4
β’ ((((πΉ + πΈ) / 2) β ((π· + πΆ) / 2)) Β· (π΅ β π΄)) = ((((πΉ + πΈ) / 2) Β· (π΅ β π΄)) β (((π· + πΆ) / 2) Β· (π΅ β π΄))) |
305 | 114 | adantl 483 |
. . . . . . 7
β’
((β€ β§ π₯
β (π΄[,]π΅)) β π β β) |
306 | 263 | mptru 1549 |
. . . . . . . . 9
β’ (π₯ β (π΄[,]π΅) β¦ π) β ((π΄[,]π΅)βcnββ) |
307 | | cniccibl 25221 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ π) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ π) β
πΏ1) |
308 | 1, 2, 306, 307 | mp3an 1462 |
. . . . . . . 8
β’ (π₯ β (π΄[,]π΅) β¦ π) β
πΏ1 |
309 | 308 | a1i 11 |
. . . . . . 7
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ π) β
πΏ1) |
310 | 113 | adantl 483 |
. . . . . . 7
β’
((β€ β§ π₯
β (π΄[,]π΅)) β π β β) |
311 | 274 | mptru 1549 |
. . . . . . . . 9
β’ (π₯ β (π΄[,]π΅) β¦ π) β ((π΄[,]π΅)βcnββ) |
312 | | cniccibl 25221 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ π) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ π) β
πΏ1) |
313 | 1, 2, 311, 312 | mp3an 1462 |
. . . . . . . 8
β’ (π₯ β (π΄[,]π΅) β¦ π) β
πΏ1 |
314 | 313 | a1i 11 |
. . . . . . 7
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ π) β
πΏ1) |
315 | 305, 309,
310, 314 | itgsub 25206 |
. . . . . 6
β’ (β€
β β«(π΄[,]π΅)(π β π) dπ₯ = (β«(π΄[,]π΅)π dπ₯ β β«(π΄[,]π΅)π dπ₯)) |
316 | 315 | mptru 1549 |
. . . . 5
β’
β«(π΄[,]π΅)(π β π) dπ₯ = (β«(π΄[,]π΅)π dπ₯ β β«(π΄[,]π΅)π dπ₯) |
317 | 58, 300, 301 | divcan4i 11909 |
. . . . . . . . . . 11
β’ ((πΈ Β· 2) / 2) = πΈ |
318 | 317 | oveq1i 7372 |
. . . . . . . . . 10
β’ (((πΈ Β· 2) / 2) Β·
(π΅ β π΄)) = (πΈ Β· (π΅ β π΄)) |
319 | 58, 300 | mulcli 11169 |
. . . . . . . . . . 11
β’ (πΈ Β· 2) β
β |
320 | | div32 11840 |
. . . . . . . . . . 11
β’ (((πΈ Β· 2) β β
β§ (2 β β β§ 2 β 0) β§ (π΅ β π΄) β β) β (((πΈ Β· 2) / 2) Β·
(π΅ β π΄)) = ((πΈ Β· 2) Β· ((π΅ β π΄) / 2))) |
321 | 319, 293,
147, 320 | mp3an 1462 |
. . . . . . . . . 10
β’ (((πΈ Β· 2) / 2) Β·
(π΅ β π΄)) = ((πΈ Β· 2) Β· ((π΅ β π΄) / 2)) |
322 | 318, 321 | eqtr3i 2767 |
. . . . . . . . 9
β’ (πΈ Β· (π΅ β π΄)) = ((πΈ Β· 2) Β· ((π΅ β π΄) / 2)) |
323 | 322 | oveq1i 7372 |
. . . . . . . 8
β’ ((πΈ Β· (π΅ β π΄)) + ((πΉ β πΈ) Β· ((π΅ β π΄) / 2))) = (((πΈ Β· 2) Β· ((π΅ β π΄) / 2)) + ((πΉ β πΈ) Β· ((π΅ β π΄) / 2))) |
324 | | itgeq2 25158 |
. . . . . . . . . 10
β’
(βπ₯ β
(π΄[,]π΅)π = (πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) β β«(π΄[,]π΅)π dπ₯ = β«(π΄[,]π΅)(πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) dπ₯) |
325 | 66 | a1i 11 |
. . . . . . . . . 10
β’ (π₯ β (π΄[,]π΅) β π = (πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)))) |
326 | 324, 325 | mprg 3071 |
. . . . . . . . 9
β’
β«(π΄[,]π΅)π dπ₯ = β«(π΄[,]π΅)(πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) dπ₯ |
327 | 57 | a1i 11 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (π΄[,]π΅)) β πΈ β β) |
328 | | cniccibl 25221 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ πΈ) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ πΈ) β
πΏ1) |
329 | 1, 2, 233, 328 | mp3an 1462 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β¦ πΈ) β
πΏ1 |
330 | 329 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ πΈ) β
πΏ1) |
331 | 126 | adantl 483 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (π΄[,]π΅)) β ((π₯ β π΄) / (π΅ β π΄)) β β) |
332 | 60 | a1i 11 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (π΄[,]π΅)) β πΉ β β) |
333 | 332, 327 | resubcld 11590 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (π΄[,]π΅)) β (πΉ β πΈ) β β) |
334 | 331, 333 | remulcld 11192 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (π΄[,]π΅)) β (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)) β β) |
335 | 261 | mptru 1549 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) β ((π΄[,]π΅)βcnββ) |
336 | | cniccibl 25221 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) β
πΏ1) |
337 | 1, 2, 335, 336 | mp3an 1462 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) β
πΏ1 |
338 | 337 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) β
πΏ1) |
339 | 327, 330,
334, 338 | itgadd 25205 |
. . . . . . . . . 10
β’ (β€
β β«(π΄[,]π΅)(πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) dπ₯ = (β«(π΄[,]π΅)πΈ dπ₯ + β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)) dπ₯)) |
340 | 339 | mptru 1549 |
. . . . . . . . 9
β’
β«(π΄[,]π΅)(πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) dπ₯ = (β«(π΄[,]π΅)πΈ dπ₯ + β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)) dπ₯) |
341 | | iccmbl 24946 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β dom vol) |
342 | 1, 2, 341 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π΄[,]π΅) β dom vol |
343 | | mblvol 24910 |
. . . . . . . . . . . . . . 15
β’ ((π΄[,]π΅) β dom vol β (volβ(π΄[,]π΅)) = (vol*β(π΄[,]π΅))) |
344 | 342, 343 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
(volβ(π΄[,]π΅)) = (vol*β(π΄[,]π΅)) |
345 | 1, 2, 17 | ltleii 11285 |
. . . . . . . . . . . . . . 15
β’ π΄ β€ π΅ |
346 | | ovolicc 24903 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (vol*β(π΄[,]π΅)) = (π΅ β π΄)) |
347 | 1, 2, 345, 346 | mp3an 1462 |
. . . . . . . . . . . . . 14
β’
(vol*β(π΄[,]π΅)) = (π΅ β π΄) |
348 | 344, 347 | eqtri 2765 |
. . . . . . . . . . . . 13
β’
(volβ(π΄[,]π΅)) = (π΅ β π΄) |
349 | 348, 12 | eqeltri 2834 |
. . . . . . . . . . . 12
β’
(volβ(π΄[,]π΅)) β β |
350 | | itgconst 25199 |
. . . . . . . . . . . 12
β’ (((π΄[,]π΅) β dom vol β§ (volβ(π΄[,]π΅)) β β β§ πΈ β β) β β«(π΄[,]π΅)πΈ dπ₯ = (πΈ Β· (volβ(π΄[,]π΅)))) |
351 | 342, 349,
58, 350 | mp3an 1462 |
. . . . . . . . . . 11
β’
β«(π΄[,]π΅)πΈ dπ₯ = (πΈ Β· (volβ(π΄[,]π΅))) |
352 | 348 | oveq2i 7373 |
. . . . . . . . . . 11
β’ (πΈ Β· (volβ(π΄[,]π΅))) = (πΈ Β· (π΅ β π΄)) |
353 | 351, 352 | eqtri 2765 |
. . . . . . . . . 10
β’
β«(π΄[,]π΅)πΈ dπ₯ = (πΈ Β· (π΅ β π΄)) |
354 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (β€
β πΉ β
β) |
355 | 58 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (β€
β πΈ β
β) |
356 | 354, 355 | subcld 11519 |
. . . . . . . . . . . . 13
β’ (β€
β (πΉ β πΈ) β
β) |
357 | 256 | mptru 1549 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β¦ ((π₯ β π΄) / (π΅ β π΄))) β ((π΄[,]π΅)βcnββ) |
358 | | cniccibl 25221 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ ((π₯ β π΄) / (π΅ β π΄))) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ ((π₯ β π΄) / (π΅ β π΄))) β
πΏ1) |
359 | 1, 2, 357, 358 | mp3an 1462 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄[,]π΅) β¦ ((π₯ β π΄) / (π΅ β π΄))) β
πΏ1 |
360 | 359 | a1i 11 |
. . . . . . . . . . . . 13
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ ((π₯ β π΄) / (π΅ β π΄))) β
πΏ1) |
361 | 356, 331,
360 | itgmulc2 25214 |
. . . . . . . . . . . 12
β’ (β€
β ((πΉ β πΈ) Β· β«(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) dπ₯) = β«(π΄[,]π΅)((πΉ β πΈ) Β· ((π₯ β π΄) / (π΅ β π΄))) dπ₯) |
362 | 361 | mptru 1549 |
. . . . . . . . . . 11
β’ ((πΉ β πΈ) Β· β«(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) dπ₯) = β«(π΄[,]π΅)((πΉ β πΈ) Β· ((π₯ β π΄) / (π΅ β π΄))) dπ₯ |
363 | | itgeq2 25158 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) = ((1 / (π΅ β π΄)) Β· (π₯ β π΄)) β β«(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) dπ₯ = β«(π΄[,]π΅)((1 / (π΅ β π΄)) Β· (π₯ β π΄)) dπ₯) |
364 | 137 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π΄[,]π΅) β (π₯ β π΄) β β) |
365 | 364, 237,
238 | divrec2d 11942 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄[,]π΅) β ((π₯ β π΄) / (π΅ β π΄)) = ((1 / (π΅ β π΄)) Β· (π₯ β π΄))) |
366 | 363, 365 | mprg 3071 |
. . . . . . . . . . . . . 14
β’
β«(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) dπ₯ = β«(π΄[,]π΅)((1 / (π΅ β π΄)) Β· (π₯ β π΄)) dπ₯ |
367 | 5 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β€ β§ π₯
β (π΄[,]π΅)) β π₯ β β) |
368 | | cncfmptid 24292 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π΄[,]π΅) β β β§ β β
β) β (π₯ β
(π΄[,]π΅) β¦ π₯) β ((π΄[,]π΅)βcnββ)) |
369 | 230, 231,
368 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (π΄[,]π΅) β¦ π₯) β ((π΄[,]π΅)βcnββ) |
370 | | cniccibl 25221 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ π₯) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ π₯) β
πΏ1) |
371 | 1, 2, 369, 370 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β (π΄[,]π΅) β¦ π₯) β
πΏ1 |
372 | 371 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ π₯) β
πΏ1) |
373 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β€ β§ π₯
β (π΄[,]π΅)) β π΄ β β) |
374 | | cncfmptc 24291 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΄ β β β§ (π΄[,]π΅) β β β§ β β
β) β (π₯ β
(π΄[,]π΅) β¦ π΄) β ((π΄[,]π΅)βcnββ)) |
375 | 139, 230,
231, 374 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (π΄[,]π΅) β¦ π΄) β ((π΄[,]π΅)βcnββ) |
376 | | cniccibl 25221 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ π΄) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ π΄) β
πΏ1) |
377 | 1, 2, 375, 376 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β (π΄[,]π΅) β¦ π΄) β
πΏ1 |
378 | 377 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ π΄) β
πΏ1) |
379 | 367, 372,
373, 378 | itgsub 25206 |
. . . . . . . . . . . . . . . . . . 19
β’ (β€
β β«(π΄[,]π΅)(π₯ β π΄) dπ₯ = (β«(π΄[,]π΅)π₯ dπ₯ β β«(π΄[,]π΅)π΄ dπ₯)) |
380 | 379 | mptru 1549 |
. . . . . . . . . . . . . . . . . 18
β’
β«(π΄[,]π΅)(π₯ β π΄) dπ₯ = (β«(π΄[,]π΅)π₯ dπ₯ β β«(π΄[,]π΅)π΄ dπ₯) |
381 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β€
β π΄ β
β) |
382 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β€
β π΅ β
β) |
383 | 345 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β€
β π΄ β€ π΅) |
384 | | 1nn0 12436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 1 β
β0 |
385 | 384 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β€
β 1 β β0) |
386 | 381, 382,
383, 385 | itgpowd 25430 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β€
β β«(π΄[,]π΅)(π₯β1) dπ₯ = (((π΅β(1 + 1)) β (π΄β(1 + 1))) / (1 + 1))) |
387 | 386 | mptru 1549 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β«(π΄[,]π΅)(π₯β1) dπ₯ = (((π΅β(1 + 1)) β (π΄β(1 + 1))) / (1 + 1)) |
388 | | 1p1e2 12285 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1 + 1) =
2 |
389 | 388 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΅β(1 + 1)) β (π΄β(1 + 1))) / (1 + 1)) =
(((π΅β(1 + 1)) β
(π΄β(1 + 1))) /
2) |
390 | 387, 389 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . 20
β’
β«(π΄[,]π΅)(π₯β1) dπ₯ = (((π΅β(1 + 1)) β (π΄β(1 + 1))) / 2) |
391 | | itgeq2 25158 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ₯ β
(π΄[,]π΅)(π₯β1) = π₯ β β«(π΄[,]π΅)(π₯β1) dπ₯ = β«(π΄[,]π΅)π₯ dπ₯) |
392 | 235 | exp1d 14053 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β (π΄[,]π΅) β (π₯β1) = π₯) |
393 | 391, 392 | mprg 3071 |
. . . . . . . . . . . . . . . . . . . 20
β’
β«(π΄[,]π΅)(π₯β1) dπ₯ = β«(π΄[,]π΅)π₯ dπ₯ |
394 | 388 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΅β(1 + 1)) = (π΅β2) |
395 | 388 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄β(1 + 1)) = (π΄β2) |
396 | 394, 395 | oveq12i 7374 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΅β(1 + 1)) β (π΄β(1 + 1))) = ((π΅β2) β (π΄β2)) |
397 | 396 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΅β(1 + 1)) β (π΄β(1 + 1))) / 2) = (((π΅β2) β (π΄β2)) / 2) |
398 | 390, 393,
397 | 3eqtr3i 2773 |
. . . . . . . . . . . . . . . . . . 19
β’
β«(π΄[,]π΅)π₯ dπ₯ = (((π΅β2) β (π΄β2)) / 2) |
399 | | itgconst 25199 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄[,]π΅) β dom vol β§ (volβ(π΄[,]π΅)) β β β§ π΄ β β) β β«(π΄[,]π΅)π΄ dπ₯ = (π΄ Β· (volβ(π΄[,]π΅)))) |
400 | 342, 349,
139, 399 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . . 20
β’
β«(π΄[,]π΅)π΄ dπ₯ = (π΄ Β· (volβ(π΄[,]π΅))) |
401 | 348 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ Β· (volβ(π΄[,]π΅))) = (π΄ Β· (π΅ β π΄)) |
402 | 400, 401 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
β’
β«(π΄[,]π΅)π΄ dπ₯ = (π΄ Β· (π΅ β π΄)) |
403 | 398, 402 | oveq12i 7374 |
. . . . . . . . . . . . . . . . . 18
β’
(β«(π΄[,]π΅)π₯ dπ₯ β β«(π΄[,]π΅)π΄ dπ₯) = ((((π΅β2) β (π΄β2)) / 2) β (π΄ Β· (π΅ β π΄))) |
404 | 380, 403 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
β’
β«(π΄[,]π΅)(π₯ β π΄) dπ₯ = ((((π΅β2) β (π΄β2)) / 2) β (π΄ Β· (π΅ β π΄))) |
405 | 404 | oveq2i 7373 |
. . . . . . . . . . . . . . . 16
β’ ((1 /
(π΅ β π΄)) Β· β«(π΄[,]π΅)(π₯ β π΄) dπ₯) = ((1 / (π΅ β π΄)) Β· ((((π΅β2) β (π΄β2)) / 2) β (π΄ Β· (π΅ β π΄)))) |
406 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β€
β π΅ β
β) |
407 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β€
β π΄ β
β) |
408 | 406, 407 | subcld 11519 |
. . . . . . . . . . . . . . . . . . 19
β’ (β€
β (π΅ β π΄) β
β) |
409 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β€
β π΅ β π΄) |
410 | 406, 407,
409 | subne0d 11528 |
. . . . . . . . . . . . . . . . . . 19
β’ (β€
β (π΅ β π΄) β 0) |
411 | 408, 410 | reccld 11931 |
. . . . . . . . . . . . . . . . . 18
β’ (β€
β (1 / (π΅ β
π΄)) β
β) |
412 | 411 | mptru 1549 |
. . . . . . . . . . . . . . . . 17
β’ (1 /
(π΅ β π΄)) β
β |
413 | 14 | sqcli 14092 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΅β2) β
β |
414 | 139 | sqcli 14092 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄β2) β
β |
415 | 413, 414 | subcli 11484 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΅β2) β (π΄β2)) β
β |
416 | 415, 300,
301 | divcli 11904 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅β2) β (π΄β2)) / 2) β
β |
417 | 139, 147 | mulcli 11169 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ Β· (π΅ β π΄)) β β |
418 | 412, 416,
417 | subdii 11611 |
. . . . . . . . . . . . . . . 16
β’ ((1 /
(π΅ β π΄)) Β· ((((π΅β2) β (π΄β2)) / 2) β (π΄ Β· (π΅ β π΄)))) = (((1 / (π΅ β π΄)) Β· (((π΅β2) β (π΄β2)) / 2)) β ((1 / (π΅ β π΄)) Β· (π΄ Β· (π΅ β π΄)))) |
419 | 405, 418 | eqtri 2765 |
. . . . . . . . . . . . . . 15
β’ ((1 /
(π΅ β π΄)) Β· β«(π΄[,]π΅)(π₯ β π΄) dπ₯) = (((1 / (π΅ β π΄)) Β· (((π΅β2) β (π΄β2)) / 2)) β ((1 / (π΅ β π΄)) Β· (π΄ Β· (π΅ β π΄)))) |
420 | 137 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (π΄[,]π΅)) β (π₯ β π΄) β β) |
421 | 367, 372,
373, 378 | iblsub 25202 |
. . . . . . . . . . . . . . . . 17
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (π₯ β π΄)) β
πΏ1) |
422 | 411, 420,
421 | itgmulc2 25214 |
. . . . . . . . . . . . . . . 16
β’ (β€
β ((1 / (π΅ β
π΄)) Β· β«(π΄[,]π΅)(π₯ β π΄) dπ₯) = β«(π΄[,]π΅)((1 / (π΅ β π΄)) Β· (π₯ β π΄)) dπ₯) |
423 | 422 | mptru 1549 |
. . . . . . . . . . . . . . 15
β’ ((1 /
(π΅ β π΄)) Β· β«(π΄[,]π΅)(π₯ β π΄) dπ₯) = β«(π΄[,]π΅)((1 / (π΅ β π΄)) Β· (π₯ β π΄)) dπ₯ |
424 | 412, 417 | mulcomi 11170 |
. . . . . . . . . . . . . . . . 17
β’ ((1 /
(π΅ β π΄)) Β· (π΄ Β· (π΅ β π΄))) = ((π΄ Β· (π΅ β π΄)) Β· (1 / (π΅ β π΄))) |
425 | 417, 147,
21 | divreci 11907 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ Β· (π΅ β π΄)) / (π΅ β π΄)) = ((π΄ Β· (π΅ β π΄)) Β· (1 / (π΅ β π΄))) |
426 | 139, 147,
21 | divcan4i 11909 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ Β· (π΅ β π΄)) / (π΅ β π΄)) = π΄ |
427 | 424, 425,
426 | 3eqtr2i 2771 |
. . . . . . . . . . . . . . . 16
β’ ((1 /
(π΅ β π΄)) Β· (π΄ Β· (π΅ β π΄))) = π΄ |
428 | 427 | oveq2i 7373 |
. . . . . . . . . . . . . . 15
β’ (((1 /
(π΅ β π΄)) Β· (((π΅β2) β (π΄β2)) / 2)) β ((1 / (π΅ β π΄)) Β· (π΄ Β· (π΅ β π΄)))) = (((1 / (π΅ β π΄)) Β· (((π΅β2) β (π΄β2)) / 2)) β π΄) |
429 | 419, 423,
428 | 3eqtr3i 2773 |
. . . . . . . . . . . . . 14
β’
β«(π΄[,]π΅)((1 / (π΅ β π΄)) Β· (π₯ β π΄)) dπ₯ = (((1 / (π΅ β π΄)) Β· (((π΅β2) β (π΄β2)) / 2)) β π΄) |
430 | 366, 429 | eqtri 2765 |
. . . . . . . . . . . . 13
β’
β«(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) dπ₯ = (((1 / (π΅ β π΄)) Β· (((π΅β2) β (π΄β2)) / 2)) β π΄) |
431 | 14, 139 | subsqi 14124 |
. . . . . . . . . . . . . . . . 17
β’ ((π΅β2) β (π΄β2)) = ((π΅ + π΄) Β· (π΅ β π΄)) |
432 | 431 | oveq1i 7372 |
. . . . . . . . . . . . . . . 16
β’ (((π΅β2) β (π΄β2)) / 2) = (((π΅ + π΄) Β· (π΅ β π΄)) / 2) |
433 | 432 | oveq2i 7373 |
. . . . . . . . . . . . . . 15
β’ ((1 /
(π΅ β π΄)) Β· (((π΅β2) β (π΄β2)) / 2)) = ((1 / (π΅ β π΄)) Β· (((π΅ + π΄) Β· (π΅ β π΄)) / 2)) |
434 | 431, 415 | eqeltrri 2835 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ + π΄) Β· (π΅ β π΄)) β β |
435 | 412, 434,
300, 301 | divassi 11918 |
. . . . . . . . . . . . . . 15
β’ (((1 /
(π΅ β π΄)) Β· ((π΅ + π΄) Β· (π΅ β π΄))) / 2) = ((1 / (π΅ β π΄)) Β· (((π΅ + π΄) Β· (π΅ β π΄)) / 2)) |
436 | 412, 434 | mulcomi 11170 |
. . . . . . . . . . . . . . . . 17
β’ ((1 /
(π΅ β π΄)) Β· ((π΅ + π΄) Β· (π΅ β π΄))) = (((π΅ + π΄) Β· (π΅ β π΄)) Β· (1 / (π΅ β π΄))) |
437 | 434, 147,
21 | divreci 11907 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅ + π΄) Β· (π΅ β π΄)) / (π΅ β π΄)) = (((π΅ + π΄) Β· (π΅ β π΄)) Β· (1 / (π΅ β π΄))) |
438 | 14, 139 | addcli 11168 |
. . . . . . . . . . . . . . . . . 18
β’ (π΅ + π΄) β β |
439 | 438, 147,
21 | divcan4i 11909 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅ + π΄) Β· (π΅ β π΄)) / (π΅ β π΄)) = (π΅ + π΄) |
440 | 436, 437,
439 | 3eqtr2i 2771 |
. . . . . . . . . . . . . . . 16
β’ ((1 /
(π΅ β π΄)) Β· ((π΅ + π΄) Β· (π΅ β π΄))) = (π΅ + π΄) |
441 | 440 | oveq1i 7372 |
. . . . . . . . . . . . . . 15
β’ (((1 /
(π΅ β π΄)) Β· ((π΅ + π΄) Β· (π΅ β π΄))) / 2) = ((π΅ + π΄) / 2) |
442 | 433, 435,
441 | 3eqtr2i 2771 |
. . . . . . . . . . . . . 14
β’ ((1 /
(π΅ β π΄)) Β· (((π΅β2) β (π΄β2)) / 2)) = ((π΅ + π΄) / 2) |
443 | 442 | oveq1i 7372 |
. . . . . . . . . . . . 13
β’ (((1 /
(π΅ β π΄)) Β· (((π΅β2) β (π΄β2)) / 2)) β π΄) = (((π΅ + π΄) / 2) β π΄) |
444 | 139, 300 | mulcli 11169 |
. . . . . . . . . . . . . . 15
β’ (π΄ Β· 2) β
β |
445 | | divsubdir 11856 |
. . . . . . . . . . . . . . 15
β’ (((π΅ + π΄) β β β§ (π΄ Β· 2) β β β§ (2 β
β β§ 2 β 0)) β (((π΅ + π΄) β (π΄ Β· 2)) / 2) = (((π΅ + π΄) / 2) β ((π΄ Β· 2) / 2))) |
446 | 438, 444,
293, 445 | mp3an 1462 |
. . . . . . . . . . . . . 14
β’ (((π΅ + π΄) β (π΄ Β· 2)) / 2) = (((π΅ + π΄) / 2) β ((π΄ Β· 2) / 2)) |
447 | 14, 139, 444 | addsubassi 11499 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ + π΄) β (π΄ Β· 2)) = (π΅ + (π΄ β (π΄ Β· 2))) |
448 | | subsub2 11436 |
. . . . . . . . . . . . . . . . 17
β’ ((π΅ β β β§ (π΄ Β· 2) β β
β§ π΄ β β)
β (π΅ β ((π΄ Β· 2) β π΄)) = (π΅ + (π΄ β (π΄ Β· 2)))) |
449 | 14, 444, 139, 448 | mp3an 1462 |
. . . . . . . . . . . . . . . 16
β’ (π΅ β ((π΄ Β· 2) β π΄)) = (π΅ + (π΄ β (π΄ Β· 2))) |
450 | 139 | times2i 12299 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ Β· 2) = (π΄ + π΄) |
451 | 450 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ Β· 2) β π΄) = ((π΄ + π΄) β π΄) |
452 | 139, 139 | pncan3oi 11424 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ + π΄) β π΄) = π΄ |
453 | 451, 452 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ Β· 2) β π΄) = π΄ |
454 | 453 | oveq2i 7373 |
. . . . . . . . . . . . . . . 16
β’ (π΅ β ((π΄ Β· 2) β π΄)) = (π΅ β π΄) |
455 | 447, 449,
454 | 3eqtr2i 2771 |
. . . . . . . . . . . . . . 15
β’ ((π΅ + π΄) β (π΄ Β· 2)) = (π΅ β π΄) |
456 | 455 | oveq1i 7372 |
. . . . . . . . . . . . . 14
β’ (((π΅ + π΄) β (π΄ Β· 2)) / 2) = ((π΅ β π΄) / 2) |
457 | 139, 300,
301 | divcan4i 11909 |
. . . . . . . . . . . . . . 15
β’ ((π΄ Β· 2) / 2) = π΄ |
458 | 457 | oveq2i 7373 |
. . . . . . . . . . . . . 14
β’ (((π΅ + π΄) / 2) β ((π΄ Β· 2) / 2)) = (((π΅ + π΄) / 2) β π΄) |
459 | 446, 456,
458 | 3eqtr3ri 2774 |
. . . . . . . . . . . . 13
β’ (((π΅ + π΄) / 2) β π΄) = ((π΅ β π΄) / 2) |
460 | 430, 443,
459 | 3eqtri 2769 |
. . . . . . . . . . . 12
β’
β«(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) dπ₯ = ((π΅ β π΄) / 2) |
461 | 460 | oveq2i 7373 |
. . . . . . . . . . 11
β’ ((πΉ β πΈ) Β· β«(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) dπ₯) = ((πΉ β πΈ) Β· ((π΅ β π΄) / 2)) |
462 | | itgeq2 25158 |
. . . . . . . . . . . 12
β’
(βπ₯ β
(π΄[,]π΅)((πΉ β πΈ) Β· ((π₯ β π΄) / (π΅ β π΄))) = (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)) β β«(π΄[,]π΅)((πΉ β πΈ) Β· ((π₯ β π΄) / (π΅ β π΄))) dπ₯ = β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)) dπ₯) |
463 | 61, 58 | subcli 11484 |
. . . . . . . . . . . . . 14
β’ (πΉ β πΈ) β β |
464 | 463 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β (πΉ β πΈ) β β) |
465 | 464, 127 | mulcomd 11183 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β ((πΉ β πΈ) Β· ((π₯ β π΄) / (π΅ β π΄))) = (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) |
466 | 462, 465 | mprg 3071 |
. . . . . . . . . . 11
β’
β«(π΄[,]π΅)((πΉ β πΈ) Β· ((π₯ β π΄) / (π΅ β π΄))) dπ₯ = β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)) dπ₯ |
467 | 362, 461,
466 | 3eqtr3ri 2774 |
. . . . . . . . . 10
β’
β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)) dπ₯ = ((πΉ β πΈ) Β· ((π΅ β π΄) / 2)) |
468 | 353, 467 | oveq12i 7374 |
. . . . . . . . 9
β’
(β«(π΄[,]π΅)πΈ dπ₯ + β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ)) dπ₯) = ((πΈ Β· (π΅ β π΄)) + ((πΉ β πΈ) Β· ((π΅ β π΄) / 2))) |
469 | 326, 340,
468 | 3eqtri 2769 |
. . . . . . . 8
β’
β«(π΄[,]π΅)π dπ₯ = ((πΈ Β· (π΅ β π΄)) + ((πΉ β πΈ) Β· ((π΅ β π΄) / 2))) |
470 | 147, 300,
301 | divcli 11904 |
. . . . . . . . 9
β’ ((π΅ β π΄) / 2) β β |
471 | 319, 463,
470 | adddiri 11175 |
. . . . . . . 8
β’ (((πΈ Β· 2) + (πΉ β πΈ)) Β· ((π΅ β π΄) / 2)) = (((πΈ Β· 2) Β· ((π΅ β π΄) / 2)) + ((πΉ β πΈ) Β· ((π΅ β π΄) / 2))) |
472 | 323, 469,
471 | 3eqtr4i 2775 |
. . . . . . 7
β’
β«(π΄[,]π΅)π dπ₯ = (((πΈ Β· 2) + (πΉ β πΈ)) Β· ((π΅ β π΄) / 2)) |
473 | | addsub12 11421 |
. . . . . . . . . 10
β’ ((πΉ β β β§ (πΈ Β· 2) β β
β§ πΈ β β)
β (πΉ + ((πΈ Β· 2) β πΈ)) = ((πΈ Β· 2) + (πΉ β πΈ))) |
474 | 61, 319, 58, 473 | mp3an 1462 |
. . . . . . . . 9
β’ (πΉ + ((πΈ Β· 2) β πΈ)) = ((πΈ Β· 2) + (πΉ β πΈ)) |
475 | 58 | times2i 12299 |
. . . . . . . . . . . 12
β’ (πΈ Β· 2) = (πΈ + πΈ) |
476 | 475 | oveq1i 7372 |
. . . . . . . . . . 11
β’ ((πΈ Β· 2) β πΈ) = ((πΈ + πΈ) β πΈ) |
477 | 58, 58 | pncan3oi 11424 |
. . . . . . . . . . 11
β’ ((πΈ + πΈ) β πΈ) = πΈ |
478 | 476, 477 | eqtri 2765 |
. . . . . . . . . 10
β’ ((πΈ Β· 2) β πΈ) = πΈ |
479 | 478 | oveq2i 7373 |
. . . . . . . . 9
β’ (πΉ + ((πΈ Β· 2) β πΈ)) = (πΉ + πΈ) |
480 | 474, 479 | eqtr3i 2767 |
. . . . . . . 8
β’ ((πΈ Β· 2) + (πΉ β πΈ)) = (πΉ + πΈ) |
481 | 480 | oveq1i 7372 |
. . . . . . 7
β’ (((πΈ Β· 2) + (πΉ β πΈ)) Β· ((π΅ β π΄) / 2)) = ((πΉ + πΈ) Β· ((π΅ β π΄) / 2)) |
482 | 472, 481 | eqtri 2765 |
. . . . . 6
β’
β«(π΄[,]π΅)π dπ₯ = ((πΉ + πΈ) Β· ((π΅ β π΄) / 2)) |
483 | 8, 300, 301 | divcan4i 11909 |
. . . . . . . . . . 11
β’ ((πΆ Β· 2) / 2) = πΆ |
484 | 483 | oveq1i 7372 |
. . . . . . . . . 10
β’ (((πΆ Β· 2) / 2) Β·
(π΅ β π΄)) = (πΆ Β· (π΅ β π΄)) |
485 | 8, 300 | mulcli 11169 |
. . . . . . . . . . 11
β’ (πΆ Β· 2) β
β |
486 | | div32 11840 |
. . . . . . . . . . 11
β’ (((πΆ Β· 2) β β
β§ (2 β β β§ 2 β 0) β§ (π΅ β π΄) β β) β (((πΆ Β· 2) / 2) Β·
(π΅ β π΄)) = ((πΆ Β· 2) Β· ((π΅ β π΄) / 2))) |
487 | 485, 293,
147, 486 | mp3an 1462 |
. . . . . . . . . 10
β’ (((πΆ Β· 2) / 2) Β·
(π΅ β π΄)) = ((πΆ Β· 2) Β· ((π΅ β π΄) / 2)) |
488 | 484, 487 | eqtr3i 2767 |
. . . . . . . . 9
β’ (πΆ Β· (π΅ β π΄)) = ((πΆ Β· 2) Β· ((π΅ β π΄) / 2)) |
489 | 488 | oveq1i 7372 |
. . . . . . . 8
β’ ((πΆ Β· (π΅ β π΄)) + ((π· β πΆ) Β· ((π΅ β π΄) / 2))) = (((πΆ Β· 2) Β· ((π΅ β π΄) / 2)) + ((π· β πΆ) Β· ((π΅ β π΄) / 2))) |
490 | 31 | a1i 11 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (π΄[,]π΅)) β π = (πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)))) |
491 | 490 | itgeq2dv 25162 |
. . . . . . . . . 10
β’ (β€
β β«(π΄[,]π΅)π dπ₯ = β«(π΄[,]π΅)(πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) dπ₯) |
492 | 491 | mptru 1549 |
. . . . . . . . 9
β’
β«(π΄[,]π΅)π dπ₯ = β«(π΄[,]π΅)(πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) dπ₯ |
493 | 7 | a1i 11 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (π΄[,]π΅)) β πΆ β β) |
494 | | cniccibl 25221 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ πΆ) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ πΆ) β
πΏ1) |
495 | 1, 2, 266, 494 | mp3an 1462 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β¦ πΆ) β
πΏ1 |
496 | 495 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ πΆ) β
πΏ1) |
497 | 25 | a1i 11 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (π΄[,]π΅)) β π· β β) |
498 | 497, 493 | resubcld 11590 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (π΄[,]π΅)) β (π· β πΆ) β β) |
499 | 331, 498 | remulcld 11192 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (π΄[,]π΅)) β (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)) β β) |
500 | 272 | mptru 1549 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) β ((π΄[,]π΅)βcnββ) |
501 | | cniccibl 25221 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) β
πΏ1) |
502 | 1, 2, 500, 501 | mp3an 1462 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) β
πΏ1 |
503 | 502 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β (π΄[,]π΅) β¦ (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) β
πΏ1) |
504 | 493, 496,
499, 503 | itgadd 25205 |
. . . . . . . . . 10
β’ (β€
β β«(π΄[,]π΅)(πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) dπ₯ = (β«(π΄[,]π΅)πΆ dπ₯ + β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)) dπ₯)) |
505 | 504 | mptru 1549 |
. . . . . . . . 9
β’
β«(π΄[,]π΅)(πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) dπ₯ = (β«(π΄[,]π΅)πΆ dπ₯ + β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)) dπ₯) |
506 | | itgconst 25199 |
. . . . . . . . . . . 12
β’ (((π΄[,]π΅) β dom vol β§ (volβ(π΄[,]π΅)) β β β§ πΆ β β) β β«(π΄[,]π΅)πΆ dπ₯ = (πΆ Β· (volβ(π΄[,]π΅)))) |
507 | 342, 349,
8, 506 | mp3an 1462 |
. . . . . . . . . . 11
β’
β«(π΄[,]π΅)πΆ dπ₯ = (πΆ Β· (volβ(π΄[,]π΅))) |
508 | 348 | oveq2i 7373 |
. . . . . . . . . . 11
β’ (πΆ Β· (volβ(π΄[,]π΅))) = (πΆ Β· (π΅ β π΄)) |
509 | 507, 508 | eqtri 2765 |
. . . . . . . . . 10
β’
β«(π΄[,]π΅)πΆ dπ₯ = (πΆ Β· (π΅ β π΄)) |
510 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (β€
β π· β
β) |
511 | 8 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (β€
β πΆ β
β) |
512 | 510, 511 | subcld 11519 |
. . . . . . . . . . . . 13
β’ (β€
β (π· β πΆ) β
β) |
513 | 512, 331,
360 | itgmulc2 25214 |
. . . . . . . . . . . 12
β’ (β€
β ((π· β πΆ) Β· β«(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) dπ₯) = β«(π΄[,]π΅)((π· β πΆ) Β· ((π₯ β π΄) / (π΅ β π΄))) dπ₯) |
514 | 513 | mptru 1549 |
. . . . . . . . . . 11
β’ ((π· β πΆ) Β· β«(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) dπ₯) = β«(π΄[,]π΅)((π· β πΆ) Β· ((π₯ β π΄) / (π΅ β π΄))) dπ₯ |
515 | 460 | oveq2i 7373 |
. . . . . . . . . . 11
β’ ((π· β πΆ) Β· β«(π΄[,]π΅)((π₯ β π΄) / (π΅ β π΄)) dπ₯) = ((π· β πΆ) Β· ((π΅ β π΄) / 2)) |
516 | | itgeq2 25158 |
. . . . . . . . . . . 12
β’
(βπ₯ β
(π΄[,]π΅)((π· β πΆ) Β· ((π₯ β π΄) / (π΅ β π΄))) = (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)) β β«(π΄[,]π΅)((π· β πΆ) Β· ((π₯ β π΄) / (π΅ β π΄))) dπ₯ = β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)) dπ₯) |
517 | 26, 8 | subcli 11484 |
. . . . . . . . . . . . . 14
β’ (π· β πΆ) β β |
518 | 517 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β (π· β πΆ) β β) |
519 | 518, 127 | mulcomd 11183 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β ((π· β πΆ) Β· ((π₯ β π΄) / (π΅ β π΄))) = (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) |
520 | 516, 519 | mprg 3071 |
. . . . . . . . . . 11
β’
β«(π΄[,]π΅)((π· β πΆ) Β· ((π₯ β π΄) / (π΅ β π΄))) dπ₯ = β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)) dπ₯ |
521 | 514, 515,
520 | 3eqtr3ri 2774 |
. . . . . . . . . 10
β’
β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)) dπ₯ = ((π· β πΆ) Β· ((π΅ β π΄) / 2)) |
522 | 509, 521 | oveq12i 7374 |
. . . . . . . . 9
β’
(β«(π΄[,]π΅)πΆ dπ₯ + β«(π΄[,]π΅)(((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ)) dπ₯) = ((πΆ Β· (π΅ β π΄)) + ((π· β πΆ) Β· ((π΅ β π΄) / 2))) |
523 | 492, 505,
522 | 3eqtri 2769 |
. . . . . . . 8
β’
β«(π΄[,]π΅)π dπ₯ = ((πΆ Β· (π΅ β π΄)) + ((π· β πΆ) Β· ((π΅ β π΄) / 2))) |
524 | 485, 517,
470 | adddiri 11175 |
. . . . . . . 8
β’ (((πΆ Β· 2) + (π· β πΆ)) Β· ((π΅ β π΄) / 2)) = (((πΆ Β· 2) Β· ((π΅ β π΄) / 2)) + ((π· β πΆ) Β· ((π΅ β π΄) / 2))) |
525 | 489, 523,
524 | 3eqtr4i 2775 |
. . . . . . 7
β’
β«(π΄[,]π΅)π dπ₯ = (((πΆ Β· 2) + (π· β πΆ)) Β· ((π΅ β π΄) / 2)) |
526 | | addsub12 11421 |
. . . . . . . . . 10
β’ ((π· β β β§ (πΆ Β· 2) β β
β§ πΆ β β)
β (π· + ((πΆ Β· 2) β πΆ)) = ((πΆ Β· 2) + (π· β πΆ))) |
527 | 26, 485, 8, 526 | mp3an 1462 |
. . . . . . . . 9
β’ (π· + ((πΆ Β· 2) β πΆ)) = ((πΆ Β· 2) + (π· β πΆ)) |
528 | 8 | times2i 12299 |
. . . . . . . . . . . 12
β’ (πΆ Β· 2) = (πΆ + πΆ) |
529 | 528 | oveq1i 7372 |
. . . . . . . . . . 11
β’ ((πΆ Β· 2) β πΆ) = ((πΆ + πΆ) β πΆ) |
530 | 8, 8 | pncan3oi 11424 |
. . . . . . . . . . 11
β’ ((πΆ + πΆ) β πΆ) = πΆ |
531 | 529, 530 | eqtri 2765 |
. . . . . . . . . 10
β’ ((πΆ Β· 2) β πΆ) = πΆ |
532 | 531 | oveq2i 7373 |
. . . . . . . . 9
β’ (π· + ((πΆ Β· 2) β πΆ)) = (π· + πΆ) |
533 | 527, 532 | eqtr3i 2767 |
. . . . . . . 8
β’ ((πΆ Β· 2) + (π· β πΆ)) = (π· + πΆ) |
534 | 533 | oveq1i 7372 |
. . . . . . 7
β’ (((πΆ Β· 2) + (π· β πΆ)) Β· ((π΅ β π΄) / 2)) = ((π· + πΆ) Β· ((π΅ β π΄) / 2)) |
535 | 525, 534 | eqtri 2765 |
. . . . . 6
β’
β«(π΄[,]π΅)π dπ₯ = ((π· + πΆ) Β· ((π΅ β π΄) / 2)) |
536 | 482, 535 | oveq12i 7374 |
. . . . 5
β’
(β«(π΄[,]π΅)π dπ₯ β β«(π΄[,]π΅)π dπ₯) = (((πΉ + πΈ) Β· ((π΅ β π΄) / 2)) β ((π· + πΆ) Β· ((π΅ β π΄) / 2))) |
537 | 316, 536 | eqtri 2765 |
. . . 4
β’
β«(π΄[,]π΅)(π β π) dπ₯ = (((πΉ + πΈ) Β· ((π΅ β π΄) / 2)) β ((π· + πΆ) Β· ((π΅ β π΄) / 2))) |
538 | 299, 304,
537 | 3eqtr4ri 2776 |
. . 3
β’
β«(π΄[,]π΅)(π β π) dπ₯ = ((((πΉ + πΈ) / 2) β ((π· + πΆ) / 2)) Β· (π΅ β π΄)) |
539 | 289, 291,
538 | 3eqtr2i 2771 |
. 2
β’
β«β(volβ(π β {π₯})) dπ₯ = ((((πΉ + πΈ) / 2) β ((π· + πΆ) / 2)) Β· (π΅ β π΄)) |
540 | 286, 539 | eqtri 2765 |
1
β’
(areaβπ) =
((((πΉ + πΈ) / 2) β ((π· + πΆ) / 2)) Β· (π΅ β π΄)) |