| Step | Hyp | Ref
| Expression |
| 1 | | 1red 11262 |
. . . 4
⊢ (⊤
→ 1 ∈ ℝ) |
| 2 | | 2re 12340 |
. . . . 5
⊢ 2 ∈
ℝ |
| 3 | 2 | a1i 11 |
. . . 4
⊢ (⊤
→ 2 ∈ ℝ) |
| 4 | | 1le2 12475 |
. . . . 5
⊢ 1 ≤
2 |
| 5 | 4 | a1i 11 |
. . . 4
⊢ (⊤
→ 1 ≤ 2) |
| 6 | | reelprrecn 11247 |
. . . . . . 7
⊢ ℝ
∈ {ℝ, ℂ} |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
| 8 | | recn 11245 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
| 9 | | 3nn0 12544 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
| 10 | | expcl 14120 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝑦↑3) ∈ ℂ) |
| 11 | 9, 10 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → (𝑦↑3) ∈
ℂ) |
| 12 | 8, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦↑3) ∈
ℂ) |
| 13 | | 3cn 12347 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
| 14 | | 3ne0 12372 |
. . . . . . . . . 10
⊢ 3 ≠
0 |
| 15 | | divcl 11928 |
. . . . . . . . . 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 11239 |
. . . . . . . . 9
⊢ ((3
∈ ℂ ∧ 𝑦
∈ ℂ) → (3 · 𝑦) ∈ ℂ) |
| 19 | 13, 8, 18 | sylancr 587 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → (3
· 𝑦) ∈
ℂ) |
| 20 | 17, 19 | subcld 11620 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → (((𝑦↑3) / 3) − (3
· 𝑦)) ∈
ℂ) |
| 21 | 20 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (((𝑦↑3) / 3) − (3 · 𝑦)) ∈
ℂ) |
| 22 | | ovexd 7466 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ ℝ) → ((𝑦↑2) − 3) ∈
V) |
| 23 | 17 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → ((𝑦↑3) / 3) ∈
ℂ) |
| 24 | | ovexd 7466 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (𝑦↑2) ∈ V) |
| 25 | | divrec2 11939 |
. . . . . . . . . . . . 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 5245 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3)) = (𝑦 ∈ ℝ ↦ ((1 / 3)
· (𝑦↑3))) |
| 29 | 28 | oveq2i 7442 |
. . . . . . . . 9
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
((𝑦↑3) / 3))) =
(ℝ D (𝑦 ∈
ℝ ↦ ((1 / 3) · (𝑦↑3)))) |
| 30 | 12 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (𝑦↑3) ∈ ℂ) |
| 31 | | ovexd 7466 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (3 · (𝑦↑2)) ∈ V) |
| 32 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ ↦ (𝑦↑3)) = (𝑦 ∈ ℂ ↦ (𝑦↑3)) |
| 33 | 32, 11 | fmpti 7132 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℂ ↦ (𝑦↑3)):ℂ⟶ℂ |
| 34 | | ssid 4006 |
. . . . . . . . . . . . . 14
⊢ ℂ
⊆ ℂ |
| 35 | | ax-resscn 11212 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
| 36 | | ovex 7464 |
. . . . . . . . . . . . . . . 16
⊢ (3
· (𝑦↑2)) ∈
V |
| 37 | | 3nn 12345 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℕ |
| 38 | | dvexp 25991 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 ∈
ℕ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3 · (𝑦↑(3 −
1))))) |
| 39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3
· (𝑦↑(3 −
1)))) |
| 40 | | 3m1e2 12394 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (3
− 1) = 2 |
| 41 | 40 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦↑(3 − 1)) = (𝑦↑2) |
| 42 | 41 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . 18
⊢ (3
· (𝑦↑(3 −
1))) = (3 · (𝑦↑2)) |
| 43 | 42 | mpteq2i 5247 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℂ ↦ (3
· (𝑦↑(3 −
1)))) = (𝑦 ∈ ℂ
↦ (3 · (𝑦↑2))) |
| 44 | 39, 43 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3
· (𝑦↑2))) |
| 45 | 36, 44 | dmmpti 6712 |
. . . . . . . . . . . . . . 15
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑3))) = ℂ |
| 46 | 35, 45 | sseqtrri 4033 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ dom (ℂ D (𝑦
∈ ℂ ↦ (𝑦↑3))) |
| 47 | | dvres3 25948 |
. . . . . . . . . . . . . 14
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (𝑦↑3)):ℂ⟶ℂ) ∧
(ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))))) → (ℝ D
((𝑦 ∈ ℂ ↦
(𝑦↑3)) ↾
ℝ)) = ((ℂ D (𝑦
∈ ℂ ↦ (𝑦↑3))) ↾ ℝ)) |
| 48 | 6, 33, 34, 46, 47 | mp4an 693 |
. . . . . . . . . . . . 13
⊢ (ℝ
D ((𝑦 ∈ ℂ
↦ (𝑦↑3)) ↾
ℝ)) = ((ℂ D (𝑦
∈ ℂ ↦ (𝑦↑3))) ↾ ℝ) |
| 49 | | resmpt 6055 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (𝑦↑3)) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3))) |
| 50 | 35, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ↦ (𝑦↑3)) ↾ ℝ) =
(𝑦 ∈ ℝ ↦
(𝑦↑3)) |
| 51 | 50 | oveq2i 7442 |
. . . . . . . . . . . . 13
⊢ (ℝ
D ((𝑦 ∈ ℂ
↦ (𝑦↑3)) ↾
ℝ)) = (ℝ D (𝑦
∈ ℝ ↦ (𝑦↑3))) |
| 52 | 44 | reseq1i 5993 |
. . . . . . . . . . . . . 14
⊢ ((ℂ
D (𝑦 ∈ ℂ ↦
(𝑦↑3))) ↾
ℝ) = ((𝑦 ∈
ℂ ↦ (3 · (𝑦↑2))) ↾ ℝ) |
| 53 | | resmpt 6055 |
. . . . . . . . . . . . . . 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 11213 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
| 59 | 58, 13, 14 | divcli 12009 |
. . . . . . . . . . . 12
⊢ (1 / 3)
∈ ℂ |
| 60 | 59 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (1 / 3) ∈ ℂ) |
| 61 | 7, 30, 31, 57, 60 | dvmptcmul 26002 |
. . . . . . . . . 10
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ ((1 / 3) · (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) · (3
· (𝑦↑2))))) |
| 62 | 61 | mptru 1547 |
. . . . . . . . 9
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
((1 / 3) · (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) · (3
· (𝑦↑2)))) |
| 63 | | sqcl 14158 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → (𝑦↑2) ∈
ℂ) |
| 64 | | mulcl 11239 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ (𝑦↑2) ∈ ℂ) → (3 ·
(𝑦↑2)) ∈
ℂ) |
| 65 | 13, 63, 64 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → (3
· (𝑦↑2)) ∈
ℂ) |
| 66 | | divrec2 11939 |
. . . . . . . . . . . . 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 11948 |
. . . . . . . . . . . . 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 5245 |
. . . . . . . . 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 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → (3 · 𝑦) ∈ ℂ) |
| 77 | | 3ex 12348 |
. . . . . . . 8
⊢ 3 ∈
V |
| 78 | 77 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ ℝ) → 3 ∈ V) |
| 79 | 8 | adantl 481 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ ℝ) → 𝑦
∈ ℂ) |
| 80 | | 1red 11262 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ ℝ) → 1 ∈ ℝ) |
| 81 | 7 | dvmptid 25995 |
. . . . . . . . 9
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ 𝑦)) =
(𝑦 ∈ ℝ ↦
1)) |
| 82 | 13 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 3 ∈ ℂ) |
| 83 | 7, 79, 80, 81, 82 | dvmptcmul 26002 |
. . . . . . . 8
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (3 · 𝑦))) = (𝑦 ∈ ℝ ↦ (3 ·
1))) |
| 84 | | 3t1e3 12431 |
. . . . . . . . 9
⊢ (3
· 1) = 3 |
| 85 | 84 | mpteq2i 5247 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ ↦ (3
· 1)) = (𝑦 ∈
ℝ ↦ 3) |
| 86 | 83, 85 | eqtrdi 2793 |
. . . . . . 7
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (3 · 𝑦))) = (𝑦 ∈ ℝ ↦ 3)) |
| 87 | 7, 23, 24, 75, 76, 78, 86 | dvmptsub 26005 |
. . . . . 6
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) − 3))) |
| 88 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 89 | | iccssre 13469 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ) → (1[,]2) ⊆
ℝ) |
| 90 | 88, 2, 89 | mp2an 692 |
. . . . . . 7
⊢ (1[,]2)
⊆ ℝ |
| 91 | 90 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1[,]2) ⊆ ℝ) |
| 92 | | tgioo4 24826 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 93 | | eqid 2737 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 94 | | iccntr 24843 |
. . . . . . . 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, 92, 93, 96 | dvmptres2 26000 |
. . . . 5
⊢ (⊤
→ (ℝ D (𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3))) |
| 98 | | ioossicc 13473 |
. . . . . . 7
⊢ (1(,)2)
⊆ (1[,]2) |
| 99 | | resmpt 6055 |
. . . . . . 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 3993 |
. . . . . . . . 9
⊢ (1[,]2)
⊆ ℂ |
| 102 | | resmpt 6055 |
. . . . . . . . 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 11507 |
. . . . . . . . . . . . . 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 7132 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ ↦ ((𝑦↑2) −
3)):ℂ⟶ℂ |
| 109 | 34, 108, 34 | 3pm3.2i 1340 |
. . . . . . . . . 10
⊢ (ℂ
⊆ ℂ ∧ (𝑦
∈ ℂ ↦ ((𝑦↑2) − 3)):ℂ⟶ℂ
∧ ℂ ⊆ ℂ) |
| 110 | | ovex 7464 |
. . . . . . . . . . 11
⊢ ((2
· (𝑦↑(2 −
1))) − 0) ∈ V |
| 111 | | cnelprrecn 11248 |
. . . . . . . . . . . . . 14
⊢ ℂ
∈ {ℝ, ℂ} |
| 112 | 111 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
| 113 | 63 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ ℂ) → (𝑦↑2) ∈ ℂ) |
| 114 | | ovexd 7466 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ ℂ) → (2 · (𝑦↑(2 − 1))) ∈
V) |
| 115 | | 2nn 12339 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ |
| 116 | | dvexp 25991 |
. . . . . . . . . . . . . . 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 11255 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
| 121 | 120 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ ℂ) → 0 ∈ V) |
| 122 | 112, 82 | dvmptc 25996 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ 3)) = (𝑦
∈ ℂ ↦ 0)) |
| 123 | 112, 113,
114, 118, 119, 121, 122 | dvmptsub 26005 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ ((𝑦↑2)
− 3))) = (𝑦 ∈
ℂ ↦ ((2 · (𝑦↑(2 − 1))) −
0))) |
| 124 | 123 | mptru 1547 |
. . . . . . . . . . 11
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
((𝑦↑2) − 3))) =
(𝑦 ∈ ℂ ↦
((2 · (𝑦↑(2
− 1))) − 0)) |
| 125 | 110, 124 | dmmpti 6712 |
. . . . . . . . . 10
⊢ dom
(ℂ D (𝑦 ∈
ℂ ↦ ((𝑦↑2)
− 3))) = ℂ |
| 126 | | dvcn 25957 |
. . . . . . . . . 10
⊢
(((ℂ ⊆ ℂ ∧ (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)):ℂ⟶ℂ
∧ ℂ ⊆ ℂ) ∧ dom (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3))) = ℂ) →
(𝑦 ∈ ℂ ↦
((𝑦↑2) − 3))
∈ (ℂ–cn→ℂ)) |
| 127 | 109, 125,
126 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ∈
(ℂ–cn→ℂ) |
| 128 | | rescncf 24923 |
. . . . . . . . 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 2838 |
. . . . . . 7
⊢ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈
((1[,]2)–cn→ℂ) |
| 131 | | rescncf 24923 |
. . . . . . 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 2838 |
. . . . 5
⊢ (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3)) ∈
((1(,)2)–cn→ℂ) |
| 134 | 97, 133 | eqeltrdi 2849 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) ∈ ((1(,)2)–cn→ℂ)) |
| 135 | 98 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1(,)2) ⊆ (1[,]2)) |
| 136 | | ioombl 25600 |
. . . . . . 7
⊢ (1(,)2)
∈ dom vol |
| 137 | 136 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1(,)2) ∈ dom vol) |
| 138 | | ovexd 7466 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (1[,]2)) → ((𝑦↑2) − 3) ∈
V) |
| 139 | | cniccibl 25876 |
. . . . . . . 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 25840 |
. . . . 5
⊢ (⊤
→ (𝑦 ∈ (1(,)2)
↦ ((𝑦↑2) −
3)) ∈ 𝐿1) |
| 143 | 97, 142 | eqeltrd 2841 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑦 ∈
(1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) ∈
𝐿1) |
| 144 | | resmpt 6055 |
. . . . . . 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 7132 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3
· 𝑦))):ℝ⟶ℂ |
| 148 | | ssid 4006 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ |
| 149 | 35, 147, 148 | 3pm3.2i 1340 |
. . . . . . . 8
⊢ (ℝ
⊆ ℂ ∧ (𝑦
∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))):ℝ⟶ℂ ∧
ℝ ⊆ ℝ) |
| 150 | | ovex 7464 |
. . . . . . . . 9
⊢ ((𝑦↑2) − 3) ∈
V |
| 151 | 87 | mptru 1547 |
. . . . . . . . 9
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
(((𝑦↑3) / 3) −
(3 · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) −
3)) |
| 152 | 150, 151 | dmmpti 6712 |
. . . . . . . 8
⊢ dom
(ℝ D (𝑦 ∈
ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = ℝ |
| 153 | | dvcn 25957 |
. . . . . . . 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 24923 |
. . . . . . 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 2838 |
. . . . 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 26085 |
. . 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 1547 |
. 2
⊢
∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) d𝑥 = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘1)) |
| 161 | | itgeq2 25813 |
. . 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 7438 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝑦↑2) = (𝑥↑2)) |
| 163 | 162 | oveq1d 7446 |
. . . 4
⊢ (𝑦 = 𝑥 → ((𝑦↑2) − 3) = ((𝑥↑2) − 3)) |
| 164 | 97 | mptru 1547 |
. . . 4
⊢ (ℝ
D (𝑦 ∈ (1[,]2) ↦
(((𝑦↑3) / 3) −
(3 · 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) −
3)) |
| 165 | | ovex 7464 |
. . . 4
⊢ ((𝑥↑2) − 3) ∈
V |
| 166 | 163, 164,
165 | fvmpt 7016 |
. . 3
⊢ (𝑥 ∈ (1(,)2) → ((ℝ
D (𝑦 ∈ (1[,]2) ↦
(((𝑦↑3) / 3) −
(3 · 𝑦))))‘𝑥) = ((𝑥↑2) − 3)) |
| 167 | 161, 166 | mprg 3067 |
. 2
⊢
∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) d𝑥 = ∫(1(,)2)((𝑥↑2) − 3) d𝑥 |
| 168 | 2 | leidi 11797 |
. . . . . . . . 9
⊢ 2 ≤
2 |
| 169 | 88, 2 | elicc2i 13453 |
. . . . . . . . 9
⊢ (2 ∈
(1[,]2) ↔ (2 ∈ ℝ ∧ 1 ≤ 2 ∧ 2 ≤
2)) |
| 170 | 2, 4, 168, 169 | mpbir3an 1342 |
. . . . . . . 8
⊢ 2 ∈
(1[,]2) |
| 171 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑦 = 2 → (𝑦↑3) = (2↑3)) |
| 172 | 171 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑦 = 2 → ((𝑦↑3) / 3) = ((2↑3) /
3)) |
| 173 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑦 = 2 → (3 · 𝑦) = (3 ·
2)) |
| 174 | 172, 173 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑦 = 2 → (((𝑦↑3) / 3) − (3
· 𝑦)) = (((2↑3)
/ 3) − (3 · 2))) |
| 175 | | cu2 14239 |
. . . . . . . . . . . . 13
⊢
(2↑3) = 8 |
| 176 | 175 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢
((2↑3) / 3) = (8 / 3) |
| 177 | | 3t2e6 12432 |
. . . . . . . . . . . 12
⊢ (3
· 2) = 6 |
| 178 | 176, 177 | oveq12i 7443 |
. . . . . . . . . . 11
⊢
(((2↑3) / 3) − (3 · 2)) = ((8 / 3) −
6) |
| 179 | | 2cn 12341 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
| 180 | | 6cn 12357 |
. . . . . . . . . . . . . . 15
⊢ 6 ∈
ℂ |
| 181 | 179, 180,
13, 14 | divdiri 12024 |
. . . . . . . . . . . . . 14
⊢ ((2 + 6)
/ 3) = ((2 / 3) + (6 / 3)) |
| 182 | | 6p2e8 12425 |
. . . . . . . . . . . . . . . 16
⊢ (6 + 2) =
8 |
| 183 | 180, 179,
182 | addcomli 11453 |
. . . . . . . . . . . . . . 15
⊢ (2 + 6) =
8 |
| 184 | 183 | oveq1i 7441 |
. . . . . . . . . . . . . 14
⊢ ((2 + 6)
/ 3) = (8 / 3) |
| 185 | 180, 13, 179, 14 | divmuli 12021 |
. . . . . . . . . . . . . . . 16
⊢ ((6 / 3)
= 2 ↔ (3 · 2) = 6) |
| 186 | 177, 185 | mpbir 231 |
. . . . . . . . . . . . . . 15
⊢ (6 / 3) =
2 |
| 187 | 186 | oveq2i 7442 |
. . . . . . . . . . . . . 14
⊢ ((2 / 3)
+ (6 / 3)) = ((2 / 3) + 2) |
| 188 | 181, 184,
187 | 3eqtr3i 2773 |
. . . . . . . . . . . . 13
⊢ (8 / 3) =
((2 / 3) + 2) |
| 189 | 188 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ ((8 / 3)
− 6) = (((2 / 3) + 2) − 6) |
| 190 | 179, 13, 14 | divcli 12009 |
. . . . . . . . . . . . 13
⊢ (2 / 3)
∈ ℂ |
| 191 | | subsub3 11541 |
. . . . . . . . . . . . 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 12351 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℂ |
| 195 | | 4p2e6 12419 |
. . . . . . . . . . . . . 14
⊢ (4 + 2) =
6 |
| 196 | 194, 179,
195 | addcomli 11453 |
. . . . . . . . . . . . 13
⊢ (2 + 4) =
6 |
| 197 | 180, 179,
194, 196 | subaddrii 11598 |
. . . . . . . . . . . 12
⊢ (6
− 2) = 4 |
| 198 | 197 | oveq2i 7442 |
. . . . . . . . . . 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 2793 |
. . . . . . . . 9
⊢ (𝑦 = 2 → (((𝑦↑3) / 3) − (3
· 𝑦)) = ((2 / 3)
− 4)) |
| 201 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦))) |
| 202 | | ovex 7464 |
. . . . . . . . 9
⊢ ((2 / 3)
− 4) ∈ V |
| 203 | 200, 201,
202 | fvmpt 7016 |
. . . . . . . 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 11797 |
. . . . . . . . 9
⊢ 1 ≤
1 |
| 206 | 88, 2 | elicc2i 13453 |
. . . . . . . . 9
⊢ (1 ∈
(1[,]2) ↔ (1 ∈ ℝ ∧ 1 ≤ 1 ∧ 1 ≤
2)) |
| 207 | 88, 205, 4, 206 | mpbir3an 1342 |
. . . . . . . 8
⊢ 1 ∈
(1[,]2) |
| 208 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑦 = 1 → (𝑦↑3) = (1↑3)) |
| 209 | 208 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → ((𝑦↑3) / 3) = ((1↑3) /
3)) |
| 210 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → (3 · 𝑦) = (3 ·
1)) |
| 211 | 209, 210 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → (((𝑦↑3) / 3) − (3
· 𝑦)) = (((1↑3)
/ 3) − (3 · 1))) |
| 212 | | 3z 12650 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℤ |
| 213 | | 1exp 14132 |
. . . . . . . . . . . . 13
⊢ (3 ∈
ℤ → (1↑3) = 1) |
| 214 | 212, 213 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(1↑3) = 1 |
| 215 | 214 | oveq1i 7441 |
. . . . . . . . . . 11
⊢
((1↑3) / 3) = (1 / 3) |
| 216 | 215, 84 | oveq12i 7443 |
. . . . . . . . . 10
⊢
(((1↑3) / 3) − (3 · 1)) = ((1 / 3) −
3) |
| 217 | 211, 216 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑦 = 1 → (((𝑦↑3) / 3) − (3
· 𝑦)) = ((1 / 3)
− 3)) |
| 218 | | ovex 7464 |
. . . . . . . . 9
⊢ ((1 / 3)
− 3) ∈ V |
| 219 | 217, 201,
218 | fvmpt 7016 |
. . . . . . . 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 7443 |
. . . . . 6
⊢ (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3
· 𝑦)))‘2)
− ((𝑦 ∈ (1[,]2)
↦ (((𝑦↑3) / 3)
− (3 · 𝑦)))‘1)) = (((2 / 3) − 4) −
((1 / 3) − 3)) |
| 222 | | sub4 11554 |
. . . . . . 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 470 |
. . . . . . . . 9
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
| 225 | | divsubdir 11961 |
. . . . . . . . 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 12392 |
. . . . . . . . 9
⊢ (2
− 1) = 1 |
| 228 | 227 | oveq1i 7441 |
. . . . . . . 8
⊢ ((2
− 1) / 3) = (1 / 3) |
| 229 | 226, 228 | eqtr3i 2767 |
. . . . . . 7
⊢ ((2 / 3)
− (1 / 3)) = (1 / 3) |
| 230 | | 3p1e4 12411 |
. . . . . . . 8
⊢ (3 + 1) =
4 |
| 231 | 194, 13, 58, 230 | subaddrii 11598 |
. . . . . . 7
⊢ (4
− 3) = 1 |
| 232 | 229, 231 | oveq12i 7443 |
. . . . . 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 12000 |
. . . . . 6
⊢ (3 / 3) =
1 |
| 235 | 234 | oveq2i 7442 |
. . . . 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 11961 |
. . . . 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 11959 |
. . . . 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 11595 |
. . . . . 6
⊢ -(3
− 1) = (1 − 3) |
| 243 | 40 | negeqi 11501 |
. . . . . 6
⊢ -(3
− 1) = -2 |
| 244 | 242, 243 | eqtr3i 2767 |
. . . . 5
⊢ (1
− 3) = -2 |
| 245 | 244 | oveq1i 7441 |
. . . 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) |