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 43391
Description: Example of the Fundamental Theorem of Calculus, part two (ftc2 25794): ∫(1(,)2)((π‘₯↑2) βˆ’ 3) dπ‘₯ = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 25794 as simply the "Fundamental Theorem of Calculus", then ftc1 25792 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 11220 . . . 4 (⊀ β†’ 1 ∈ ℝ)
2 2re 12291 . . . . 5 2 ∈ ℝ
32a1i 11 . . . 4 (⊀ β†’ 2 ∈ ℝ)
4 1le2 12426 . . . . 5 1 ≀ 2
54a1i 11 . . . 4 (⊀ β†’ 1 ≀ 2)
6 reelprrecn 11205 . . . . . . 7 ℝ ∈ {ℝ, β„‚}
76a1i 11 . . . . . 6 (⊀ β†’ ℝ ∈ {ℝ, β„‚})
8 recn 11203 . . . . . . . . . 10 (𝑦 ∈ ℝ β†’ 𝑦 ∈ β„‚)
9 3nn0 12495 . . . . . . . . . . 11 3 ∈ β„•0
10 expcl 14050 . . . . . . . . . . 11 ((𝑦 ∈ β„‚ ∧ 3 ∈ β„•0) β†’ (𝑦↑3) ∈ β„‚)
119, 10mpan2 688 . . . . . . . . . 10 (𝑦 ∈ β„‚ β†’ (𝑦↑3) ∈ β„‚)
128, 11syl 17 . . . . . . . . 9 (𝑦 ∈ ℝ β†’ (𝑦↑3) ∈ β„‚)
13 3cn 12298 . . . . . . . . . 10 3 ∈ β„‚
14 3ne0 12323 . . . . . . . . . 10 3 β‰  0
15 divcl 11883 . . . . . . . . . 10 (((𝑦↑3) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((𝑦↑3) / 3) ∈ β„‚)
1613, 14, 15mp3an23 1452 . . . . . . . . 9 ((𝑦↑3) ∈ β„‚ β†’ ((𝑦↑3) / 3) ∈ β„‚)
1712, 16syl 17 . . . . . . . 8 (𝑦 ∈ ℝ β†’ ((𝑦↑3) / 3) ∈ β„‚)
18 mulcl 11197 . . . . . . . . 9 ((3 ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ (3 Β· 𝑦) ∈ β„‚)
1913, 8, 18sylancr 586 . . . . . . . 8 (𝑦 ∈ ℝ β†’ (3 Β· 𝑦) ∈ β„‚)
2017, 19subcld 11576 . . . . . . 7 (𝑦 ∈ ℝ β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) ∈ β„‚)
2120adantl 481 . . . . . 6 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) ∈ β„‚)
22 ovexd 7447 . . . . . 6 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ ((𝑦↑2) βˆ’ 3) ∈ V)
2317adantl 481 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ ((𝑦↑3) / 3) ∈ β„‚)
24 ovexd 7447 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (𝑦↑2) ∈ V)
25 divrec2 11894 . . . . . . . . . . . . 13 (((𝑦↑3) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((𝑦↑3) / 3) = ((1 / 3) Β· (𝑦↑3)))
2613, 14, 25mp3an23 1452 . . . . . . . . . . . 12 ((𝑦↑3) ∈ β„‚ β†’ ((𝑦↑3) / 3) = ((1 / 3) Β· (𝑦↑3)))
2712, 26syl 17 . . . . . . . . . . 11 (𝑦 ∈ ℝ β†’ ((𝑦↑3) / 3) = ((1 / 3) Β· (𝑦↑3)))
2827mpteq2ia 5252 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3)) = (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3)))
2928oveq2i 7423 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3))))
3012adantl 481 . . . . . . . . . . 11 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (𝑦↑3) ∈ β„‚)
31 ovexd 7447 . . . . . . . . . . 11 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (3 Β· (𝑦↑2)) ∈ V)
32 eqid 2731 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„‚ ↦ (𝑦↑3)) = (𝑦 ∈ β„‚ ↦ (𝑦↑3))
3332, 11fmpti 7114 . . . . . . . . . . . . . 14 (𝑦 ∈ β„‚ ↦ (𝑦↑3)):β„‚βŸΆβ„‚
34 ssid 4005 . . . . . . . . . . . . . 14 β„‚ βŠ† β„‚
35 ax-resscn 11170 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
36 ovex 7445 . . . . . . . . . . . . . . . 16 (3 Β· (𝑦↑2)) ∈ V
37 3nn 12296 . . . . . . . . . . . . . . . . . 18 3 ∈ β„•
38 dvexp 25703 . . . . . . . . . . . . . . . . . 18 (3 ∈ β„• β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑(3 βˆ’ 1)))))
3937, 38ax-mp 5 . . . . . . . . . . . . . . . . 17 (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑(3 βˆ’ 1))))
40 3m1e2 12345 . . . . . . . . . . . . . . . . . . . 20 (3 βˆ’ 1) = 2
4140oveq2i 7423 . . . . . . . . . . . . . . . . . . 19 (𝑦↑(3 βˆ’ 1)) = (𝑦↑2)
4241oveq2i 7423 . . . . . . . . . . . . . . . . . 18 (3 Β· (𝑦↑(3 βˆ’ 1))) = (3 Β· (𝑦↑2))
4342mpteq2i 5254 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑(3 βˆ’ 1)))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2)))
4439, 43eqtri 2759 . . . . . . . . . . . . . . . 16 (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = (𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2)))
4536, 44dmmpti 6695 . . . . . . . . . . . . . . 15 dom (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) = β„‚
4635, 45sseqtrri 4020 . . . . . . . . . . . . . 14 ℝ βŠ† dom (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3)))
47 dvres3 25663 . . . . . . . . . . . . . 14 (((ℝ ∈ {ℝ, β„‚} ∧ (𝑦 ∈ β„‚ ↦ (𝑦↑3)):β„‚βŸΆβ„‚) ∧ (β„‚ βŠ† β„‚ ∧ ℝ βŠ† dom (β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))))) β†’ (ℝ D ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ)) = ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ))
486, 33, 34, 46, 47mp4an 690 . . . . . . . . . . . . 13 (ℝ D ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ)) = ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ)
49 resmpt 6038 . . . . . . . . . . . . . . 15 (ℝ βŠ† β„‚ β†’ ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3)))
5035, 49ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3))
5150oveq2i 7423 . . . . . . . . . . . . 13 (ℝ D ((𝑦 ∈ β„‚ ↦ (𝑦↑3)) β†Ύ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3)))
5244reseq1i 5978 . . . . . . . . . . . . . 14 ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ) = ((𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2))) β†Ύ ℝ)
53 resmpt 6038 . . . . . . . . . . . . . . 15 (ℝ βŠ† β„‚ β†’ ((𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2))) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2))))
5435, 53ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ β„‚ ↦ (3 Β· (𝑦↑2))) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2)))
5552, 54eqtri 2759 . . . . . . . . . . . . 13 ((β„‚ D (𝑦 ∈ β„‚ ↦ (𝑦↑3))) β†Ύ ℝ) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2)))
5648, 51, 553eqtr3i 2767 . . . . . . . . . . . 12 (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2)))
5756a1i 11 . . . . . . . . . . 11 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3 Β· (𝑦↑2))))
58 ax-1cn 11171 . . . . . . . . . . . . 13 1 ∈ β„‚
5958, 13, 14divcli 11961 . . . . . . . . . . . 12 (1 / 3) ∈ β„‚
6059a1i 11 . . . . . . . . . . 11 (⊀ β†’ (1 / 3) ∈ β„‚)
617, 30, 31, 57, 60dvmptcmul 25714 . . . . . . . . . 10 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (3 Β· (𝑦↑2)))))
6261mptru 1547 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (3 Β· (𝑦↑2))))
63 sqcl 14088 . . . . . . . . . . . . 13 (𝑦 ∈ β„‚ β†’ (𝑦↑2) ∈ β„‚)
64 mulcl 11197 . . . . . . . . . . . . 13 ((3 ∈ β„‚ ∧ (𝑦↑2) ∈ β„‚) β†’ (3 Β· (𝑦↑2)) ∈ β„‚)
6513, 63, 64sylancr 586 . . . . . . . . . . . 12 (𝑦 ∈ β„‚ β†’ (3 Β· (𝑦↑2)) ∈ β„‚)
66 divrec2 11894 . . . . . . . . . . . . 13 (((3 Β· (𝑦↑2)) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((3 Β· (𝑦↑2)) / 3) = ((1 / 3) Β· (3 Β· (𝑦↑2))))
6713, 14, 66mp3an23 1452 . . . . . . . . . . . 12 ((3 Β· (𝑦↑2)) ∈ β„‚ β†’ ((3 Β· (𝑦↑2)) / 3) = ((1 / 3) Β· (3 Β· (𝑦↑2))))
688, 65, 673syl 18 . . . . . . . . . . 11 (𝑦 ∈ ℝ β†’ ((3 Β· (𝑦↑2)) / 3) = ((1 / 3) Β· (3 Β· (𝑦↑2))))
69 divcan3 11903 . . . . . . . . . . . . 13 (((𝑦↑2) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ ((3 Β· (𝑦↑2)) / 3) = (𝑦↑2))
7013, 14, 69mp3an23 1452 . . . . . . . . . . . 12 ((𝑦↑2) ∈ β„‚ β†’ ((3 Β· (𝑦↑2)) / 3) = (𝑦↑2))
718, 63, 703syl 18 . . . . . . . . . . 11 (𝑦 ∈ ℝ β†’ ((3 Β· (𝑦↑2)) / 3) = (𝑦↑2))
7268, 71eqtr3d 2773 . . . . . . . . . 10 (𝑦 ∈ ℝ β†’ ((1 / 3) Β· (3 Β· (𝑦↑2))) = (𝑦↑2))
7372mpteq2ia 5252 . . . . . . . . 9 (𝑦 ∈ ℝ ↦ ((1 / 3) Β· (3 Β· (𝑦↑2)))) = (𝑦 ∈ ℝ ↦ (𝑦↑2))
7429, 62, 733eqtri 2763 . . . . . . . 8 (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (𝑦 ∈ ℝ ↦ (𝑦↑2))
7574a1i 11 . . . . . . 7 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (𝑦 ∈ ℝ ↦ (𝑦↑2)))
7619adantl 481 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ (3 Β· 𝑦) ∈ β„‚)
77 3ex 12299 . . . . . . . 8 3 ∈ V
7877a1i 11 . . . . . . 7 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ 3 ∈ V)
798adantl 481 . . . . . . . . 9 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ β„‚)
80 1red 11220 . . . . . . . . 9 ((⊀ ∧ 𝑦 ∈ ℝ) β†’ 1 ∈ ℝ)
817dvmptid 25707 . . . . . . . . 9 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
8213a1i 11 . . . . . . . . 9 (⊀ β†’ 3 ∈ β„‚)
837, 79, 80, 81, 82dvmptcmul 25714 . . . . . . . 8 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (3 Β· 𝑦))) = (𝑦 ∈ ℝ ↦ (3 Β· 1)))
84 3t1e3 12382 . . . . . . . . 9 (3 Β· 1) = 3
8584mpteq2i 5254 . . . . . . . 8 (𝑦 ∈ ℝ ↦ (3 Β· 1)) = (𝑦 ∈ ℝ ↦ 3)
8683, 85eqtrdi 2787 . . . . . . 7 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (3 Β· 𝑦))) = (𝑦 ∈ ℝ ↦ 3))
877, 23, 24, 75, 76, 78, 86dvmptsub 25717 . . . . . 6 (⊀ β†’ (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) βˆ’ 3)))
88 1re 11219 . . . . . . . 8 1 ∈ ℝ
89 iccssre 13411 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ) β†’ (1[,]2) βŠ† ℝ)
9088, 2, 89mp2an 689 . . . . . . 7 (1[,]2) βŠ† ℝ
9190a1i 11 . . . . . 6 (⊀ β†’ (1[,]2) βŠ† ℝ)
92 eqid 2731 . . . . . . 7 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
9392tgioo2 24540 . . . . . 6 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
94 iccntr 24558 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ) β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(1[,]2)) = (1(,)2))
9588, 2, 94mp2an 689 . . . . . . 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 25712 . . . . 5 (⊀ β†’ (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3)))
98 ioossicc 13415 . . . . . . 7 (1(,)2) βŠ† (1[,]2)
99 resmpt 6038 . . . . . . 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 3992 . . . . . . . . 9 (1[,]2) βŠ† β„‚
102 resmpt 6038 . . . . . . . . 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 2731 . . . . . . . . . . . 12 (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) = (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))
105 subcl 11464 . . . . . . . . . . . . . 14 (((𝑦↑2) ∈ β„‚ ∧ 3 ∈ β„‚) β†’ ((𝑦↑2) βˆ’ 3) ∈ β„‚)
10613, 105mpan2 688 . . . . . . . . . . . . 13 ((𝑦↑2) ∈ β„‚ β†’ ((𝑦↑2) βˆ’ 3) ∈ β„‚)
10763, 106syl 17 . . . . . . . . . . . 12 (𝑦 ∈ β„‚ β†’ ((𝑦↑2) βˆ’ 3) ∈ β„‚)
108104, 107fmpti 7114 . . . . . . . . . . 11 (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)):β„‚βŸΆβ„‚
10934, 108, 343pm3.2i 1338 . . . . . . . . . 10 (β„‚ βŠ† β„‚ ∧ (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)):β„‚βŸΆβ„‚ ∧ β„‚ βŠ† β„‚)
110 ovex 7445 . . . . . . . . . . 11 ((2 Β· (𝑦↑(2 βˆ’ 1))) βˆ’ 0) ∈ V
111 cnelprrecn 11206 . . . . . . . . . . . . . 14 β„‚ ∈ {ℝ, β„‚}
112111a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ β„‚ ∈ {ℝ, β„‚})
11363adantl 481 . . . . . . . . . . . . 13 ((⊀ ∧ 𝑦 ∈ β„‚) β†’ (𝑦↑2) ∈ β„‚)
114 ovexd 7447 . . . . . . . . . . . . 13 ((⊀ ∧ 𝑦 ∈ β„‚) β†’ (2 Β· (𝑦↑(2 βˆ’ 1))) ∈ V)
115 2nn 12290 . . . . . . . . . . . . . . 15 2 ∈ β„•
116 dvexp 25703 . . . . . . . . . . . . . . 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 11213 . . . . . . . . . . . . . 14 0 ∈ V
121120a1i 11 . . . . . . . . . . . . 13 ((⊀ ∧ 𝑦 ∈ β„‚) β†’ 0 ∈ V)
122112, 82dvmptc 25708 . . . . . . . . . . . . 13 (⊀ β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ 3)) = (𝑦 ∈ β„‚ ↦ 0))
123112, 113, 114, 118, 119, 121, 122dvmptsub 25717 . . . . . . . . . . . 12 (⊀ β†’ (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = (𝑦 ∈ β„‚ ↦ ((2 Β· (𝑦↑(2 βˆ’ 1))) βˆ’ 0)))
124123mptru 1547 . . . . . . . . . . 11 (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = (𝑦 ∈ β„‚ ↦ ((2 Β· (𝑦↑(2 βˆ’ 1))) βˆ’ 0))
125110, 124dmmpti 6695 . . . . . . . . . 10 dom (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = β„‚
126 dvcn 25671 . . . . . . . . . 10 (((β„‚ βŠ† β„‚ ∧ (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)):β„‚βŸΆβ„‚ ∧ β„‚ βŠ† β„‚) ∧ dom (β„‚ D (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3))) = β„‚) β†’ (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) ∈ (ℂ–cnβ†’β„‚))
127109, 125, 126mp2an 689 . . . . . . . . 9 (𝑦 ∈ β„‚ ↦ ((𝑦↑2) βˆ’ 3)) ∈ (ℂ–cnβ†’β„‚)
128 rescncf 24638 . . . . . . . . 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 2829 . . . . . . 7 (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ ((1[,]2)–cnβ†’β„‚)
131 rescncf 24638 . . . . . . 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 2829 . . . . 5 (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ ((1(,)2)–cnβ†’β„‚)
13497, 133eqeltrdi 2840 . . . 4 (⊀ β†’ (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) ∈ ((1(,)2)–cnβ†’β„‚))
13598a1i 11 . . . . . 6 (⊀ β†’ (1(,)2) βŠ† (1[,]2))
136 ioombl 25315 . . . . . . 7 (1(,)2) ∈ dom vol
137136a1i 11 . . . . . 6 (⊀ β†’ (1(,)2) ∈ dom vol)
138 ovexd 7447 . . . . . 6 ((⊀ ∧ 𝑦 ∈ (1[,]2)) β†’ ((𝑦↑2) βˆ’ 3) ∈ V)
139 cniccibl 25591 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ ((1[,]2)–cnβ†’β„‚)) β†’ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1)
14088, 2, 130, 139mp3an 1460 . . . . . . 7 (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1
141140a1i 11 . . . . . 6 (⊀ β†’ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1)
142135, 137, 138, 141iblss 25555 . . . . 5 (⊀ β†’ (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3)) ∈ 𝐿1)
14397, 142eqeltrd 2832 . . . 4 (⊀ β†’ (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) ∈ 𝐿1)
144 resmpt 6038 . . . . . . 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 2731 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) = (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))
147146, 20fmpti 7114 . . . . . . . . 9 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))):β„βŸΆβ„‚
148 ssid 4005 . . . . . . . . 9 ℝ βŠ† ℝ
14935, 147, 1483pm3.2i 1338 . . . . . . . 8 (ℝ βŠ† β„‚ ∧ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))):β„βŸΆβ„‚ ∧ ℝ βŠ† ℝ)
150 ovex 7445 . . . . . . . . 9 ((𝑦↑2) βˆ’ 3) ∈ V
15187mptru 1547 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) βˆ’ 3))
152150, 151dmmpti 6695 . . . . . . . 8 dom (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = ℝ
153 dvcn 25671 . . . . . . . 8 (((ℝ βŠ† β„‚ ∧ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))):β„βŸΆβ„‚ ∧ ℝ βŠ† ℝ) ∧ dom (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = ℝ) β†’ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) ∈ (ℝ–cnβ†’β„‚))
154149, 152, 153mp2an 689 . . . . . . 7 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) ∈ (ℝ–cnβ†’β„‚)
155 rescncf 24638 . . . . . . 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 2829 . . . . 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 25794 . . 3 (⊀ β†’ ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) dπ‘₯ = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)))
160159mptru 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 25528 . . 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 7419 . . . . 5 (𝑦 = π‘₯ β†’ (𝑦↑2) = (π‘₯↑2))
163162oveq1d 7427 . . . 4 (𝑦 = π‘₯ β†’ ((𝑦↑2) βˆ’ 3) = ((π‘₯↑2) βˆ’ 3))
16497mptru 1547 . . . 4 (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) βˆ’ 3))
165 ovex 7445 . . . 4 ((π‘₯↑2) βˆ’ 3) ∈ V
166163, 164, 165fvmpt 6999 . . 3 (π‘₯ ∈ (1(,)2) β†’ ((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) = ((π‘₯↑2) βˆ’ 3))
167161, 166mprg 3066 . 2 ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))))β€˜π‘₯) dπ‘₯ = ∫(1(,)2)((π‘₯↑2) βˆ’ 3) dπ‘₯
1682leidi 11753 . . . . . . . . 9 2 ≀ 2
16988, 2elicc2i 13395 . . . . . . . . 9 (2 ∈ (1[,]2) ↔ (2 ∈ ℝ ∧ 1 ≀ 2 ∧ 2 ≀ 2))
1702, 4, 168, 169mpbir3an 1340 . . . . . . . 8 2 ∈ (1[,]2)
171 oveq1 7419 . . . . . . . . . . . 12 (𝑦 = 2 β†’ (𝑦↑3) = (2↑3))
172171oveq1d 7427 . . . . . . . . . . 11 (𝑦 = 2 β†’ ((𝑦↑3) / 3) = ((2↑3) / 3))
173 oveq2 7420 . . . . . . . . . . 11 (𝑦 = 2 β†’ (3 Β· 𝑦) = (3 Β· 2))
174172, 173oveq12d 7430 . . . . . . . . . 10 (𝑦 = 2 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = (((2↑3) / 3) βˆ’ (3 Β· 2)))
175 cu2 14169 . . . . . . . . . . . . 13 (2↑3) = 8
176175oveq1i 7422 . . . . . . . . . . . 12 ((2↑3) / 3) = (8 / 3)
177 3t2e6 12383 . . . . . . . . . . . 12 (3 Β· 2) = 6
178176, 177oveq12i 7424 . . . . . . . . . . 11 (((2↑3) / 3) βˆ’ (3 Β· 2)) = ((8 / 3) βˆ’ 6)
179 2cn 12292 . . . . . . . . . . . . . . 15 2 ∈ β„‚
180 6cn 12308 . . . . . . . . . . . . . . 15 6 ∈ β„‚
181179, 180, 13, 14divdiri 11976 . . . . . . . . . . . . . 14 ((2 + 6) / 3) = ((2 / 3) + (6 / 3))
182 6p2e8 12376 . . . . . . . . . . . . . . . 16 (6 + 2) = 8
183180, 179, 182addcomli 11411 . . . . . . . . . . . . . . 15 (2 + 6) = 8
184183oveq1i 7422 . . . . . . . . . . . . . 14 ((2 + 6) / 3) = (8 / 3)
185180, 13, 179, 14divmuli 11973 . . . . . . . . . . . . . . . 16 ((6 / 3) = 2 ↔ (3 Β· 2) = 6)
186177, 185mpbir 230 . . . . . . . . . . . . . . 15 (6 / 3) = 2
187186oveq2i 7423 . . . . . . . . . . . . . 14 ((2 / 3) + (6 / 3)) = ((2 / 3) + 2)
188181, 184, 1873eqtr3i 2767 . . . . . . . . . . . . 13 (8 / 3) = ((2 / 3) + 2)
189188oveq1i 7422 . . . . . . . . . . . 12 ((8 / 3) βˆ’ 6) = (((2 / 3) + 2) βˆ’ 6)
190179, 13, 14divcli 11961 . . . . . . . . . . . . 13 (2 / 3) ∈ β„‚
191 subsub3 11497 . . . . . . . . . . . . 13 (((2 / 3) ∈ β„‚ ∧ 6 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((2 / 3) βˆ’ (6 βˆ’ 2)) = (((2 / 3) + 2) βˆ’ 6))
192190, 180, 179, 191mp3an 1460 . . . . . . . . . . . 12 ((2 / 3) βˆ’ (6 βˆ’ 2)) = (((2 / 3) + 2) βˆ’ 6)
193189, 192eqtr4i 2762 . . . . . . . . . . 11 ((8 / 3) βˆ’ 6) = ((2 / 3) βˆ’ (6 βˆ’ 2))
194 4cn 12302 . . . . . . . . . . . . 13 4 ∈ β„‚
195 4p2e6 12370 . . . . . . . . . . . . . 14 (4 + 2) = 6
196194, 179, 195addcomli 11411 . . . . . . . . . . . . 13 (2 + 4) = 6
197180, 179, 194, 196subaddrii 11554 . . . . . . . . . . . 12 (6 βˆ’ 2) = 4
198197oveq2i 7423 . . . . . . . . . . 11 ((2 / 3) βˆ’ (6 βˆ’ 2)) = ((2 / 3) βˆ’ 4)
199178, 193, 1983eqtri 2763 . . . . . . . . . 10 (((2↑3) / 3) βˆ’ (3 Β· 2)) = ((2 / 3) βˆ’ 4)
200174, 199eqtrdi 2787 . . . . . . . . 9 (𝑦 = 2 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = ((2 / 3) βˆ’ 4))
201 eqid 2731 . . . . . . . . 9 (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦))) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))
202 ovex 7445 . . . . . . . . 9 ((2 / 3) βˆ’ 4) ∈ V
203200, 201, 202fvmpt 6999 . . . . . . . 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 11753 . . . . . . . . 9 1 ≀ 1
20688, 2elicc2i 13395 . . . . . . . . 9 (1 ∈ (1[,]2) ↔ (1 ∈ ℝ ∧ 1 ≀ 1 ∧ 1 ≀ 2))
20788, 205, 4, 206mpbir3an 1340 . . . . . . . 8 1 ∈ (1[,]2)
208 oveq1 7419 . . . . . . . . . . . 12 (𝑦 = 1 β†’ (𝑦↑3) = (1↑3))
209208oveq1d 7427 . . . . . . . . . . 11 (𝑦 = 1 β†’ ((𝑦↑3) / 3) = ((1↑3) / 3))
210 oveq2 7420 . . . . . . . . . . 11 (𝑦 = 1 β†’ (3 Β· 𝑦) = (3 Β· 1))
211209, 210oveq12d 7430 . . . . . . . . . 10 (𝑦 = 1 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = (((1↑3) / 3) βˆ’ (3 Β· 1)))
212 3z 12600 . . . . . . . . . . . . 13 3 ∈ β„€
213 1exp 14062 . . . . . . . . . . . . 13 (3 ∈ β„€ β†’ (1↑3) = 1)
214212, 213ax-mp 5 . . . . . . . . . . . 12 (1↑3) = 1
215214oveq1i 7422 . . . . . . . . . . 11 ((1↑3) / 3) = (1 / 3)
216215, 84oveq12i 7424 . . . . . . . . . 10 (((1↑3) / 3) βˆ’ (3 Β· 1)) = ((1 / 3) βˆ’ 3)
217211, 216eqtrdi 2787 . . . . . . . . 9 (𝑦 = 1 β†’ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)) = ((1 / 3) βˆ’ 3))
218 ovex 7445 . . . . . . . . 9 ((1 / 3) βˆ’ 3) ∈ V
219217, 201, 218fvmpt 6999 . . . . . . . 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 7424 . . . . . 6 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = (((2 / 3) βˆ’ 4) βˆ’ ((1 / 3) βˆ’ 3))
222 sub4 11510 . . . . . . 7 ((((2 / 3) ∈ β„‚ ∧ 4 ∈ β„‚) ∧ ((1 / 3) ∈ β„‚ ∧ 3 ∈ β„‚)) β†’ (((2 / 3) βˆ’ 4) βˆ’ ((1 / 3) βˆ’ 3)) = (((2 / 3) βˆ’ (1 / 3)) βˆ’ (4 βˆ’ 3)))
223190, 194, 59, 13, 222mp4an 690 . . . . . 6 (((2 / 3) βˆ’ 4) βˆ’ ((1 / 3) βˆ’ 3)) = (((2 / 3) βˆ’ (1 / 3)) βˆ’ (4 βˆ’ 3))
22413, 14pm3.2i 470 . . . . . . . . 9 (3 ∈ β„‚ ∧ 3 β‰  0)
225 divsubdir 11913 . . . . . . . . 9 ((2 ∈ β„‚ ∧ 1 ∈ β„‚ ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((2 βˆ’ 1) / 3) = ((2 / 3) βˆ’ (1 / 3)))
226179, 58, 224, 225mp3an 1460 . . . . . . . 8 ((2 βˆ’ 1) / 3) = ((2 / 3) βˆ’ (1 / 3))
227 2m1e1 12343 . . . . . . . . 9 (2 βˆ’ 1) = 1
228227oveq1i 7422 . . . . . . . 8 ((2 βˆ’ 1) / 3) = (1 / 3)
229226, 228eqtr3i 2761 . . . . . . 7 ((2 / 3) βˆ’ (1 / 3)) = (1 / 3)
230 3p1e4 12362 . . . . . . . 8 (3 + 1) = 4
231194, 13, 58, 230subaddrii 11554 . . . . . . 7 (4 βˆ’ 3) = 1
232229, 231oveq12i 7424 . . . . . 6 (((2 / 3) βˆ’ (1 / 3)) βˆ’ (4 βˆ’ 3)) = ((1 / 3) βˆ’ 1)
233221, 223, 2323eqtri 2763 . . . . 5 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = ((1 / 3) βˆ’ 1)
23413, 14dividi 11952 . . . . . 6 (3 / 3) = 1
235234oveq2i 7423 . . . . 5 ((1 / 3) βˆ’ (3 / 3)) = ((1 / 3) βˆ’ 1)
236233, 235eqtr4i 2762 . . . 4 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = ((1 / 3) βˆ’ (3 / 3))
237 divsubdir 11913 . . . . 5 ((1 ∈ β„‚ ∧ 3 ∈ β„‚ ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((1 βˆ’ 3) / 3) = ((1 / 3) βˆ’ (3 / 3)))
23858, 13, 224, 237mp3an 1460 . . . 4 ((1 βˆ’ 3) / 3) = ((1 / 3) βˆ’ (3 / 3))
239236, 238eqtr4i 2762 . . 3 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = ((1 βˆ’ 3) / 3)
240 divneg 11911 . . . . 5 ((2 ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ -(2 / 3) = (-2 / 3))
241179, 13, 14, 240mp3an 1460 . . . 4 -(2 / 3) = (-2 / 3)
24213, 58negsubdi2i 11551 . . . . . 6 -(3 βˆ’ 1) = (1 βˆ’ 3)
24340negeqi 11458 . . . . . 6 -(3 βˆ’ 1) = -2
244242, 243eqtr3i 2761 . . . . 5 (1 βˆ’ 3) = -2
245244oveq1i 7422 . . . 4 ((1 βˆ’ 3) / 3) = (-2 / 3)
246241, 245eqtr4i 2762 . . 3 -(2 / 3) = ((1 βˆ’ 3) / 3)
247239, 246eqtr4i 2762 . 2 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜2) βˆ’ ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) βˆ’ (3 Β· 𝑦)))β€˜1)) = -(2 / 3)
248160, 167, 2473eqtr3i 2767 1 ∫(1(,)2)((π‘₯↑2) βˆ’ 3) dπ‘₯ = -(2 / 3)
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 395   ∧ w3a 1086   = wceq 1540  βŠ€wtru 1541   ∈ wcel 2105   β‰  wne 2939  Vcvv 3473   βŠ† wss 3949  {cpr 4631   class class class wbr 5149   ↦ cmpt 5232  dom cdm 5677  ran crn 5678   β†Ύ cres 5679  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7412  β„‚cc 11111  β„cr 11112  0cc0 11113  1c1 11114   + caddc 11116   Β· cmul 11118   ≀ cle 11254   βˆ’ cmin 11449  -cneg 11450   / cdiv 11876  β„•cn 12217  2c2 12272  3c3 12273  4c4 12274  6c6 12276  8c8 12278  β„•0cn0 12477  β„€cz 12563  (,)cioo 13329  [,]cicc 13332  β†‘cexp 14032  TopOpenctopn 17372  topGenctg 17388  β„‚fldccnfld 21145  intcnt 22742  β€“cnβ†’ccncf 24617  volcvol 25213  πΏ1cibl 25367  βˆ«citg 25368   D cdv 25613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-inf2 9639  ax-cc 10433  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190  ax-pre-sup 11191  ax-addf 11192  ax-mulf 11193
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-symdif 4243  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7673  df-ofr 7674  df-om 7859  df-1st 7978  df-2nd 7979  df-supp 8150  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-2o 8470  df-oadd 8473  df-omul 8474  df-er 8706  df-map 8825  df-pm 8826  df-ixp 8895  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-fsupp 9365  df-fi 9409  df-sup 9440  df-inf 9441  df-oi 9508  df-dju 9899  df-card 9937  df-acn 9940  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12478  df-z 12564  df-dec 12683  df-uz 12828  df-q 12938  df-rp 12980  df-xneg 13097  df-xadd 13098  df-xmul 13099  df-ioo 13333  df-ioc 13334  df-ico 13335  df-icc 13336  df-fz 13490  df-fzo 13633  df-fl 13762  df-mod 13840  df-seq 13972  df-exp 14033  df-hash 14296  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188  df-limsup 15420  df-clim 15437  df-rlim 15438  df-sum 15638  df-struct 17085  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179  df-plusg 17215  df-mulr 17216  df-starv 17217  df-sca 17218  df-vsca 17219  df-ip 17220  df-tset 17221  df-ple 17222  df-ds 17224  df-unif 17225  df-hom 17226  df-cco 17227  df-rest 17373  df-topn 17374  df-0g 17392  df-gsum 17393  df-topgen 17394  df-pt 17395  df-prds 17398  df-xrs 17453  df-qtop 17458  df-imas 17459  df-xps 17461  df-mre 17535  df-mrc 17536  df-acs 17538  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-submnd 18707  df-mulg 18988  df-cntz 19223  df-cmn 19692  df-psmet 21137  df-xmet 21138  df-met 21139  df-bl 21140  df-mopn 21141  df-fbas 21142  df-fg 21143  df-cnfld 21146  df-top 22617  df-topon 22634  df-topsp 22656  df-bases 22670  df-cld 22744  df-ntr 22745  df-cls 22746  df-nei 22823  df-lp 22861  df-perf 22862  df-cn 22952  df-cnp 22953  df-haus 23040  df-cmp 23112  df-tx 23287  df-hmeo 23480  df-fil 23571  df-fm 23663  df-flim 23664  df-flf 23665  df-xms 24047  df-ms 24048  df-tms 24049  df-cncf 24619  df-ovol 25214  df-vol 25215  df-mbf 25369  df-itg1 25370  df-itg2 25371  df-ibl 25372  df-itg 25373  df-0p 25420  df-limc 25616  df-dv 25617
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator