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 37447
Description: Example of the Fundamental Theorem of Calculus, part two (ftc2 23486): ∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 23486 as simply the "Fundamental Theorem of Calculus", then ftc1 23484 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 9810 . . . 4 (⊤ → 1 ∈ ℝ)
2 2re 10845 . . . . 5 2 ∈ ℝ
32a1i 11 . . . 4 (⊤ → 2 ∈ ℝ)
4 1le2 10996 . . . . 5 1 ≤ 2
54a1i 11 . . . 4 (⊤ → 1 ≤ 2)
6 reelprrecn 9783 . . . . . . 7 ℝ ∈ {ℝ, ℂ}
76a1i 11 . . . . . 6 (⊤ → ℝ ∈ {ℝ, ℂ})
8 recn 9781 . . . . . . . . . 10 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
9 3nn0 11065 . . . . . . . . . . 11 3 ∈ ℕ0
10 expcl 12608 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑦↑3) ∈ ℂ)
119, 10mpan2 702 . . . . . . . . . 10 (𝑦 ∈ ℂ → (𝑦↑3) ∈ ℂ)
128, 11syl 17 . . . . . . . . 9 (𝑦 ∈ ℝ → (𝑦↑3) ∈ ℂ)
13 3cn 10850 . . . . . . . . . 10 3 ∈ ℂ
14 3ne0 10870 . . . . . . . . . 10 3 ≠ 0
15 divcl 10440 . . . . . . . . . 10 (((𝑦↑3) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → ((𝑦↑3) / 3) ∈ ℂ)
1613, 14, 15mp3an23 1407 . . . . . . . . 9 ((𝑦↑3) ∈ ℂ → ((𝑦↑3) / 3) ∈ ℂ)
1712, 16syl 17 . . . . . . . 8 (𝑦 ∈ ℝ → ((𝑦↑3) / 3) ∈ ℂ)
18 mulcl 9775 . . . . . . . . 9 ((3 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (3 · 𝑦) ∈ ℂ)
1913, 8, 18sylancr 693 . . . . . . . 8 (𝑦 ∈ ℝ → (3 · 𝑦) ∈ ℂ)
2017, 19subcld 10143 . . . . . . 7 (𝑦 ∈ ℝ → (((𝑦↑3) / 3) − (3 · 𝑦)) ∈ ℂ)
2120adantl 480 . . . . . 6 ((⊤ ∧ 𝑦 ∈ ℝ) → (((𝑦↑3) / 3) − (3 · 𝑦)) ∈ ℂ)
22 ovex 6454 . . . . . . 7 ((𝑦↑2) − 3) ∈ V
2322a1i 11 . . . . . 6 ((⊤ ∧ 𝑦 ∈ ℝ) → ((𝑦↑2) − 3) ∈ V)
2417adantl 480 . . . . . . 7 ((⊤ ∧ 𝑦 ∈ ℝ) → ((𝑦↑3) / 3) ∈ ℂ)
25 ovex 6454 . . . . . . . 8 (𝑦↑2) ∈ V
2625a1i 11 . . . . . . 7 ((⊤ ∧ 𝑦 ∈ ℝ) → (𝑦↑2) ∈ V)
27 divrec2 10451 . . . . . . . . . . . . 13 (((𝑦↑3) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → ((𝑦↑3) / 3) = ((1 / 3) · (𝑦↑3)))
2813, 14, 27mp3an23 1407 . . . . . . . . . . . 12 ((𝑦↑3) ∈ ℂ → ((𝑦↑3) / 3) = ((1 / 3) · (𝑦↑3)))
2912, 28syl 17 . . . . . . . . . . 11 (𝑦 ∈ ℝ → ((𝑦↑3) / 3) = ((1 / 3) · (𝑦↑3)))
3029mpteq2ia 4566 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3)) = (𝑦 ∈ ℝ ↦ ((1 / 3) · (𝑦↑3)))
3130oveq2i 6437 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) · (𝑦↑3))))
3212adantl 480 . . . . . . . . . . 11 ((⊤ ∧ 𝑦 ∈ ℝ) → (𝑦↑3) ∈ ℂ)
33 ovex 6454 . . . . . . . . . . . 12 (3 · (𝑦↑2)) ∈ V
3433a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑦 ∈ ℝ) → (3 · (𝑦↑2)) ∈ V)
35 eqid 2514 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℂ ↦ (𝑦↑3)) = (𝑦 ∈ ℂ ↦ (𝑦↑3))
3635, 11fmpti 6175 . . . . . . . . . . . . . 14 (𝑦 ∈ ℂ ↦ (𝑦↑3)):ℂ⟶ℂ
37 ssid 3491 . . . . . . . . . . . . . 14 ℂ ⊆ ℂ
38 ax-resscn 9748 . . . . . . . . . . . . . . 15 ℝ ⊆ ℂ
39 3nn 10941 . . . . . . . . . . . . . . . . . 18 3 ∈ ℕ
40 dvexp 23397 . . . . . . . . . . . . . . . . . 18 (3 ∈ ℕ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3 · (𝑦↑(3 − 1)))))
4139, 40ax-mp 5 . . . . . . . . . . . . . . . . 17 (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3 · (𝑦↑(3 − 1))))
42 3m1e2 10892 . . . . . . . . . . . . . . . . . . . 20 (3 − 1) = 2
4342oveq2i 6437 . . . . . . . . . . . . . . . . . . 19 (𝑦↑(3 − 1)) = (𝑦↑2)
4443oveq2i 6437 . . . . . . . . . . . . . . . . . 18 (3 · (𝑦↑(3 − 1))) = (3 · (𝑦↑2))
4544mpteq2i 4567 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℂ ↦ (3 · (𝑦↑(3 − 1)))) = (𝑦 ∈ ℂ ↦ (3 · (𝑦↑2)))
4641, 45eqtri 2536 . . . . . . . . . . . . . . . 16 (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) = (𝑦 ∈ ℂ ↦ (3 · (𝑦↑2)))
4733, 46dmmpti 5821 . . . . . . . . . . . . . . 15 dom (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) = ℂ
4838, 47sseqtr4i 3505 . . . . . . . . . . . . . 14 ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3)))
49 dvres3 23358 . . . . . . . . . . . . . 14 (((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (𝑦↑3)):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))))) → (ℝ D ((𝑦 ∈ ℂ ↦ (𝑦↑3)) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) ↾ ℝ))
506, 36, 37, 48, 49mp4an 704 . . . . . . . . . . . . 13 (ℝ D ((𝑦 ∈ ℂ ↦ (𝑦↑3)) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) ↾ ℝ)
51 resmpt 5260 . . . . . . . . . . . . . . 15 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (𝑦↑3)) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3)))
5238, 51ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℂ ↦ (𝑦↑3)) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (𝑦↑3))
5352oveq2i 6437 . . . . . . . . . . . . 13 (ℝ D ((𝑦 ∈ ℂ ↦ (𝑦↑3)) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3)))
5446reseq1i 5204 . . . . . . . . . . . . . 14 ((ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ (3 · (𝑦↑2))) ↾ ℝ)
55 resmpt 5260 . . . . . . . . . . . . . . 15 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (3 · (𝑦↑2))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (3 · (𝑦↑2))))
5638, 55ax-mp 5 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℂ ↦ (3 · (𝑦↑2))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (3 · (𝑦↑2)))
5754, 56eqtri 2536 . . . . . . . . . . . . 13 ((ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑3))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (3 · (𝑦↑2)))
5850, 53, 573eqtr3i 2544 . . . . . . . . . . . 12 (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3 · (𝑦↑2)))
5958a1i 11 . . . . . . . . . . 11 (⊤ → (ℝ D (𝑦 ∈ ℝ ↦ (𝑦↑3))) = (𝑦 ∈ ℝ ↦ (3 · (𝑦↑2))))
60 ax-1cn 9749 . . . . . . . . . . . . 13 1 ∈ ℂ
6160, 13, 14divcli 10516 . . . . . . . . . . . 12 (1 / 3) ∈ ℂ
6261a1i 11 . . . . . . . . . . 11 (⊤ → (1 / 3) ∈ ℂ)
637, 32, 34, 59, 62dvmptcmul 23408 . . . . . . . . . 10 (⊤ → (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) · (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) · (3 · (𝑦↑2)))))
6463trud 1483 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ ((1 / 3) · (𝑦↑3)))) = (𝑦 ∈ ℝ ↦ ((1 / 3) · (3 · (𝑦↑2))))
65 sqcl 12655 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ → (𝑦↑2) ∈ ℂ)
66 mulcl 9775 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (𝑦↑2) ∈ ℂ) → (3 · (𝑦↑2)) ∈ ℂ)
6713, 65, 66sylancr 693 . . . . . . . . . . . 12 (𝑦 ∈ ℂ → (3 · (𝑦↑2)) ∈ ℂ)
68 divrec2 10451 . . . . . . . . . . . . 13 (((3 · (𝑦↑2)) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → ((3 · (𝑦↑2)) / 3) = ((1 / 3) · (3 · (𝑦↑2))))
6913, 14, 68mp3an23 1407 . . . . . . . . . . . 12 ((3 · (𝑦↑2)) ∈ ℂ → ((3 · (𝑦↑2)) / 3) = ((1 / 3) · (3 · (𝑦↑2))))
708, 67, 693syl 18 . . . . . . . . . . 11 (𝑦 ∈ ℝ → ((3 · (𝑦↑2)) / 3) = ((1 / 3) · (3 · (𝑦↑2))))
71 divcan3 10460 . . . . . . . . . . . . 13 (((𝑦↑2) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → ((3 · (𝑦↑2)) / 3) = (𝑦↑2))
7213, 14, 71mp3an23 1407 . . . . . . . . . . . 12 ((𝑦↑2) ∈ ℂ → ((3 · (𝑦↑2)) / 3) = (𝑦↑2))
738, 65, 723syl 18 . . . . . . . . . . 11 (𝑦 ∈ ℝ → ((3 · (𝑦↑2)) / 3) = (𝑦↑2))
7470, 73eqtr3d 2550 . . . . . . . . . 10 (𝑦 ∈ ℝ → ((1 / 3) · (3 · (𝑦↑2))) = (𝑦↑2))
7574mpteq2ia 4566 . . . . . . . . 9 (𝑦 ∈ ℝ ↦ ((1 / 3) · (3 · (𝑦↑2)))) = (𝑦 ∈ ℝ ↦ (𝑦↑2))
7631, 64, 753eqtri 2540 . . . . . . . 8 (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (𝑦 ∈ ℝ ↦ (𝑦↑2))
7776a1i 11 . . . . . . 7 (⊤ → (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦↑3) / 3))) = (𝑦 ∈ ℝ ↦ (𝑦↑2)))
7819adantl 480 . . . . . . 7 ((⊤ ∧ 𝑦 ∈ ℝ) → (3 · 𝑦) ∈ ℂ)
79 3ex 10851 . . . . . . . 8 3 ∈ V
8079a1i 11 . . . . . . 7 ((⊤ ∧ 𝑦 ∈ ℝ) → 3 ∈ V)
818adantl 480 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
82 1red 9810 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ ℝ) → 1 ∈ ℝ)
837dvmptid 23401 . . . . . . . . 9 (⊤ → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
8413a1i 11 . . . . . . . . 9 (⊤ → 3 ∈ ℂ)
857, 81, 82, 83, 84dvmptcmul 23408 . . . . . . . 8 (⊤ → (ℝ D (𝑦 ∈ ℝ ↦ (3 · 𝑦))) = (𝑦 ∈ ℝ ↦ (3 · 1)))
86 3t1e3 10933 . . . . . . . . 9 (3 · 1) = 3
8786mpteq2i 4567 . . . . . . . 8 (𝑦 ∈ ℝ ↦ (3 · 1)) = (𝑦 ∈ ℝ ↦ 3)
8885, 87syl6eq 2564 . . . . . . 7 (⊤ → (ℝ D (𝑦 ∈ ℝ ↦ (3 · 𝑦))) = (𝑦 ∈ ℝ ↦ 3))
897, 24, 26, 77, 78, 80, 88dvmptsub 23411 . . . . . 6 (⊤ → (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) − 3)))
90 1re 9794 . . . . . . . 8 1 ∈ ℝ
91 iccssre 11995 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ) → (1[,]2) ⊆ ℝ)
9290, 2, 91mp2an 703 . . . . . . 7 (1[,]2) ⊆ ℝ
9392a1i 11 . . . . . 6 (⊤ → (1[,]2) ⊆ ℝ)
94 eqid 2514 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
9594tgioo2 22323 . . . . . 6 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
96 iccntr 22341 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(1[,]2)) = (1(,)2))
9790, 2, 96mp2an 703 . . . . . . 7 ((int‘(topGen‘ran (,)))‘(1[,]2)) = (1(,)2)
9897a1i 11 . . . . . 6 (⊤ → ((int‘(topGen‘ran (,)))‘(1[,]2)) = (1(,)2))
997, 21, 23, 89, 93, 95, 94, 98dvmptres2 23406 . . . . 5 (⊤ → (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3)))
100 ioossicc 11999 . . . . . . 7 (1(,)2) ⊆ (1[,]2)
101 resmpt 5260 . . . . . . 7 ((1(,)2) ⊆ (1[,]2) → ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ↾ (1(,)2)) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3)))
102100, 101ax-mp 5 . . . . . 6 ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ↾ (1(,)2)) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3))
10392, 38sstri 3481 . . . . . . . . 9 (1[,]2) ⊆ ℂ
104 resmpt 5260 . . . . . . . . 9 ((1[,]2) ⊆ ℂ → ((𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ↾ (1[,]2)) = (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)))
105103, 104ax-mp 5 . . . . . . . 8 ((𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ↾ (1[,]2)) = (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3))
106 eqid 2514 . . . . . . . . . . . 12 (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) = (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3))
107 subcl 10031 . . . . . . . . . . . . . 14 (((𝑦↑2) ∈ ℂ ∧ 3 ∈ ℂ) → ((𝑦↑2) − 3) ∈ ℂ)
10813, 107mpan2 702 . . . . . . . . . . . . 13 ((𝑦↑2) ∈ ℂ → ((𝑦↑2) − 3) ∈ ℂ)
10965, 108syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ℂ → ((𝑦↑2) − 3) ∈ ℂ)
110106, 109fmpti 6175 . . . . . . . . . . 11 (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)):ℂ⟶ℂ
11137, 110, 373pm3.2i 1231 . . . . . . . . . 10 (ℂ ⊆ ℂ ∧ (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)):ℂ⟶ℂ ∧ ℂ ⊆ ℂ)
112 ovex 6454 . . . . . . . . . . 11 ((2 · (𝑦↑(2 − 1))) − 0) ∈ V
113 cnelprrecn 9784 . . . . . . . . . . . . . 14 ℂ ∈ {ℝ, ℂ}
114113a1i 11 . . . . . . . . . . . . 13 (⊤ → ℂ ∈ {ℝ, ℂ})
11565adantl 480 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ ℂ) → (𝑦↑2) ∈ ℂ)
116 ovex 6454 . . . . . . . . . . . . . 14 (2 · (𝑦↑(2 − 1))) ∈ V
117116a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ ℂ) → (2 · (𝑦↑(2 − 1))) ∈ V)
118 2nn 10940 . . . . . . . . . . . . . . 15 2 ∈ ℕ
119 dvexp 23397 . . . . . . . . . . . . . . 15 (2 ∈ ℕ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑2))) = (𝑦 ∈ ℂ ↦ (2 · (𝑦↑(2 − 1)))))
120118, 119ax-mp 5 . . . . . . . . . . . . . 14 (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑2))) = (𝑦 ∈ ℂ ↦ (2 · (𝑦↑(2 − 1))))
121120a1i 11 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑2))) = (𝑦 ∈ ℂ ↦ (2 · (𝑦↑(2 − 1)))))
12213a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ ℂ) → 3 ∈ ℂ)
123 c0ex 9789 . . . . . . . . . . . . . 14 0 ∈ V
124123a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ ℂ) → 0 ∈ V)
125114, 84dvmptc 23402 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ 3)) = (𝑦 ∈ ℂ ↦ 0))
126114, 115, 117, 121, 122, 124, 125dvmptsub 23411 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3))) = (𝑦 ∈ ℂ ↦ ((2 · (𝑦↑(2 − 1))) − 0)))
127126trud 1483 . . . . . . . . . . 11 (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3))) = (𝑦 ∈ ℂ ↦ ((2 · (𝑦↑(2 − 1))) − 0))
128112, 127dmmpti 5821 . . . . . . . . . 10 dom (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3))) = ℂ
129 dvcn 23365 . . . . . . . . . 10 (((ℂ ⊆ ℂ ∧ (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)):ℂ⟶ℂ ∧ ℂ ⊆ ℂ) ∧ dom (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3))) = ℂ) → (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ∈ (ℂ–cn→ℂ))
130111, 128, 129mp2an 703 . . . . . . . . 9 (𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ∈ (ℂ–cn→ℂ)
131 rescncf 22431 . . . . . . . . 9 ((1[,]2) ⊆ ℂ → ((𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ∈ (ℂ–cn→ℂ) → ((𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ↾ (1[,]2)) ∈ ((1[,]2)–cn→ℂ)))
132103, 130, 131mp2 9 . . . . . . . 8 ((𝑦 ∈ ℂ ↦ ((𝑦↑2) − 3)) ↾ (1[,]2)) ∈ ((1[,]2)–cn→ℂ)
133105, 132eqeltrri 2589 . . . . . . 7 (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈ ((1[,]2)–cn→ℂ)
134 rescncf 22431 . . . . . . 7 ((1(,)2) ⊆ (1[,]2) → ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈ ((1[,]2)–cn→ℂ) → ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ↾ (1(,)2)) ∈ ((1(,)2)–cn→ℂ)))
135100, 133, 134mp2 9 . . . . . 6 ((𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ↾ (1(,)2)) ∈ ((1(,)2)–cn→ℂ)
136102, 135eqeltrri 2589 . . . . 5 (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3)) ∈ ((1(,)2)–cn→ℂ)
13799, 136syl6eqel 2600 . . . 4 (⊤ → (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) ∈ ((1(,)2)–cn→ℂ))
138100a1i 11 . . . . . 6 (⊤ → (1(,)2) ⊆ (1[,]2))
139 ioombl 23015 . . . . . . 7 (1(,)2) ∈ dom vol
140139a1i 11 . . . . . 6 (⊤ → (1(,)2) ∈ dom vol)
14122a1i 11 . . . . . 6 ((⊤ ∧ 𝑦 ∈ (1[,]2)) → ((𝑦↑2) − 3) ∈ V)
142 cniccibl 23288 . . . . . . . 8 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈ ((1[,]2)–cn→ℂ)) → (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈ 𝐿1)
14390, 2, 133, 142mp3an 1415 . . . . . . 7 (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈ 𝐿1
144143a1i 11 . . . . . 6 (⊤ → (𝑦 ∈ (1[,]2) ↦ ((𝑦↑2) − 3)) ∈ 𝐿1)
145138, 140, 141, 144iblss 23252 . . . . 5 (⊤ → (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3)) ∈ 𝐿1)
14699, 145eqeltrd 2592 . . . 4 (⊤ → (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) ∈ 𝐿1)
147 resmpt 5260 . . . . . . 7 ((1[,]2) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ↾ (1[,]2)) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))
14892, 147ax-mp 5 . . . . . 6 ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ↾ (1[,]2)) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))
149 eqid 2514 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) = (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))
150149, 20fmpti 6175 . . . . . . . . 9 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))):ℝ⟶ℂ
151 ssid 3491 . . . . . . . . 9 ℝ ⊆ ℝ
15238, 150, 1513pm3.2i 1231 . . . . . . . 8 (ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))):ℝ⟶ℂ ∧ ℝ ⊆ ℝ)
15389trud 1483 . . . . . . . . 9 (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑦↑2) − 3))
15422, 153dmmpti 5821 . . . . . . . 8 dom (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = ℝ
155 dvcn 23365 . . . . . . . 8 (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))):ℝ⟶ℂ ∧ ℝ ⊆ ℝ) ∧ dom (ℝ D (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = ℝ) → (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ∈ (ℝ–cn→ℂ))
156152, 154, 155mp2an 703 . . . . . . 7 (𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ∈ (ℝ–cn→ℂ)
157 rescncf 22431 . . . . . . 7 ((1[,]2) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ∈ (ℝ–cn→ℂ) → ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ↾ (1[,]2)) ∈ ((1[,]2)–cn→ℂ)))
15892, 156, 157mp2 9 . . . . . 6 ((𝑦 ∈ ℝ ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ↾ (1[,]2)) ∈ ((1[,]2)–cn→ℂ)
159148, 158eqeltrri 2589 . . . . 5 (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ∈ ((1[,]2)–cn→ℂ)
160159a1i 11 . . . 4 (⊤ → (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) ∈ ((1[,]2)–cn→ℂ))
1611, 3, 5, 137, 146, 160ftc2 23486 . . 3 (⊤ → ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) d𝑥 = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘1)))
162161trud 1483 . 2 ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) d𝑥 = (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘1))
163 itgeq2 23225 . . 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𝑥)
164 oveq1 6433 . . . . 5 (𝑦 = 𝑥 → (𝑦↑2) = (𝑥↑2))
165164oveq1d 6441 . . . 4 (𝑦 = 𝑥 → ((𝑦↑2) − 3) = ((𝑥↑2) − 3))
16699trud 1483 . . . 4 (ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))) = (𝑦 ∈ (1(,)2) ↦ ((𝑦↑2) − 3))
167 ovex 6454 . . . 4 ((𝑥↑2) − 3) ∈ V
168165, 166, 167fvmpt 6075 . . 3 (𝑥 ∈ (1(,)2) → ((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) = ((𝑥↑2) − 3))
169163, 168mprg 2814 . 2 ∫(1(,)2)((ℝ D (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))))‘𝑥) d𝑥 = ∫(1(,)2)((𝑥↑2) − 3) d𝑥
1702leidi 10311 . . . . . . . . 9 2 ≤ 2
17190, 2elicc2i 11979 . . . . . . . . 9 (2 ∈ (1[,]2) ↔ (2 ∈ ℝ ∧ 1 ≤ 2 ∧ 2 ≤ 2))
1722, 4, 170, 171mpbir3an 1236 . . . . . . . 8 2 ∈ (1[,]2)
173 oveq1 6433 . . . . . . . . . . . 12 (𝑦 = 2 → (𝑦↑3) = (2↑3))
174173oveq1d 6441 . . . . . . . . . . 11 (𝑦 = 2 → ((𝑦↑3) / 3) = ((2↑3) / 3))
175 oveq2 6434 . . . . . . . . . . 11 (𝑦 = 2 → (3 · 𝑦) = (3 · 2))
176174, 175oveq12d 6444 . . . . . . . . . 10 (𝑦 = 2 → (((𝑦↑3) / 3) − (3 · 𝑦)) = (((2↑3) / 3) − (3 · 2)))
177 cu2 12693 . . . . . . . . . . . . 13 (2↑3) = 8
178177oveq1i 6436 . . . . . . . . . . . 12 ((2↑3) / 3) = (8 / 3)
179 3t2e6 10934 . . . . . . . . . . . 12 (3 · 2) = 6
180178, 179oveq12i 6438 . . . . . . . . . . 11 (((2↑3) / 3) − (3 · 2)) = ((8 / 3) − 6)
181 2cn 10846 . . . . . . . . . . . . . . 15 2 ∈ ℂ
182 6cn 10857 . . . . . . . . . . . . . . 15 6 ∈ ℂ
183181, 182, 13, 14divdiri 10531 . . . . . . . . . . . . . 14 ((2 + 6) / 3) = ((2 / 3) + (6 / 3))
184 6p2e8 10924 . . . . . . . . . . . . . . . 16 (6 + 2) = 8
185182, 181, 184addcomli 9979 . . . . . . . . . . . . . . 15 (2 + 6) = 8
186185oveq1i 6436 . . . . . . . . . . . . . 14 ((2 + 6) / 3) = (8 / 3)
187182, 13, 181, 14divmuli 10528 . . . . . . . . . . . . . . . 16 ((6 / 3) = 2 ↔ (3 · 2) = 6)
188179, 187mpbir 219 . . . . . . . . . . . . . . 15 (6 / 3) = 2
189188oveq2i 6437 . . . . . . . . . . . . . 14 ((2 / 3) + (6 / 3)) = ((2 / 3) + 2)
190183, 186, 1893eqtr3i 2544 . . . . . . . . . . . . 13 (8 / 3) = ((2 / 3) + 2)
191190oveq1i 6436 . . . . . . . . . . . 12 ((8 / 3) − 6) = (((2 / 3) + 2) − 6)
192181, 13, 14divcli 10516 . . . . . . . . . . . . 13 (2 / 3) ∈ ℂ
193 subsub3 10064 . . . . . . . . . . . . 13 (((2 / 3) ∈ ℂ ∧ 6 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 / 3) − (6 − 2)) = (((2 / 3) + 2) − 6))
194192, 182, 181, 193mp3an 1415 . . . . . . . . . . . 12 ((2 / 3) − (6 − 2)) = (((2 / 3) + 2) − 6)
195191, 194eqtr4i 2539 . . . . . . . . . . 11 ((8 / 3) − 6) = ((2 / 3) − (6 − 2))
196 4cn 10853 . . . . . . . . . . . . 13 4 ∈ ℂ
197 4p2e6 10917 . . . . . . . . . . . . . 14 (4 + 2) = 6
198196, 181, 197addcomli 9979 . . . . . . . . . . . . 13 (2 + 4) = 6
199182, 181, 196, 198subaddrii 10121 . . . . . . . . . . . 12 (6 − 2) = 4
200199oveq2i 6437 . . . . . . . . . . 11 ((2 / 3) − (6 − 2)) = ((2 / 3) − 4)
201180, 195, 2003eqtri 2540 . . . . . . . . . 10 (((2↑3) / 3) − (3 · 2)) = ((2 / 3) − 4)
202176, 201syl6eq 2564 . . . . . . . . 9 (𝑦 = 2 → (((𝑦↑3) / 3) − (3 · 𝑦)) = ((2 / 3) − 4))
203 eqid 2514 . . . . . . . . 9 (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦))) = (𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))
204 ovex 6454 . . . . . . . . 9 ((2 / 3) − 4) ∈ V
205202, 203, 204fvmpt 6075 . . . . . . . 8 (2 ∈ (1[,]2) → ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) = ((2 / 3) − 4))
206172, 205ax-mp 5 . . . . . . 7 ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) = ((2 / 3) − 4)
20790leidi 10311 . . . . . . . . 9 1 ≤ 1
20890, 2elicc2i 11979 . . . . . . . . 9 (1 ∈ (1[,]2) ↔ (1 ∈ ℝ ∧ 1 ≤ 1 ∧ 1 ≤ 2))
20990, 207, 4, 208mpbir3an 1236 . . . . . . . 8 1 ∈ (1[,]2)
210 oveq1 6433 . . . . . . . . . . . 12 (𝑦 = 1 → (𝑦↑3) = (1↑3))
211210oveq1d 6441 . . . . . . . . . . 11 (𝑦 = 1 → ((𝑦↑3) / 3) = ((1↑3) / 3))
212 oveq2 6434 . . . . . . . . . . 11 (𝑦 = 1 → (3 · 𝑦) = (3 · 1))
213211, 212oveq12d 6444 . . . . . . . . . 10 (𝑦 = 1 → (((𝑦↑3) / 3) − (3 · 𝑦)) = (((1↑3) / 3) − (3 · 1)))
214 3z 11151 . . . . . . . . . . . . 13 3 ∈ ℤ
215 1exp 12619 . . . . . . . . . . . . 13 (3 ∈ ℤ → (1↑3) = 1)
216214, 215ax-mp 5 . . . . . . . . . . . 12 (1↑3) = 1
217216oveq1i 6436 . . . . . . . . . . 11 ((1↑3) / 3) = (1 / 3)
218217, 86oveq12i 6438 . . . . . . . . . 10 (((1↑3) / 3) − (3 · 1)) = ((1 / 3) − 3)
219213, 218syl6eq 2564 . . . . . . . . 9 (𝑦 = 1 → (((𝑦↑3) / 3) − (3 · 𝑦)) = ((1 / 3) − 3))
220 ovex 6454 . . . . . . . . 9 ((1 / 3) − 3) ∈ V
221219, 203, 220fvmpt 6075 . . . . . . . 8 (1 ∈ (1[,]2) → ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘1) = ((1 / 3) − 3))
222209, 221ax-mp 5 . . . . . . 7 ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘1) = ((1 / 3) − 3)
223206, 222oveq12i 6438 . . . . . 6 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘1)) = (((2 / 3) − 4) − ((1 / 3) − 3))
224 sub4 10077 . . . . . . 7 ((((2 / 3) ∈ ℂ ∧ 4 ∈ ℂ) ∧ ((1 / 3) ∈ ℂ ∧ 3 ∈ ℂ)) → (((2 / 3) − 4) − ((1 / 3) − 3)) = (((2 / 3) − (1 / 3)) − (4 − 3)))
225192, 196, 61, 13, 224mp4an 704 . . . . . 6 (((2 / 3) − 4) − ((1 / 3) − 3)) = (((2 / 3) − (1 / 3)) − (4 − 3))
22613, 14pm3.2i 469 . . . . . . . . 9 (3 ∈ ℂ ∧ 3 ≠ 0)
227 divsubdir 10470 . . . . . . . . 9 ((2 ∈ ℂ ∧ 1 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 − 1) / 3) = ((2 / 3) − (1 / 3)))
228181, 60, 226, 227mp3an 1415 . . . . . . . 8 ((2 − 1) / 3) = ((2 / 3) − (1 / 3))
229 2m1e1 10890 . . . . . . . . 9 (2 − 1) = 1
230229oveq1i 6436 . . . . . . . 8 ((2 − 1) / 3) = (1 / 3)
231228, 230eqtr3i 2538 . . . . . . 7 ((2 / 3) − (1 / 3)) = (1 / 3)
232 3p1e4 10908 . . . . . . . 8 (3 + 1) = 4
233196, 13, 60, 232subaddrii 10121 . . . . . . 7 (4 − 3) = 1
234231, 233oveq12i 6438 . . . . . 6 (((2 / 3) − (1 / 3)) − (4 − 3)) = ((1 / 3) − 1)
235223, 225, 2343eqtri 2540 . . . . 5 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘1)) = ((1 / 3) − 1)
23613, 14dividi 10507 . . . . . 6 (3 / 3) = 1
237236oveq2i 6437 . . . . 5 ((1 / 3) − (3 / 3)) = ((1 / 3) − 1)
238235, 237eqtr4i 2539 . . . 4 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘1)) = ((1 / 3) − (3 / 3))
239 divsubdir 10470 . . . . 5 ((1 ∈ ℂ ∧ 3 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((1 − 3) / 3) = ((1 / 3) − (3 / 3)))
24060, 13, 226, 239mp3an 1415 . . . 4 ((1 − 3) / 3) = ((1 / 3) − (3 / 3))
241238, 240eqtr4i 2539 . . 3 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘1)) = ((1 − 3) / 3)
242 divneg 10468 . . . . 5 ((2 ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → -(2 / 3) = (-2 / 3))
243181, 13, 14, 242mp3an 1415 . . . 4 -(2 / 3) = (-2 / 3)
24413, 60negsubdi2i 10118 . . . . . 6 -(3 − 1) = (1 − 3)
24542negeqi 10025 . . . . . 6 -(3 − 1) = -2
246244, 245eqtr3i 2538 . . . . 5 (1 − 3) = -2
247246oveq1i 6436 . . . 4 ((1 − 3) / 3) = (-2 / 3)
248243, 247eqtr4i 2539 . . 3 -(2 / 3) = ((1 − 3) / 3)
249241, 248eqtr4i 2539 . 2 (((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘2) − ((𝑦 ∈ (1[,]2) ↦ (((𝑦↑3) / 3) − (3 · 𝑦)))‘1)) = -(2 / 3)
250162, 169, 2493eqtr3i 2544 1 ∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3)
Colors of variables: wff setvar class
Syntax hints:  wa 382  w3a 1030   = wceq 1474  wtru 1475  wcel 1938  wne 2684  Vcvv 3077  wss 3444  {cpr 4030   class class class wbr 4481  cmpt 4541  dom cdm 4932  ran crn 4933  cres 4934  wf 5685  cfv 5689  (class class class)co 6426  cc 9689  cr 9690  0cc0 9691  1c1 9692   + caddc 9694   · cmul 9696  cle 9830  cmin 10017  -cneg 10018   / cdiv 10433  cn 10775  2c2 10825  3c3 10826  4c4 10827  6c6 10829  8c8 10831  0cn0 11047  cz 11118  (,)cioo 11915  [,]cicc 11918  cexp 12590  TopOpenctopn 15789  topGenctg 15805  fldccnfld 19471  intcnt 20534  cnccncf 22410  volcvol 22914  𝐿1cibl 23067  citg 23068   D cdv 23308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-inf2 8297  ax-cc 9016  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768  ax-pre-sup 9769  ax-addf 9770  ax-mulf 9771
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-iin 4356  df-disj 4452  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-se 4892  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-isom 5698  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-of 6671  df-ofr 6672  df-om 6834  df-1st 6934  df-2nd 6935  df-supp 7058  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-1o 7323  df-2o 7324  df-oadd 7327  df-omul 7328  df-er 7505  df-map 7622  df-pm 7623  df-ixp 7671  df-en 7718  df-dom 7719  df-sdom 7720  df-fin 7721  df-fsupp 8035  df-fi 8076  df-sup 8107  df-inf 8108  df-oi 8174  df-card 8524  df-acn 8527  df-cda 8749  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-div 10434  df-nn 10776  df-2 10834  df-3 10835  df-4 10836  df-5 10837  df-6 10838  df-7 10839  df-8 10840  df-9 10841  df-n0 11048  df-z 11119  df-dec 11234  df-uz 11428  df-q 11531  df-rp 11575  df-xneg 11688  df-xadd 11689  df-xmul 11690  df-ioo 11919  df-ioc 11920  df-ico 11921  df-icc 11922  df-fz 12066  df-fzo 12203  df-fl 12323  df-mod 12399  df-seq 12532  df-exp 12591  df-hash 12848  df-cj 13546  df-re 13547  df-im 13548  df-sqrt 13682  df-abs 13683  df-limsup 13910  df-clim 13933  df-rlim 13934  df-sum 14134  df-struct 15581  df-ndx 15582  df-slot 15583  df-base 15584  df-sets 15585  df-ress 15586  df-plusg 15665  df-mulr 15666  df-starv 15667  df-sca 15668  df-vsca 15669  df-ip 15670  df-tset 15671  df-ple 15672  df-ds 15675  df-unif 15676  df-hom 15677  df-cco 15678  df-rest 15790  df-topn 15791  df-0g 15809  df-gsum 15810  df-topgen 15811  df-pt 15812  df-prds 15815  df-xrs 15869  df-qtop 15875  df-imas 15876  df-xps 15879  df-mre 15961  df-mrc 15962  df-acs 15964  df-mgm 16957  df-sgrp 16999  df-mnd 17010  df-submnd 17051  df-mulg 17256  df-cntz 17465  df-cmn 17926  df-psmet 19463  df-xmet 19464  df-met 19465  df-bl 19466  df-mopn 19467  df-fbas 19468  df-fg 19469  df-cnfld 19472  df-top 20424  df-bases 20425  df-topon 20426  df-topsp 20427  df-cld 20536  df-ntr 20537  df-cls 20538  df-nei 20615  df-lp 20653  df-perf 20654  df-cn 20744  df-cnp 20745  df-haus 20832  df-cmp 20903  df-tx 21078  df-hmeo 21271  df-fil 21363  df-fm 21455  df-flim 21456  df-flf 21457  df-xms 21837  df-ms 21838  df-tms 21839  df-cncf 22412  df-ovol 22915  df-vol 22916  df-mbf 23069  df-itg1 23070  df-itg2 23071  df-ibl 23072  df-itg 23073  df-0p 23118  df-limc 23311  df-dv 23312
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator