Step | Hyp | Ref
| Expression |
1 | | 1red 9934 |
. . . 4
⊢ (⊤
→ 1 ∈ ℝ) |
2 | | 2re 10967 |
. . . . 5
⊢ 2 ∈
ℝ |
3 | 2 | a1i 11 |
. . . 4
⊢ (⊤
→ 2 ∈ ℝ) |
4 | | 1le2 11118 |
. . . . 5
⊢ 1 ≤
2 |
5 | 4 | a1i 11 |
. . . 4
⊢ (⊤
→ 1 ≤ 2) |
6 | | reelprrecn 9907 |
. . . . . . 7
⊢ ℝ
∈ {ℝ, ℂ} |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
8 | | recn 9905 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
9 | | 3nn0 11187 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
10 | | expcl 12740 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝑦↑3) ∈ ℂ) |
11 | 9, 10 | mpan2 703 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → (𝑦↑3) ∈
ℂ) |
12 | 8, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦↑3) ∈
ℂ) |
13 | | 3cn 10972 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
14 | | 3ne0 10992 |
. . . . . . . . . 10
⊢ 3 ≠
0 |
15 | | divcl 10570 |
. . . . . . . . . 10
⊢ (((𝑦↑3) ∈ ℂ ∧ 3
∈ ℂ ∧ 3 ≠ 0) → ((𝑦↑3) / 3) ∈
ℂ) |
16 | 13, 14, 15 | mp3an23 1408 |
. . . . . . . . 9
⊢ ((𝑦↑3) ∈ ℂ →
((𝑦↑3) / 3) ∈
ℂ) |
17 | 12, 16 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → ((𝑦↑3) / 3) ∈
ℂ) |
18 | | mulcl 9899 |
. . . . . . . . 9
⊢ ((3
∈ ℂ ∧ 𝑦
∈ ℂ) → (3 · 𝑦) ∈ ℂ) |
19 | 13, 8, 18 | sylancr 694 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → (3
· 𝑦) ∈
ℂ) |
20 | 17, 19 | subcld 10271 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → (((𝑦↑3) / 3) − (3
· 𝑦)) ∈
ℂ) |
21 | 20 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (((𝑦↑3) / 3) − (3 · 𝑦)) ∈
ℂ) |
22 | | ovex 6577 |
. . . . . . 7
⊢ ((𝑦↑2) − 3) ∈
V |
23 | 22 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ ℝ) → ((𝑦↑2) − 3) ∈
V) |
24 | 17 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → ((𝑦↑3) / 3) ∈
ℂ) |
25 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑦↑2) ∈
V |
26 | 25 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (𝑦↑2) ∈ V) |
27 | | divrec2 10581 |
. . . . . . . . . . . . 13
⊢ (((𝑦↑3) ∈ ℂ ∧ 3
∈ ℂ ∧ 3 ≠ 0) → ((𝑦↑3) / 3) = ((1 / 3) · (𝑦↑3))) |
28 | 13, 14, 27 | mp3an23 1408 |
. . . . . . . . . . . 12
⊢ ((𝑦↑3) ∈ ℂ →
((𝑦↑3) / 3) = ((1 / 3)
· (𝑦↑3))) |
29 | 12, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → ((𝑦↑3) / 3) = ((1 / 3)
· (𝑦↑3))) |
30 | 29 | mpteq2ia 4668 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3)) = (𝑦 ∈ ℝ ↦ ((1 / 3)
· (𝑦↑3))) |
31 | 30 | oveq2i 6560 |
. . . . . . . . 9
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
((𝑦↑3) / 3))) =
(ℝ D (𝑦 ∈
ℝ ↦ ((1 / 3) · (𝑦↑3)))) |
32 | 12 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (𝑦↑3) ∈ ℂ) |
33 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (3
· (𝑦↑2)) ∈
V |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (3 · (𝑦↑2)) ∈ V) |
35 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ ↦ (𝑦↑3)) = (𝑦 ∈ ℂ ↦ (𝑦↑3)) |
36 | 35, 11 | fmpti 6291 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℂ ↦ (𝑦↑3)):ℂ⟶ℂ |
37 | | ssid 3587 |
. . . . . . . . . . . . . 14
⊢ ℂ
⊆ ℂ |
38 | | ax-resscn 9872 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
39 | | 3nn 11063 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℕ |
40 | | dvexp 23522 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 ∈
ℕ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3 · (𝑦↑(3 −
1))))) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3
· (𝑦↑(3 −
1)))) |
42 | | 3m1e2 11014 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (3
− 1) = 2 |
43 | 42 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦↑(3 − 1)) = (𝑦↑2) |
44 | 43 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . 18
⊢ (3
· (𝑦↑(3 −
1))) = (3 · (𝑦↑2)) |
45 | 44 | mpteq2i 4669 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℂ ↦ (3
· (𝑦↑(3 −
1)))) = (𝑦 ∈ ℂ
↦ (3 · (𝑦↑2))) |
46 | 41, 45 | eqtri 2632 |
. . . . . . . . . . . . . . . 16
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3
· (𝑦↑2))) |
47 | 33, 46 | dmmpti 5936 |
. . . . . . . . . . . . . . 15
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑3))) = ℂ |
48 | 38, 47 | sseqtr4i 3601 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ dom (ℂ D (𝑦
∈ ℂ ↦ (𝑦↑3))) |
49 | | dvres3 23483 |
. . . . . . . . . . . . . 14
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (𝑦↑3)):ℂ⟶ℂ) ∧
(ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))))) → (ℝ D
((𝑦 ∈ ℂ ↦
(𝑦↑3)) ↾
ℝ)) = ((ℂ D (𝑦
∈ ℂ ↦ (𝑦↑3))) ↾ ℝ)) |
50 | 6, 36, 37, 48, 49 | mp4an 705 |
. . . . . . . . . . . . 13
⊢ (ℝ
D ((𝑦 ∈ ℂ
↦ (𝑦↑3)) ↾
ℝ)) = ((ℂ D (𝑦
∈ ℂ ↦ (𝑦↑3))) ↾ ℝ) |
51 | | resmpt 5369 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (𝑦↑3)) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3))) |
52 | 38, 51 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ↦ (𝑦↑3)) ↾ ℝ) =
(𝑦 ∈ ℝ ↦
(𝑦↑3)) |
53 | 52 | oveq2i 6560 |
. . . . . . . . . . . . 13
⊢ (ℝ
D ((𝑦 ∈ ℂ
↦ (𝑦↑3)) ↾
ℝ)) = (ℝ D (𝑦
∈ ℝ ↦ (𝑦↑3))) |
54 | 46 | reseq1i 5313 |
. . . . . . . . . . . . . 14
⊢ ((ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) ↾
ℝ) = ((𝑦 ∈
ℂ ↦ (3 · (𝑦↑2))) ↾ ℝ) |
55 | | resmpt 5369 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (3 · (𝑦↑2))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (3
· (𝑦↑2)))) |
56 | 38, 55 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ↦ (3
· (𝑦↑2)))
↾ ℝ) = (𝑦
∈ ℝ ↦ (3 · (𝑦↑2))) |
57 | 54, 56 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ ((ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) ↾
ℝ) = (𝑦 ∈
ℝ ↦ (3 · (𝑦↑2))) |
58 | 50, 53, 57 | 3eqtr3i 2640 |
. . . . . . . . . . . 12
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
(𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3
· (𝑦↑2))) |
59 | 58 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3 · (𝑦↑2)))) |
60 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
61 | 60, 13, 14 | divcli 10646 |
. . . . . . . . . . . 12
⊢ (1 / 3)
∈ ℂ |
62 | 61 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (1 / 3) ∈ ℂ) |
63 | 7, 32, 34, 59, 62 | dvmptcmul 23533 |
. . . . . . . . . 10
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ ((1 / 3) · (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) · (3
· (𝑦↑2))))) |
64 | 63 | trud 1484 |
. . . . . . . . 9
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
((1 / 3) · (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) · (3
· (𝑦↑2)))) |
65 | | sqcl 12787 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → (𝑦↑2) ∈
ℂ) |
66 | | mulcl 9899 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ (𝑦↑2) ∈ ℂ) → (3 ·
(𝑦↑2)) ∈
ℂ) |
67 | 13, 65, 66 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → (3
· (𝑦↑2)) ∈
ℂ) |
68 | | divrec2 10581 |
. . . . . . . . . . . . 13
⊢ (((3
· (𝑦↑2)) ∈
ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → ((3 · (𝑦↑2)) / 3) = ((1 / 3)
· (3 · (𝑦↑2)))) |
69 | 13, 14, 68 | mp3an23 1408 |
. . . . . . . . . . . 12
⊢ ((3
· (𝑦↑2)) ∈
ℂ → ((3 · (𝑦↑2)) / 3) = ((1 / 3) · (3
· (𝑦↑2)))) |
70 | 8, 67, 69 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → ((3
· (𝑦↑2)) / 3) =
((1 / 3) · (3 · (𝑦↑2)))) |
71 | | divcan3 10590 |
. . . . . . . . . . . . 13
⊢ (((𝑦↑2) ∈ ℂ ∧ 3
∈ ℂ ∧ 3 ≠ 0) → ((3 · (𝑦↑2)) / 3) = (𝑦↑2)) |
72 | 13, 14, 71 | mp3an23 1408 |
. . . . . . . . . . . 12
⊢ ((𝑦↑2) ∈ ℂ →
((3 · (𝑦↑2)) /
3) = (𝑦↑2)) |
73 | 8, 65, 72 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → ((3
· (𝑦↑2)) / 3) =
(𝑦↑2)) |
74 | 70, 73 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → ((1 / 3)
· (3 · (𝑦↑2))) = (𝑦↑2)) |
75 | 74 | mpteq2ia 4668 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ ↦ ((1 / 3)
· (3 · (𝑦↑2)))) = (𝑦 ∈ ℝ ↦ (𝑦↑2)) |
76 | 31, 64, 75 | 3eqtri 2636 |
. . . . . . . 8
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
((𝑦↑3) / 3))) = (𝑦 ∈ ℝ ↦ (𝑦↑2)) |
77 | 76 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ ((𝑦↑3)
/ 3))) = (𝑦 ∈ ℝ
↦ (𝑦↑2))) |
78 | 19 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (3 · 𝑦) ∈ ℂ) |
79 | | 3ex 10973 |
. . . . . . . 8
⊢ 3 ∈
V |
80 | 79 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → 3 ∈ V) |
81 | 8 | adantl 481 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ ℝ) → 𝑦
∈ ℂ) |
82 | | 1red 9934 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ ℝ) → 1 ∈ ℝ) |
83 | 7 | dvmptid 23526 |
. . . . . . . . 9
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ 𝑦)) =
(𝑦 ∈ ℝ ↦
1)) |
84 | 13 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 3 ∈ ℂ) |
85 | 7, 81, 82, 83, 84 | dvmptcmul 23533 |
. . . . . . . 8
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (3 · 𝑦))) = (𝑦 ∈ ℝ ↦ (3 ·
1))) |
86 | | 3t1e3 11055 |
. . . . . . . . 9
⊢ (3
· 1) = 3 |
87 | 86 | mpteq2i 4669 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ ↦ (3
· 1)) = (𝑦 ∈
ℝ ↦ 3) |
88 | 85, 87 | syl6eq 2660 |
. . . . . . 7
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (3 · 𝑦))) = (𝑦 ∈ ℝ ↦ 3)) |
89 | 7, 24, 26, 77, 78, 80, 88 | dvmptsub 23536 |
. . . . . 6
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) − 3))) |
90 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
91 | | iccssre 12126 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ) → (1[,]2) ⊆
ℝ) |
92 | 90, 2, 91 | mp2an 704 |
. . . . . . 7
⊢ (1[,]2)
⊆ ℝ |
93 | 92 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1[,]2) ⊆ ℝ) |
94 | | eqid 2610 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
95 | 94 | tgioo2 22414 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
96 | | iccntr 22432 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ) → ((int‘(topGen‘ran
(,)))‘(1[,]2)) = (1(,)2)) |
97 | 90, 2, 96 | mp2an 704 |
. . . . . . 7
⊢
((int‘(topGen‘ran (,)))‘(1[,]2)) =
(1(,)2) |
98 | 97 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ((int‘(topGen‘ran (,)))‘(1[,]2)) =
(1(,)2)) |
99 | 7, 21, 23, 89, 93, 95, 94, 98 | dvmptres2 23531 |
. . . . 5
⊢ (⊤
→ (ℝ D (𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3))) |
100 | | ioossicc 12130 |
. . . . . . 7
⊢ (1(,)2)
⊆ (1[,]2) |
101 | | resmpt 5369 |
. . . . . . 7
⊢ ((1(,)2)
⊆ (1[,]2) → ((𝑦
∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ↾ (1(,)2)) =
(𝑦 ∈ (1(,)2) ↦
((𝑦↑2) −
3))) |
102 | 100, 101 | ax-mp 5 |
. . . . . 6
⊢ ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ↾
(1(,)2)) = (𝑦 ∈
(1(,)2) ↦ ((𝑦↑2)
− 3)) |
103 | 92, 38 | sstri 3577 |
. . . . . . . . 9
⊢ (1[,]2)
⊆ ℂ |
104 | | resmpt 5369 |
. . . . . . . . 9
⊢ ((1[,]2)
⊆ ℂ → ((𝑦
∈ ℂ ↦ ((𝑦↑2) − 3)) ↾ (1[,]2)) =
(𝑦 ∈ (1[,]2) ↦
((𝑦↑2) −
3))) |
105 | 103, 104 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ↾
(1[,]2)) = (𝑦 ∈
(1[,]2) ↦ ((𝑦↑2)
− 3)) |
106 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) = (𝑦 ∈ ℂ ↦ ((𝑦↑2) −
3)) |
107 | | subcl 10159 |
. . . . . . . . . . . . . 14
⊢ (((𝑦↑2) ∈ ℂ ∧ 3
∈ ℂ) → ((𝑦↑2) − 3) ∈
ℂ) |
108 | 13, 107 | mpan2 703 |
. . . . . . . . . . . . 13
⊢ ((𝑦↑2) ∈ ℂ →
((𝑦↑2) − 3)
∈ ℂ) |
109 | 65, 108 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → ((𝑦↑2) − 3) ∈
ℂ) |
110 | 106, 109 | fmpti 6291 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ ↦ ((𝑦↑2) −
3)):ℂ⟶ℂ |
111 | 37, 110, 37 | 3pm3.2i 1232 |
. . . . . . . . . 10
⊢ (ℂ
⊆ ℂ ∧ (𝑦
∈ ℂ ↦ ((𝑦↑2) − 3)):ℂ⟶ℂ
∧ ℂ ⊆ ℂ) |
112 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((2
· (𝑦↑(2 −
1))) − 0) ∈ V |
113 | | cnelprrecn 9908 |
. . . . . . . . . . . . . 14
⊢ ℂ
∈ {ℝ, ℂ} |
114 | 113 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
115 | 65 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ ℂ) → (𝑦↑2) ∈ ℂ) |
116 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (2
· (𝑦↑(2 −
1))) ∈ V |
117 | 116 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ ℂ) → (2 · (𝑦↑(2 − 1))) ∈
V) |
118 | | 2nn 11062 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ |
119 | | dvexp 23522 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℕ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑2))) = (𝑦 ∈ ℂ ↦ (2 · (𝑦↑(2 −
1))))) |
120 | 118, 119 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑2))) = (𝑦 ∈ ℂ ↦ (2
· (𝑦↑(2 −
1)))) |
121 | 120 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑2))) = (𝑦 ∈ ℂ ↦ (2 · (𝑦↑(2 −
1))))) |
122 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ ℂ) → 3 ∈ ℂ) |
123 | | c0ex 9913 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
124 | 123 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ ℂ) → 0 ∈ V) |
125 | 114, 84 | dvmptc 23527 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ 3)) = (𝑦
∈ ℂ ↦ 0)) |
126 | 114, 115,
117, 121, 122, 124, 125 | dvmptsub 23536 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ ((𝑦↑2)
− 3))) = (𝑦 ∈
ℂ ↦ ((2 · (𝑦↑(2 − 1))) −
0))) |
127 | 126 | trud 1484 |
. . . . . . . . . . 11
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
((𝑦↑2) − 3))) =
(𝑦 ∈ ℂ ↦
((2 · (𝑦↑(2
− 1))) − 0)) |
128 | 112, 127 | dmmpti 5936 |
. . . . . . . . . 10
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ ((𝑦↑2)
− 3))) = ℂ |
129 | | dvcn 23490 |
. . . . . . . . . 10
⊢
(((ℂ ⊆ ℂ ∧ (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)):ℂ⟶ℂ
∧ ℂ ⊆ ℂ) ∧ dom (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3))) = ℂ) →
(𝑦 ∈ ℂ ↦
((𝑦↑2) − 3))
∈ (ℂ–cn→ℂ)) |
130 | 111, 128,
129 | mp2an 704 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ∈
(ℂ–cn→ℂ) |
131 | | rescncf 22508 |
. . . . . . . . 9
⊢ ((1[,]2)
⊆ ℂ → ((𝑦
∈ ℂ ↦ ((𝑦↑2) − 3)) ∈
(ℂ–cn→ℂ) →
((𝑦 ∈ ℂ ↦
((𝑦↑2) − 3))
↾ (1[,]2)) ∈ ((1[,]2)–cn→ℂ))) |
132 | 103, 130,
131 | mp2 9 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ↾
(1[,]2)) ∈ ((1[,]2)–cn→ℂ) |
133 | 105, 132 | eqeltrri 2685 |
. . . . . . 7
⊢ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈
((1[,]2)–cn→ℂ) |
134 | | rescncf 22508 |
. . . . . . 7
⊢ ((1(,)2)
⊆ (1[,]2) → ((𝑦
∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈
((1[,]2)–cn→ℂ) →
((𝑦 ∈ (1[,]2) ↦
((𝑦↑2) − 3))
↾ (1(,)2)) ∈ ((1(,)2)–cn→ℂ))) |
135 | 100, 133,
134 | mp2 9 |
. . . . . 6
⊢ ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ↾
(1(,)2)) ∈ ((1(,)2)–cn→ℂ) |
136 | 102, 135 | eqeltrri 2685 |
. . . . 5
⊢ (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3)) ∈
((1(,)2)–cn→ℂ) |
137 | 99, 136 | syl6eqel 2696 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) ∈ ((1(,)2)–cn→ℂ)) |
138 | 100 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1(,)2) ⊆ (1[,]2)) |
139 | | ioombl 23140 |
. . . . . . 7
⊢ (1(,)2)
∈ dom vol |
140 | 139 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1(,)2) ∈ dom vol) |
141 | 22 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (1[,]2)) → ((𝑦↑2) − 3) ∈
V) |
142 | | cniccibl 23413 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈
((1[,]2)–cn→ℂ)) →
(𝑦 ∈ (1[,]2) ↦
((𝑦↑2) − 3))
∈ 𝐿1) |
143 | 90, 2, 133, 142 | mp3an 1416 |
. . . . . . 7
⊢ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈
𝐿1 |
144 | 143 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑦 ∈ (1[,]2)
↦ ((𝑦↑2) −
3)) ∈ 𝐿1) |
145 | 138, 140,
141, 144 | iblss 23377 |
. . . . 5
⊢ (⊤
→ (𝑦 ∈ (1(,)2)
↦ ((𝑦↑2) −
3)) ∈ 𝐿1) |
146 | 99, 145 | eqeltrd 2688 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) ∈
𝐿1) |
147 | | resmpt 5369 |
. . . . . . 7
⊢ ((1[,]2)
⊆ ℝ → ((𝑦
∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ↾ (1[,]2)) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))) |
148 | 92, 147 | ax-mp 5 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) ↾
(1[,]2)) = (𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) |
149 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) = (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) |
150 | 149, 20 | fmpti 6291 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))):ℝ⟶ℂ |
151 | | ssid 3587 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ |
152 | 38, 150, 151 | 3pm3.2i 1232 |
. . . . . . . 8
⊢ (ℝ
⊆ ℂ ∧ (𝑦
∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))):ℝ⟶ℂ ∧
ℝ ⊆ ℝ) |
153 | 89 | trud 1484 |
. . . . . . . . 9
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
(((𝑦↑3) / 3) −
(3 · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) −
3)) |
154 | 22, 153 | dmmpti 5936 |
. . . . . . . 8
⊢ dom
(ℝ D (𝑦 ∈
ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = ℝ |
155 | | dvcn 23490 |
. . . . . . . 8
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))):ℝ⟶ℂ ∧
ℝ ⊆ ℝ) ∧ dom (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = ℝ) → (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) ∈
(ℝ–cn→ℂ)) |
156 | 152, 154,
155 | mp2an 704 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) ∈
(ℝ–cn→ℂ) |
157 | | rescncf 22508 |
. . . . . . 7
⊢ ((1[,]2)
⊆ ℝ → ((𝑦
∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ∈ (ℝ–cn→ℂ) → ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ↾ (1[,]2)) ∈
((1[,]2)–cn→ℂ))) |
158 | 92, 156, 157 | mp2 9 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) ↾
(1[,]2)) ∈ ((1[,]2)–cn→ℂ) |
159 | 148, 158 | eqeltrri 2685 |
. . . . 5
⊢ (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) ∈
((1[,]2)–cn→ℂ) |
160 | 159 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))
∈ ((1[,]2)–cn→ℂ)) |
161 | 1, 3, 5, 137, 146, 160 | ftc2 23611 |
. . 3
⊢ (⊤
→ ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) d𝑥 = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘1))) |
162 | 161 | trud 1484 |
. 2
⊢
∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) d𝑥 = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘1)) |
163 | | itgeq2 23350 |
. . 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𝑥) |
164 | | oveq1 6556 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝑦↑2) = (𝑥↑2)) |
165 | 164 | oveq1d 6564 |
. . . 4
⊢ (𝑦 = 𝑥 → ((𝑦↑2) − 3) = ((𝑥↑2) − 3)) |
166 | 99 | trud 1484 |
. . . 4
⊢ (ℝ
D (𝑦 ∈ (1[,]2) ↦
(((𝑦↑3) / 3) −
(3 · 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) −
3)) |
167 | | ovex 6577 |
. . . 4
⊢ ((𝑥↑2) − 3) ∈
V |
168 | 165, 166,
167 | fvmpt 6191 |
. . 3
⊢ (𝑥 ∈ (1(,)2) → ((ℝ
D (𝑦 ∈ (1[,]2) ↦
(((𝑦↑3) / 3) −
(3 · 𝑦))))‘𝑥) = ((𝑥↑2) − 3)) |
169 | 163, 168 | mprg 2910 |
. 2
⊢
∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) d𝑥 = ∫(1(,)2)((𝑥↑2) − 3) d𝑥 |
170 | 2 | leidi 10441 |
. . . . . . . . 9
⊢ 2 ≤
2 |
171 | 90, 2 | elicc2i 12110 |
. . . . . . . . 9
⊢ (2 ∈
(1[,]2) ↔ (2 ∈ ℝ ∧ 1 ≤ 2 ∧ 2 ≤
2)) |
172 | 2, 4, 170, 171 | mpbir3an 1237 |
. . . . . . . 8
⊢ 2 ∈
(1[,]2) |
173 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑦 = 2 → (𝑦↑3) = (2↑3)) |
174 | 173 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑦 = 2 → ((𝑦↑3) / 3) = ((2↑3) /
3)) |
175 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑦 = 2 → (3 · 𝑦) = (3 ·
2)) |
176 | 174, 175 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑦 = 2 → (((𝑦↑3) / 3) − (3
· 𝑦)) = (((2↑3)
/ 3) − (3 · 2))) |
177 | | cu2 12825 |
. . . . . . . . . . . . 13
⊢
(2↑3) = 8 |
178 | 177 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢
((2↑3) / 3) = (8 / 3) |
179 | | 3t2e6 11056 |
. . . . . . . . . . . 12
⊢ (3
· 2) = 6 |
180 | 178, 179 | oveq12i 6561 |
. . . . . . . . . . 11
⊢
(((2↑3) / 3) − (3 · 2)) = ((8 / 3) −
6) |
181 | | 2cn 10968 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
182 | | 6cn 10979 |
. . . . . . . . . . . . . . 15
⊢ 6 ∈
ℂ |
183 | 181, 182,
13, 14 | divdiri 10661 |
. . . . . . . . . . . . . 14
⊢ ((2 + 6)
/ 3) = ((2 / 3) + (6 / 3)) |
184 | | 6p2e8 11046 |
. . . . . . . . . . . . . . . 16
⊢ (6 + 2) =
8 |
185 | 182, 181,
184 | addcomli 10107 |
. . . . . . . . . . . . . . 15
⊢ (2 + 6) =
8 |
186 | 185 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ ((2 + 6)
/ 3) = (8 / 3) |
187 | 182, 13, 181, 14 | divmuli 10658 |
. . . . . . . . . . . . . . . 16
⊢ ((6 / 3)
= 2 ↔ (3 · 2) = 6) |
188 | 179, 187 | mpbir 220 |
. . . . . . . . . . . . . . 15
⊢ (6 / 3) =
2 |
189 | 188 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ ((2 / 3)
+ (6 / 3)) = ((2 / 3) + 2) |
190 | 183, 186,
189 | 3eqtr3i 2640 |
. . . . . . . . . . . . 13
⊢ (8 / 3) =
((2 / 3) + 2) |
191 | 190 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ ((8 / 3)
− 6) = (((2 / 3) + 2) − 6) |
192 | 181, 13, 14 | divcli 10646 |
. . . . . . . . . . . . 13
⊢ (2 / 3)
∈ ℂ |
193 | | subsub3 10192 |
. . . . . . . . . . . . 13
⊢ (((2 / 3)
∈ ℂ ∧ 6 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 / 3)
− (6 − 2)) = (((2 / 3) + 2) − 6)) |
194 | 192, 182,
181, 193 | mp3an 1416 |
. . . . . . . . . . . 12
⊢ ((2 / 3)
− (6 − 2)) = (((2 / 3) + 2) − 6) |
195 | 191, 194 | eqtr4i 2635 |
. . . . . . . . . . 11
⊢ ((8 / 3)
− 6) = ((2 / 3) − (6 − 2)) |
196 | | 4cn 10975 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℂ |
197 | | 4p2e6 11039 |
. . . . . . . . . . . . . 14
⊢ (4 + 2) =
6 |
198 | 196, 181,
197 | addcomli 10107 |
. . . . . . . . . . . . 13
⊢ (2 + 4) =
6 |
199 | 182, 181,
196, 198 | subaddrii 10249 |
. . . . . . . . . . . 12
⊢ (6
− 2) = 4 |
200 | 199 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ ((2 / 3)
− (6 − 2)) = ((2 / 3) − 4) |
201 | 180, 195,
200 | 3eqtri 2636 |
. . . . . . . . . 10
⊢
(((2↑3) / 3) − (3 · 2)) = ((2 / 3) −
4) |
202 | 176, 201 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑦 = 2 → (((𝑦↑3) / 3) − (3
· 𝑦)) = ((2 / 3)
− 4)) |
203 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) |
204 | | ovex 6577 |
. . . . . . . . 9
⊢ ((2 / 3)
− 4) ∈ V |
205 | 202, 203,
204 | fvmpt 6191 |
. . . . . . . 8
⊢ (2 ∈
(1[,]2) → ((𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) = ((2 / 3) −
4)) |
206 | 172, 205 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2) =
((2 / 3) − 4) |
207 | 90 | leidi 10441 |
. . . . . . . . 9
⊢ 1 ≤
1 |
208 | 90, 2 | elicc2i 12110 |
. . . . . . . . 9
⊢ (1 ∈
(1[,]2) ↔ (1 ∈ ℝ ∧ 1 ≤ 1 ∧ 1 ≤
2)) |
209 | 90, 207, 4, 208 | mpbir3an 1237 |
. . . . . . . 8
⊢ 1 ∈
(1[,]2) |
210 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑦 = 1 → (𝑦↑3) = (1↑3)) |
211 | 210 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → ((𝑦↑3) / 3) = ((1↑3) /
3)) |
212 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → (3 · 𝑦) = (3 ·
1)) |
213 | 211, 212 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → (((𝑦↑3) / 3) − (3
· 𝑦)) = (((1↑3)
/ 3) − (3 · 1))) |
214 | | 3z 11287 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℤ |
215 | | 1exp 12751 |
. . . . . . . . . . . . 13
⊢ (3 ∈
ℤ → (1↑3) = 1) |
216 | 214, 215 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(1↑3) = 1 |
217 | 216 | oveq1i 6559 |
. . . . . . . . . . 11
⊢
((1↑3) / 3) = (1 / 3) |
218 | 217, 86 | oveq12i 6561 |
. . . . . . . . . 10
⊢
(((1↑3) / 3) − (3 · 1)) = ((1 / 3) −
3) |
219 | 213, 218 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑦 = 1 → (((𝑦↑3) / 3) − (3
· 𝑦)) = ((1 / 3)
− 3)) |
220 | | ovex 6577 |
. . . . . . . . 9
⊢ ((1 / 3)
− 3) ∈ V |
221 | 219, 203,
220 | fvmpt 6191 |
. . . . . . . 8
⊢ (1 ∈
(1[,]2) → ((𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘1) = ((1 / 3) −
3)) |
222 | 209, 221 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘1) =
((1 / 3) − 3) |
223 | 206, 222 | oveq12i 6561 |
. . . . . 6
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = (((2 / 3) − 4) −
((1 / 3) − 3)) |
224 | | sub4 10205 |
. . . . . . 7
⊢ ((((2 /
3) ∈ ℂ ∧ 4 ∈ ℂ) ∧ ((1 / 3) ∈ ℂ ∧ 3
∈ ℂ)) → (((2 / 3) − 4) − ((1 / 3) − 3)) =
(((2 / 3) − (1 / 3)) − (4 − 3))) |
225 | 192, 196,
61, 13, 224 | mp4an 705 |
. . . . . 6
⊢ (((2 / 3)
− 4) − ((1 / 3) − 3)) = (((2 / 3) − (1 / 3)) − (4
− 3)) |
226 | 13, 14 | pm3.2i 470 |
. . . . . . . . 9
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
227 | | divsubdir 10600 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ 1 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0))
→ ((2 − 1) / 3) = ((2 / 3) − (1 / 3))) |
228 | 181, 60, 226, 227 | mp3an 1416 |
. . . . . . . 8
⊢ ((2
− 1) / 3) = ((2 / 3) − (1 / 3)) |
229 | | 2m1e1 11012 |
. . . . . . . . 9
⊢ (2
− 1) = 1 |
230 | 229 | oveq1i 6559 |
. . . . . . . 8
⊢ ((2
− 1) / 3) = (1 / 3) |
231 | 228, 230 | eqtr3i 2634 |
. . . . . . 7
⊢ ((2 / 3)
− (1 / 3)) = (1 / 3) |
232 | | 3p1e4 11030 |
. . . . . . . 8
⊢ (3 + 1) =
4 |
233 | 196, 13, 60, 232 | subaddrii 10249 |
. . . . . . 7
⊢ (4
− 3) = 1 |
234 | 231, 233 | oveq12i 6561 |
. . . . . 6
⊢ (((2 / 3)
− (1 / 3)) − (4 − 3)) = ((1 / 3) − 1) |
235 | 223, 225,
234 | 3eqtri 2636 |
. . . . 5
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = ((1 / 3) −
1) |
236 | 13, 14 | dividi 10637 |
. . . . . 6
⊢ (3 / 3) =
1 |
237 | 236 | oveq2i 6560 |
. . . . 5
⊢ ((1 / 3)
− (3 / 3)) = ((1 / 3) − 1) |
238 | 235, 237 | eqtr4i 2635 |
. . . 4
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = ((1 / 3) − (3 /
3)) |
239 | | divsubdir 10600 |
. . . . 5
⊢ ((1
∈ ℂ ∧ 3 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0))
→ ((1 − 3) / 3) = ((1 / 3) − (3 / 3))) |
240 | 60, 13, 226, 239 | mp3an 1416 |
. . . 4
⊢ ((1
− 3) / 3) = ((1 / 3) − (3 / 3)) |
241 | 238, 240 | eqtr4i 2635 |
. . 3
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = ((1 − 3) /
3) |
242 | | divneg 10598 |
. . . . 5
⊢ ((2
∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → -(2 / 3) = (-2 /
3)) |
243 | 181, 13, 14, 242 | mp3an 1416 |
. . . 4
⊢ -(2 / 3)
= (-2 / 3) |
244 | 13, 60 | negsubdi2i 10246 |
. . . . . 6
⊢ -(3
− 1) = (1 − 3) |
245 | 42 | negeqi 10153 |
. . . . . 6
⊢ -(3
− 1) = -2 |
246 | 244, 245 | eqtr3i 2634 |
. . . . 5
⊢ (1
− 3) = -2 |
247 | 246 | oveq1i 6559 |
. . . 4
⊢ ((1
− 3) / 3) = (-2 / 3) |
248 | 243, 247 | eqtr4i 2635 |
. . 3
⊢ -(2 / 3)
= ((1 − 3) / 3) |
249 | 241, 248 | eqtr4i 2635 |
. 2
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = -(2 / 3) |
250 | 162, 169,
249 | 3eqtr3i 2640 |
1
⊢
∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3) |