Step | Hyp | Ref
| Expression |
1 | | 1red 11211 |
. . . 4
β’ (β€
β 1 β β) |
2 | | 2re 12282 |
. . . . 5
β’ 2 β
β |
3 | 2 | a1i 11 |
. . . 4
β’ (β€
β 2 β β) |
4 | | 1le2 12417 |
. . . . 5
β’ 1 β€
2 |
5 | 4 | a1i 11 |
. . . 4
β’ (β€
β 1 β€ 2) |
6 | | reelprrecn 11198 |
. . . . . . 7
β’ β
β {β, β} |
7 | 6 | a1i 11 |
. . . . . 6
β’ (β€
β β β {β, β}) |
8 | | recn 11196 |
. . . . . . . . . 10
β’ (π¦ β β β π¦ β
β) |
9 | | 3nn0 12486 |
. . . . . . . . . . 11
β’ 3 β
β0 |
10 | | expcl 14041 |
. . . . . . . . . . 11
β’ ((π¦ β β β§ 3 β
β0) β (π¦β3) β β) |
11 | 9, 10 | mpan2 690 |
. . . . . . . . . 10
β’ (π¦ β β β (π¦β3) β
β) |
12 | 8, 11 | syl 17 |
. . . . . . . . 9
β’ (π¦ β β β (π¦β3) β
β) |
13 | | 3cn 12289 |
. . . . . . . . . 10
β’ 3 β
β |
14 | | 3ne0 12314 |
. . . . . . . . . 10
β’ 3 β
0 |
15 | | divcl 11874 |
. . . . . . . . . 10
β’ (((π¦β3) β β β§ 3
β β β§ 3 β 0) β ((π¦β3) / 3) β
β) |
16 | 13, 14, 15 | mp3an23 1454 |
. . . . . . . . 9
β’ ((π¦β3) β β β
((π¦β3) / 3) β
β) |
17 | 12, 16 | syl 17 |
. . . . . . . 8
β’ (π¦ β β β ((π¦β3) / 3) β
β) |
18 | | mulcl 11190 |
. . . . . . . . 9
β’ ((3
β β β§ π¦
β β) β (3 Β· π¦) β β) |
19 | 13, 8, 18 | sylancr 588 |
. . . . . . . 8
β’ (π¦ β β β (3
Β· π¦) β
β) |
20 | 17, 19 | subcld 11567 |
. . . . . . 7
β’ (π¦ β β β (((π¦β3) / 3) β (3
Β· π¦)) β
β) |
21 | 20 | adantl 483 |
. . . . . 6
β’
((β€ β§ π¦
β β) β (((π¦β3) / 3) β (3 Β· π¦)) β
β) |
22 | | ovexd 7439 |
. . . . . 6
β’
((β€ β§ π¦
β β) β ((π¦β2) β 3) β
V) |
23 | 17 | adantl 483 |
. . . . . . 7
β’
((β€ β§ π¦
β β) β ((π¦β3) / 3) β
β) |
24 | | ovexd 7439 |
. . . . . . 7
β’
((β€ β§ π¦
β β) β (π¦β2) β V) |
25 | | divrec2 11885 |
. . . . . . . . . . . . 13
β’ (((π¦β3) β β β§ 3
β β β§ 3 β 0) β ((π¦β3) / 3) = ((1 / 3) Β· (π¦β3))) |
26 | 13, 14, 25 | mp3an23 1454 |
. . . . . . . . . . . 12
β’ ((π¦β3) β β β
((π¦β3) / 3) = ((1 / 3)
Β· (π¦β3))) |
27 | 12, 26 | syl 17 |
. . . . . . . . . . 11
β’ (π¦ β β β ((π¦β3) / 3) = ((1 / 3)
Β· (π¦β3))) |
28 | 27 | mpteq2ia 5250 |
. . . . . . . . . 10
β’ (π¦ β β β¦ ((π¦β3) / 3)) = (π¦ β β β¦ ((1 / 3)
Β· (π¦β3))) |
29 | 28 | oveq2i 7415 |
. . . . . . . . 9
β’ (β
D (π¦ β β β¦
((π¦β3) / 3))) =
(β D (π¦ β
β β¦ ((1 / 3) Β· (π¦β3)))) |
30 | 12 | adantl 483 |
. . . . . . . . . . 11
β’
((β€ β§ π¦
β β) β (π¦β3) β β) |
31 | | ovexd 7439 |
. . . . . . . . . . 11
β’
((β€ β§ π¦
β β) β (3 Β· (π¦β2)) β V) |
32 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β¦ (π¦β3)) = (π¦ β β β¦ (π¦β3)) |
33 | 32, 11 | fmpti 7107 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β¦ (π¦β3)):ββΆβ |
34 | | ssid 4003 |
. . . . . . . . . . . . . 14
β’ β
β β |
35 | | ax-resscn 11163 |
. . . . . . . . . . . . . . 15
β’ β
β β |
36 | | ovex 7437 |
. . . . . . . . . . . . . . . 16
β’ (3
Β· (π¦β2)) β
V |
37 | | 3nn 12287 |
. . . . . . . . . . . . . . . . . 18
β’ 3 β
β |
38 | | dvexp 25452 |
. . . . . . . . . . . . . . . . . 18
β’ (3 β
β β (β D (π¦ β β β¦ (π¦β3))) = (π¦ β β β¦ (3 Β· (π¦β(3 β
1))))) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ (β
D (π¦ β β β¦
(π¦β3))) = (π¦ β β β¦ (3
Β· (π¦β(3 β
1)))) |
40 | | 3m1e2 12336 |
. . . . . . . . . . . . . . . . . . . 20
β’ (3
β 1) = 2 |
41 | 40 | oveq2i 7415 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦β(3 β 1)) = (π¦β2) |
42 | 41 | oveq2i 7415 |
. . . . . . . . . . . . . . . . . 18
β’ (3
Β· (π¦β(3 β
1))) = (3 Β· (π¦β2)) |
43 | 42 | mpteq2i 5252 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β¦ (3
Β· (π¦β(3 β
1)))) = (π¦ β β
β¦ (3 Β· (π¦β2))) |
44 | 39, 43 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
β’ (β
D (π¦ β β β¦
(π¦β3))) = (π¦ β β β¦ (3
Β· (π¦β2))) |
45 | 36, 44 | dmmpti 6691 |
. . . . . . . . . . . . . . 15
β’ dom
(β D (π¦ β
β β¦ (π¦β3))) = β |
46 | 35, 45 | sseqtrri 4018 |
. . . . . . . . . . . . . 14
β’ β
β dom (β D (π¦
β β β¦ (π¦β3))) |
47 | | dvres3 25412 |
. . . . . . . . . . . . . 14
β’
(((β β {β, β} β§ (π¦ β β β¦ (π¦β3)):ββΆβ) β§
(β β β β§ β β dom (β D (π¦ β β β¦ (π¦β3))))) β (β D
((π¦ β β β¦
(π¦β3)) βΎ
β)) = ((β D (π¦
β β β¦ (π¦β3))) βΎ β)) |
48 | 6, 33, 34, 46, 47 | mp4an 692 |
. . . . . . . . . . . . 13
β’ (β
D ((π¦ β β
β¦ (π¦β3)) βΎ
β)) = ((β D (π¦
β β β¦ (π¦β3))) βΎ β) |
49 | | resmpt 6035 |
. . . . . . . . . . . . . . 15
β’ (β
β β β ((π¦
β β β¦ (π¦β3)) βΎ β) = (π¦ β β β¦ (π¦β3))) |
50 | 35, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β¦ (π¦β3)) βΎ β) =
(π¦ β β β¦
(π¦β3)) |
51 | 50 | oveq2i 7415 |
. . . . . . . . . . . . 13
β’ (β
D ((π¦ β β
β¦ (π¦β3)) βΎ
β)) = (β D (π¦
β β β¦ (π¦β3))) |
52 | 44 | reseq1i 5975 |
. . . . . . . . . . . . . 14
β’ ((β
D (π¦ β β β¦
(π¦β3))) βΎ
β) = ((π¦ β
β β¦ (3 Β· (π¦β2))) βΎ β) |
53 | | resmpt 6035 |
. . . . . . . . . . . . . . 15
β’ (β
β β β ((π¦
β β β¦ (3 Β· (π¦β2))) βΎ β) = (π¦ β β β¦ (3
Β· (π¦β2)))) |
54 | 35, 53 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β¦ (3
Β· (π¦β2)))
βΎ β) = (π¦
β β β¦ (3 Β· (π¦β2))) |
55 | 52, 54 | eqtri 2761 |
. . . . . . . . . . . . 13
β’ ((β
D (π¦ β β β¦
(π¦β3))) βΎ
β) = (π¦ β
β β¦ (3 Β· (π¦β2))) |
56 | 48, 51, 55 | 3eqtr3i 2769 |
. . . . . . . . . . . 12
β’ (β
D (π¦ β β β¦
(π¦β3))) = (π¦ β β β¦ (3
Β· (π¦β2))) |
57 | 56 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β (β D (π¦ β
β β¦ (π¦β3))) = (π¦ β β β¦ (3 Β· (π¦β2)))) |
58 | | ax-1cn 11164 |
. . . . . . . . . . . . 13
β’ 1 β
β |
59 | 58, 13, 14 | divcli 11952 |
. . . . . . . . . . . 12
β’ (1 / 3)
β β |
60 | 59 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β (1 / 3) β β) |
61 | 7, 30, 31, 57, 60 | dvmptcmul 25463 |
. . . . . . . . . 10
β’ (β€
β (β D (π¦ β
β β¦ ((1 / 3) Β· (π¦β3)))) = (π¦ β β β¦ ((1 / 3) Β· (3
Β· (π¦β2))))) |
62 | 61 | mptru 1549 |
. . . . . . . . 9
β’ (β
D (π¦ β β β¦
((1 / 3) Β· (π¦β3)))) = (π¦ β β β¦ ((1 / 3) Β· (3
Β· (π¦β2)))) |
63 | | sqcl 14079 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (π¦β2) β
β) |
64 | | mulcl 11190 |
. . . . . . . . . . . . 13
β’ ((3
β β β§ (π¦β2) β β) β (3 Β·
(π¦β2)) β
β) |
65 | 13, 63, 64 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π¦ β β β (3
Β· (π¦β2)) β
β) |
66 | | divrec2 11885 |
. . . . . . . . . . . . 13
β’ (((3
Β· (π¦β2)) β
β β§ 3 β β β§ 3 β 0) β ((3 Β· (π¦β2)) / 3) = ((1 / 3)
Β· (3 Β· (π¦β2)))) |
67 | 13, 14, 66 | mp3an23 1454 |
. . . . . . . . . . . 12
β’ ((3
Β· (π¦β2)) β
β β ((3 Β· (π¦β2)) / 3) = ((1 / 3) Β· (3
Β· (π¦β2)))) |
68 | 8, 65, 67 | 3syl 18 |
. . . . . . . . . . 11
β’ (π¦ β β β ((3
Β· (π¦β2)) / 3) =
((1 / 3) Β· (3 Β· (π¦β2)))) |
69 | | divcan3 11894 |
. . . . . . . . . . . . 13
β’ (((π¦β2) β β β§ 3
β β β§ 3 β 0) β ((3 Β· (π¦β2)) / 3) = (π¦β2)) |
70 | 13, 14, 69 | mp3an23 1454 |
. . . . . . . . . . . 12
β’ ((π¦β2) β β β
((3 Β· (π¦β2)) /
3) = (π¦β2)) |
71 | 8, 63, 70 | 3syl 18 |
. . . . . . . . . . 11
β’ (π¦ β β β ((3
Β· (π¦β2)) / 3) =
(π¦β2)) |
72 | 68, 71 | eqtr3d 2775 |
. . . . . . . . . 10
β’ (π¦ β β β ((1 / 3)
Β· (3 Β· (π¦β2))) = (π¦β2)) |
73 | 72 | mpteq2ia 5250 |
. . . . . . . . 9
β’ (π¦ β β β¦ ((1 / 3)
Β· (3 Β· (π¦β2)))) = (π¦ β β β¦ (π¦β2)) |
74 | 29, 62, 73 | 3eqtri 2765 |
. . . . . . . 8
β’ (β
D (π¦ β β β¦
((π¦β3) / 3))) = (π¦ β β β¦ (π¦β2)) |
75 | 74 | a1i 11 |
. . . . . . 7
β’ (β€
β (β D (π¦ β
β β¦ ((π¦β3)
/ 3))) = (π¦ β β
β¦ (π¦β2))) |
76 | 19 | adantl 483 |
. . . . . . 7
β’
((β€ β§ π¦
β β) β (3 Β· π¦) β β) |
77 | | 3ex 12290 |
. . . . . . . 8
β’ 3 β
V |
78 | 77 | a1i 11 |
. . . . . . 7
β’
((β€ β§ π¦
β β) β 3 β V) |
79 | 8 | adantl 483 |
. . . . . . . . 9
β’
((β€ β§ π¦
β β) β π¦
β β) |
80 | | 1red 11211 |
. . . . . . . . 9
β’
((β€ β§ π¦
β β) β 1 β β) |
81 | 7 | dvmptid 25456 |
. . . . . . . . 9
β’ (β€
β (β D (π¦ β
β β¦ π¦)) =
(π¦ β β β¦
1)) |
82 | 13 | a1i 11 |
. . . . . . . . 9
β’ (β€
β 3 β β) |
83 | 7, 79, 80, 81, 82 | dvmptcmul 25463 |
. . . . . . . 8
β’ (β€
β (β D (π¦ β
β β¦ (3 Β· π¦))) = (π¦ β β β¦ (3 Β·
1))) |
84 | | 3t1e3 12373 |
. . . . . . . . 9
β’ (3
Β· 1) = 3 |
85 | 84 | mpteq2i 5252 |
. . . . . . . 8
β’ (π¦ β β β¦ (3
Β· 1)) = (π¦ β
β β¦ 3) |
86 | 83, 85 | eqtrdi 2789 |
. . . . . . 7
β’ (β€
β (β D (π¦ β
β β¦ (3 Β· π¦))) = (π¦ β β β¦ 3)) |
87 | 7, 23, 24, 75, 76, 78, 86 | dvmptsub 25466 |
. . . . . 6
β’ (β€
β (β D (π¦ β
β β¦ (((π¦β3) / 3) β (3 Β· π¦)))) = (π¦ β β β¦ ((π¦β2) β 3))) |
88 | | 1re 11210 |
. . . . . . . 8
β’ 1 β
β |
89 | | iccssre 13402 |
. . . . . . . 8
β’ ((1
β β β§ 2 β β) β (1[,]2) β
β) |
90 | 88, 2, 89 | mp2an 691 |
. . . . . . 7
β’ (1[,]2)
β β |
91 | 90 | a1i 11 |
. . . . . 6
β’ (β€
β (1[,]2) β β) |
92 | | eqid 2733 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
93 | 92 | tgioo2 24301 |
. . . . . 6
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
94 | | iccntr 24319 |
. . . . . . . 8
β’ ((1
β β β§ 2 β β) β ((intβ(topGenβran
(,)))β(1[,]2)) = (1(,)2)) |
95 | 88, 2, 94 | mp2an 691 |
. . . . . . 7
β’
((intβ(topGenβran (,)))β(1[,]2)) =
(1(,)2) |
96 | 95 | a1i 11 |
. . . . . 6
β’ (β€
β ((intβ(topGenβran (,)))β(1[,]2)) =
(1(,)2)) |
97 | 7, 21, 22, 87, 91, 93, 92, 96 | dvmptres2 25461 |
. . . . 5
β’ (β€
β (β D (π¦ β
(1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦)))) = (π¦ β (1(,)2) β¦ ((π¦β2) β 3))) |
98 | | ioossicc 13406 |
. . . . . . 7
β’ (1(,)2)
β (1[,]2) |
99 | | resmpt 6035 |
. . . . . . 7
β’ ((1(,)2)
β (1[,]2) β ((π¦
β (1[,]2) β¦ ((π¦β2) β 3)) βΎ (1(,)2)) =
(π¦ β (1(,)2) β¦
((π¦β2) β
3))) |
100 | 98, 99 | ax-mp 5 |
. . . . . 6
β’ ((π¦ β (1[,]2) β¦ ((π¦β2) β 3)) βΎ
(1(,)2)) = (π¦ β
(1(,)2) β¦ ((π¦β2)
β 3)) |
101 | 90, 35 | sstri 3990 |
. . . . . . . . 9
β’ (1[,]2)
β β |
102 | | resmpt 6035 |
. . . . . . . . 9
β’ ((1[,]2)
β β β ((π¦
β β β¦ ((π¦β2) β 3)) βΎ (1[,]2)) =
(π¦ β (1[,]2) β¦
((π¦β2) β
3))) |
103 | 101, 102 | ax-mp 5 |
. . . . . . . 8
β’ ((π¦ β β β¦ ((π¦β2) β 3)) βΎ
(1[,]2)) = (π¦ β
(1[,]2) β¦ ((π¦β2)
β 3)) |
104 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π¦ β β β¦ ((π¦β2) β 3)) = (π¦ β β β¦ ((π¦β2) β
3)) |
105 | | subcl 11455 |
. . . . . . . . . . . . . 14
β’ (((π¦β2) β β β§ 3
β β) β ((π¦β2) β 3) β
β) |
106 | 13, 105 | mpan2 690 |
. . . . . . . . . . . . 13
β’ ((π¦β2) β β β
((π¦β2) β 3)
β β) |
107 | 63, 106 | syl 17 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((π¦β2) β 3) β
β) |
108 | 104, 107 | fmpti 7107 |
. . . . . . . . . . 11
β’ (π¦ β β β¦ ((π¦β2) β
3)):ββΆβ |
109 | 34, 108, 34 | 3pm3.2i 1340 |
. . . . . . . . . 10
β’ (β
β β β§ (π¦
β β β¦ ((π¦β2) β 3)):ββΆβ
β§ β β β) |
110 | | ovex 7437 |
. . . . . . . . . . 11
β’ ((2
Β· (π¦β(2 β
1))) β 0) β V |
111 | | cnelprrecn 11199 |
. . . . . . . . . . . . . 14
β’ β
β {β, β} |
112 | 111 | a1i 11 |
. . . . . . . . . . . . 13
β’ (β€
β β β {β, β}) |
113 | 63 | adantl 483 |
. . . . . . . . . . . . 13
β’
((β€ β§ π¦
β β) β (π¦β2) β β) |
114 | | ovexd 7439 |
. . . . . . . . . . . . 13
β’
((β€ β§ π¦
β β) β (2 Β· (π¦β(2 β 1))) β
V) |
115 | | 2nn 12281 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
116 | | dvexp 25452 |
. . . . . . . . . . . . . . 15
β’ (2 β
β β (β D (π¦ β β β¦ (π¦β2))) = (π¦ β β β¦ (2 Β· (π¦β(2 β
1))))) |
117 | 115, 116 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (β
D (π¦ β β β¦
(π¦β2))) = (π¦ β β β¦ (2
Β· (π¦β(2 β
1)))) |
118 | 117 | a1i 11 |
. . . . . . . . . . . . 13
β’ (β€
β (β D (π¦ β
β β¦ (π¦β2))) = (π¦ β β β¦ (2 Β· (π¦β(2 β
1))))) |
119 | 13 | a1i 11 |
. . . . . . . . . . . . 13
β’
((β€ β§ π¦
β β) β 3 β β) |
120 | | c0ex 11204 |
. . . . . . . . . . . . . 14
β’ 0 β
V |
121 | 120 | a1i 11 |
. . . . . . . . . . . . 13
β’
((β€ β§ π¦
β β) β 0 β V) |
122 | 112, 82 | dvmptc 25457 |
. . . . . . . . . . . . 13
β’ (β€
β (β D (π¦ β
β β¦ 3)) = (π¦
β β β¦ 0)) |
123 | 112, 113,
114, 118, 119, 121, 122 | dvmptsub 25466 |
. . . . . . . . . . . 12
β’ (β€
β (β D (π¦ β
β β¦ ((π¦β2)
β 3))) = (π¦ β
β β¦ ((2 Β· (π¦β(2 β 1))) β
0))) |
124 | 123 | mptru 1549 |
. . . . . . . . . . 11
β’ (β
D (π¦ β β β¦
((π¦β2) β 3))) =
(π¦ β β β¦
((2 Β· (π¦β(2
β 1))) β 0)) |
125 | 110, 124 | dmmpti 6691 |
. . . . . . . . . 10
β’ dom
(β D (π¦ β
β β¦ ((π¦β2)
β 3))) = β |
126 | | dvcn 25420 |
. . . . . . . . . 10
β’
(((β β β β§ (π¦ β β β¦ ((π¦β2) β 3)):ββΆβ
β§ β β β) β§ dom (β D (π¦ β β β¦ ((π¦β2) β 3))) = β) β
(π¦ β β β¦
((π¦β2) β 3))
β (ββcnββ)) |
127 | 109, 125,
126 | mp2an 691 |
. . . . . . . . 9
β’ (π¦ β β β¦ ((π¦β2) β 3)) β
(ββcnββ) |
128 | | rescncf 24395 |
. . . . . . . . 9
β’ ((1[,]2)
β β β ((π¦
β β β¦ ((π¦β2) β 3)) β
(ββcnββ) β
((π¦ β β β¦
((π¦β2) β 3))
βΎ (1[,]2)) β ((1[,]2)βcnββ))) |
129 | 101, 127,
128 | mp2 9 |
. . . . . . . 8
β’ ((π¦ β β β¦ ((π¦β2) β 3)) βΎ
(1[,]2)) β ((1[,]2)βcnββ) |
130 | 103, 129 | eqeltrri 2831 |
. . . . . . 7
β’ (π¦ β (1[,]2) β¦ ((π¦β2) β 3)) β
((1[,]2)βcnββ) |
131 | | rescncf 24395 |
. . . . . . 7
β’ ((1(,)2)
β (1[,]2) β ((π¦
β (1[,]2) β¦ ((π¦β2) β 3)) β
((1[,]2)βcnββ) β
((π¦ β (1[,]2) β¦
((π¦β2) β 3))
βΎ (1(,)2)) β ((1(,)2)βcnββ))) |
132 | 98, 130, 131 | mp2 9 |
. . . . . 6
β’ ((π¦ β (1[,]2) β¦ ((π¦β2) β 3)) βΎ
(1(,)2)) β ((1(,)2)βcnββ) |
133 | 100, 132 | eqeltrri 2831 |
. . . . 5
β’ (π¦ β (1(,)2) β¦ ((π¦β2) β 3)) β
((1(,)2)βcnββ) |
134 | 97, 133 | eqeltrdi 2842 |
. . . 4
β’ (β€
β (β D (π¦ β
(1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦)))) β ((1(,)2)βcnββ)) |
135 | 98 | a1i 11 |
. . . . . 6
β’ (β€
β (1(,)2) β (1[,]2)) |
136 | | ioombl 25064 |
. . . . . . 7
β’ (1(,)2)
β dom vol |
137 | 136 | a1i 11 |
. . . . . 6
β’ (β€
β (1(,)2) β dom vol) |
138 | | ovexd 7439 |
. . . . . 6
β’
((β€ β§ π¦
β (1[,]2)) β ((π¦β2) β 3) β
V) |
139 | | cniccibl 25340 |
. . . . . . . 8
β’ ((1
β β β§ 2 β β β§ (π¦ β (1[,]2) β¦ ((π¦β2) β 3)) β
((1[,]2)βcnββ)) β
(π¦ β (1[,]2) β¦
((π¦β2) β 3))
β πΏ1) |
140 | 88, 2, 130, 139 | mp3an 1462 |
. . . . . . 7
β’ (π¦ β (1[,]2) β¦ ((π¦β2) β 3)) β
πΏ1 |
141 | 140 | a1i 11 |
. . . . . 6
β’ (β€
β (π¦ β (1[,]2)
β¦ ((π¦β2) β
3)) β πΏ1) |
142 | 135, 137,
138, 141 | iblss 25304 |
. . . . 5
β’ (β€
β (π¦ β (1(,)2)
β¦ ((π¦β2) β
3)) β πΏ1) |
143 | 97, 142 | eqeltrd 2834 |
. . . 4
β’ (β€
β (β D (π¦ β
(1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦)))) β
πΏ1) |
144 | | resmpt 6035 |
. . . . . . 7
β’ ((1[,]2)
β β β ((π¦
β β β¦ (((π¦β3) / 3) β (3 Β· π¦))) βΎ (1[,]2)) = (π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦)))) |
145 | 90, 144 | ax-mp 5 |
. . . . . 6
β’ ((π¦ β β β¦ (((π¦β3) / 3) β (3
Β· π¦))) βΎ
(1[,]2)) = (π¦ β
(1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦))) |
146 | | eqid 2733 |
. . . . . . . . . 10
β’ (π¦ β β β¦ (((π¦β3) / 3) β (3
Β· π¦))) = (π¦ β β β¦ (((π¦β3) / 3) β (3
Β· π¦))) |
147 | 146, 20 | fmpti 7107 |
. . . . . . . . 9
β’ (π¦ β β β¦ (((π¦β3) / 3) β (3
Β· π¦))):ββΆβ |
148 | | ssid 4003 |
. . . . . . . . 9
β’ β
β β |
149 | 35, 147, 148 | 3pm3.2i 1340 |
. . . . . . . 8
β’ (β
β β β§ (π¦
β β β¦ (((π¦β3) / 3) β (3 Β· π¦))):ββΆβ β§
β β β) |
150 | | ovex 7437 |
. . . . . . . . 9
β’ ((π¦β2) β 3) β
V |
151 | 87 | mptru 1549 |
. . . . . . . . 9
β’ (β
D (π¦ β β β¦
(((π¦β3) / 3) β
(3 Β· π¦)))) = (π¦ β β β¦ ((π¦β2) β
3)) |
152 | 150, 151 | dmmpti 6691 |
. . . . . . . 8
β’ dom
(β D (π¦ β
β β¦ (((π¦β3) / 3) β (3 Β· π¦)))) = β |
153 | | dvcn 25420 |
. . . . . . . 8
β’
(((β β β β§ (π¦ β β β¦ (((π¦β3) / 3) β (3 Β· π¦))):ββΆβ β§
β β β) β§ dom (β D (π¦ β β β¦ (((π¦β3) / 3) β (3 Β· π¦)))) = β) β (π¦ β β β¦ (((π¦β3) / 3) β (3
Β· π¦))) β
(ββcnββ)) |
154 | 149, 152,
153 | mp2an 691 |
. . . . . . 7
β’ (π¦ β β β¦ (((π¦β3) / 3) β (3
Β· π¦))) β
(ββcnββ) |
155 | | rescncf 24395 |
. . . . . . 7
β’ ((1[,]2)
β β β ((π¦
β β β¦ (((π¦β3) / 3) β (3 Β· π¦))) β (ββcnββ) β ((π¦ β β β¦ (((π¦β3) / 3) β (3 Β· π¦))) βΎ (1[,]2)) β
((1[,]2)βcnββ))) |
156 | 90, 154, 155 | mp2 9 |
. . . . . 6
β’ ((π¦ β β β¦ (((π¦β3) / 3) β (3
Β· π¦))) βΎ
(1[,]2)) β ((1[,]2)βcnββ) |
157 | 145, 156 | eqeltrri 2831 |
. . . . 5
β’ (π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦))) β
((1[,]2)βcnββ) |
158 | 157 | a1i 11 |
. . . 4
β’ (β€
β (π¦ β (1[,]2)
β¦ (((π¦β3) / 3)
β (3 Β· π¦)))
β ((1[,]2)βcnββ)) |
159 | 1, 3, 5, 134, 143, 158 | ftc2 25543 |
. . 3
β’ (β€
β β«(1(,)2)((β D (π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦))))βπ₯) dπ₯ = (((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦)))β2) β ((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦)))β1))) |
160 | 159 | mptru 1549 |
. 2
β’
β«(1(,)2)((β D (π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦))))βπ₯) dπ₯ = (((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦)))β2) β ((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦)))β1)) |
161 | | itgeq2 25277 |
. . 3
β’
(βπ₯ β
(1(,)2)((β D (π¦
β (1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦))))βπ₯) = ((π₯β2) β 3) β
β«(1(,)2)((β D (π¦
β (1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦))))βπ₯) dπ₯ = β«(1(,)2)((π₯β2) β 3) dπ₯) |
162 | | oveq1 7411 |
. . . . 5
β’ (π¦ = π₯ β (π¦β2) = (π₯β2)) |
163 | 162 | oveq1d 7419 |
. . . 4
β’ (π¦ = π₯ β ((π¦β2) β 3) = ((π₯β2) β 3)) |
164 | 97 | mptru 1549 |
. . . 4
β’ (β
D (π¦ β (1[,]2) β¦
(((π¦β3) / 3) β
(3 Β· π¦)))) = (π¦ β (1(,)2) β¦ ((π¦β2) β
3)) |
165 | | ovex 7437 |
. . . 4
β’ ((π₯β2) β 3) β
V |
166 | 163, 164,
165 | fvmpt 6994 |
. . 3
β’ (π₯ β (1(,)2) β ((β
D (π¦ β (1[,]2) β¦
(((π¦β3) / 3) β
(3 Β· π¦))))βπ₯) = ((π₯β2) β 3)) |
167 | 161, 166 | mprg 3068 |
. 2
β’
β«(1(,)2)((β D (π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦))))βπ₯) dπ₯ = β«(1(,)2)((π₯β2) β 3) dπ₯ |
168 | 2 | leidi 11744 |
. . . . . . . . 9
β’ 2 β€
2 |
169 | 88, 2 | elicc2i 13386 |
. . . . . . . . 9
β’ (2 β
(1[,]2) β (2 β β β§ 1 β€ 2 β§ 2 β€
2)) |
170 | 2, 4, 168, 169 | mpbir3an 1342 |
. . . . . . . 8
β’ 2 β
(1[,]2) |
171 | | oveq1 7411 |
. . . . . . . . . . . 12
β’ (π¦ = 2 β (π¦β3) = (2β3)) |
172 | 171 | oveq1d 7419 |
. . . . . . . . . . 11
β’ (π¦ = 2 β ((π¦β3) / 3) = ((2β3) /
3)) |
173 | | oveq2 7412 |
. . . . . . . . . . 11
β’ (π¦ = 2 β (3 Β· π¦) = (3 Β·
2)) |
174 | 172, 173 | oveq12d 7422 |
. . . . . . . . . 10
β’ (π¦ = 2 β (((π¦β3) / 3) β (3
Β· π¦)) = (((2β3)
/ 3) β (3 Β· 2))) |
175 | | cu2 14160 |
. . . . . . . . . . . . 13
β’
(2β3) = 8 |
176 | 175 | oveq1i 7414 |
. . . . . . . . . . . 12
β’
((2β3) / 3) = (8 / 3) |
177 | | 3t2e6 12374 |
. . . . . . . . . . . 12
β’ (3
Β· 2) = 6 |
178 | 176, 177 | oveq12i 7416 |
. . . . . . . . . . 11
β’
(((2β3) / 3) β (3 Β· 2)) = ((8 / 3) β
6) |
179 | | 2cn 12283 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
180 | | 6cn 12299 |
. . . . . . . . . . . . . . 15
β’ 6 β
β |
181 | 179, 180,
13, 14 | divdiri 11967 |
. . . . . . . . . . . . . 14
β’ ((2 + 6)
/ 3) = ((2 / 3) + (6 / 3)) |
182 | | 6p2e8 12367 |
. . . . . . . . . . . . . . . 16
β’ (6 + 2) =
8 |
183 | 180, 179,
182 | addcomli 11402 |
. . . . . . . . . . . . . . 15
β’ (2 + 6) =
8 |
184 | 183 | oveq1i 7414 |
. . . . . . . . . . . . . 14
β’ ((2 + 6)
/ 3) = (8 / 3) |
185 | 180, 13, 179, 14 | divmuli 11964 |
. . . . . . . . . . . . . . . 16
β’ ((6 / 3)
= 2 β (3 Β· 2) = 6) |
186 | 177, 185 | mpbir 230 |
. . . . . . . . . . . . . . 15
β’ (6 / 3) =
2 |
187 | 186 | oveq2i 7415 |
. . . . . . . . . . . . . 14
β’ ((2 / 3)
+ (6 / 3)) = ((2 / 3) + 2) |
188 | 181, 184,
187 | 3eqtr3i 2769 |
. . . . . . . . . . . . 13
β’ (8 / 3) =
((2 / 3) + 2) |
189 | 188 | oveq1i 7414 |
. . . . . . . . . . . 12
β’ ((8 / 3)
β 6) = (((2 / 3) + 2) β 6) |
190 | 179, 13, 14 | divcli 11952 |
. . . . . . . . . . . . 13
β’ (2 / 3)
β β |
191 | | subsub3 11488 |
. . . . . . . . . . . . 13
β’ (((2 / 3)
β β β§ 6 β β β§ 2 β β) β ((2 / 3)
β (6 β 2)) = (((2 / 3) + 2) β 6)) |
192 | 190, 180,
179, 191 | mp3an 1462 |
. . . . . . . . . . . 12
β’ ((2 / 3)
β (6 β 2)) = (((2 / 3) + 2) β 6) |
193 | 189, 192 | eqtr4i 2764 |
. . . . . . . . . . 11
β’ ((8 / 3)
β 6) = ((2 / 3) β (6 β 2)) |
194 | | 4cn 12293 |
. . . . . . . . . . . . 13
β’ 4 β
β |
195 | | 4p2e6 12361 |
. . . . . . . . . . . . . 14
β’ (4 + 2) =
6 |
196 | 194, 179,
195 | addcomli 11402 |
. . . . . . . . . . . . 13
β’ (2 + 4) =
6 |
197 | 180, 179,
194, 196 | subaddrii 11545 |
. . . . . . . . . . . 12
β’ (6
β 2) = 4 |
198 | 197 | oveq2i 7415 |
. . . . . . . . . . 11
β’ ((2 / 3)
β (6 β 2)) = ((2 / 3) β 4) |
199 | 178, 193,
198 | 3eqtri 2765 |
. . . . . . . . . 10
β’
(((2β3) / 3) β (3 Β· 2)) = ((2 / 3) β
4) |
200 | 174, 199 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π¦ = 2 β (((π¦β3) / 3) β (3
Β· π¦)) = ((2 / 3)
β 4)) |
201 | | eqid 2733 |
. . . . . . . . 9
β’ (π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦))) = (π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦))) |
202 | | ovex 7437 |
. . . . . . . . 9
β’ ((2 / 3)
β 4) β V |
203 | 200, 201,
202 | fvmpt 6994 |
. . . . . . . 8
β’ (2 β
(1[,]2) β ((π¦ β
(1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦)))β2) = ((2 / 3) β
4)) |
204 | 170, 203 | ax-mp 5 |
. . . . . . 7
β’ ((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦)))β2) =
((2 / 3) β 4) |
205 | 88 | leidi 11744 |
. . . . . . . . 9
β’ 1 β€
1 |
206 | 88, 2 | elicc2i 13386 |
. . . . . . . . 9
β’ (1 β
(1[,]2) β (1 β β β§ 1 β€ 1 β§ 1 β€
2)) |
207 | 88, 205, 4, 206 | mpbir3an 1342 |
. . . . . . . 8
β’ 1 β
(1[,]2) |
208 | | oveq1 7411 |
. . . . . . . . . . . 12
β’ (π¦ = 1 β (π¦β3) = (1β3)) |
209 | 208 | oveq1d 7419 |
. . . . . . . . . . 11
β’ (π¦ = 1 β ((π¦β3) / 3) = ((1β3) /
3)) |
210 | | oveq2 7412 |
. . . . . . . . . . 11
β’ (π¦ = 1 β (3 Β· π¦) = (3 Β·
1)) |
211 | 209, 210 | oveq12d 7422 |
. . . . . . . . . 10
β’ (π¦ = 1 β (((π¦β3) / 3) β (3
Β· π¦)) = (((1β3)
/ 3) β (3 Β· 1))) |
212 | | 3z 12591 |
. . . . . . . . . . . . 13
β’ 3 β
β€ |
213 | | 1exp 14053 |
. . . . . . . . . . . . 13
β’ (3 β
β€ β (1β3) = 1) |
214 | 212, 213 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(1β3) = 1 |
215 | 214 | oveq1i 7414 |
. . . . . . . . . . 11
β’
((1β3) / 3) = (1 / 3) |
216 | 215, 84 | oveq12i 7416 |
. . . . . . . . . 10
β’
(((1β3) / 3) β (3 Β· 1)) = ((1 / 3) β
3) |
217 | 211, 216 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π¦ = 1 β (((π¦β3) / 3) β (3
Β· π¦)) = ((1 / 3)
β 3)) |
218 | | ovex 7437 |
. . . . . . . . 9
β’ ((1 / 3)
β 3) β V |
219 | 217, 201,
218 | fvmpt 6994 |
. . . . . . . 8
β’ (1 β
(1[,]2) β ((π¦ β
(1[,]2) β¦ (((π¦β3) / 3) β (3 Β· π¦)))β1) = ((1 / 3) β
3)) |
220 | 207, 219 | ax-mp 5 |
. . . . . . 7
β’ ((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦)))β1) =
((1 / 3) β 3) |
221 | 204, 220 | oveq12i 7416 |
. . . . . 6
β’ (((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦)))β2)
β ((π¦ β (1[,]2)
β¦ (((π¦β3) / 3)
β (3 Β· π¦)))β1)) = (((2 / 3) β 4) β
((1 / 3) β 3)) |
222 | | sub4 11501 |
. . . . . . 7
β’ ((((2 /
3) β β β§ 4 β β) β§ ((1 / 3) β β β§ 3
β β)) β (((2 / 3) β 4) β ((1 / 3) β 3)) =
(((2 / 3) β (1 / 3)) β (4 β 3))) |
223 | 190, 194,
59, 13, 222 | mp4an 692 |
. . . . . 6
β’ (((2 / 3)
β 4) β ((1 / 3) β 3)) = (((2 / 3) β (1 / 3)) β (4
β 3)) |
224 | 13, 14 | pm3.2i 472 |
. . . . . . . . 9
β’ (3 β
β β§ 3 β 0) |
225 | | divsubdir 11904 |
. . . . . . . . 9
β’ ((2
β β β§ 1 β β β§ (3 β β β§ 3 β 0))
β ((2 β 1) / 3) = ((2 / 3) β (1 / 3))) |
226 | 179, 58, 224, 225 | mp3an 1462 |
. . . . . . . 8
β’ ((2
β 1) / 3) = ((2 / 3) β (1 / 3)) |
227 | | 2m1e1 12334 |
. . . . . . . . 9
β’ (2
β 1) = 1 |
228 | 227 | oveq1i 7414 |
. . . . . . . 8
β’ ((2
β 1) / 3) = (1 / 3) |
229 | 226, 228 | eqtr3i 2763 |
. . . . . . 7
β’ ((2 / 3)
β (1 / 3)) = (1 / 3) |
230 | | 3p1e4 12353 |
. . . . . . . 8
β’ (3 + 1) =
4 |
231 | 194, 13, 58, 230 | subaddrii 11545 |
. . . . . . 7
β’ (4
β 3) = 1 |
232 | 229, 231 | oveq12i 7416 |
. . . . . 6
β’ (((2 / 3)
β (1 / 3)) β (4 β 3)) = ((1 / 3) β 1) |
233 | 221, 223,
232 | 3eqtri 2765 |
. . . . 5
β’ (((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦)))β2)
β ((π¦ β (1[,]2)
β¦ (((π¦β3) / 3)
β (3 Β· π¦)))β1)) = ((1 / 3) β
1) |
234 | 13, 14 | dividi 11943 |
. . . . . 6
β’ (3 / 3) =
1 |
235 | 234 | oveq2i 7415 |
. . . . 5
β’ ((1 / 3)
β (3 / 3)) = ((1 / 3) β 1) |
236 | 233, 235 | eqtr4i 2764 |
. . . 4
β’ (((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦)))β2)
β ((π¦ β (1[,]2)
β¦ (((π¦β3) / 3)
β (3 Β· π¦)))β1)) = ((1 / 3) β (3 /
3)) |
237 | | divsubdir 11904 |
. . . . 5
β’ ((1
β β β§ 3 β β β§ (3 β β β§ 3 β 0))
β ((1 β 3) / 3) = ((1 / 3) β (3 / 3))) |
238 | 58, 13, 224, 237 | mp3an 1462 |
. . . 4
β’ ((1
β 3) / 3) = ((1 / 3) β (3 / 3)) |
239 | 236, 238 | eqtr4i 2764 |
. . 3
β’ (((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦)))β2)
β ((π¦ β (1[,]2)
β¦ (((π¦β3) / 3)
β (3 Β· π¦)))β1)) = ((1 β 3) /
3) |
240 | | divneg 11902 |
. . . . 5
β’ ((2
β β β§ 3 β β β§ 3 β 0) β -(2 / 3) = (-2 /
3)) |
241 | 179, 13, 14, 240 | mp3an 1462 |
. . . 4
β’ -(2 / 3)
= (-2 / 3) |
242 | 13, 58 | negsubdi2i 11542 |
. . . . . 6
β’ -(3
β 1) = (1 β 3) |
243 | 40 | negeqi 11449 |
. . . . . 6
β’ -(3
β 1) = -2 |
244 | 242, 243 | eqtr3i 2763 |
. . . . 5
β’ (1
β 3) = -2 |
245 | 244 | oveq1i 7414 |
. . . 4
β’ ((1
β 3) / 3) = (-2 / 3) |
246 | 241, 245 | eqtr4i 2764 |
. . 3
β’ -(2 / 3)
= ((1 β 3) / 3) |
247 | 239, 246 | eqtr4i 2764 |
. 2
β’ (((π¦ β (1[,]2) β¦ (((π¦β3) / 3) β (3
Β· π¦)))β2)
β ((π¦ β (1[,]2)
β¦ (((π¦β3) / 3)
β (3 Β· π¦)))β1)) = -(2 / 3) |
248 | 160, 167,
247 | 3eqtr3i 2769 |
1
β’
β«(1(,)2)((π₯β2) β 3) dπ₯ = -(2 / 3) |