Metamath Proof Explorer

Theorem lhe4.4ex1a

Description: Example of the Fundamental Theorem of Calculus, part two ( ftc2 ): S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x = -u ( 2 / 3 ) . Section 4.4 example 1a of LarsonHostetlerEdwards p. 311. (The book teaches ftc2 as simply the "Fundamental Theorem of Calculus", then ftc1 as the "Second Fundamental Theorem of Calculus".) (Contributed by Steve Rodriguez, 28-Oct-2015) (Revised by Steve Rodriguez, 31-Oct-2015)

Ref Expression
Assertion lhe4.4ex1a ∫ ( 1 (,) 2 ) ( ( 𝑥 ↑ 2 ) − 3 ) d 𝑥 = - ( 2 / 3 )

Proof

Step Hyp Ref Expression
1 1red ⊢ ( ⊤ → 1 ∈ ℝ )
2 2re ⊢ 2 ∈ ℝ
3 2 a1i ⊢ ( ⊤ → 2 ∈ ℝ )
4 1le2 ⊢ 1 ≤ 2
5 4 a1i ⊢ ( ⊤ → 1 ≤ 2 )
6 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
7 6 a1i ⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } )
8 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
9 3nn0 ⊢ 3 ∈ ℕ0
10 expcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑦 ↑ 3 ) ∈ ℂ )
11 9 10 mpan2 ⊢ ( 𝑦 ∈ ℂ → ( 𝑦 ↑ 3 ) ∈ ℂ )
12 8 11 syl ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 ↑ 3 ) ∈ ℂ )
13 3cn ⊢ 3 ∈ ℂ
14 3ne0 ⊢ 3 ≠ 0
15 divcl ⊢ ( ( ( 𝑦 ↑ 3 ) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( ( 𝑦 ↑ 3 ) / 3 ) ∈ ℂ )
16 13 14 15 mp3an23 ⊢ ( ( 𝑦 ↑ 3 ) ∈ ℂ → ( ( 𝑦 ↑ 3 ) / 3 ) ∈ ℂ )
17 12 16 syl ⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 ↑ 3 ) / 3 ) ∈ ℂ )
18 mulcl ⊢ ( ( 3 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 3 · 𝑦 ) ∈ ℂ )
19 13 8 18 sylancr ⊢ ( 𝑦 ∈ ℝ → ( 3 · 𝑦 ) ∈ ℂ )
20 17 19 subcld ⊢ ( 𝑦 ∈ ℝ → ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ∈ ℂ )
21 20 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ∈ ℂ )
22 ovexd ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 ↑ 2 ) − 3 ) ∈ V )
23 17 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 ↑ 3 ) / 3 ) ∈ ℂ )
24 ovexd ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ↑ 2 ) ∈ V )
25 divrec2 ⊢ ( ( ( 𝑦 ↑ 3 ) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( ( 𝑦 ↑ 3 ) / 3 ) = ( ( 1 / 3 ) · ( 𝑦 ↑ 3 ) ) )
26 13 14 25 mp3an23 ⊢ ( ( 𝑦 ↑ 3 ) ∈ ℂ → ( ( 𝑦 ↑ 3 ) / 3 ) = ( ( 1 / 3 ) · ( 𝑦 ↑ 3 ) ) )
27 12 26 syl ⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 ↑ 3 ) / 3 ) = ( ( 1 / 3 ) · ( 𝑦 ↑ 3 ) ) )
28 27 mpteq2ia ⊢ ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ 3 ) / 3 ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 1 / 3 ) · ( 𝑦 ↑ 3 ) ) )
29 28 oveq2i ⊢ ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ 3 ) / 3 ) ) ) = ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 1 / 3 ) · ( 𝑦 ↑ 3 ) ) ) )
30 12 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ↑ 3 ) ∈ ℂ )
31 ovexd ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → ( 3 · ( 𝑦 ↑ 2 ) ) ∈ V )
32 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) )
33 32 11 fmpti ⊢ ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) : ℂ ⟶ ℂ
34 ssid ⊢ ℂ ⊆ ℂ
35 ax-resscn ⊢ ℝ ⊆ ℂ
36 ovex ⊢ ( 3 · ( 𝑦 ↑ 2 ) ) ∈ V
37 3nn ⊢ 3 ∈ ℕ
38 dvexp ⊢ ( 3 ∈ ℕ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 3 · ( 𝑦 ↑ ( 3 − 1 ) ) ) ) )
39 37 38 ax-mp ⊢ ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 3 · ( 𝑦 ↑ ( 3 − 1 ) ) ) )
40 3m1e2 ⊢ ( 3 − 1 ) = 2
41 40 oveq2i ⊢ ( 𝑦 ↑ ( 3 − 1 ) ) = ( 𝑦 ↑ 2 )
42 41 oveq2i ⊢ ( 3 · ( 𝑦 ↑ ( 3 − 1 ) ) ) = ( 3 · ( 𝑦 ↑ 2 ) )
43 42 mpteq2i ⊢ ( 𝑦 ∈ ℂ ↦ ( 3 · ( 𝑦 ↑ ( 3 − 1 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 3 · ( 𝑦 ↑ 2 ) ) )
44 39 43 eqtri ⊢ ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 3 · ( 𝑦 ↑ 2 ) ) )
45 36 44 dmmpti ⊢ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ) = ℂ
46 35 45 sseqtrri ⊢ ℝ ⊆ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) )
47 dvres3 ⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ) ) ) → ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ) ↾ ℝ ) )
48 6 33 34 46 47 mp4an ⊢ ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ) ↾ ℝ )
49 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( 𝑦 ↑ 3 ) ) )
50 35 49 ax-mp ⊢ ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( 𝑦 ↑ 3 ) )
51 50 oveq2i ⊢ ( ℝ D ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ↾ ℝ ) ) = ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 ↑ 3 ) ) )
52 44 reseq1i ⊢ ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ) ↾ ℝ ) = ( ( 𝑦 ∈ ℂ ↦ ( 3 · ( 𝑦 ↑ 2 ) ) ) ↾ ℝ )
53 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( 3 · ( 𝑦 ↑ 2 ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( 3 · ( 𝑦 ↑ 2 ) ) ) )
54 35 53 ax-mp ⊢ ( ( 𝑦 ∈ ℂ ↦ ( 3 · ( 𝑦 ↑ 2 ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( 3 · ( 𝑦 ↑ 2 ) ) )
55 52 54 eqtri ⊢ ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 3 ) ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( 3 · ( 𝑦 ↑ 2 ) ) )
56 48 51 55 3eqtr3i ⊢ ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 ↑ 3 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 3 · ( 𝑦 ↑ 2 ) ) )
57 56 a1i ⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 ↑ 3 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 3 · ( 𝑦 ↑ 2 ) ) ) )
58 ax-1cn ⊢ 1 ∈ ℂ
59 58 13 14 divcli ⊢ ( 1 / 3 ) ∈ ℂ
60 59 a1i ⊢ ( ⊤ → ( 1 / 3 ) ∈ ℂ )
61 7 30 31 57 60 dvmptcmul ⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 1 / 3 ) · ( 𝑦 ↑ 3 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 1 / 3 ) · ( 3 · ( 𝑦 ↑ 2 ) ) ) ) )
62 61 mptru ⊢ ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 1 / 3 ) · ( 𝑦 ↑ 3 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 1 / 3 ) · ( 3 · ( 𝑦 ↑ 2 ) ) ) )
63 sqcl ⊢ ( 𝑦 ∈ ℂ → ( 𝑦 ↑ 2 ) ∈ ℂ )
64 mulcl ⊢ ( ( 3 ∈ ℂ ∧ ( 𝑦 ↑ 2 ) ∈ ℂ ) → ( 3 · ( 𝑦 ↑ 2 ) ) ∈ ℂ )
65 13 63 64 sylancr ⊢ ( 𝑦 ∈ ℂ → ( 3 · ( 𝑦 ↑ 2 ) ) ∈ ℂ )
66 divrec2 ⊢ ( ( ( 3 · ( 𝑦 ↑ 2 ) ) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( ( 3 · ( 𝑦 ↑ 2 ) ) / 3 ) = ( ( 1 / 3 ) · ( 3 · ( 𝑦 ↑ 2 ) ) ) )
67 13 14 66 mp3an23 ⊢ ( ( 3 · ( 𝑦 ↑ 2 ) ) ∈ ℂ → ( ( 3 · ( 𝑦 ↑ 2 ) ) / 3 ) = ( ( 1 / 3 ) · ( 3 · ( 𝑦 ↑ 2 ) ) ) )
68 8 65 67 3syl ⊢ ( 𝑦 ∈ ℝ → ( ( 3 · ( 𝑦 ↑ 2 ) ) / 3 ) = ( ( 1 / 3 ) · ( 3 · ( 𝑦 ↑ 2 ) ) ) )
69 divcan3 ⊢ ( ( ( 𝑦 ↑ 2 ) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( ( 3 · ( 𝑦 ↑ 2 ) ) / 3 ) = ( 𝑦 ↑ 2 ) )
70 13 14 69 mp3an23 ⊢ ( ( 𝑦 ↑ 2 ) ∈ ℂ → ( ( 3 · ( 𝑦 ↑ 2 ) ) / 3 ) = ( 𝑦 ↑ 2 ) )
71 8 63 70 3syl ⊢ ( 𝑦 ∈ ℝ → ( ( 3 · ( 𝑦 ↑ 2 ) ) / 3 ) = ( 𝑦 ↑ 2 ) )
72 68 71 eqtr3d ⊢ ( 𝑦 ∈ ℝ → ( ( 1 / 3 ) · ( 3 · ( 𝑦 ↑ 2 ) ) ) = ( 𝑦 ↑ 2 ) )
73 72 mpteq2ia ⊢ ( 𝑦 ∈ ℝ ↦ ( ( 1 / 3 ) · ( 3 · ( 𝑦 ↑ 2 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝑦 ↑ 2 ) )
74 29 62 73 3eqtri ⊢ ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ 3 ) / 3 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝑦 ↑ 2 ) )
75 74 a1i ⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ 3 ) / 3 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝑦 ↑ 2 ) ) )
76 19 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → ( 3 · 𝑦 ) ∈ ℂ )
77 3ex ⊢ 3 ∈ V
78 77 a1i ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → 3 ∈ V )
79 8 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
80 1red ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℝ )
81 7 dvmptid ⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℝ ↦ 1 ) )
82 13 a1i ⊢ ( ⊤ → 3 ∈ ℂ )
83 7 79 80 81 82 dvmptcmul ⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 3 · 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 3 · 1 ) ) )
84 3t1e3 ⊢ ( 3 · 1 ) = 3
85 84 mpteq2i ⊢ ( 𝑦 ∈ ℝ ↦ ( 3 · 1 ) ) = ( 𝑦 ∈ ℝ ↦ 3 )
86 83 85 eqtrdi ⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 3 · 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ 3 ) )
87 7 23 24 75 76 78 86 dvmptsub ⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) )
88 1re ⊢ 1 ∈ ℝ
89 iccssre ⊢ ( ( 1 ∈ ℝ ∧ 2 ∈ ℝ ) → ( 1 [,] 2 ) ⊆ ℝ )
90 88 2 89 mp2an ⊢ ( 1 [,] 2 ) ⊆ ℝ
91 90 a1i ⊢ ( ⊤ → ( 1 [,] 2 ) ⊆ ℝ )
92 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
93 92 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
94 iccntr ⊢ ( ( 1 ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 1 [,] 2 ) ) = ( 1 (,) 2 ) )
95 88 2 94 mp2an ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 1 [,] 2 ) ) = ( 1 (,) 2 )
96 95 a1i ⊢ ( ⊤ → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 1 [,] 2 ) ) = ( 1 (,) 2 ) )
97 7 21 22 87 91 93 92 96 dvmptres2 ⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 1 (,) 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) )
98 ioossicc ⊢ ( 1 (,) 2 ) ⊆ ( 1 [,] 2 )
99 resmpt ⊢ ( ( 1 (,) 2 ) ⊆ ( 1 [,] 2 ) → ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ↾ ( 1 (,) 2 ) ) = ( 𝑦 ∈ ( 1 (,) 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) )
100 98 99 ax-mp ⊢ ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ↾ ( 1 (,) 2 ) ) = ( 𝑦 ∈ ( 1 (,) 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) )
101 90 35 sstri ⊢ ( 1 [,] 2 ) ⊆ ℂ
102 resmpt ⊢ ( ( 1 [,] 2 ) ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ↾ ( 1 [,] 2 ) ) = ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) )
103 101 102 ax-mp ⊢ ( ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ↾ ( 1 [,] 2 ) ) = ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) )
104 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) )
105 subcl ⊢ ( ( ( 𝑦 ↑ 2 ) ∈ ℂ ∧ 3 ∈ ℂ ) → ( ( 𝑦 ↑ 2 ) − 3 ) ∈ ℂ )
106 13 105 mpan2 ⊢ ( ( 𝑦 ↑ 2 ) ∈ ℂ → ( ( 𝑦 ↑ 2 ) − 3 ) ∈ ℂ )
107 63 106 syl ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 ↑ 2 ) − 3 ) ∈ ℂ )
108 104 107 fmpti ⊢ ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) : ℂ ⟶ ℂ
109 34 108 34 3pm3.2i ⊢ ( ℂ ⊆ ℂ ∧ ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) : ℂ ⟶ ℂ ∧ ℂ ⊆ ℂ )
110 ovex ⊢ ( ( 2 · ( 𝑦 ↑ ( 2 − 1 ) ) ) − 0 ) ∈ V
111 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
112 111 a1i ⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } )
113 63 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ 2 ) ∈ ℂ )
114 ovexd ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℂ ) → ( 2 · ( 𝑦 ↑ ( 2 − 1 ) ) ) ∈ V )
115 2nn ⊢ 2 ∈ ℕ
116 dvexp ⊢ ( 2 ∈ ℕ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 2 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 2 · ( 𝑦 ↑ ( 2 − 1 ) ) ) ) )
117 115 116 ax-mp ⊢ ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 2 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 2 · ( 𝑦 ↑ ( 2 − 1 ) ) ) )
118 117 a1i ⊢ ( ⊤ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 2 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 2 · ( 𝑦 ↑ ( 2 − 1 ) ) ) ) )
119 13 a1i ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℂ ) → 3 ∈ ℂ )
120 c0ex ⊢ 0 ∈ V
121 120 a1i ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℂ ) → 0 ∈ V )
122 112 82 dvmptc ⊢ ( ⊤ → ( ℂ D ( 𝑦 ∈ ℂ ↦ 3 ) ) = ( 𝑦 ∈ ℂ ↦ 0 ) )
123 112 113 114 118 119 121 122 dvmptsub ⊢ ( ⊤ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 2 · ( 𝑦 ↑ ( 2 − 1 ) ) ) − 0 ) ) )
124 123 mptru ⊢ ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 2 · ( 𝑦 ↑ ( 2 − 1 ) ) ) − 0 ) )
125 110 124 dmmpti ⊢ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ) = ℂ
126 dvcn ⊢ ( ( ( ℂ ⊆ ℂ ∧ ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) : ℂ ⟶ ℂ ∧ ℂ ⊆ ℂ ) ∧ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ) = ℂ ) → ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ∈ ( ℂ –cn→ ℂ ) )
127 109 125 126 mp2an ⊢ ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ∈ ( ℂ –cn→ ℂ )
128 rescncf ⊢ ( ( 1 [,] 2 ) ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ↾ ( 1 [,] 2 ) ) ∈ ( ( 1 [,] 2 ) –cn→ ℂ ) ) )
129 101 127 128 mp2 ⊢ ( ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ↾ ( 1 [,] 2 ) ) ∈ ( ( 1 [,] 2 ) –cn→ ℂ )
130 103 129 eqeltrri ⊢ ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ∈ ( ( 1 [,] 2 ) –cn→ ℂ )
131 rescncf ⊢ ( ( 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 ⊢ ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ↾ ( 1 (,) 2 ) ) ∈ ( ( 1 (,) 2 ) –cn→ ℂ )
133 100 132 eqeltrri ⊢ ( 𝑦 ∈ ( 1 (,) 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ∈ ( ( 1 (,) 2 ) –cn→ ℂ )
134 97 133 eqeltrdi ⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) ∈ ( ( 1 (,) 2 ) –cn→ ℂ ) )
135 98 a1i ⊢ ( ⊤ → ( 1 (,) 2 ) ⊆ ( 1 [,] 2 ) )
136 ioombl ⊢ ( 1 (,) 2 ) ∈ dom vol
137 136 a1i ⊢ ( ⊤ → ( 1 (,) 2 ) ∈ dom vol )
138 ovexd ⊢ ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,] 2 ) ) → ( ( 𝑦 ↑ 2 ) − 3 ) ∈ V )
139 cniccibl ⊢ ( ( 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ∈ ( ( 1 [,] 2 ) –cn→ ℂ ) ) → ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ∈ 𝐿1 )
140 88 2 130 139 mp3an ⊢ ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ∈ 𝐿1
141 140 a1i ⊢ ( ⊤ → ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ∈ 𝐿1 )
142 135 137 138 141 iblss ⊢ ( ⊤ → ( 𝑦 ∈ ( 1 (,) 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) ) ∈ 𝐿1 )
143 97 142 eqeltrd ⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) ∈ 𝐿1 )
144 resmpt ⊢ ( ( 1 [,] 2 ) ⊆ ℝ → ( ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ↾ ( 1 [,] 2 ) ) = ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) )
145 90 144 ax-mp ⊢ ( ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ↾ ( 1 [,] 2 ) ) = ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) )
146 eqid ⊢ ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) )
147 146 20 fmpti ⊢ ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) : ℝ ⟶ ℂ
148 ssid ⊢ ℝ ⊆ ℝ
149 35 147 148 3pm3.2i ⊢ ( ℝ ⊆ ℂ ∧ ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) : ℝ ⟶ ℂ ∧ ℝ ⊆ ℝ )
150 ovex ⊢ ( ( 𝑦 ↑ 2 ) − 3 ) ∈ V
151 87 mptru ⊢ ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ 2 ) − 3 ) )
152 150 151 dmmpti ⊢ dom ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) = ℝ
153 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) : ℝ ⟶ ℂ ∧ ℝ ⊆ ℝ ) ∧ dom ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) = ℝ ) → ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ∈ ( ℝ –cn→ ℂ ) )
154 149 152 153 mp2an ⊢ ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ∈ ( ℝ –cn→ ℂ )
155 rescncf ⊢ ( ( 1 [,] 2 ) ⊆ ℝ → ( ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ∈ ( ℝ –cn→ ℂ ) → ( ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ↾ ( 1 [,] 2 ) ) ∈ ( ( 1 [,] 2 ) –cn→ ℂ ) ) )
156 90 154 155 mp2 ⊢ ( ( 𝑦 ∈ ℝ ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ↾ ( 1 [,] 2 ) ) ∈ ( ( 1 [,] 2 ) –cn→ ℂ )
157 145 156 eqeltrri ⊢ ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ∈ ( ( 1 [,] 2 ) –cn→ ℂ )
158 157 a1i ⊢ ( ⊤ → ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ∈ ( ( 1 [,] 2 ) –cn→ ℂ ) )
159 1 3 5 134 143 158 ftc2 ⊢ ( ⊤ → ∫ ( 1 (,) 2 ) ( ( ℝ D ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) ‘ 𝑥 ) d 𝑥 = ( ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 2 ) − ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 1 ) ) )
160 159 mptru ⊢ ∫ ( 1 (,) 2 ) ( ( ℝ D ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) ‘ 𝑥 ) d 𝑥 = ( ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 2 ) − ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 1 ) )
161 itgeq2 ⊢ ( ∀ 𝑥 ∈ ( 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 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ↑ 2 ) = ( 𝑥 ↑ 2 ) )
163 162 oveq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ↑ 2 ) − 3 ) = ( ( 𝑥 ↑ 2 ) − 3 ) )
164 97 mptru ⊢ ( ℝ D ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 1 (,) 2 ) ↦ ( ( 𝑦 ↑ 2 ) − 3 ) )
165 ovex ⊢ ( ( 𝑥 ↑ 2 ) − 3 ) ∈ V
166 163 164 165 fvmpt ⊢ ( 𝑥 ∈ ( 1 (,) 2 ) → ( ( ℝ D ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑥 ↑ 2 ) − 3 ) )
167 161 166 mprg ⊢ ∫ ( 1 (,) 2 ) ( ( ℝ D ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( 1 (,) 2 ) ( ( 𝑥 ↑ 2 ) − 3 ) d 𝑥
168 2 leidi ⊢ 2 ≤ 2
169 88 2 elicc2i ⊢ ( 2 ∈ ( 1 [,] 2 ) ↔ ( 2 ∈ ℝ ∧ 1 ≤ 2 ∧ 2 ≤ 2 ) )
170 2 4 168 169 mpbir3an ⊢ 2 ∈ ( 1 [,] 2 )
171 oveq1 ⊢ ( 𝑦 = 2 → ( 𝑦 ↑ 3 ) = ( 2 ↑ 3 ) )
172 171 oveq1d ⊢ ( 𝑦 = 2 → ( ( 𝑦 ↑ 3 ) / 3 ) = ( ( 2 ↑ 3 ) / 3 ) )
173 oveq2 ⊢ ( 𝑦 = 2 → ( 3 · 𝑦 ) = ( 3 · 2 ) )
174 172 173 oveq12d ⊢ ( 𝑦 = 2 → ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) = ( ( ( 2 ↑ 3 ) / 3 ) − ( 3 · 2 ) ) )
175 cu2 ⊢ ( 2 ↑ 3 ) = 8
176 175 oveq1i ⊢ ( ( 2 ↑ 3 ) / 3 ) = ( 8 / 3 )
177 3t2e6 ⊢ ( 3 · 2 ) = 6
178 176 177 oveq12i ⊢ ( ( ( 2 ↑ 3 ) / 3 ) − ( 3 · 2 ) ) = ( ( 8 / 3 ) − 6 )
179 2cn ⊢ 2 ∈ ℂ
180 6cn ⊢ 6 ∈ ℂ
181 179 180 13 14 divdiri ⊢ ( ( 2 + 6 ) / 3 ) = ( ( 2 / 3 ) + ( 6 / 3 ) )
182 6p2e8 ⊢ ( 6 + 2 ) = 8
183 180 179 182 addcomli ⊢ ( 2 + 6 ) = 8
184 183 oveq1i ⊢ ( ( 2 + 6 ) / 3 ) = ( 8 / 3 )
185 180 13 179 14 divmuli ⊢ ( ( 6 / 3 ) = 2 ↔ ( 3 · 2 ) = 6 )
186 177 185 mpbir ⊢ ( 6 / 3 ) = 2
187 186 oveq2i ⊢ ( ( 2 / 3 ) + ( 6 / 3 ) ) = ( ( 2 / 3 ) + 2 )
188 181 184 187 3eqtr3i ⊢ ( 8 / 3 ) = ( ( 2 / 3 ) + 2 )
189 188 oveq1i ⊢ ( ( 8 / 3 ) − 6 ) = ( ( ( 2 / 3 ) + 2 ) − 6 )
190 179 13 14 divcli ⊢ ( 2 / 3 ) ∈ ℂ
191 subsub3 ⊢ ( ( ( 2 / 3 ) ∈ ℂ ∧ 6 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 2 / 3 ) − ( 6 − 2 ) ) = ( ( ( 2 / 3 ) + 2 ) − 6 ) )
192 190 180 179 191 mp3an ⊢ ( ( 2 / 3 ) − ( 6 − 2 ) ) = ( ( ( 2 / 3 ) + 2 ) − 6 )
193 189 192 eqtr4i ⊢ ( ( 8 / 3 ) − 6 ) = ( ( 2 / 3 ) − ( 6 − 2 ) )
194 4cn ⊢ 4 ∈ ℂ
195 4p2e6 ⊢ ( 4 + 2 ) = 6
196 194 179 195 addcomli ⊢ ( 2 + 4 ) = 6
197 180 179 194 196 subaddrii ⊢ ( 6 − 2 ) = 4
198 197 oveq2i ⊢ ( ( 2 / 3 ) − ( 6 − 2 ) ) = ( ( 2 / 3 ) − 4 )
199 178 193 198 3eqtri ⊢ ( ( ( 2 ↑ 3 ) / 3 ) − ( 3 · 2 ) ) = ( ( 2 / 3 ) − 4 )
200 174 199 eqtrdi ⊢ ( 𝑦 = 2 → ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) = ( ( 2 / 3 ) − 4 ) )
201 eqid ⊢ ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) )
202 ovex ⊢ ( ( 2 / 3 ) − 4 ) ∈ V
203 200 201 202 fvmpt ⊢ ( 2 ∈ ( 1 [,] 2 ) → ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 2 ) = ( ( 2 / 3 ) − 4 ) )
204 170 203 ax-mp ⊢ ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 2 ) = ( ( 2 / 3 ) − 4 )
205 88 leidi ⊢ 1 ≤ 1
206 88 2 elicc2i ⊢ ( 1 ∈ ( 1 [,] 2 ) ↔ ( 1 ∈ ℝ ∧ 1 ≤ 1 ∧ 1 ≤ 2 ) )
207 88 205 4 206 mpbir3an ⊢ 1 ∈ ( 1 [,] 2 )
208 oveq1 ⊢ ( 𝑦 = 1 → ( 𝑦 ↑ 3 ) = ( 1 ↑ 3 ) )
209 208 oveq1d ⊢ ( 𝑦 = 1 → ( ( 𝑦 ↑ 3 ) / 3 ) = ( ( 1 ↑ 3 ) / 3 ) )
210 oveq2 ⊢ ( 𝑦 = 1 → ( 3 · 𝑦 ) = ( 3 · 1 ) )
211 209 210 oveq12d ⊢ ( 𝑦 = 1 → ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) = ( ( ( 1 ↑ 3 ) / 3 ) − ( 3 · 1 ) ) )
212 3z ⊢ 3 ∈ ℤ
213 1exp ⊢ ( 3 ∈ ℤ → ( 1 ↑ 3 ) = 1 )
214 212 213 ax-mp ⊢ ( 1 ↑ 3 ) = 1
215 214 oveq1i ⊢ ( ( 1 ↑ 3 ) / 3 ) = ( 1 / 3 )
216 215 84 oveq12i ⊢ ( ( ( 1 ↑ 3 ) / 3 ) − ( 3 · 1 ) ) = ( ( 1 / 3 ) − 3 )
217 211 216 eqtrdi ⊢ ( 𝑦 = 1 → ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) = ( ( 1 / 3 ) − 3 ) )
218 ovex ⊢ ( ( 1 / 3 ) − 3 ) ∈ V
219 217 201 218 fvmpt ⊢ ( 1 ∈ ( 1 [,] 2 ) → ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 1 ) = ( ( 1 / 3 ) − 3 ) )
220 207 219 ax-mp ⊢ ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 1 ) = ( ( 1 / 3 ) − 3 )
221 204 220 oveq12i ⊢ ( ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 2 ) − ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 1 ) ) = ( ( ( 2 / 3 ) − 4 ) − ( ( 1 / 3 ) − 3 ) )
222 sub4 ⊢ ( ( ( ( 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 ⊢ ( ( ( 2 / 3 ) − 4 ) − ( ( 1 / 3 ) − 3 ) ) = ( ( ( 2 / 3 ) − ( 1 / 3 ) ) − ( 4 − 3 ) )
224 13 14 pm3.2i ⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 )
225 divsubdir ⊢ ( ( 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 2 − 1 ) / 3 ) = ( ( 2 / 3 ) − ( 1 / 3 ) ) )
226 179 58 224 225 mp3an ⊢ ( ( 2 − 1 ) / 3 ) = ( ( 2 / 3 ) − ( 1 / 3 ) )
227 2m1e1 ⊢ ( 2 − 1 ) = 1
228 227 oveq1i ⊢ ( ( 2 − 1 ) / 3 ) = ( 1 / 3 )
229 226 228 eqtr3i ⊢ ( ( 2 / 3 ) − ( 1 / 3 ) ) = ( 1 / 3 )
230 3p1e4 ⊢ ( 3 + 1 ) = 4
231 194 13 58 230 subaddrii ⊢ ( 4 − 3 ) = 1
232 229 231 oveq12i ⊢ ( ( ( 2 / 3 ) − ( 1 / 3 ) ) − ( 4 − 3 ) ) = ( ( 1 / 3 ) − 1 )
233 221 223 232 3eqtri ⊢ ( ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 2 ) − ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 1 ) ) = ( ( 1 / 3 ) − 1 )
234 13 14 dividi ⊢ ( 3 / 3 ) = 1
235 234 oveq2i ⊢ ( ( 1 / 3 ) − ( 3 / 3 ) ) = ( ( 1 / 3 ) − 1 )
236 233 235 eqtr4i ⊢ ( ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 2 ) − ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 1 ) ) = ( ( 1 / 3 ) − ( 3 / 3 ) )
237 divsubdir ⊢ ( ( 1 ∈ ℂ ∧ 3 ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 1 − 3 ) / 3 ) = ( ( 1 / 3 ) − ( 3 / 3 ) ) )
238 58 13 224 237 mp3an ⊢ ( ( 1 − 3 ) / 3 ) = ( ( 1 / 3 ) − ( 3 / 3 ) )
239 236 238 eqtr4i ⊢ ( ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 2 ) − ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 1 ) ) = ( ( 1 − 3 ) / 3 )
240 divneg ⊢ ( ( 2 ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → - ( 2 / 3 ) = ( - 2 / 3 ) )
241 179 13 14 240 mp3an ⊢ - ( 2 / 3 ) = ( - 2 / 3 )
242 13 58 negsubdi2i ⊢ - ( 3 − 1 ) = ( 1 − 3 )
243 40 negeqi ⊢ - ( 3 − 1 ) = - 2
244 242 243 eqtr3i ⊢ ( 1 − 3 ) = - 2
245 244 oveq1i ⊢ ( ( 1 − 3 ) / 3 ) = ( - 2 / 3 )
246 241 245 eqtr4i ⊢ - ( 2 / 3 ) = ( ( 1 − 3 ) / 3 )
247 239 246 eqtr4i ⊢ ( ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 2 ) − ( ( 𝑦 ∈ ( 1 [,] 2 ) ↦ ( ( ( 𝑦 ↑ 3 ) / 3 ) − ( 3 · 𝑦 ) ) ) ‘ 1 ) ) = - ( 2 / 3 )
248 160 167 247 3eqtr3i ⊢ ∫ ( 1 (,) 2 ) ( ( 𝑥 ↑ 2 ) − 3 ) d 𝑥 = - ( 2 / 3 )