Users' Mathboxes Mathbox for Steve Rodriguez < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lhe4.4ex1a Structured version   Visualization version   GIF version

Theorem lhe4.4ex1a 43170
Description: Example of the Fundamental Theorem of Calculus, part two (ftc2 25568): ∫(1(,)2)((π‘₯↑2) βˆ’ 3) dπ‘₯ = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 25568 as simply the "Fundamental Theorem of Calculus", then ftc1 25566 as the "Second Fundamental Theorem of Calculus".) (Contributed by Steve Rodriguez, 28-Oct-2015.) (Revised by Steve Rodriguez, 31-Oct-2015.)
Assertion
Ref Expression
lhe4.4ex1a ∫(1(,)2)((π‘₯↑2) βˆ’ 3) dπ‘₯ = -(2 / 3)

Proof of Theorem lhe4.4ex1a
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 1red 11217 . . . 4 (⊀ β†’ 1 ∈ ℝ)
2 2re 12288 . . . . 5 2 ∈ ℝ
32a1i 11 . . . 4 (⊀ β†’ 2 ∈ ℝ)
4 1le2 12423 . . . . 5 1 ≀ 2
54a1i 11 . . . 4 (⊀ β†’ 1 ≀ 2)
6 reelprrecn 11204 . . . . . . 7 ℝ ∈ {ℝ, β„‚}
76a1i 11 . . . . . 6 (⊀ β†’ ℝ ∈ {ℝ, β„‚})
8 recn 11202 . . . . . . . . . 10 (𝑦 ∈ ℝ β†’ 𝑦 ∈ β„‚)
9 3nn0 12492 . . . . . . . . . . 11 3 ∈ β„•0
10 expcl 14047 . . . . . . . . . . 11 ((𝑦 ∈ β„‚ ∧ 3 ∈ β„•0) β†’ (𝑦↑3) ∈ β„‚)
119, 10mpan2 689 . . . . . . . . . 10 (𝑦 ∈ β„‚ β†’ (𝑦↑3) ∈ β„‚)
128, 11syl 17 . . . . . . . . 9 (𝑦 ∈ ℝ β†’ (𝑦↑3) ∈ β„‚)
13 3cn 12295 . . . . . . . . . 10 3 ∈ β„‚
14 3ne0 12320 . . . . . . . . . 10 3 β‰  0
15 divcl 11880 . . . . . . . . . 10 (((𝑦↑3) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((𝑦↑3) / 3) ∈ β„‚)
1613, 14, 15mp3an23 1453 . . . . . . . . 9 ((𝑦↑3) ∈ β„‚ β†’ ((𝑦↑3) / 3) ∈ β„‚)
1712, 16syl 17 . . . . . . . 8 (𝑦 ∈ ℝ β†’ ((𝑦↑3) / 3) ∈ β„‚)
18 mulcl 11196 . . . . . . . . 9 ((3 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (3 Β· 𝑦) ∈ β„‚)
1913, 8, 18sylancr 587 . . . . . . . 8 (𝑦 ∈ ℝ β†’ (3 Β· 𝑦) ∈ β„‚)
2017, 19subcld 11573 . . . . . . 7 (𝑦 ∈ ℝ β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) ∈ β„‚)
2120adantl 482 . . . . . 6 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) ∈ β„‚)
22 ovexd 7446 . . . . . 6 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ ((𝑦↑2) βˆ’ 3) ∈ V)
2317adantl 482 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ ((𝑦↑3) / 3) ∈ β„‚)
24 ovexd 7446 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (𝑦↑2) ∈ V)
25 divrec2 11891 . . . . . . . . . . . . 13 (((𝑦↑3) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((𝑦↑3) / 3) = ((1 / 3) Β· (𝑦↑3)))
2613, 14, 25mp3an23 1453 . . . . . . . . . . . 12 ((𝑦↑3) ∈ β„‚ β†’ ((𝑦↑3) / 3) = ((1 / 3) Β· (𝑦↑3)))
2712, 26syl 17 . . . . . . . . . . 11 (𝑦 ∈ ℝ β†’ ((𝑦↑3) / 3) = ((1 / 3) Β· (𝑦↑3)))
2827mpteq2ia 5251 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3)) = (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3)))
2928oveq2i 7422 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3))))
3012adantl 482 . . . . . . . . . . 11 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (𝑦↑3) ∈ β„‚)
31 ovexd 7446 . . . . . . . . . . 11 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (3 Β· (𝑦↑2)) ∈ V)
32 eqid 2732 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„‚ ↦ (𝑦↑3)) = (𝑦 ∈ β„‚ ↦ (𝑦↑3))
3332, 11fmpti 7113 . . . . . . . . . . . . . 14 (𝑦 ∈ β„‚ ↦ (𝑦↑3)):β„‚βŸΆβ„‚
34 ssid 4004 . . . . . . . . . . . . . 14 β„‚ βŠ† β„‚
35 ax-resscn 11169 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
36 ovex 7444 . . . . . . . . . . . . . . . 16 (3 Β· (𝑦↑2)) ∈ V
37 3nn 12293 . . . . . . . . . . . . . . . . . 18 3 ∈ β„•
38 dvexp 25477 . . . . . . . . . . . . . . . . . 18 (3 ∈ β„• β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑(3 βˆ’ 1)))))
3937, 38ax-mp 5 . . . . . . . . . . . . . . . . 17 (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑(3 βˆ’ 1))))
40 3m1e2 12342 . . . . . . . . . . . . . . . . . . . 20 (3 βˆ’ 1) = 2
4140oveq2i 7422 . . . . . . . . . . . . . . . . . . 19 (𝑦↑(3 βˆ’ 1)) = (𝑦↑2)
4241oveq2i 7422 . . . . . . . . . . . . . . . . . 18 (3 Β· (𝑦↑(3 βˆ’ 1))) = (3 Β· (𝑦↑2))
4342mpteq2i 5253 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑(3 βˆ’ 1)))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2)))
4439, 43eqtri 2760 . . . . . . . . . . . . . . . 16 (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2)))
4536, 44dmmpti 6694 . . . . . . . . . . . . . . 15 dom (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = β„‚
4635, 45sseqtrri 4019 . . . . . . . . . . . . . 14 ℝ βŠ† dom (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3)))
47 dvres3 25437 . . . . . . . . . . . . . 14 (((ℝ ∈ {ℝ, β„‚} ∧ (𝑦 ∈ β„‚ ↦ (𝑦↑3)):β„‚βŸΆβ„‚) ∧ (β„‚ βŠ† β„‚ ∧ ℝ βŠ† dom (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))))) β†’ (ℝ D ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ)) = ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ))
486, 33, 34, 46, 47mp4an 691 . . . . . . . . . . . . 13 (ℝ D ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ)) = ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ)
49 resmpt 6037 . . . . . . . . . . . . . . 15 (ℝ βŠ† β„‚ β†’ ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3)))
5035, 49ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3))
5150oveq2i 7422 . . . . . . . . . . . . 13 (ℝ D ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3)))
5244reseq1i 5977 . . . . . . . . . . . . . 14 ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ) = ((𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2))) β†Ύ ℝ)
53 resmpt 6037 . . . . . . . . . . . . . . 15 (ℝ βŠ† β„‚ β†’ ((𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2))) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2))))
5435, 53ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2))) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2)))
5552, 54eqtri 2760 . . . . . . . . . . . . 13 ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2)))
5648, 51, 553eqtr3i 2768 . . . . . . . . . . . 12 (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2)))
5756a1i 11 . . . . . . . . . . 11 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2))))
58 ax-1cn 11170 . . . . . . . . . . . . 13 1 ∈ β„‚
5958, 13, 14divcli 11958 . . . . . . . . . . . 12 (1 / 3) ∈ β„‚
6059a1i 11 . . . . . . . . . . 11 (⊀ β†’ (1 / 3) ∈ β„‚)
617, 30, 31, 57, 60dvmptcmul 25488 . . . . . . . . . 10 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (3 Β· (𝑦↑2)))))
6261mptru 1548 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (3 Β· (𝑦↑2))))
63 sqcl 14085 . . . . . . . . . . . . 13 (𝑦 ∈ β„‚ β†’ (𝑦↑2) ∈ β„‚)
64 mulcl 11196 . . . . . . . . . . . . 13 ((3 ∈ β„‚ ∧ (𝑦↑2) ∈ β„‚) β†’ (3 Β· (𝑦↑2)) ∈ β„‚)
6513, 63, 64sylancr 587 . . . . . . . . . . . 12 (𝑦 ∈ β„‚ β†’ (3 Β· (𝑦↑2)) ∈ β„‚)
66 divrec2 11891 . . . . . . . . . . . . 13 (((3 Β· (𝑦↑2)) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((3 Β· (𝑦↑2)) / 3) = ((1 / 3) Β· (3 Β· (𝑦↑2))))
6713, 14, 66mp3an23 1453 . . . . . . . . . . . 12 ((3 Β· (𝑦↑2)) ∈ β„‚ β†’ ((3 Β· (𝑦↑2)) / 3) = ((1 / 3) Β· (3 Β· (𝑦↑2))))
688, 65, 673syl 18 . . . . . . . . . . 11 (𝑦 ∈ ℝ β†’ ((3 Β· (𝑦↑2)) / 3) = ((1 / 3) Β· (3 Β· (𝑦↑2))))
69 divcan3 11900 . . . . . . . . . . . . 13 (((𝑦↑2) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((3 Β· (𝑦↑2)) / 3) = (𝑦↑2))
7013, 14, 69mp3an23 1453 . . . . . . . . . . . 12 ((𝑦↑2) ∈ β„‚ β†’ ((3 Β· (𝑦↑2)) / 3) = (𝑦↑2))
718, 63, 703syl 18 . . . . . . . . . . 11 (𝑦 ∈ ℝ β†’ ((3 Β· (𝑦↑2)) / 3) = (𝑦↑2))
7268, 71eqtr3d 2774 . . . . . . . . . 10 (𝑦 ∈ ℝ β†’ ((1 / 3) Β· (3 Β· (𝑦↑2))) = (𝑦↑2))
7372mpteq2ia 5251 . . . . . . . . 9 (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (3 Β· (𝑦↑2)))) = (𝑦 ∈ ℝ ↦ (𝑦↑2))
7429, 62, 733eqtri 2764 . . . . . . . 8 (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (𝑦 ∈ ℝ ↦ (𝑦↑2))
7574a1i 11 . . . . . . 7 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (𝑦 ∈ ℝ ↦ (𝑦↑2)))
7619adantl 482 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (3 Β· 𝑦) ∈ β„‚)
77 3ex 12296 . . . . . . . 8 3 ∈ V
7877a1i 11 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ 3 ∈ V)
798adantl 482 . . . . . . . . 9 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ β„‚)
80 1red 11217 . . . . . . . . 9 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ 1 ∈ ℝ)
817dvmptid 25481 . . . . . . . . 9 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
8213a1i 11 . . . . . . . . 9 (⊀ β†’ 3 ∈ β„‚)
837, 79, 80, 81, 82dvmptcmul 25488 . . . . . . . 8 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (3 Β· 𝑦))) = (𝑦 ∈ ℝ ↦ (3 Β· 1)))
84 3t1e3 12379 . . . . . . . . 9 (3 Β· 1) = 3
8584mpteq2i 5253 . . . . . . . 8 (𝑦 ∈ ℝ ↦ (3 Β· 1)) = (𝑦 ∈ ℝ ↦ 3)
8683, 85eqtrdi 2788 . . . . . . 7 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (3 Β· 𝑦))) = (𝑦 ∈ ℝ ↦ 3))
877, 23, 24, 75, 76, 78, 86dvmptsub 25491 . . . . . 6 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) βˆ’ 3)))
88 1re 11216 . . . . . . . 8 1 ∈ ℝ
89 iccssre 13408 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ) β†’ (1[,]2) βŠ† ℝ)
9088, 2, 89mp2an 690 . . . . . . 7 (1[,]2) βŠ† ℝ
9190a1i 11 . . . . . 6 (⊀ β†’ (1[,]2) βŠ† ℝ)
92 eqid 2732 . . . . . . 7 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
9392tgioo2 24326 . . . . . 6 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
94 iccntr 24344 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ) β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(1[,]2)) = (1(,)2))
9588, 2, 94mp2an 690 . . . . . . 7 ((intβ€˜(topGenβ€˜ran (,)))β€˜(1[,]2)) = (1(,)2)
9695a1i 11 . . . . . 6 (⊀ β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(1[,]2)) = (1(,)2))
977, 21, 22, 87, 91, 93, 92, 96dvmptres2 25486 . . . . 5 (⊀ β†’ (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3)))
98 ioossicc 13412 . . . . . . 7 (1(,)2) βŠ† (1[,]2)
99 resmpt 6037 . . . . . . 7 ((1(,)2) βŠ† (1[,]2) β†’ ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) β†Ύ (1(,)2)) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3)))
10098, 99ax-mp 5 . . . . . 6 ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) β†Ύ (1(,)2)) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3))
10190, 35sstri 3991 . . . . . . . . 9 (1[,]2) βŠ† β„‚
102 resmpt 6037 . . . . . . . . 9 ((1[,]2) βŠ† β„‚ β†’ ((𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) β†Ύ (1[,]2)) = (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)))
103101, 102ax-mp 5 . . . . . . . 8 ((𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) β†Ύ (1[,]2)) = (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3))
104 eqid 2732 . . . . . . . . . . . 12 (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) = (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))
105 subcl 11461 . . . . . . . . . . . . . 14 (((𝑦↑2) ∈ β„‚ ∧ 3 ∈ β„‚) β†’ ((𝑦↑2) βˆ’ 3) ∈ β„‚)
10613, 105mpan2 689 . . . . . . . . . . . . 13 ((𝑦↑2) ∈ β„‚ β†’ ((𝑦↑2) βˆ’ 3) ∈ β„‚)
10763, 106syl 17 . . . . . . . . . . . 12 (𝑦 ∈ β„‚ β†’ ((𝑦↑2) βˆ’ 3) ∈ β„‚)
108104, 107fmpti 7113 . . . . . . . . . . 11 (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)):β„‚βŸΆβ„‚
10934, 108, 343pm3.2i 1339 . . . . . . . . . 10 (β„‚ βŠ† β„‚ ∧ (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)):β„‚βŸΆβ„‚ ∧ β„‚ βŠ† β„‚)
110 ovex 7444 . . . . . . . . . . 11 ((2 Β· (𝑦↑(2 βˆ’ 1))) βˆ’ 0) ∈ V
111 cnelprrecn 11205 . . . . . . . . . . . . . 14 β„‚ ∈ {ℝ, β„‚}
112111a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ β„‚ ∈ {ℝ, β„‚})
11363adantl 482 . . . . . . . . . . . . 13 ((⊀ ∧ 𝑦 ∈ β„‚) β†’ (𝑦↑2) ∈ β„‚)
114 ovexd 7446 . . . . . . . . . . . . 13 ((⊀ ∧ 𝑦 ∈ β„‚) β†’ (2 Β· (𝑦↑(2 βˆ’ 1))) ∈ V)
115 2nn 12287 . . . . . . . . . . . . . . 15 2 ∈ β„•
116 dvexp 25477 . . . . . . . . . . . . . . 15 (2 ∈ β„• β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑2))) = (𝑦 ∈ β„‚ ↦ (2 Β· (𝑦↑(2 βˆ’ 1)))))
117115, 116ax-mp 5 . . . . . . . . . . . . . 14 (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑2))) = (𝑦 ∈ β„‚ ↦ (2 Β· (𝑦↑(2 βˆ’ 1))))
118117a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑2))) = (𝑦 ∈ β„‚ ↦ (2 Β· (𝑦↑(2 βˆ’ 1)))))
11913a1i 11 . . . . . . . . . . . . 13 ((⊀ ∧ 𝑦 ∈ β„‚) β†’ 3 ∈ β„‚)
120 c0ex 11210 . . . . . . . . . . . . . 14 0 ∈ V
121120a1i 11 . . . . . . . . . . . . 13 ((⊀ ∧ 𝑦 ∈ β„‚) β†’ 0 ∈ V)
122112, 82dvmptc 25482 . . . . . . . . . . . . 13 (⊀ β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ 3)) = (𝑦 ∈ β„‚ ↦ 0))
123112, 113, 114, 118, 119, 121, 122dvmptsub 25491 . . . . . . . . . . . 12 (⊀ β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = (𝑦 ∈ β„‚ ↦ ((2 Β· (𝑦↑(2 βˆ’ 1))) βˆ’ 0)))
124123mptru 1548 . . . . . . . . . . 11 (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = (𝑦 ∈ β„‚ ↦ ((2 Β· (𝑦↑(2 βˆ’ 1))) βˆ’ 0))
125110, 124dmmpti 6694 . . . . . . . . . 10 dom (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = β„‚
126 dvcn 25445 . . . . . . . . . 10 (((β„‚ βŠ† β„‚ ∧ (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)):β„‚βŸΆβ„‚ ∧ β„‚ βŠ† β„‚) ∧ dom (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = β„‚) β†’ (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) ∈ (ℂ–cnβ†’β„‚))
127109, 125, 126mp2an 690 . . . . . . . . 9 (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) ∈ (ℂ–cnβ†’β„‚)
128 rescncf 24420 . . . . . . . . 9 ((1[,]2) βŠ† β„‚ β†’ ((𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) ∈ (ℂ–cnβ†’β„‚) β†’ ((𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) β†Ύ (1[,]2)) ∈ ((1[,]2)–cnβ†’β„‚)))
129101, 127, 128mp2 9 . . . . . . . 8 ((𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) β†Ύ (1[,]2)) ∈ ((1[,]2)–cnβ†’β„‚)
130103, 129eqeltrri 2830 . . . . . . 7 (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ ((1[,]2)–cnβ†’β„‚)
131 rescncf 24420 . . . . . . 7 ((1(,)2) βŠ† (1[,]2) β†’ ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ ((1[,]2)–cnβ†’β„‚) β†’ ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) β†Ύ (1(,)2)) ∈ ((1(,)2)–cnβ†’β„‚)))
13298, 130, 131mp2 9 . . . . . 6 ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) β†Ύ (1(,)2)) ∈ ((1(,)2)–cnβ†’β„‚)
133100, 132eqeltrri 2830 . . . . 5 (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ ((1(,)2)–cnβ†’β„‚)
13497, 133eqeltrdi 2841 . . . 4 (⊀ β†’ (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) ∈ ((1(,)2)–cnβ†’β„‚))
13598a1i 11 . . . . . 6 (⊀ β†’ (1(,)2) βŠ† (1[,]2))
136 ioombl 25089 . . . . . . 7 (1(,)2) ∈ dom vol
137136a1i 11 . . . . . 6 (⊀ β†’ (1(,)2) ∈ dom vol)
138 ovexd 7446 . . . . . 6 ((⊀ ∧ 𝑦 ∈ (1[,]2)) β†’ ((𝑦↑2) βˆ’ 3) ∈ V)
139 cniccibl 25365 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ ((1[,]2)–cnβ†’β„‚)) β†’ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1)
14088, 2, 130, 139mp3an 1461 . . . . . . 7 (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1
141140a1i 11 . . . . . 6 (⊀ β†’ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1)
142135, 137, 138, 141iblss 25329 . . . . 5 (⊀ β†’ (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1)
14397, 142eqeltrd 2833 . . . 4 (⊀ β†’ (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) ∈ 𝐿1)
144 resmpt 6037 . . . . . . 7 ((1[,]2) βŠ† ℝ β†’ ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) β†Ύ (1[,]2)) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))
14590, 144ax-mp 5 . . . . . 6 ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) β†Ύ (1[,]2)) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))
146 eqid 2732 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) = (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))
147146, 20fmpti 7113 . . . . . . . . 9 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))):β„βŸΆβ„‚
148 ssid 4004 . . . . . . . . 9 ℝ βŠ† ℝ
14935, 147, 1483pm3.2i 1339 . . . . . . . 8 (ℝ βŠ† β„‚ ∧ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))):β„βŸΆβ„‚ ∧ ℝ βŠ† ℝ)
150 ovex 7444 . . . . . . . . 9 ((𝑦↑2) βˆ’ 3) ∈ V
15187mptru 1548 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) βˆ’ 3))
152150, 151dmmpti 6694 . . . . . . . 8 dom (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = ℝ
153 dvcn 25445 . . . . . . . 8 (((ℝ βŠ† β„‚ ∧ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))):β„βŸΆβ„‚ ∧ ℝ βŠ† ℝ) ∧ dom (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = ℝ) β†’ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) ∈ (ℝ–cnβ†’β„‚))
154149, 152, 153mp2an 690 . . . . . . 7 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) ∈ (ℝ–cnβ†’β„‚)
155 rescncf 24420 . . . . . . 7 ((1[,]2) βŠ† ℝ β†’ ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) ∈ (ℝ–cnβ†’β„‚) β†’ ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) β†Ύ (1[,]2)) ∈ ((1[,]2)–cnβ†’β„‚)))
15690, 154, 155mp2 9 . . . . . 6 ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) β†Ύ (1[,]2)) ∈ ((1[,]2)–cnβ†’β„‚)
157145, 156eqeltrri 2830 . . . . 5 (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) ∈ ((1[,]2)–cnβ†’β„‚)
158157a1i 11 . . . 4 (⊀ β†’ (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) ∈ ((1[,]2)–cnβ†’β„‚))
1591, 3, 5, 134, 143, 158ftc2 25568 . . 3 (⊀ β†’ ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) dπ‘₯ = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)))
160159mptru 1548 . 2 ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) dπ‘₯ = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1))
161 itgeq2 25302 . . 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 7418 . . . . 5 (𝑦 = π‘₯ β†’ (𝑦↑2) = (π‘₯↑2))
163162oveq1d 7426 . . . 4 (𝑦 = π‘₯ β†’ ((𝑦↑2) βˆ’ 3) = ((π‘₯↑2) βˆ’ 3))
16497mptru 1548 . . . 4 (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3))
165 ovex 7444 . . . 4 ((π‘₯↑2) βˆ’ 3) ∈ V
166163, 164, 165fvmpt 6998 . . 3 (π‘₯ ∈ (1(,)2) β†’ ((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) = ((π‘₯↑2) βˆ’ 3))
167161, 166mprg 3067 . 2 ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) dπ‘₯ = ∫(1(,)2)((π‘₯↑2) βˆ’ 3) dπ‘₯
1682leidi 11750 . . . . . . . . 9 2 ≀ 2
16988, 2elicc2i 13392 . . . . . . . . 9 (2 ∈ (1[,]2) ↔ (2 ∈ ℝ ∧ 1 ≀ 2 ∧ 2 ≀ 2))
1702, 4, 168, 169mpbir3an 1341 . . . . . . . 8 2 ∈ (1[,]2)
171 oveq1 7418 . . . . . . . . . . . 12 (𝑦 = 2 β†’ (𝑦↑3) = (2↑3))
172171oveq1d 7426 . . . . . . . . . . 11 (𝑦 = 2 β†’ ((𝑦↑3) / 3) = ((2↑3) / 3))
173 oveq2 7419 . . . . . . . . . . 11 (𝑦 = 2 β†’ (3 Β· 𝑦) = (3 Β· 2))
174172, 173oveq12d 7429 . . . . . . . . . 10 (𝑦 = 2 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = (((2↑3) / 3) βˆ’ (3 Β· 2)))
175 cu2 14166 . . . . . . . . . . . . 13 (2↑3) = 8
176175oveq1i 7421 . . . . . . . . . . . 12 ((2↑3) / 3) = (8 / 3)
177 3t2e6 12380 . . . . . . . . . . . 12 (3 Β· 2) = 6
178176, 177oveq12i 7423 . . . . . . . . . . 11 (((2↑3) / 3) βˆ’ (3 Β· 2)) = ((8 / 3) βˆ’ 6)
179 2cn 12289 . . . . . . . . . . . . . . 15 2 ∈ β„‚
180 6cn 12305 . . . . . . . . . . . . . . 15 6 ∈ β„‚
181179, 180, 13, 14divdiri 11973 . . . . . . . . . . . . . 14 ((2 + 6) / 3) = ((2 / 3) + (6 / 3))
182 6p2e8 12373 . . . . . . . . . . . . . . . 16 (6 + 2) = 8
183180, 179, 182addcomli 11408 . . . . . . . . . . . . . . 15 (2 + 6) = 8
184183oveq1i 7421 . . . . . . . . . . . . . 14 ((2 + 6) / 3) = (8 / 3)
185180, 13, 179, 14divmuli 11970 . . . . . . . . . . . . . . . 16 ((6 / 3) = 2 ↔ (3 Β· 2) = 6)
186177, 185mpbir 230 . . . . . . . . . . . . . . 15 (6 / 3) = 2
187186oveq2i 7422 . . . . . . . . . . . . . 14 ((2 / 3) + (6 / 3)) = ((2 / 3) + 2)
188181, 184, 1873eqtr3i 2768 . . . . . . . . . . . . 13 (8 / 3) = ((2 / 3) + 2)
189188oveq1i 7421 . . . . . . . . . . . 12 ((8 / 3) βˆ’ 6) = (((2 / 3) + 2) βˆ’ 6)
190179, 13, 14divcli 11958 . . . . . . . . . . . . 13 (2 / 3) ∈ β„‚
191 subsub3 11494 . . . . . . . . . . . . 13 (((2 / 3) ∈ β„‚ ∧ 6 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((2 / 3) βˆ’ (6 βˆ’ 2)) = (((2 / 3) + 2) βˆ’ 6))
192190, 180, 179, 191mp3an 1461 . . . . . . . . . . . 12 ((2 / 3) βˆ’ (6 βˆ’ 2)) = (((2 / 3) + 2) βˆ’ 6)
193189, 192eqtr4i 2763 . . . . . . . . . . 11 ((8 / 3) βˆ’ 6) = ((2 / 3) βˆ’ (6 βˆ’ 2))
194 4cn 12299 . . . . . . . . . . . . 13 4 ∈ β„‚
195 4p2e6 12367 . . . . . . . . . . . . . 14 (4 + 2) = 6
196194, 179, 195addcomli 11408 . . . . . . . . . . . . 13 (2 + 4) = 6
197180, 179, 194, 196subaddrii 11551 . . . . . . . . . . . 12 (6 βˆ’ 2) = 4
198197oveq2i 7422 . . . . . . . . . . 11 ((2 / 3) βˆ’ (6 βˆ’ 2)) = ((2 / 3) βˆ’ 4)
199178, 193, 1983eqtri 2764 . . . . . . . . . 10 (((2↑3) / 3) βˆ’ (3 Β· 2)) = ((2 / 3) βˆ’ 4)
200174, 199eqtrdi 2788 . . . . . . . . 9 (𝑦 = 2 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = ((2 / 3) βˆ’ 4))
201 eqid 2732 . . . . . . . . 9 (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))
202 ovex 7444 . . . . . . . . 9 ((2 / 3) βˆ’ 4) ∈ V
203200, 201, 202fvmpt 6998 . . . . . . . 8 (2 ∈ (1[,]2) β†’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) = ((2 / 3) βˆ’ 4))
204170, 203ax-mp 5 . . . . . . 7 ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) = ((2 / 3) βˆ’ 4)
20588leidi 11750 . . . . . . . . 9 1 ≀ 1
20688, 2elicc2i 13392 . . . . . . . . 9 (1 ∈ (1[,]2) ↔ (1 ∈ ℝ ∧ 1 ≀ 1 ∧ 1 ≀ 2))
20788, 205, 4, 206mpbir3an 1341 . . . . . . . 8 1 ∈ (1[,]2)
208 oveq1 7418 . . . . . . . . . . . 12 (𝑦 = 1 β†’ (𝑦↑3) = (1↑3))
209208oveq1d 7426 . . . . . . . . . . 11 (𝑦 = 1 β†’ ((𝑦↑3) / 3) = ((1↑3) / 3))
210 oveq2 7419 . . . . . . . . . . 11 (𝑦 = 1 β†’ (3 Β· 𝑦) = (3 Β· 1))
211209, 210oveq12d 7429 . . . . . . . . . 10 (𝑦 = 1 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = (((1↑3) / 3) βˆ’ (3 Β· 1)))
212 3z 12597 . . . . . . . . . . . . 13 3 ∈ β„€
213 1exp 14059 . . . . . . . . . . . . 13 (3 ∈ β„€ β†’ (1↑3) = 1)
214212, 213ax-mp 5 . . . . . . . . . . . 12 (1↑3) = 1
215214oveq1i 7421 . . . . . . . . . . 11 ((1↑3) / 3) = (1 / 3)
216215, 84oveq12i 7423 . . . . . . . . . 10 (((1↑3) / 3) βˆ’ (3 Β· 1)) = ((1 / 3) βˆ’ 3)
217211, 216eqtrdi 2788 . . . . . . . . 9 (𝑦 = 1 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = ((1 / 3) βˆ’ 3))
218 ovex 7444 . . . . . . . . 9 ((1 / 3) βˆ’ 3) ∈ V
219217, 201, 218fvmpt 6998 . . . . . . . 8 (1 ∈ (1[,]2) β†’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1) = ((1 / 3) βˆ’ 3))
220207, 219ax-mp 5 . . . . . . 7 ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1) = ((1 / 3) βˆ’ 3)
221204, 220oveq12i 7423 . . . . . 6 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = (((2 / 3) βˆ’ 4) βˆ’ ((1 / 3) βˆ’ 3))
222 sub4 11507 . . . . . . 7 ((((2 / 3) ∈ β„‚ ∧ 4 ∈ β„‚) ∧ ((1 / 3) ∈ β„‚ ∧ 3 ∈ β„‚)) β†’ (((2 / 3) βˆ’ 4) βˆ’ ((1 / 3) βˆ’ 3)) = (((2 / 3) βˆ’ (1 / 3)) βˆ’ (4 βˆ’ 3)))
223190, 194, 59, 13, 222mp4an 691 . . . . . 6 (((2 / 3) βˆ’ 4) βˆ’ ((1 / 3) βˆ’ 3)) = (((2 / 3) βˆ’ (1 / 3)) βˆ’ (4 βˆ’ 3))
22413, 14pm3.2i 471 . . . . . . . . 9 (3 ∈ β„‚ ∧ 3 β‰  0)
225 divsubdir 11910 . . . . . . . . 9 ((2 ∈ β„‚ ∧ 1 ∈ β„‚ ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((2 βˆ’ 1) / 3) = ((2 / 3) βˆ’ (1 / 3)))
226179, 58, 224, 225mp3an 1461 . . . . . . . 8 ((2 βˆ’ 1) / 3) = ((2 / 3) βˆ’ (1 / 3))
227 2m1e1 12340 . . . . . . . . 9 (2 βˆ’ 1) = 1
228227oveq1i 7421 . . . . . . . 8 ((2 βˆ’ 1) / 3) = (1 / 3)
229226, 228eqtr3i 2762 . . . . . . 7 ((2 / 3) βˆ’ (1 / 3)) = (1 / 3)
230 3p1e4 12359 . . . . . . . 8 (3 + 1) = 4
231194, 13, 58, 230subaddrii 11551 . . . . . . 7 (4 βˆ’ 3) = 1
232229, 231oveq12i 7423 . . . . . 6 (((2 / 3) βˆ’ (1 / 3)) βˆ’ (4 βˆ’ 3)) = ((1 / 3) βˆ’ 1)
233221, 223, 2323eqtri 2764 . . . . 5 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = ((1 / 3) βˆ’ 1)
23413, 14dividi 11949 . . . . . 6 (3 / 3) = 1
235234oveq2i 7422 . . . . 5 ((1 / 3) βˆ’ (3 / 3)) = ((1 / 3) βˆ’ 1)
236233, 235eqtr4i 2763 . . . 4 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = ((1 / 3) βˆ’ (3 / 3))
237 divsubdir 11910 . . . . 5 ((1 ∈ β„‚ ∧ 3 ∈ β„‚ ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((1 βˆ’ 3) / 3) = ((1 / 3) βˆ’ (3 / 3)))
23858, 13, 224, 237mp3an 1461 . . . 4 ((1 βˆ’ 3) / 3) = ((1 / 3) βˆ’ (3 / 3))
239236, 238eqtr4i 2763 . . 3 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = ((1 βˆ’ 3) / 3)
240 divneg 11908 . . . . 5 ((2 ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ -(2 / 3) = (-2 / 3))
241179, 13, 14, 240mp3an 1461 . . . 4 -(2 / 3) = (-2 / 3)
24213, 58negsubdi2i 11548 . . . . . 6 -(3 βˆ’ 1) = (1 βˆ’ 3)
24340negeqi 11455 . . . . . 6 -(3 βˆ’ 1) = -2
244242, 243eqtr3i 2762 . . . . 5 (1 βˆ’ 3) = -2
245244oveq1i 7421 . . . 4 ((1 βˆ’ 3) / 3) = (-2 / 3)
246241, 245eqtr4i 2763 . . 3 -(2 / 3) = ((1 βˆ’ 3) / 3)
247239, 246eqtr4i 2763 . 2 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = -(2 / 3)
248160, 167, 2473eqtr3i 2768 1 ∫(1(,)2)((π‘₯↑2) βˆ’ 3) dπ‘₯ = -(2 / 3)
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βŠ€wtru 1542   ∈ wcel 2106   β‰  wne 2940  Vcvv 3474   βŠ† wss 3948  {cpr 4630   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676  ran crn 5677   β†Ύ cres 5678  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117   ≀ cle 11251   βˆ’ cmin 11446  -cneg 11447   / cdiv 11873  β„•cn 12214  2c2 12269  3c3 12270  4c4 12271  6c6 12273  8c8 12275  β„•0cn0 12474  β„€cz 12560  (,)cioo 13326  [,]cicc 13329  β†‘cexp 14029  TopOpenctopn 17369  topGenctg 17385  β„‚fldccnfld 20950  intcnt 22528  β€“cnβ†’ccncf 24399  volcvol 24987  πΏ1cibl 25141  βˆ«citg 25142   D cdv 25387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cc 10432  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-symdif 4242  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-ofr 7673  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-omul 8473  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-acn 9939  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-z 12561  df-dec 12680  df-uz 12825  df-q 12935  df-rp 12977  df-xneg 13094  df-xadd 13095  df-xmul 13096  df-ioo 13330  df-ioc 13331  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-fl 13759  df-mod 13837  df-seq 13969  df-exp 14030  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-limsup 15417  df-clim 15434  df-rlim 15435  df-sum 15635  df-struct 17082  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-ress 17176  df-plusg 17212  df-mulr 17213  df-starv 17214  df-sca 17215  df-vsca 17216  df-ip 17217  df-tset 17218  df-ple 17219  df-ds 17221  df-unif 17222  df-hom 17223  df-cco 17224  df-rest 17370  df-topn 17371  df-0g 17389  df-gsum 17390  df-topgen 17391  df-pt 17392  df-prds 17395  df-xrs 17450  df-qtop 17455  df-imas 17456  df-xps 17458  df-mre 17532  df-mrc 17533  df-acs 17535  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-submnd 18674  df-mulg 18953  df-cntz 19183  df-cmn 19652  df-psmet 20942  df-xmet 20943  df-met 20944  df-bl 20945  df-mopn 20946  df-fbas 20947  df-fg 20948  df-cnfld 20951  df-top 22403  df-topon 22420  df-topsp 22442  df-bases 22456  df-cld 22530  df-ntr 22531  df-cls 22532  df-nei 22609  df-lp 22647  df-perf 22648  df-cn 22738  df-cnp 22739  df-haus 22826  df-cmp 22898  df-tx 23073  df-hmeo 23266  df-fil 23357  df-fm 23449  df-flim 23450  df-flf 23451  df-xms 23833  df-ms 23834  df-tms 23835  df-cncf 24401  df-ovol 24988  df-vol 24989  df-mbf 25143  df-itg1 25144  df-itg2 25145  df-ibl 25146  df-itg 25147  df-0p 25194  df-limc 25390  df-dv 25391
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator