Metamath Proof Explorer

Theorem itgioocnicc

Description: The integral of a piecewise continuous function F on an open interval is equal to the integral of the continuous function G , in the corresponding closed interval. G is equal to F on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgioocnicc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
itgioocnicc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
itgioocnicc.f ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
itgioocnicc.fcn ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
itgioocnicc.fdom ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 )
itgioocnicc.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) )
itgioocnicc.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) )
itgioocnicc.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
Assertion itgioocnicc ( 𝜑 → ( 𝐺 ∈ 𝐿1 ∧ ∫ ( 𝐴 [,] 𝐵 ) ( 𝐺 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 itgioocnicc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 itgioocnicc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 itgioocnicc.f ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
4 itgioocnicc.fcn ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
5 itgioocnicc.fdom ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 )
6 itgioocnicc.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) )
7 itgioocnicc.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) )
8 itgioocnicc.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
9 iftrue ⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
10 iftrue ⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = 𝑅 )
11 9 10 eqtr4d ⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
12 11 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
13 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = 𝐿 )
14 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = 𝐿 )
15 13 14 eqtr4d ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
16 15 adantl ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
17 16 ifeq2d ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
18 17 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
19 iffalse ⊢ ( ¬ 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
20 19 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
21 iffalse ⊢ ( ¬ 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
22 21 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
23 iffalse ⊢ ( ¬ 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
24 23 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
25 iffalse ⊢ ( ¬ 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
26 25 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
27 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ )
28 27 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ* )
29 28 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 ∈ ℝ* )
30 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
31 30 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ* )
32 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
34 eliccre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
35 27 32 33 34 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
36 35 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ℝ )
37 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 ∈ ℝ )
38 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ∈ ℝ )
39 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ* )
40 iccgelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑥 )
41 28 39 33 40 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑥 )
42 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 ≤ 𝑥 )
43 neqne ⊢ ( ¬ 𝑥 = 𝐴 → 𝑥 ≠ 𝐴 )
44 43 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ≠ 𝐴 )
45 37 38 42 44 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 < 𝑥 )
46 45 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 < 𝑥 )
47 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ℝ )
48 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ )
49 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
50 28 39 33 49 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
51 50 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ≤ 𝐵 )
52 eqcom ⊢ ( 𝑥 = 𝐵 ↔ 𝐵 = 𝑥 )
53 52 notbii ⊢ ( ¬ 𝑥 = 𝐵 ↔ ¬ 𝐵 = 𝑥 )
54 53 biimpi ⊢ ( ¬ 𝑥 = 𝐵 → ¬ 𝐵 = 𝑥 )
55 54 neqned ⊢ ( ¬ 𝑥 = 𝐵 → 𝐵 ≠ 𝑥 )
56 55 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ≠ 𝑥 )
57 47 48 51 56 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 < 𝐵 )
58 57 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 < 𝐵 )
59 29 31 36 46 58 eliood ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
60 fvres ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
61 59 60 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
62 24 26 61 3eqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
63 20 22 62 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
64 18 63 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
65 12 64 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
66 65 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) ) )
67 8 66 syl5eq ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) ) )
68 nfv ⊢ Ⅎ 𝑥 𝜑
69 eqid ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
70 68 69 1 2 4 7 6 cncfiooicc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
71 67 70 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
72 cniccibl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐺 ∈ 𝐿1 )
73 1 2 71 72 syl3anc ⊢ ( 𝜑 → 𝐺 ∈ 𝐿1 )
74 9 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
75 limccl ⊢ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) ⊆ ℂ
76 75 6 sseldi ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
77 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑥 = 𝐴 ) → 𝑅 ∈ ℂ )
78 74 77 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℂ )
79 19 13 sylan9eq ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝐿 )
80 79 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝐿 )
81 limccl ⊢ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) ⊆ ℂ
82 81 7 sseldi ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
83 82 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → 𝐿 ∈ ℂ )
84 80 83 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℂ )
85 19 21 sylan9eq ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
86 85 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
87 61 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
88 cncff ⊢ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
89 4 88 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
90 89 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
91 90 59 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ∈ ℂ )
92 87 91 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
93 86 92 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℂ )
94 84 93 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℂ )
95 78 94 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℂ )
96 8 fvmpt2 ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
97 33 95 96 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
98 97 95 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
99 1 2 98 itgioo ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐺 ‘ 𝑥 ) d 𝑥 )
100 99 eqcomd ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐺 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑥 ) d 𝑥 )
101 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
102 101 sseli ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
103 102 97 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
104 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
105 eliooord ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
106 105 simpld ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝐴 < 𝑥 )
107 106 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑥 )
108 104 107 gtned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ≠ 𝐴 )
109 108 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 = 𝐴 )
110 109 19 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
111 102 35 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℝ )
112 105 simprd ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 < 𝐵 )
113 112 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 < 𝐵 )
114 111 113 ltned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ≠ 𝐵 )
115 114 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 = 𝐵 )
116 115 21 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
117 103 110 116 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
118 117 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
119 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
120 5 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ dom 𝐹 )
121 119 120 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
122 1 2 121 itgioo ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
123 100 118 122 3eqtrd ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐺 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
124 73 123 jca ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐿1 ∧ ∫ ( 𝐴 [,] 𝐵 ) ( 𝐺 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )