Metamath Proof Explorer

Theorem ftc1cn

Description: Strengthen the assumptions of ftc1 to when the function F is continuous on the entire interval ( A , B ) ; in this case we can calculate _D G exactly. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses ftc1cn.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
ftc1cn.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ftc1cn.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ftc1cn.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ftc1cn.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
ftc1cn.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
Assertion ftc1cn ( 𝜑 → ( ℝ D 𝐺 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 ftc1cn.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2 ftc1cn.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ftc1cn.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 ftc1cn.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 ftc1cn.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
6 ftc1cn.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
7 dvf ⊢ ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ
8 7 a1i ⊢ ( 𝜑 → ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ )
9 8 ffund ⊢ ( 𝜑 → Fun ( ℝ D 𝐺 ) )
10 ax-resscn ⊢ ℝ ⊆ ℂ
11 10 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
12 ssidd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
13 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
14 13 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
15 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
16 5 15 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
17 1 2 3 4 12 14 6 16 ftc1lem2 ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
18 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
19 2 3 18 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
20 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
21 20 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
22 11 17 19 21 20 dvbssntr ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) )
23 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
24 2 3 23 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
25 22 24 sseqtrd ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) ⊆ ( 𝐴 (,) 𝐵 ) )
26 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
27 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
28 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ≤ 𝐵 )
29 ssidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
30 13 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
31 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 ∈ 𝐿1 )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( 𝐴 (,) 𝐵 ) )
33 13 10 sstri ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
34 ssid ⊢ ℂ ⊆ ℂ
35 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) )
36 20 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
37 36 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
38 20 35 37 cncfcn ⊢ ( ( ( 𝐴 (,) 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
39 33 34 38 mp2an ⊢ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) )
40 5 39 eleqtrdi ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
42 33 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
43 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) )
44 36 42 43 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) )
45 toponuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) )
46 44 45 syl ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) )
47 46 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↔ 𝑦 ∈ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ) )
48 47 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) )
49 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) )
50 49 cncnpi ⊢ ( ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ∧ 𝑦 ∈ ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
51 41 48 50 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,) 𝐵 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
52 1 26 27 28 29 30 31 32 51 21 35 20 ftc1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝑦 ) )
53 vex ⊢ 𝑦 ∈ V
54 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
55 53 54 breldm ⊢ ( 𝑦 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝑦 ) → 𝑦 ∈ dom ( ℝ D 𝐺 ) )
56 52 55 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ dom ( ℝ D 𝐺 ) )
57 25 56 eqelssd ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
58 df-fn ⊢ ( ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) ↔ ( Fun ( ℝ D 𝐺 ) ∧ dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) ) )
59 9 57 58 sylanbrc ⊢ ( 𝜑 → ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) )
60 16 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( 𝐴 (,) 𝐵 ) )
61 9 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → Fun ( ℝ D 𝐺 ) )
62 funbrfv ⊢ ( Fun ( ℝ D 𝐺 ) → ( 𝑦 ( ℝ D 𝐺 ) ( 𝐹 ‘ 𝑦 ) → ( ( ℝ D 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) )
63 61 52 62 sylc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
64 59 60 63 eqfnfvd ⊢ ( 𝜑 → ( ℝ D 𝐺 ) = 𝐹 )