Step | Hyp | Ref
| Expression |
1 | | 1red 10834 |
. . . 4
⊢ (⊤
→ 1 ∈ ℝ) |
2 | | 2re 11904 |
. . . . 5
⊢ 2 ∈
ℝ |
3 | 2 | a1i 11 |
. . . 4
⊢ (⊤
→ 2 ∈ ℝ) |
4 | | 1le2 12039 |
. . . . 5
⊢ 1 ≤
2 |
5 | 4 | a1i 11 |
. . . 4
⊢ (⊤
→ 1 ≤ 2) |
6 | | reelprrecn 10821 |
. . . . . . 7
⊢ ℝ
∈ {ℝ, ℂ} |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
8 | | recn 10819 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
9 | | 3nn0 12108 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
10 | | expcl 13653 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝑦↑3) ∈ ℂ) |
11 | 9, 10 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → (𝑦↑3) ∈
ℂ) |
12 | 8, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦↑3) ∈
ℂ) |
13 | | 3cn 11911 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
14 | | 3ne0 11936 |
. . . . . . . . . 10
⊢ 3 ≠
0 |
15 | | divcl 11496 |
. . . . . . . . . 10
⊢ (((𝑦↑3) ∈ ℂ ∧ 3
∈ ℂ ∧ 3 ≠ 0) → ((𝑦↑3) / 3) ∈
ℂ) |
16 | 13, 14, 15 | mp3an23 1455 |
. . . . . . . . 9
⊢ ((𝑦↑3) ∈ ℂ →
((𝑦↑3) / 3) ∈
ℂ) |
17 | 12, 16 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → ((𝑦↑3) / 3) ∈
ℂ) |
18 | | mulcl 10813 |
. . . . . . . . 9
⊢ ((3
∈ ℂ ∧ 𝑦
∈ ℂ) → (3 · 𝑦) ∈ ℂ) |
19 | 13, 8, 18 | sylancr 590 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → (3
· 𝑦) ∈
ℂ) |
20 | 17, 19 | subcld 11189 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → (((𝑦↑3) / 3) − (3
· 𝑦)) ∈
ℂ) |
21 | 20 | adantl 485 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (((𝑦↑3) / 3) − (3 · 𝑦)) ∈
ℂ) |
22 | | ovexd 7248 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ ℝ) → ((𝑦↑2) − 3) ∈
V) |
23 | 17 | adantl 485 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → ((𝑦↑3) / 3) ∈
ℂ) |
24 | | ovexd 7248 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (𝑦↑2) ∈ V) |
25 | | divrec2 11507 |
. . . . . . . . . . . . 13
⊢ (((𝑦↑3) ∈ ℂ ∧ 3
∈ ℂ ∧ 3 ≠ 0) → ((𝑦↑3) / 3) = ((1 / 3) · (𝑦↑3))) |
26 | 13, 14, 25 | mp3an23 1455 |
. . . . . . . . . . . 12
⊢ ((𝑦↑3) ∈ ℂ →
((𝑦↑3) / 3) = ((1 / 3)
· (𝑦↑3))) |
27 | 12, 26 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → ((𝑦↑3) / 3) = ((1 / 3)
· (𝑦↑3))) |
28 | 27 | mpteq2ia 5146 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3)) = (𝑦 ∈ ℝ ↦ ((1 / 3)
· (𝑦↑3))) |
29 | 28 | oveq2i 7224 |
. . . . . . . . 9
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
((𝑦↑3) / 3))) =
(ℝ D (𝑦 ∈
ℝ ↦ ((1 / 3) · (𝑦↑3)))) |
30 | 12 | adantl 485 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (𝑦↑3) ∈ ℂ) |
31 | | ovexd 7248 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (3 · (𝑦↑2)) ∈ V) |
32 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ ↦ (𝑦↑3)) = (𝑦 ∈ ℂ ↦ (𝑦↑3)) |
33 | 32, 11 | fmpti 6929 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℂ ↦ (𝑦↑3)):ℂ⟶ℂ |
34 | | ssid 3923 |
. . . . . . . . . . . . . 14
⊢ ℂ
⊆ ℂ |
35 | | ax-resscn 10786 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
36 | | ovex 7246 |
. . . . . . . . . . . . . . . 16
⊢ (3
· (𝑦↑2)) ∈
V |
37 | | 3nn 11909 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℕ |
38 | | dvexp 24850 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 ∈
ℕ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3 · (𝑦↑(3 −
1))))) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3
· (𝑦↑(3 −
1)))) |
40 | | 3m1e2 11958 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (3
− 1) = 2 |
41 | 40 | oveq2i 7224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦↑(3 − 1)) = (𝑦↑2) |
42 | 41 | oveq2i 7224 |
. . . . . . . . . . . . . . . . . 18
⊢ (3
· (𝑦↑(3 −
1))) = (3 · (𝑦↑2)) |
43 | 42 | mpteq2i 5147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℂ ↦ (3
· (𝑦↑(3 −
1)))) = (𝑦 ∈ ℂ
↦ (3 · (𝑦↑2))) |
44 | 39, 43 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3
· (𝑦↑2))) |
45 | 36, 44 | dmmpti 6522 |
. . . . . . . . . . . . . . 15
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑3))) = ℂ |
46 | 35, 45 | sseqtrri 3938 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ dom (ℂ D (𝑦
∈ ℂ ↦ (𝑦↑3))) |
47 | | dvres3 24810 |
. . . . . . . . . . . . . 14
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (𝑦↑3)):ℂ⟶ℂ) ∧
(ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))))) → (ℝ D
((𝑦 ∈ ℂ ↦
(𝑦↑3)) ↾
ℝ)) = ((ℂ D (𝑦
∈ ℂ ↦ (𝑦↑3))) ↾ ℝ)) |
48 | 6, 33, 34, 46, 47 | mp4an 693 |
. . . . . . . . . . . . 13
⊢ (ℝ
D ((𝑦 ∈ ℂ
↦ (𝑦↑3)) ↾
ℝ)) = ((ℂ D (𝑦
∈ ℂ ↦ (𝑦↑3))) ↾ ℝ) |
49 | | resmpt 5905 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (𝑦↑3)) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3))) |
50 | 35, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ↦ (𝑦↑3)) ↾ ℝ) =
(𝑦 ∈ ℝ ↦
(𝑦↑3)) |
51 | 50 | oveq2i 7224 |
. . . . . . . . . . . . 13
⊢ (ℝ
D ((𝑦 ∈ ℂ
↦ (𝑦↑3)) ↾
ℝ)) = (ℝ D (𝑦
∈ ℝ ↦ (𝑦↑3))) |
52 | 44 | reseq1i 5847 |
. . . . . . . . . . . . . 14
⊢ ((ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) ↾
ℝ) = ((𝑦 ∈
ℂ ↦ (3 · (𝑦↑2))) ↾ ℝ) |
53 | | resmpt 5905 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (3 · (𝑦↑2))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (3
· (𝑦↑2)))) |
54 | 35, 53 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ↦ (3
· (𝑦↑2)))
↾ ℝ) = (𝑦
∈ ℝ ↦ (3 · (𝑦↑2))) |
55 | 52, 54 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ((ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) ↾
ℝ) = (𝑦 ∈
ℝ ↦ (3 · (𝑦↑2))) |
56 | 48, 51, 55 | 3eqtr3i 2773 |
. . . . . . . . . . . 12
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
(𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3
· (𝑦↑2))) |
57 | 56 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3 · (𝑦↑2)))) |
58 | | ax-1cn 10787 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
59 | 58, 13, 14 | divcli 11574 |
. . . . . . . . . . . 12
⊢ (1 / 3)
∈ ℂ |
60 | 59 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (1 / 3) ∈ ℂ) |
61 | 7, 30, 31, 57, 60 | dvmptcmul 24861 |
. . . . . . . . . 10
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ ((1 / 3) · (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) · (3
· (𝑦↑2))))) |
62 | 61 | mptru 1550 |
. . . . . . . . 9
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
((1 / 3) · (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) · (3
· (𝑦↑2)))) |
63 | | sqcl 13690 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → (𝑦↑2) ∈
ℂ) |
64 | | mulcl 10813 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ (𝑦↑2) ∈ ℂ) → (3 ·
(𝑦↑2)) ∈
ℂ) |
65 | 13, 63, 64 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → (3
· (𝑦↑2)) ∈
ℂ) |
66 | | divrec2 11507 |
. . . . . . . . . . . . 13
⊢ (((3
· (𝑦↑2)) ∈
ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → ((3 · (𝑦↑2)) / 3) = ((1 / 3)
· (3 · (𝑦↑2)))) |
67 | 13, 14, 66 | mp3an23 1455 |
. . . . . . . . . . . 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 11516 |
. . . . . . . . . . . . 13
⊢ (((𝑦↑2) ∈ ℂ ∧ 3
∈ ℂ ∧ 3 ≠ 0) → ((3 · (𝑦↑2)) / 3) = (𝑦↑2)) |
70 | 13, 14, 69 | mp3an23 1455 |
. . . . . . . . . . . 12
⊢ ((𝑦↑2) ∈ ℂ →
((3 · (𝑦↑2)) /
3) = (𝑦↑2)) |
71 | 8, 63, 70 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → ((3
· (𝑦↑2)) / 3) =
(𝑦↑2)) |
72 | 68, 71 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → ((1 / 3)
· (3 · (𝑦↑2))) = (𝑦↑2)) |
73 | 72 | mpteq2ia 5146 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ ↦ ((1 / 3)
· (3 · (𝑦↑2)))) = (𝑦 ∈ ℝ ↦ (𝑦↑2)) |
74 | 29, 62, 73 | 3eqtri 2769 |
. . . . . . . 8
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
((𝑦↑3) / 3))) = (𝑦 ∈ ℝ ↦ (𝑦↑2)) |
75 | 74 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ ((𝑦↑3)
/ 3))) = (𝑦 ∈ ℝ
↦ (𝑦↑2))) |
76 | 19 | adantl 485 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (3 · 𝑦) ∈ ℂ) |
77 | | 3ex 11912 |
. . . . . . . 8
⊢ 3 ∈
V |
78 | 77 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → 3 ∈ V) |
79 | 8 | adantl 485 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ ℝ) → 𝑦
∈ ℂ) |
80 | | 1red 10834 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ ℝ) → 1 ∈ ℝ) |
81 | 7 | dvmptid 24854 |
. . . . . . . . 9
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ 𝑦)) =
(𝑦 ∈ ℝ ↦
1)) |
82 | 13 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 3 ∈ ℂ) |
83 | 7, 79, 80, 81, 82 | dvmptcmul 24861 |
. . . . . . . 8
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (3 · 𝑦))) = (𝑦 ∈ ℝ ↦ (3 ·
1))) |
84 | | 3t1e3 11995 |
. . . . . . . . 9
⊢ (3
· 1) = 3 |
85 | 84 | mpteq2i 5147 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ ↦ (3
· 1)) = (𝑦 ∈
ℝ ↦ 3) |
86 | 83, 85 | eqtrdi 2794 |
. . . . . . 7
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (3 · 𝑦))) = (𝑦 ∈ ℝ ↦ 3)) |
87 | 7, 23, 24, 75, 76, 78, 86 | dvmptsub 24864 |
. . . . . 6
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) − 3))) |
88 | | 1re 10833 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
89 | | iccssre 13017 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ) → (1[,]2) ⊆
ℝ) |
90 | 88, 2, 89 | mp2an 692 |
. . . . . . 7
⊢ (1[,]2)
⊆ ℝ |
91 | 90 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1[,]2) ⊆ ℝ) |
92 | | eqid 2737 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
93 | 92 | tgioo2 23700 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
94 | | iccntr 23718 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ) → ((int‘(topGen‘ran
(,)))‘(1[,]2)) = (1(,)2)) |
95 | 88, 2, 94 | mp2an 692 |
. . . . . . 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 24859 |
. . . . 5
⊢ (⊤
→ (ℝ D (𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3))) |
98 | | ioossicc 13021 |
. . . . . . 7
⊢ (1(,)2)
⊆ (1[,]2) |
99 | | resmpt 5905 |
. . . . . . 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 3910 |
. . . . . . . . 9
⊢ (1[,]2)
⊆ ℂ |
102 | | resmpt 5905 |
. . . . . . . . 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 2737 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) = (𝑦 ∈ ℂ ↦ ((𝑦↑2) −
3)) |
105 | | subcl 11077 |
. . . . . . . . . . . . . 14
⊢ (((𝑦↑2) ∈ ℂ ∧ 3
∈ ℂ) → ((𝑦↑2) − 3) ∈
ℂ) |
106 | 13, 105 | mpan2 691 |
. . . . . . . . . . . . 13
⊢ ((𝑦↑2) ∈ ℂ →
((𝑦↑2) − 3)
∈ ℂ) |
107 | 63, 106 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → ((𝑦↑2) − 3) ∈
ℂ) |
108 | 104, 107 | fmpti 6929 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ ↦ ((𝑦↑2) −
3)):ℂ⟶ℂ |
109 | 34, 108, 34 | 3pm3.2i 1341 |
. . . . . . . . . 10
⊢ (ℂ
⊆ ℂ ∧ (𝑦
∈ ℂ ↦ ((𝑦↑2) − 3)):ℂ⟶ℂ
∧ ℂ ⊆ ℂ) |
110 | | ovex 7246 |
. . . . . . . . . . 11
⊢ ((2
· (𝑦↑(2 −
1))) − 0) ∈ V |
111 | | cnelprrecn 10822 |
. . . . . . . . . . . . . 14
⊢ ℂ
∈ {ℝ, ℂ} |
112 | 111 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
113 | 63 | adantl 485 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ ℂ) → (𝑦↑2) ∈ ℂ) |
114 | | ovexd 7248 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ ℂ) → (2 · (𝑦↑(2 − 1))) ∈
V) |
115 | | 2nn 11903 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ |
116 | | dvexp 24850 |
. . . . . . . . . . . . . . 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 10827 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
121 | 120 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ ℂ) → 0 ∈ V) |
122 | 112, 82 | dvmptc 24855 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ 3)) = (𝑦
∈ ℂ ↦ 0)) |
123 | 112, 113,
114, 118, 119, 121, 122 | dvmptsub 24864 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ ((𝑦↑2)
− 3))) = (𝑦 ∈
ℂ ↦ ((2 · (𝑦↑(2 − 1))) −
0))) |
124 | 123 | mptru 1550 |
. . . . . . . . . . 11
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
((𝑦↑2) − 3))) =
(𝑦 ∈ ℂ ↦
((2 · (𝑦↑(2
− 1))) − 0)) |
125 | 110, 124 | dmmpti 6522 |
. . . . . . . . . 10
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ ((𝑦↑2)
− 3))) = ℂ |
126 | | dvcn 24818 |
. . . . . . . . . 10
⊢
(((ℂ ⊆ ℂ ∧ (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)):ℂ⟶ℂ
∧ ℂ ⊆ ℂ) ∧ dom (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3))) = ℂ) →
(𝑦 ∈ ℂ ↦
((𝑦↑2) − 3))
∈ (ℂ–cn→ℂ)) |
127 | 109, 125,
126 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ∈
(ℂ–cn→ℂ) |
128 | | rescncf 23794 |
. . . . . . . . 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 2835 |
. . . . . . 7
⊢ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈
((1[,]2)–cn→ℂ) |
131 | | rescncf 23794 |
. . . . . . 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 2835 |
. . . . 5
⊢ (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3)) ∈
((1(,)2)–cn→ℂ) |
134 | 97, 133 | eqeltrdi 2846 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) ∈ ((1(,)2)–cn→ℂ)) |
135 | 98 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1(,)2) ⊆ (1[,]2)) |
136 | | ioombl 24462 |
. . . . . . 7
⊢ (1(,)2)
∈ dom vol |
137 | 136 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1(,)2) ∈ dom vol) |
138 | | ovexd 7248 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (1[,]2)) → ((𝑦↑2) − 3) ∈
V) |
139 | | cniccibl 24738 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈
((1[,]2)–cn→ℂ)) →
(𝑦 ∈ (1[,]2) ↦
((𝑦↑2) − 3))
∈ 𝐿1) |
140 | 88, 2, 130, 139 | mp3an 1463 |
. . . . . . 7
⊢ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈
𝐿1 |
141 | 140 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑦 ∈ (1[,]2)
↦ ((𝑦↑2) −
3)) ∈ 𝐿1) |
142 | 135, 137,
138, 141 | iblss 24702 |
. . . . 5
⊢ (⊤
→ (𝑦 ∈ (1(,)2)
↦ ((𝑦↑2) −
3)) ∈ 𝐿1) |
143 | 97, 142 | eqeltrd 2838 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) ∈
𝐿1) |
144 | | resmpt 5905 |
. . . . . . 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 2737 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) = (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) |
147 | 146, 20 | fmpti 6929 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))):ℝ⟶ℂ |
148 | | ssid 3923 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ |
149 | 35, 147, 148 | 3pm3.2i 1341 |
. . . . . . . 8
⊢ (ℝ
⊆ ℂ ∧ (𝑦
∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))):ℝ⟶ℂ ∧
ℝ ⊆ ℝ) |
150 | | ovex 7246 |
. . . . . . . . 9
⊢ ((𝑦↑2) − 3) ∈
V |
151 | 87 | mptru 1550 |
. . . . . . . . 9
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
(((𝑦↑3) / 3) −
(3 · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) −
3)) |
152 | 150, 151 | dmmpti 6522 |
. . . . . . . 8
⊢ dom
(ℝ D (𝑦 ∈
ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = ℝ |
153 | | dvcn 24818 |
. . . . . . . 8
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))):ℝ⟶ℂ ∧
ℝ ⊆ ℝ) ∧ dom (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = ℝ) → (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) ∈
(ℝ–cn→ℂ)) |
154 | 149, 152,
153 | mp2an 692 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) ∈
(ℝ–cn→ℂ) |
155 | | rescncf 23794 |
. . . . . . 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 2835 |
. . . . 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 24941 |
. . 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 1550 |
. 2
⊢
∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) d𝑥 = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘1)) |
161 | | itgeq2 24675 |
. . 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 7220 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝑦↑2) = (𝑥↑2)) |
163 | 162 | oveq1d 7228 |
. . . 4
⊢ (𝑦 = 𝑥 → ((𝑦↑2) − 3) = ((𝑥↑2) − 3)) |
164 | 97 | mptru 1550 |
. . . 4
⊢ (ℝ
D (𝑦 ∈ (1[,]2) ↦
(((𝑦↑3) / 3) −
(3 · 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) −
3)) |
165 | | ovex 7246 |
. . . 4
⊢ ((𝑥↑2) − 3) ∈
V |
166 | 163, 164,
165 | fvmpt 6818 |
. . 3
⊢ (𝑥 ∈ (1(,)2) → ((ℝ
D (𝑦 ∈ (1[,]2) ↦
(((𝑦↑3) / 3) −
(3 · 𝑦))))‘𝑥) = ((𝑥↑2) − 3)) |
167 | 161, 166 | mprg 3075 |
. 2
⊢
∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) d𝑥 = ∫(1(,)2)((𝑥↑2) − 3) d𝑥 |
168 | 2 | leidi 11366 |
. . . . . . . . 9
⊢ 2 ≤
2 |
169 | 88, 2 | elicc2i 13001 |
. . . . . . . . 9
⊢ (2 ∈
(1[,]2) ↔ (2 ∈ ℝ ∧ 1 ≤ 2 ∧ 2 ≤
2)) |
170 | 2, 4, 168, 169 | mpbir3an 1343 |
. . . . . . . 8
⊢ 2 ∈
(1[,]2) |
171 | | oveq1 7220 |
. . . . . . . . . . . 12
⊢ (𝑦 = 2 → (𝑦↑3) = (2↑3)) |
172 | 171 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝑦 = 2 → ((𝑦↑3) / 3) = ((2↑3) /
3)) |
173 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑦 = 2 → (3 · 𝑦) = (3 ·
2)) |
174 | 172, 173 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑦 = 2 → (((𝑦↑3) / 3) − (3
· 𝑦)) = (((2↑3)
/ 3) − (3 · 2))) |
175 | | cu2 13769 |
. . . . . . . . . . . . 13
⊢
(2↑3) = 8 |
176 | 175 | oveq1i 7223 |
. . . . . . . . . . . 12
⊢
((2↑3) / 3) = (8 / 3) |
177 | | 3t2e6 11996 |
. . . . . . . . . . . 12
⊢ (3
· 2) = 6 |
178 | 176, 177 | oveq12i 7225 |
. . . . . . . . . . 11
⊢
(((2↑3) / 3) − (3 · 2)) = ((8 / 3) −
6) |
179 | | 2cn 11905 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
180 | | 6cn 11921 |
. . . . . . . . . . . . . . 15
⊢ 6 ∈
ℂ |
181 | 179, 180,
13, 14 | divdiri 11589 |
. . . . . . . . . . . . . 14
⊢ ((2 + 6)
/ 3) = ((2 / 3) + (6 / 3)) |
182 | | 6p2e8 11989 |
. . . . . . . . . . . . . . . 16
⊢ (6 + 2) =
8 |
183 | 180, 179,
182 | addcomli 11024 |
. . . . . . . . . . . . . . 15
⊢ (2 + 6) =
8 |
184 | 183 | oveq1i 7223 |
. . . . . . . . . . . . . 14
⊢ ((2 + 6)
/ 3) = (8 / 3) |
185 | 180, 13, 179, 14 | divmuli 11586 |
. . . . . . . . . . . . . . . 16
⊢ ((6 / 3)
= 2 ↔ (3 · 2) = 6) |
186 | 177, 185 | mpbir 234 |
. . . . . . . . . . . . . . 15
⊢ (6 / 3) =
2 |
187 | 186 | oveq2i 7224 |
. . . . . . . . . . . . . 14
⊢ ((2 / 3)
+ (6 / 3)) = ((2 / 3) + 2) |
188 | 181, 184,
187 | 3eqtr3i 2773 |
. . . . . . . . . . . . 13
⊢ (8 / 3) =
((2 / 3) + 2) |
189 | 188 | oveq1i 7223 |
. . . . . . . . . . . 12
⊢ ((8 / 3)
− 6) = (((2 / 3) + 2) − 6) |
190 | 179, 13, 14 | divcli 11574 |
. . . . . . . . . . . . 13
⊢ (2 / 3)
∈ ℂ |
191 | | subsub3 11110 |
. . . . . . . . . . . . 13
⊢ (((2 / 3)
∈ ℂ ∧ 6 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 / 3)
− (6 − 2)) = (((2 / 3) + 2) − 6)) |
192 | 190, 180,
179, 191 | mp3an 1463 |
. . . . . . . . . . . 12
⊢ ((2 / 3)
− (6 − 2)) = (((2 / 3) + 2) − 6) |
193 | 189, 192 | eqtr4i 2768 |
. . . . . . . . . . 11
⊢ ((8 / 3)
− 6) = ((2 / 3) − (6 − 2)) |
194 | | 4cn 11915 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℂ |
195 | | 4p2e6 11983 |
. . . . . . . . . . . . . 14
⊢ (4 + 2) =
6 |
196 | 194, 179,
195 | addcomli 11024 |
. . . . . . . . . . . . 13
⊢ (2 + 4) =
6 |
197 | 180, 179,
194, 196 | subaddrii 11167 |
. . . . . . . . . . . 12
⊢ (6
− 2) = 4 |
198 | 197 | oveq2i 7224 |
. . . . . . . . . . 11
⊢ ((2 / 3)
− (6 − 2)) = ((2 / 3) − 4) |
199 | 178, 193,
198 | 3eqtri 2769 |
. . . . . . . . . 10
⊢
(((2↑3) / 3) − (3 · 2)) = ((2 / 3) −
4) |
200 | 174, 199 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑦 = 2 → (((𝑦↑3) / 3) − (3
· 𝑦)) = ((2 / 3)
− 4)) |
201 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) |
202 | | ovex 7246 |
. . . . . . . . 9
⊢ ((2 / 3)
− 4) ∈ V |
203 | 200, 201,
202 | fvmpt 6818 |
. . . . . . . 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 11366 |
. . . . . . . . 9
⊢ 1 ≤
1 |
206 | 88, 2 | elicc2i 13001 |
. . . . . . . . 9
⊢ (1 ∈
(1[,]2) ↔ (1 ∈ ℝ ∧ 1 ≤ 1 ∧ 1 ≤
2)) |
207 | 88, 205, 4, 206 | mpbir3an 1343 |
. . . . . . . 8
⊢ 1 ∈
(1[,]2) |
208 | | oveq1 7220 |
. . . . . . . . . . . 12
⊢ (𝑦 = 1 → (𝑦↑3) = (1↑3)) |
209 | 208 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → ((𝑦↑3) / 3) = ((1↑3) /
3)) |
210 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → (3 · 𝑦) = (3 ·
1)) |
211 | 209, 210 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → (((𝑦↑3) / 3) − (3
· 𝑦)) = (((1↑3)
/ 3) − (3 · 1))) |
212 | | 3z 12210 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℤ |
213 | | 1exp 13664 |
. . . . . . . . . . . . 13
⊢ (3 ∈
ℤ → (1↑3) = 1) |
214 | 212, 213 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(1↑3) = 1 |
215 | 214 | oveq1i 7223 |
. . . . . . . . . . 11
⊢
((1↑3) / 3) = (1 / 3) |
216 | 215, 84 | oveq12i 7225 |
. . . . . . . . . 10
⊢
(((1↑3) / 3) − (3 · 1)) = ((1 / 3) −
3) |
217 | 211, 216 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑦 = 1 → (((𝑦↑3) / 3) − (3
· 𝑦)) = ((1 / 3)
− 3)) |
218 | | ovex 7246 |
. . . . . . . . 9
⊢ ((1 / 3)
− 3) ∈ V |
219 | 217, 201,
218 | fvmpt 6818 |
. . . . . . . 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 7225 |
. . . . . 6
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = (((2 / 3) − 4) −
((1 / 3) − 3)) |
222 | | sub4 11123 |
. . . . . . 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 693 |
. . . . . 6
⊢ (((2 / 3)
− 4) − ((1 / 3) − 3)) = (((2 / 3) − (1 / 3)) − (4
− 3)) |
224 | 13, 14 | pm3.2i 474 |
. . . . . . . . 9
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
225 | | divsubdir 11526 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ 1 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0))
→ ((2 − 1) / 3) = ((2 / 3) − (1 / 3))) |
226 | 179, 58, 224, 225 | mp3an 1463 |
. . . . . . . 8
⊢ ((2
− 1) / 3) = ((2 / 3) − (1 / 3)) |
227 | | 2m1e1 11956 |
. . . . . . . . 9
⊢ (2
− 1) = 1 |
228 | 227 | oveq1i 7223 |
. . . . . . . 8
⊢ ((2
− 1) / 3) = (1 / 3) |
229 | 226, 228 | eqtr3i 2767 |
. . . . . . 7
⊢ ((2 / 3)
− (1 / 3)) = (1 / 3) |
230 | | 3p1e4 11975 |
. . . . . . . 8
⊢ (3 + 1) =
4 |
231 | 194, 13, 58, 230 | subaddrii 11167 |
. . . . . . 7
⊢ (4
− 3) = 1 |
232 | 229, 231 | oveq12i 7225 |
. . . . . 6
⊢ (((2 / 3)
− (1 / 3)) − (4 − 3)) = ((1 / 3) − 1) |
233 | 221, 223,
232 | 3eqtri 2769 |
. . . . 5
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = ((1 / 3) −
1) |
234 | 13, 14 | dividi 11565 |
. . . . . 6
⊢ (3 / 3) =
1 |
235 | 234 | oveq2i 7224 |
. . . . 5
⊢ ((1 / 3)
− (3 / 3)) = ((1 / 3) − 1) |
236 | 233, 235 | eqtr4i 2768 |
. . . 4
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = ((1 / 3) − (3 /
3)) |
237 | | divsubdir 11526 |
. . . . 5
⊢ ((1
∈ ℂ ∧ 3 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0))
→ ((1 − 3) / 3) = ((1 / 3) − (3 / 3))) |
238 | 58, 13, 224, 237 | mp3an 1463 |
. . . 4
⊢ ((1
− 3) / 3) = ((1 / 3) − (3 / 3)) |
239 | 236, 238 | eqtr4i 2768 |
. . 3
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = ((1 − 3) /
3) |
240 | | divneg 11524 |
. . . . 5
⊢ ((2
∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → -(2 / 3) = (-2 /
3)) |
241 | 179, 13, 14, 240 | mp3an 1463 |
. . . 4
⊢ -(2 / 3)
= (-2 / 3) |
242 | 13, 58 | negsubdi2i 11164 |
. . . . . 6
⊢ -(3
− 1) = (1 − 3) |
243 | 40 | negeqi 11071 |
. . . . . 6
⊢ -(3
− 1) = -2 |
244 | 242, 243 | eqtr3i 2767 |
. . . . 5
⊢ (1
− 3) = -2 |
245 | 244 | oveq1i 7223 |
. . . 4
⊢ ((1
− 3) / 3) = (-2 / 3) |
246 | 241, 245 | eqtr4i 2768 |
. . 3
⊢ -(2 / 3)
= ((1 − 3) / 3) |
247 | 239, 246 | eqtr4i 2768 |
. 2
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = -(2 / 3) |
248 | 160, 167,
247 | 3eqtr3i 2773 |
1
⊢
∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3) |