MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ftc2 Structured version   Visualization version   GIF version

Theorem ftc2 26097
Description: The Fundamental Theorem of Calculus, part two. If 𝐹 is a function continuous on [𝐴, 𝐵] and continuously differentiable on (𝐴, 𝐵), then the integral of the derivative of 𝐹 is equal to 𝐹(𝐵) − 𝐹(𝐴). This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 2-Sep-2014.)
Hypotheses
Ref Expression
ftc2.a (𝜑𝐴 ∈ ℝ)
ftc2.b (𝜑𝐵 ∈ ℝ)
ftc2.le (𝜑𝐴𝐵)
ftc2.c (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
ftc2.i (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)
ftc2.f (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Assertion
Ref Expression
ftc2 (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹𝐵) − (𝐹𝐴)))
Distinct variable groups:   𝑡,𝐴   𝑡,𝐵   𝑡,𝐹   𝜑,𝑡

Proof of Theorem ftc2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ftc2.a . . . . . . 7 (𝜑𝐴 ∈ ℝ)
21rexrd 11334 . . . . . 6 (𝜑𝐴 ∈ ℝ*)
3 ftc2.b . . . . . . 7 (𝜑𝐵 ∈ ℝ)
43rexrd 11334 . . . . . 6 (𝜑𝐵 ∈ ℝ*)
5 ftc2.le . . . . . 6 (𝜑𝐴𝐵)
6 ubicc2 13519 . . . . . 6 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
72, 4, 5, 6syl3anc 1371 . . . . 5 (𝜑𝐵 ∈ (𝐴[,]𝐵))
8 fvex 6928 . . . . . 6 ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐴) ∈ V
98fvconst2 7236 . . . . 5 (𝐵 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐴))
107, 9syl 17 . . . 4 (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐴))
11 eqid 2740 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
1211subcn 24899 . . . . . . . . 9 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
1312a1i 11 . . . . . . . 8 (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
14 eqid 2740 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)
15 ssidd 4032 . . . . . . . . 9 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
16 ioossre 13462 . . . . . . . . . 10 (𝐴(,)𝐵) ⊆ ℝ
1716a1i 11 . . . . . . . . 9 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
18 ftc2.i . . . . . . . . 9 (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)
19 ftc2.c . . . . . . . . . 10 (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
20 cncff 24930 . . . . . . . . . 10 ((ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
2119, 20syl 17 . . . . . . . . 9 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
2214, 1, 3, 5, 15, 17, 18, 21ftc1a 26090 . . . . . . . 8 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ))
23 ftc2.f . . . . . . . . . . 11 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
24 cncff 24930 . . . . . . . . . . 11 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
2523, 24syl 17 . . . . . . . . . 10 (𝜑𝐹:(𝐴[,]𝐵)⟶ℂ)
2625feqmptd 6985 . . . . . . . . 9 (𝜑𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)))
2726, 23eqeltrrd 2845 . . . . . . . 8 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2811, 13, 22, 27cncfmpt2f 24952 . . . . . . 7 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
29 ax-resscn 11235 . . . . . . . . . . 11 ℝ ⊆ ℂ
3029a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
31 iccssre 13483 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
321, 3, 31syl2anc 583 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
33 fvex 6928 . . . . . . . . . . . . 13 ((ℝ D 𝐹)‘𝑡) ∈ V
3433a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑥)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
353adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
3635rexrd 11334 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ*)
37 elicc2 13466 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
381, 3, 37syl2anc 583 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
3938biimpa 476 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵))
4039simp3d 1144 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝑥𝐵)
41 iooss2 13437 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℝ*𝑥𝐵) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
4236, 40, 41syl2anc 583 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵))
43 ioombl 25611 . . . . . . . . . . . . . 14 (𝐴(,)𝑥) ∈ dom vol
4443a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ∈ dom vol)
4533a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
4621feqmptd 6985 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)))
4746, 18eqeltrrd 2845 . . . . . . . . . . . . . 14 (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
4847adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
4942, 44, 45, 48iblss 25852 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑥) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
5034, 49itgcl 25831 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
5125ffvelcdmda 7113 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℂ)
5250, 51subcld 11641 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)) ∈ ℂ)
5311tgioo2 24836 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
54 iccntr 24854 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
551, 3, 54syl2anc 583 . . . . . . . . . 10 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
5630, 32, 52, 53, 11, 55dvmptntr 26021 . . . . . . . . 9 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))))
57 reelprrecn 11270 . . . . . . . . . . 11 ℝ ∈ {ℝ, ℂ}
5857a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ {ℝ, ℂ})
59 ioossicc 13487 . . . . . . . . . . . 12 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
6059sseli 4004 . . . . . . . . . . 11 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ (𝐴[,]𝐵))
6160, 50sylan2 592 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
6221ffvelcdmda 7113 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
6314, 1, 3, 5, 19, 18ftc1cn 26096 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D 𝐹))
6430, 32, 50, 53, 11, 55dvmptntr 26021 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)))
6521feqmptd 6985 . . . . . . . . . . 11 (𝜑 → (ℝ D 𝐹) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
6663, 64, 653eqtr3d 2788 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
6760, 51sylan2 592 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐹𝑥) ∈ ℂ)
6830, 32, 51, 53, 11, 55dvmptntr 26021 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥))))
6926oveq2d 7459 . . . . . . . . . . . 12 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥))))
7069, 65eqtr3d 2782 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
7168, 70eqtr3d 2782 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥)))
7258, 61, 62, 66, 67, 62, 71dvmptsub 26017 . . . . . . . . 9 (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))))
7362subidd 11629 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥)) = 0)
7473mpteq2dva 5266 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
7556, 72, 743eqtrd 2784 . . . . . . . 8 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0))
76 fconstmpt 5757 . . . . . . . 8 ((𝐴(,)𝐵) × {0}) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)
7775, 76eqtr4di 2798 . . . . . . 7 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))) = ((𝐴(,)𝐵) × {0}))
781, 3, 28, 77dveq0 26051 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥))) = ((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐴)}))
7978fveq1d 6917 . . . . 5 (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐵) = (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐴)})‘𝐵))
80 oveq2 7451 . . . . . . . . 9 (𝑥 = 𝐵 → (𝐴(,)𝑥) = (𝐴(,)𝐵))
81 itgeq1 25820 . . . . . . . . 9 ((𝐴(,)𝑥) = (𝐴(,)𝐵) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
8280, 81syl 17 . . . . . . . 8 (𝑥 = 𝐵 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
83 fveq2 6915 . . . . . . . 8 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
8482, 83oveq12d 7461 . . . . . . 7 (𝑥 = 𝐵 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝐵)))
85 eqid 2740 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))
86 ovex 7476 . . . . . . 7 (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝐵)) ∈ V
8784, 85, 86fvmpt 7024 . . . . . 6 (𝐵 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝐵)))
887, 87syl 17 . . . . 5 (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝐵)))
8979, 88eqtr3d 2782 . . . 4 (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐴)})‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝐵)))
90 lbicc2 13518 . . . . . 6 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
912, 4, 5, 90syl3anc 1371 . . . . 5 (𝜑𝐴 ∈ (𝐴[,]𝐵))
92 oveq2 7451 . . . . . . . . . . 11 (𝑥 = 𝐴 → (𝐴(,)𝑥) = (𝐴(,)𝐴))
93 iooid 13429 . . . . . . . . . . 11 (𝐴(,)𝐴) = ∅
9492, 93eqtrdi 2796 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝐴(,)𝑥) = ∅)
95 itgeq1 25820 . . . . . . . . . 10 ((𝐴(,)𝑥) = ∅ → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
9694, 95syl 17 . . . . . . . . 9 (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡)
97 itg0 25827 . . . . . . . . 9 ∫∅((ℝ D 𝐹)‘𝑡) d𝑡 = 0
9896, 97eqtrdi 2796 . . . . . . . 8 (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = 0)
99 fveq2 6915 . . . . . . . 8 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
10098, 99oveq12d 7461 . . . . . . 7 (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)) = (0 − (𝐹𝐴)))
101 df-neg 11517 . . . . . . 7 -(𝐹𝐴) = (0 − (𝐹𝐴))
102100, 101eqtr4di 2798 . . . . . 6 (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)) = -(𝐹𝐴))
103 negex 11528 . . . . . 6 -(𝐹𝐴) ∈ V
104102, 85, 103fvmpt 7024 . . . . 5 (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐴) = -(𝐹𝐴))
10591, 104syl 17 . . . 4 (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝑥)))‘𝐴) = -(𝐹𝐴))
10610, 89, 1053eqtr3d 2788 . . 3 (𝜑 → (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝐵)) = -(𝐹𝐴))
107106oveq2d 7459 . 2 (𝜑 → ((𝐹𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝐵))) = ((𝐹𝐵) + -(𝐹𝐴)))
10825, 7ffvelcdmd 7114 . . 3 (𝜑 → (𝐹𝐵) ∈ ℂ)
10933a1i 11 . . . 4 ((𝜑𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
110109, 47itgcl 25831 . . 3 (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ)
111108, 110pncan3d 11644 . 2 (𝜑 → ((𝐹𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹𝐵))) = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
11225, 91ffvelcdmd 7114 . . 3 (𝜑 → (𝐹𝐴) ∈ ℂ)
113108, 112negsubd 11647 . 2 (𝜑 → ((𝐹𝐵) + -(𝐹𝐴)) = ((𝐹𝐵) − (𝐹𝐴)))
114107, 111, 1133eqtr3d 2788 1 (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹𝐵) − (𝐹𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1537  wcel 2108  Vcvv 3488  wss 3976  c0 4352  {csn 4648  {cpr 4650   class class class wbr 5166  cmpt 5249   × cxp 5693  dom cdm 5695  ran crn 5696  wf 6564  cfv 6568  (class class class)co 7443  cc 11176  cr 11177  0cc0 11178   + caddc 11181  *cxr 11317  cle 11319  cmin 11514  -cneg 11515  (,)cioo 13401  [,]cicc 13404  TopOpenctopn 17475  topGenctg 17491  fldccnfld 21381  intcnt 23038   Cn ccn 23245   ×t ctx 23581  cnccncf 24913  volcvol 25509  𝐿1cibl 25663  citg 25664   D cdv 25910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7764  ax-inf2 9704  ax-cc 10498  ax-cnex 11234  ax-resscn 11235  ax-1cn 11236  ax-icn 11237  ax-addcl 11238  ax-addrcl 11239  ax-mulcl 11240  ax-mulrcl 11241  ax-mulcom 11242  ax-addass 11243  ax-mulass 11244  ax-distr 11245  ax-i2m1 11246  ax-1ne0 11247  ax-1rid 11248  ax-rnegex 11249  ax-rrecex 11250  ax-cnre 11251  ax-pre-lttri 11252  ax-pre-lttrn 11253  ax-pre-ltadd 11254  ax-pre-mulgt0 11255  ax-pre-sup 11256  ax-addf 11257
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-symdif 4272  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-disj 5134  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5650  df-se 5651  df-we 5652  df-xp 5701  df-rel 5702  df-cnv 5703  df-co 5704  df-dm 5705  df-rn 5706  df-res 5707  df-ima 5708  df-pred 6327  df-ord 6393  df-on 6394  df-lim 6395  df-suc 6396  df-iota 6520  df-fun 6570  df-fn 6571  df-f 6572  df-f1 6573  df-fo 6574  df-f1o 6575  df-fv 6576  df-isom 6577  df-riota 7399  df-ov 7446  df-oprab 7447  df-mpo 7448  df-of 7708  df-ofr 7709  df-om 7898  df-1st 8024  df-2nd 8025  df-supp 8196  df-frecs 8316  df-wrecs 8347  df-recs 8421  df-rdg 8460  df-1o 8516  df-2o 8517  df-oadd 8520  df-omul 8521  df-er 8757  df-map 8880  df-pm 8881  df-ixp 8950  df-en 8998  df-dom 8999  df-sdom 9000  df-fin 9001  df-fsupp 9426  df-fi 9474  df-sup 9505  df-inf 9506  df-oi 9573  df-dju 9964  df-card 10002  df-acn 10005  df-pnf 11320  df-mnf 11321  df-xr 11322  df-ltxr 11323  df-le 11324  df-sub 11516  df-neg 11517  df-div 11942  df-nn 12288  df-2 12350  df-3 12351  df-4 12352  df-5 12353  df-6 12354  df-7 12355  df-8 12356  df-9 12357  df-n0 12548  df-z 12634  df-dec 12753  df-uz 12898  df-q 13008  df-rp 13052  df-xneg 13169  df-xadd 13170  df-xmul 13171  df-ioo 13405  df-ioc 13406  df-ico 13407  df-icc 13408  df-fz 13562  df-fzo 13706  df-fl 13837  df-mod 13915  df-seq 14047  df-exp 14107  df-hash 14374  df-cj 15142  df-re 15143  df-im 15144  df-sqrt 15278  df-abs 15279  df-clim 15528  df-rlim 15529  df-sum 15729  df-struct 17188  df-sets 17205  df-slot 17223  df-ndx 17235  df-base 17253  df-ress 17282  df-plusg 17318  df-mulr 17319  df-starv 17320  df-sca 17321  df-vsca 17322  df-ip 17323  df-tset 17324  df-ple 17325  df-ds 17327  df-unif 17328  df-hom 17329  df-cco 17330  df-rest 17476  df-topn 17477  df-0g 17495  df-gsum 17496  df-topgen 17497  df-pt 17498  df-prds 17501  df-xrs 17556  df-qtop 17561  df-imas 17562  df-xps 17564  df-mre 17638  df-mrc 17639  df-acs 17641  df-mgm 18672  df-sgrp 18751  df-mnd 18767  df-submnd 18813  df-mulg 19102  df-cntz 19351  df-cmn 19818  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22913  df-topon 22930  df-topsp 22952  df-bases 22966  df-cld 23040  df-ntr 23041  df-cls 23042  df-nei 23119  df-lp 23157  df-perf 23158  df-cn 23248  df-cnp 23249  df-haus 23336  df-cmp 23408  df-tx 23583  df-hmeo 23776  df-fil 23867  df-fm 23959  df-flim 23960  df-flf 23961  df-xms 24343  df-ms 24344  df-tms 24345  df-cncf 24915  df-ovol 25510  df-vol 25511  df-mbf 25665  df-itg1 25666  df-itg2 25667  df-ibl 25668  df-itg 25669  df-0p 25716  df-limc 25913  df-dv 25914
This theorem is referenced by:  ftc2ditglem  26098  itgparts  26100  itgsubstlem  26101  itgpowd  26103  ftc2re  34567  lcmineqlem12  41990  intlewftc  42011  lhe4.4ex1a  44294  itgsin0pilem1  45861  itgcoscmulx  45880  itgsincmulx  45885  dirkeritg  46013  etransclem46  46191
  Copyright terms: Public domain W3C validator