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 43021
Description: Example of the Fundamental Theorem of Calculus, part two (ftc2 25543): ∫(1(,)2)((π‘₯↑2) βˆ’ 3) dπ‘₯ = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 25543 as simply the "Fundamental Theorem of Calculus", then ftc1 25541 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 11211 . . . 4 (⊀ β†’ 1 ∈ ℝ)
2 2re 12282 . . . . 5 2 ∈ ℝ
32a1i 11 . . . 4 (⊀ β†’ 2 ∈ ℝ)
4 1le2 12417 . . . . 5 1 ≀ 2
54a1i 11 . . . 4 (⊀ β†’ 1 ≀ 2)
6 reelprrecn 11198 . . . . . . 7 ℝ ∈ {ℝ, β„‚}
76a1i 11 . . . . . 6 (⊀ β†’ ℝ ∈ {ℝ, β„‚})
8 recn 11196 . . . . . . . . . 10 (𝑦 ∈ ℝ β†’ 𝑦 ∈ β„‚)
9 3nn0 12486 . . . . . . . . . . 11 3 ∈ β„•0
10 expcl 14041 . . . . . . . . . . 11 ((𝑦 ∈ β„‚ ∧ 3 ∈ β„•0) β†’ (𝑦↑3) ∈ β„‚)
119, 10mpan2 690 . . . . . . . . . 10 (𝑦 ∈ β„‚ β†’ (𝑦↑3) ∈ β„‚)
128, 11syl 17 . . . . . . . . 9 (𝑦 ∈ ℝ β†’ (𝑦↑3) ∈ β„‚)
13 3cn 12289 . . . . . . . . . 10 3 ∈ β„‚
14 3ne0 12314 . . . . . . . . . 10 3 β‰  0
15 divcl 11874 . . . . . . . . . 10 (((𝑦↑3) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((𝑦↑3) / 3) ∈ β„‚)
1613, 14, 15mp3an23 1454 . . . . . . . . 9 ((𝑦↑3) ∈ β„‚ β†’ ((𝑦↑3) / 3) ∈ β„‚)
1712, 16syl 17 . . . . . . . 8 (𝑦 ∈ ℝ β†’ ((𝑦↑3) / 3) ∈ β„‚)
18 mulcl 11190 . . . . . . . . 9 ((3 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (3 Β· 𝑦) ∈ β„‚)
1913, 8, 18sylancr 588 . . . . . . . 8 (𝑦 ∈ ℝ β†’ (3 Β· 𝑦) ∈ β„‚)
2017, 19subcld 11567 . . . . . . 7 (𝑦 ∈ ℝ β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) ∈ β„‚)
2120adantl 483 . . . . . 6 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) ∈ β„‚)
22 ovexd 7439 . . . . . 6 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ ((𝑦↑2) βˆ’ 3) ∈ V)
2317adantl 483 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ ((𝑦↑3) / 3) ∈ β„‚)
24 ovexd 7439 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (𝑦↑2) ∈ V)
25 divrec2 11885 . . . . . . . . . . . . 13 (((𝑦↑3) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((𝑦↑3) / 3) = ((1 / 3) Β· (𝑦↑3)))
2613, 14, 25mp3an23 1454 . . . . . . . . . . . 12 ((𝑦↑3) ∈ β„‚ β†’ ((𝑦↑3) / 3) = ((1 / 3) Β· (𝑦↑3)))
2712, 26syl 17 . . . . . . . . . . 11 (𝑦 ∈ ℝ β†’ ((𝑦↑3) / 3) = ((1 / 3) Β· (𝑦↑3)))
2827mpteq2ia 5250 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3)) = (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3)))
2928oveq2i 7415 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3))))
3012adantl 483 . . . . . . . . . . 11 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (𝑦↑3) ∈ β„‚)
31 ovexd 7439 . . . . . . . . . . 11 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (3 Β· (𝑦↑2)) ∈ V)
32 eqid 2733 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„‚ ↦ (𝑦↑3)) = (𝑦 ∈ β„‚ ↦ (𝑦↑3))
3332, 11fmpti 7107 . . . . . . . . . . . . . 14 (𝑦 ∈ β„‚ ↦ (𝑦↑3)):β„‚βŸΆβ„‚
34 ssid 4003 . . . . . . . . . . . . . 14 β„‚ βŠ† β„‚
35 ax-resscn 11163 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
36 ovex 7437 . . . . . . . . . . . . . . . 16 (3 Β· (𝑦↑2)) ∈ V
37 3nn 12287 . . . . . . . . . . . . . . . . . 18 3 ∈ β„•
38 dvexp 25452 . . . . . . . . . . . . . . . . . 18 (3 ∈ β„• β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑(3 βˆ’ 1)))))
3937, 38ax-mp 5 . . . . . . . . . . . . . . . . 17 (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑(3 βˆ’ 1))))
40 3m1e2 12336 . . . . . . . . . . . . . . . . . . . 20 (3 βˆ’ 1) = 2
4140oveq2i 7415 . . . . . . . . . . . . . . . . . . 19 (𝑦↑(3 βˆ’ 1)) = (𝑦↑2)
4241oveq2i 7415 . . . . . . . . . . . . . . . . . 18 (3 Β· (𝑦↑(3 βˆ’ 1))) = (3 Β· (𝑦↑2))
4342mpteq2i 5252 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑(3 βˆ’ 1)))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2)))
4439, 43eqtri 2761 . . . . . . . . . . . . . . . 16 (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2)))
4536, 44dmmpti 6691 . . . . . . . . . . . . . . 15 dom (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = β„‚
4635, 45sseqtrri 4018 . . . . . . . . . . . . . 14 ℝ βŠ† dom (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3)))
47 dvres3 25412 . . . . . . . . . . . . . 14 (((ℝ ∈ {ℝ, β„‚} ∧ (𝑦 ∈ β„‚ ↦ (𝑦↑3)):β„‚βŸΆβ„‚) ∧ (β„‚ βŠ† β„‚ ∧ ℝ βŠ† dom (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))))) β†’ (ℝ D ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ)) = ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ))
486, 33, 34, 46, 47mp4an 692 . . . . . . . . . . . . 13 (ℝ D ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ)) = ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ)
49 resmpt 6035 . . . . . . . . . . . . . . 15 (ℝ βŠ† β„‚ β†’ ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3)))
5035, 49ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3))
5150oveq2i 7415 . . . . . . . . . . . . 13 (ℝ D ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3)))
5244reseq1i 5975 . . . . . . . . . . . . . 14 ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ) = ((𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2))) β†Ύ ℝ)
53 resmpt 6035 . . . . . . . . . . . . . . 15 (ℝ βŠ† β„‚ β†’ ((𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2))) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2))))
5435, 53ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2))) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2)))
5552, 54eqtri 2761 . . . . . . . . . . . . 13 ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2)))
5648, 51, 553eqtr3i 2769 . . . . . . . . . . . 12 (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2)))
5756a1i 11 . . . . . . . . . . 11 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2))))
58 ax-1cn 11164 . . . . . . . . . . . . 13 1 ∈ β„‚
5958, 13, 14divcli 11952 . . . . . . . . . . . 12 (1 / 3) ∈ β„‚
6059a1i 11 . . . . . . . . . . 11 (⊀ β†’ (1 / 3) ∈ β„‚)
617, 30, 31, 57, 60dvmptcmul 25463 . . . . . . . . . 10 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (3 Β· (𝑦↑2)))))
6261mptru 1549 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (3 Β· (𝑦↑2))))
63 sqcl 14079 . . . . . . . . . . . . 13 (𝑦 ∈ β„‚ β†’ (𝑦↑2) ∈ β„‚)
64 mulcl 11190 . . . . . . . . . . . . 13 ((3 ∈ β„‚ ∧ (𝑦↑2) ∈ β„‚) β†’ (3 Β· (𝑦↑2)) ∈ β„‚)
6513, 63, 64sylancr 588 . . . . . . . . . . . 12 (𝑦 ∈ β„‚ β†’ (3 Β· (𝑦↑2)) ∈ β„‚)
66 divrec2 11885 . . . . . . . . . . . . 13 (((3 Β· (𝑦↑2)) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((3 Β· (𝑦↑2)) / 3) = ((1 / 3) Β· (3 Β· (𝑦↑2))))
6713, 14, 66mp3an23 1454 . . . . . . . . . . . 12 ((3 Β· (𝑦↑2)) ∈ β„‚ β†’ ((3 Β· (𝑦↑2)) / 3) = ((1 / 3) Β· (3 Β· (𝑦↑2))))
688, 65, 673syl 18 . . . . . . . . . . 11 (𝑦 ∈ ℝ β†’ ((3 Β· (𝑦↑2)) / 3) = ((1 / 3) Β· (3 Β· (𝑦↑2))))
69 divcan3 11894 . . . . . . . . . . . . 13 (((𝑦↑2) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((3 Β· (𝑦↑2)) / 3) = (𝑦↑2))
7013, 14, 69mp3an23 1454 . . . . . . . . . . . 12 ((𝑦↑2) ∈ β„‚ β†’ ((3 Β· (𝑦↑2)) / 3) = (𝑦↑2))
718, 63, 703syl 18 . . . . . . . . . . 11 (𝑦 ∈ ℝ β†’ ((3 Β· (𝑦↑2)) / 3) = (𝑦↑2))
7268, 71eqtr3d 2775 . . . . . . . . . 10 (𝑦 ∈ ℝ β†’ ((1 / 3) Β· (3 Β· (𝑦↑2))) = (𝑦↑2))
7372mpteq2ia 5250 . . . . . . . . 9 (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (3 Β· (𝑦↑2)))) = (𝑦 ∈ ℝ ↦ (𝑦↑2))
7429, 62, 733eqtri 2765 . . . . . . . 8 (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (𝑦 ∈ ℝ ↦ (𝑦↑2))
7574a1i 11 . . . . . . 7 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (𝑦 ∈ ℝ ↦ (𝑦↑2)))
7619adantl 483 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (3 Β· 𝑦) ∈ β„‚)
77 3ex 12290 . . . . . . . 8 3 ∈ V
7877a1i 11 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ 3 ∈ V)
798adantl 483 . . . . . . . . 9 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ β„‚)
80 1red 11211 . . . . . . . . 9 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ 1 ∈ ℝ)
817dvmptid 25456 . . . . . . . . 9 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
8213a1i 11 . . . . . . . . 9 (⊀ β†’ 3 ∈ β„‚)
837, 79, 80, 81, 82dvmptcmul 25463 . . . . . . . 8 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (3 Β· 𝑦))) = (𝑦 ∈ ℝ ↦ (3 Β· 1)))
84 3t1e3 12373 . . . . . . . . 9 (3 Β· 1) = 3
8584mpteq2i 5252 . . . . . . . 8 (𝑦 ∈ ℝ ↦ (3 Β· 1)) = (𝑦 ∈ ℝ ↦ 3)
8683, 85eqtrdi 2789 . . . . . . 7 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (3 Β· 𝑦))) = (𝑦 ∈ ℝ ↦ 3))
877, 23, 24, 75, 76, 78, 86dvmptsub 25466 . . . . . 6 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) βˆ’ 3)))
88 1re 11210 . . . . . . . 8 1 ∈ ℝ
89 iccssre 13402 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ) β†’ (1[,]2) βŠ† ℝ)
9088, 2, 89mp2an 691 . . . . . . 7 (1[,]2) βŠ† ℝ
9190a1i 11 . . . . . 6 (⊀ β†’ (1[,]2) βŠ† ℝ)
92 eqid 2733 . . . . . . 7 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
9392tgioo2 24301 . . . . . 6 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
94 iccntr 24319 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ) β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(1[,]2)) = (1(,)2))
9588, 2, 94mp2an 691 . . . . . . 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 25461 . . . . 5 (⊀ β†’ (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3)))
98 ioossicc 13406 . . . . . . 7 (1(,)2) βŠ† (1[,]2)
99 resmpt 6035 . . . . . . 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 3990 . . . . . . . . 9 (1[,]2) βŠ† β„‚
102 resmpt 6035 . . . . . . . . 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 2733 . . . . . . . . . . . 12 (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) = (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))
105 subcl 11455 . . . . . . . . . . . . . 14 (((𝑦↑2) ∈ β„‚ ∧ 3 ∈ β„‚) β†’ ((𝑦↑2) βˆ’ 3) ∈ β„‚)
10613, 105mpan2 690 . . . . . . . . . . . . 13 ((𝑦↑2) ∈ β„‚ β†’ ((𝑦↑2) βˆ’ 3) ∈ β„‚)
10763, 106syl 17 . . . . . . . . . . . 12 (𝑦 ∈ β„‚ β†’ ((𝑦↑2) βˆ’ 3) ∈ β„‚)
108104, 107fmpti 7107 . . . . . . . . . . 11 (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)):β„‚βŸΆβ„‚
10934, 108, 343pm3.2i 1340 . . . . . . . . . 10 (β„‚ βŠ† β„‚ ∧ (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)):β„‚βŸΆβ„‚ ∧ β„‚ βŠ† β„‚)
110 ovex 7437 . . . . . . . . . . 11 ((2 Β· (𝑦↑(2 βˆ’ 1))) βˆ’ 0) ∈ V
111 cnelprrecn 11199 . . . . . . . . . . . . . 14 β„‚ ∈ {ℝ, β„‚}
112111a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ β„‚ ∈ {ℝ, β„‚})
11363adantl 483 . . . . . . . . . . . . 13 ((⊀ ∧ 𝑦 ∈ β„‚) β†’ (𝑦↑2) ∈ β„‚)
114 ovexd 7439 . . . . . . . . . . . . 13 ((⊀ ∧ 𝑦 ∈ β„‚) β†’ (2 Β· (𝑦↑(2 βˆ’ 1))) ∈ V)
115 2nn 12281 . . . . . . . . . . . . . . 15 2 ∈ β„•
116 dvexp 25452 . . . . . . . . . . . . . . 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 11204 . . . . . . . . . . . . . 14 0 ∈ V
121120a1i 11 . . . . . . . . . . . . 13 ((⊀ ∧ 𝑦 ∈ β„‚) β†’ 0 ∈ V)
122112, 82dvmptc 25457 . . . . . . . . . . . . 13 (⊀ β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ 3)) = (𝑦 ∈ β„‚ ↦ 0))
123112, 113, 114, 118, 119, 121, 122dvmptsub 25466 . . . . . . . . . . . 12 (⊀ β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = (𝑦 ∈ β„‚ ↦ ((2 Β· (𝑦↑(2 βˆ’ 1))) βˆ’ 0)))
124123mptru 1549 . . . . . . . . . . 11 (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = (𝑦 ∈ β„‚ ↦ ((2 Β· (𝑦↑(2 βˆ’ 1))) βˆ’ 0))
125110, 124dmmpti 6691 . . . . . . . . . 10 dom (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = β„‚
126 dvcn 25420 . . . . . . . . . 10 (((β„‚ βŠ† β„‚ ∧ (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)):β„‚βŸΆβ„‚ ∧ β„‚ βŠ† β„‚) ∧ dom (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = β„‚) β†’ (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) ∈ (ℂ–cnβ†’β„‚))
127109, 125, 126mp2an 691 . . . . . . . . 9 (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) ∈ (ℂ–cnβ†’β„‚)
128 rescncf 24395 . . . . . . . . 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 2831 . . . . . . 7 (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ ((1[,]2)–cnβ†’β„‚)
131 rescncf 24395 . . . . . . 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 2831 . . . . 5 (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ ((1(,)2)–cnβ†’β„‚)
13497, 133eqeltrdi 2842 . . . 4 (⊀ β†’ (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) ∈ ((1(,)2)–cnβ†’β„‚))
13598a1i 11 . . . . . 6 (⊀ β†’ (1(,)2) βŠ† (1[,]2))
136 ioombl 25064 . . . . . . 7 (1(,)2) ∈ dom vol
137136a1i 11 . . . . . 6 (⊀ β†’ (1(,)2) ∈ dom vol)
138 ovexd 7439 . . . . . 6 ((⊀ ∧ 𝑦 ∈ (1[,]2)) β†’ ((𝑦↑2) βˆ’ 3) ∈ V)
139 cniccibl 25340 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ ((1[,]2)–cnβ†’β„‚)) β†’ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1)
14088, 2, 130, 139mp3an 1462 . . . . . . 7 (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1
141140a1i 11 . . . . . 6 (⊀ β†’ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1)
142135, 137, 138, 141iblss 25304 . . . . 5 (⊀ β†’ (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1)
14397, 142eqeltrd 2834 . . . 4 (⊀ β†’ (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) ∈ 𝐿1)
144 resmpt 6035 . . . . . . 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 2733 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) = (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))
147146, 20fmpti 7107 . . . . . . . . 9 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))):β„βŸΆβ„‚
148 ssid 4003 . . . . . . . . 9 ℝ βŠ† ℝ
14935, 147, 1483pm3.2i 1340 . . . . . . . 8 (ℝ βŠ† β„‚ ∧ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))):β„βŸΆβ„‚ ∧ ℝ βŠ† ℝ)
150 ovex 7437 . . . . . . . . 9 ((𝑦↑2) βˆ’ 3) ∈ V
15187mptru 1549 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) βˆ’ 3))
152150, 151dmmpti 6691 . . . . . . . 8 dom (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = ℝ
153 dvcn 25420 . . . . . . . 8 (((ℝ βŠ† β„‚ ∧ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))):β„βŸΆβ„‚ ∧ ℝ βŠ† ℝ) ∧ dom (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = ℝ) β†’ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) ∈ (ℝ–cnβ†’β„‚))
154149, 152, 153mp2an 691 . . . . . . 7 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) ∈ (ℝ–cnβ†’β„‚)
155 rescncf 24395 . . . . . . 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 2831 . . . . 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 25543 . . 3 (⊀ β†’ ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) dπ‘₯ = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)))
160159mptru 1549 . 2 ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) dπ‘₯ = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1))
161 itgeq2 25277 . . 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 7411 . . . . 5 (𝑦 = π‘₯ β†’ (𝑦↑2) = (π‘₯↑2))
163162oveq1d 7419 . . . 4 (𝑦 = π‘₯ β†’ ((𝑦↑2) βˆ’ 3) = ((π‘₯↑2) βˆ’ 3))
16497mptru 1549 . . . 4 (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3))
165 ovex 7437 . . . 4 ((π‘₯↑2) βˆ’ 3) ∈ V
166163, 164, 165fvmpt 6994 . . 3 (π‘₯ ∈ (1(,)2) β†’ ((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) = ((π‘₯↑2) βˆ’ 3))
167161, 166mprg 3068 . 2 ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) dπ‘₯ = ∫(1(,)2)((π‘₯↑2) βˆ’ 3) dπ‘₯
1682leidi 11744 . . . . . . . . 9 2 ≀ 2
16988, 2elicc2i 13386 . . . . . . . . 9 (2 ∈ (1[,]2) ↔ (2 ∈ ℝ ∧ 1 ≀ 2 ∧ 2 ≀ 2))
1702, 4, 168, 169mpbir3an 1342 . . . . . . . 8 2 ∈ (1[,]2)
171 oveq1 7411 . . . . . . . . . . . 12 (𝑦 = 2 β†’ (𝑦↑3) = (2↑3))
172171oveq1d 7419 . . . . . . . . . . 11 (𝑦 = 2 β†’ ((𝑦↑3) / 3) = ((2↑3) / 3))
173 oveq2 7412 . . . . . . . . . . 11 (𝑦 = 2 β†’ (3 Β· 𝑦) = (3 Β· 2))
174172, 173oveq12d 7422 . . . . . . . . . 10 (𝑦 = 2 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = (((2↑3) / 3) βˆ’ (3 Β· 2)))
175 cu2 14160 . . . . . . . . . . . . 13 (2↑3) = 8
176175oveq1i 7414 . . . . . . . . . . . 12 ((2↑3) / 3) = (8 / 3)
177 3t2e6 12374 . . . . . . . . . . . 12 (3 Β· 2) = 6
178176, 177oveq12i 7416 . . . . . . . . . . 11 (((2↑3) / 3) βˆ’ (3 Β· 2)) = ((8 / 3) βˆ’ 6)
179 2cn 12283 . . . . . . . . . . . . . . 15 2 ∈ β„‚
180 6cn 12299 . . . . . . . . . . . . . . 15 6 ∈ β„‚
181179, 180, 13, 14divdiri 11967 . . . . . . . . . . . . . 14 ((2 + 6) / 3) = ((2 / 3) + (6 / 3))
182 6p2e8 12367 . . . . . . . . . . . . . . . 16 (6 + 2) = 8
183180, 179, 182addcomli 11402 . . . . . . . . . . . . . . 15 (2 + 6) = 8
184183oveq1i 7414 . . . . . . . . . . . . . 14 ((2 + 6) / 3) = (8 / 3)
185180, 13, 179, 14divmuli 11964 . . . . . . . . . . . . . . . 16 ((6 / 3) = 2 ↔ (3 Β· 2) = 6)
186177, 185mpbir 230 . . . . . . . . . . . . . . 15 (6 / 3) = 2
187186oveq2i 7415 . . . . . . . . . . . . . 14 ((2 / 3) + (6 / 3)) = ((2 / 3) + 2)
188181, 184, 1873eqtr3i 2769 . . . . . . . . . . . . 13 (8 / 3) = ((2 / 3) + 2)
189188oveq1i 7414 . . . . . . . . . . . 12 ((8 / 3) βˆ’ 6) = (((2 / 3) + 2) βˆ’ 6)
190179, 13, 14divcli 11952 . . . . . . . . . . . . 13 (2 / 3) ∈ β„‚
191 subsub3 11488 . . . . . . . . . . . . 13 (((2 / 3) ∈ β„‚ ∧ 6 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((2 / 3) βˆ’ (6 βˆ’ 2)) = (((2 / 3) + 2) βˆ’ 6))
192190, 180, 179, 191mp3an 1462 . . . . . . . . . . . 12 ((2 / 3) βˆ’ (6 βˆ’ 2)) = (((2 / 3) + 2) βˆ’ 6)
193189, 192eqtr4i 2764 . . . . . . . . . . 11 ((8 / 3) βˆ’ 6) = ((2 / 3) βˆ’ (6 βˆ’ 2))
194 4cn 12293 . . . . . . . . . . . . 13 4 ∈ β„‚
195 4p2e6 12361 . . . . . . . . . . . . . 14 (4 + 2) = 6
196194, 179, 195addcomli 11402 . . . . . . . . . . . . 13 (2 + 4) = 6
197180, 179, 194, 196subaddrii 11545 . . . . . . . . . . . 12 (6 βˆ’ 2) = 4
198197oveq2i 7415 . . . . . . . . . . 11 ((2 / 3) βˆ’ (6 βˆ’ 2)) = ((2 / 3) βˆ’ 4)
199178, 193, 1983eqtri 2765 . . . . . . . . . 10 (((2↑3) / 3) βˆ’ (3 Β· 2)) = ((2 / 3) βˆ’ 4)
200174, 199eqtrdi 2789 . . . . . . . . 9 (𝑦 = 2 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = ((2 / 3) βˆ’ 4))
201 eqid 2733 . . . . . . . . 9 (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))
202 ovex 7437 . . . . . . . . 9 ((2 / 3) βˆ’ 4) ∈ V
203200, 201, 202fvmpt 6994 . . . . . . . 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 11744 . . . . . . . . 9 1 ≀ 1
20688, 2elicc2i 13386 . . . . . . . . 9 (1 ∈ (1[,]2) ↔ (1 ∈ ℝ ∧ 1 ≀ 1 ∧ 1 ≀ 2))
20788, 205, 4, 206mpbir3an 1342 . . . . . . . 8 1 ∈ (1[,]2)
208 oveq1 7411 . . . . . . . . . . . 12 (𝑦 = 1 β†’ (𝑦↑3) = (1↑3))
209208oveq1d 7419 . . . . . . . . . . 11 (𝑦 = 1 β†’ ((𝑦↑3) / 3) = ((1↑3) / 3))
210 oveq2 7412 . . . . . . . . . . 11 (𝑦 = 1 β†’ (3 Β· 𝑦) = (3 Β· 1))
211209, 210oveq12d 7422 . . . . . . . . . 10 (𝑦 = 1 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = (((1↑3) / 3) βˆ’ (3 Β· 1)))
212 3z 12591 . . . . . . . . . . . . 13 3 ∈ β„€
213 1exp 14053 . . . . . . . . . . . . 13 (3 ∈ β„€ β†’ (1↑3) = 1)
214212, 213ax-mp 5 . . . . . . . . . . . 12 (1↑3) = 1
215214oveq1i 7414 . . . . . . . . . . 11 ((1↑3) / 3) = (1 / 3)
216215, 84oveq12i 7416 . . . . . . . . . 10 (((1↑3) / 3) βˆ’ (3 Β· 1)) = ((1 / 3) βˆ’ 3)
217211, 216eqtrdi 2789 . . . . . . . . 9 (𝑦 = 1 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = ((1 / 3) βˆ’ 3))
218 ovex 7437 . . . . . . . . 9 ((1 / 3) βˆ’ 3) ∈ V
219217, 201, 218fvmpt 6994 . . . . . . . 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 7416 . . . . . 6 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = (((2 / 3) βˆ’ 4) βˆ’ ((1 / 3) βˆ’ 3))
222 sub4 11501 . . . . . . 7 ((((2 / 3) ∈ β„‚ ∧ 4 ∈ β„‚) ∧ ((1 / 3) ∈ β„‚ ∧ 3 ∈ β„‚)) β†’ (((2 / 3) βˆ’ 4) βˆ’ ((1 / 3) βˆ’ 3)) = (((2 / 3) βˆ’ (1 / 3)) βˆ’ (4 βˆ’ 3)))
223190, 194, 59, 13, 222mp4an 692 . . . . . 6 (((2 / 3) βˆ’ 4) βˆ’ ((1 / 3) βˆ’ 3)) = (((2 / 3) βˆ’ (1 / 3)) βˆ’ (4 βˆ’ 3))
22413, 14pm3.2i 472 . . . . . . . . 9 (3 ∈ β„‚ ∧ 3 β‰  0)
225 divsubdir 11904 . . . . . . . . 9 ((2 ∈ β„‚ ∧ 1 ∈ β„‚ ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((2 βˆ’ 1) / 3) = ((2 / 3) βˆ’ (1 / 3)))
226179, 58, 224, 225mp3an 1462 . . . . . . . 8 ((2 βˆ’ 1) / 3) = ((2 / 3) βˆ’ (1 / 3))
227 2m1e1 12334 . . . . . . . . 9 (2 βˆ’ 1) = 1
228227oveq1i 7414 . . . . . . . 8 ((2 βˆ’ 1) / 3) = (1 / 3)
229226, 228eqtr3i 2763 . . . . . . 7 ((2 / 3) βˆ’ (1 / 3)) = (1 / 3)
230 3p1e4 12353 . . . . . . . 8 (3 + 1) = 4
231194, 13, 58, 230subaddrii 11545 . . . . . . 7 (4 βˆ’ 3) = 1
232229, 231oveq12i 7416 . . . . . 6 (((2 / 3) βˆ’ (1 / 3)) βˆ’ (4 βˆ’ 3)) = ((1 / 3) βˆ’ 1)
233221, 223, 2323eqtri 2765 . . . . 5 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = ((1 / 3) βˆ’ 1)
23413, 14dividi 11943 . . . . . 6 (3 / 3) = 1
235234oveq2i 7415 . . . . 5 ((1 / 3) βˆ’ (3 / 3)) = ((1 / 3) βˆ’ 1)
236233, 235eqtr4i 2764 . . . 4 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = ((1 / 3) βˆ’ (3 / 3))
237 divsubdir 11904 . . . . 5 ((1 ∈ β„‚ ∧ 3 ∈ β„‚ ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((1 βˆ’ 3) / 3) = ((1 / 3) βˆ’ (3 / 3)))
23858, 13, 224, 237mp3an 1462 . . . 4 ((1 βˆ’ 3) / 3) = ((1 / 3) βˆ’ (3 / 3))
239236, 238eqtr4i 2764 . . 3 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = ((1 βˆ’ 3) / 3)
240 divneg 11902 . . . . 5 ((2 ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ -(2 / 3) = (-2 / 3))
241179, 13, 14, 240mp3an 1462 . . . 4 -(2 / 3) = (-2 / 3)
24213, 58negsubdi2i 11542 . . . . . 6 -(3 βˆ’ 1) = (1 βˆ’ 3)
24340negeqi 11449 . . . . . 6 -(3 βˆ’ 1) = -2
244242, 243eqtr3i 2763 . . . . 5 (1 βˆ’ 3) = -2
245244oveq1i 7414 . . . 4 ((1 βˆ’ 3) / 3) = (-2 / 3)
246241, 245eqtr4i 2764 . . 3 -(2 / 3) = ((1 βˆ’ 3) / 3)
247239, 246eqtr4i 2764 . 2 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = -(2 / 3)
248160, 167, 2473eqtr3i 2769 1 ∫(1(,)2)((π‘₯↑2) βˆ’ 3) dπ‘₯ = -(2 / 3)
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107   β‰  wne 2941  Vcvv 3475   βŠ† wss 3947  {cpr 4629   class class class wbr 5147   ↦ cmpt 5230  dom cdm 5675  ran crn 5676   β†Ύ cres 5677  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7404  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   Β· cmul 11111   ≀ cle 11245   βˆ’ cmin 11440  -cneg 11441   / cdiv 11867  β„•cn 12208  2c2 12263  3c3 12264  4c4 12265  6c6 12267  8c8 12269  β„•0cn0 12468  β„€cz 12554  (,)cioo 13320  [,]cicc 13323  β†‘cexp 14023  TopOpenctopn 17363  topGenctg 17379  β„‚fldccnfld 20929  intcnt 22503  β€“cnβ†’ccncf 24374  volcvol 24962  πΏ1cibl 25116  βˆ«citg 25117   D cdv 25362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632  ax-cc 10426  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-symdif 4241  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-disj 5113  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-ofr 7666  df-om 7851  df-1st 7970  df-2nd 7971  df-supp 8142  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-omul 8466  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-acn 9933  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-submnd 18668  df-mulg 18945  df-cntz 19175  df-cmn 19643  df-psmet 20921  df-xmet 20922  df-met 20923  df-bl 20924  df-mopn 20925  df-fbas 20926  df-fg 20927  df-cnfld 20930  df-top 22378  df-topon 22395  df-topsp 22417  df-bases 22431  df-cld 22505  df-ntr 22506  df-cls 22507  df-nei 22584  df-lp 22622  df-perf 22623  df-cn 22713  df-cnp 22714  df-haus 22801  df-cmp 22873  df-tx 23048  df-hmeo 23241  df-fil 23332  df-fm 23424  df-flim 23425  df-flf 23426  df-xms 23808  df-ms 23809  df-tms 23810  df-cncf 24376  df-ovol 24963  df-vol 24964  df-mbf 25118  df-itg1 25119  df-itg2 25120  df-ibl 25121  df-itg 25122  df-0p 25169  df-limc 25365  df-dv 25366
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator