Metamath Proof Explorer

Theorem fourierdlem82

Description: Integral by substitution, adding a constant to the function's argument, for a function on an open interval with finite limits ad boundary points. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem82.1 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
fourierdlem82.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem82.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem82.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem82.5 ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
fourierdlem82.6 ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
fourierdlem82.7 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
fourierdlem82.8 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 limℂ 𝐴 ) )
fourierdlem82.9 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
Assertion fourierdlem82 ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )

Proof

Step Hyp Ref Expression
1 fourierdlem82.1 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) )
2 fourierdlem82.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 fourierdlem82.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 fourierdlem82.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
5 fourierdlem82.5 ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
6 fourierdlem82.6 ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
7 fourierdlem82.7 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
8 fourierdlem82.8 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 limℂ 𝐴 ) )
9 fourierdlem82.9 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
10 2 3 4 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
11 2 3 9 10 lesub1dd ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ≤ ( 𝐵 − 𝑋 ) )
12 11 ditgpos ⊢ ( 𝜑 → ⨜ [ ( 𝐴 − 𝑋 ) → ( 𝐵 − 𝑋 ) ] ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ∫ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
13 iftrue ⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = 𝑅 )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = 𝑅 )
15 iftrue ⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
17 14 16 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
18 17 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
19 iffalse ⊢ ( ¬ 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
20 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = 𝐿 )
21 19 20 sylan9eq ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = 𝐿 )
22 21 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = 𝐿 )
23 iffalse ⊢ ( ¬ 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
24 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = 𝐿 )
25 23 24 sylan9eq ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝐿 )
26 25 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝐿 )
27 22 26 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
28 iffalse ⊢ ( ¬ 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
29 28 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
30 19 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
31 iffalse ⊢ ( ¬ 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
32 31 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
33 23 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
34 2 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
35 34 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 ∈ ℝ* )
36 3 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
37 36 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ* )
38 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ )
39 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
40 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
41 eliccre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
42 38 39 40 41 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
43 42 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ℝ )
44 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 ∈ ℝ )
45 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ∈ ℝ )
46 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
47 38 39 46 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
48 40 47 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
49 48 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑥 )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 ≤ 𝑥 )
51 neqne ⊢ ( ¬ 𝑥 = 𝐴 → 𝑥 ≠ 𝐴 )
52 51 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ≠ 𝐴 )
53 44 45 50 52 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 < 𝑥 )
54 53 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 < 𝑥 )
55 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ℝ )
56 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ )
57 48 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ≤ 𝐵 )
59 nesym ⊢ ( 𝐵 ≠ 𝑥 ↔ ¬ 𝑥 = 𝐵 )
60 59 bilanri ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ≠ 𝑥 )
61 55 56 58 60 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 < 𝐵 )
62 61 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 < 𝐵 )
63 35 37 43 54 62 eliood ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
64 fvres ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
65 63 64 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
66 32 33 65 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
67 29 30 66 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
68 27 67 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
69 18 68 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
70 69 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
71 1 70 eqtrid ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
73 eqeq1 ⊢ ( 𝑥 = ( 𝑋 + 𝑡 ) → ( 𝑥 = 𝐴 ↔ ( 𝑋 + 𝑡 ) = 𝐴 ) )
74 eqeq1 ⊢ ( 𝑥 = ( 𝑋 + 𝑡 ) → ( 𝑥 = 𝐵 ↔ ( 𝑋 + 𝑡 ) = 𝐵 ) )
75 fveq2 ⊢ ( 𝑥 = ( 𝑋 + 𝑡 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
76 74 75 ifbieq2d ⊢ ( 𝑥 = ( 𝑋 + 𝑡 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) )
77 73 76 ifbieq2d ⊢ ( 𝑥 = ( 𝑋 + 𝑡 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( ( 𝑋 + 𝑡 ) = 𝐴 , 𝑅 , if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) ) )
78 2 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝐴 ∈ ℝ )
79 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) )
80 2 9 resubcld ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ∈ ℝ )
81 80 rexrd ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ∈ ℝ* )
82 81 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ* )
83 3 9 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ )
84 83 rexrd ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ* )
85 84 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐵 − 𝑋 ) ∈ ℝ* )
86 elioo2 ⊢ ( ( ( 𝐴 − 𝑋 ) ∈ ℝ* ∧ ( 𝐵 − 𝑋 ) ∈ ℝ* ) → ( 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) < 𝑡 ∧ 𝑡 < ( 𝐵 − 𝑋 ) ) ) )
87 82 85 86 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) < 𝑡 ∧ 𝑡 < ( 𝐵 − 𝑋 ) ) ) )
88 79 87 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) < 𝑡 ∧ 𝑡 < ( 𝐵 − 𝑋 ) ) )
89 88 simp2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) < 𝑡 )
90 9 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝑋 ∈ ℝ )
91 88 simp1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝑡 ∈ ℝ )
92 78 90 91 ltsubadd2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( ( 𝐴 − 𝑋 ) < 𝑡 ↔ 𝐴 < ( 𝑋 + 𝑡 ) ) )
93 89 92 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝐴 < ( 𝑋 + 𝑡 ) )
94 78 93 gtned ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ≠ 𝐴 )
95 94 neneqd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ¬ ( 𝑋 + 𝑡 ) = 𝐴 )
96 95 iffalsed ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → if ( ( 𝑋 + 𝑡 ) = 𝐴 , 𝑅 , if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) ) = if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) )
97 90 91 readdcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ℝ )
98 88 simp3d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝑡 < ( 𝐵 − 𝑋 ) )
99 3 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝐵 ∈ ℝ )
100 90 91 99 ltaddsub2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( ( 𝑋 + 𝑡 ) < 𝐵 ↔ 𝑡 < ( 𝐵 − 𝑋 ) ) )
101 98 100 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) < 𝐵 )
102 97 101 ltned ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ≠ 𝐵 )
103 102 neneqd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ¬ ( 𝑋 + 𝑡 ) = 𝐵 )
104 103 iffalsed ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
105 96 104 eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → if ( ( 𝑋 + 𝑡 ) = 𝐴 , 𝑅 , if ( ( 𝑋 + 𝑡 ) = 𝐵 , 𝐿 , ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
106 77 105 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) ∧ 𝑥 = ( 𝑋 + 𝑡 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
107 78 97 93 ltled ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → 𝐴 ≤ ( 𝑋 + 𝑡 ) )
108 97 99 101 ltled ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ≤ 𝐵 )
109 78 99 97 107 108 eliccd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ( 𝐴 [,] 𝐵 ) )
110 5 ffund ⊢ ( 𝜑 → Fun 𝐹 )
111 110 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → Fun 𝐹 )
112 5 fdmd ⊢ ( 𝜑 → dom 𝐹 = ( 𝐴 [,] 𝐵 ) )
113 112 eqcomd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
114 113 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
115 109 114 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ dom 𝐹 )
116 fvelrn ⊢ ( ( Fun 𝐹 ∧ ( 𝑋 + 𝑡 ) ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ran 𝐹 )
117 111 115 116 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ran 𝐹 )
118 72 106 109 117 fvmptd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ) → ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
119 118 itgeq2dv ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ∫ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
120 5 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℂ )
121 120 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ran 𝐹 ⊆ ℂ )
122 110 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → Fun 𝐹 )
123 2 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝐴 ∈ ℝ )
124 3 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝐵 ∈ ℝ )
125 9 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑋 ∈ ℝ )
126 80 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
127 83 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
128 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) )
129 eliccre ⊢ ( ( ( 𝐴 − 𝑋 ) ∈ ℝ ∧ ( 𝐵 − 𝑋 ) ∈ ℝ ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑡 ∈ ℝ )
130 126 127 128 129 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑡 ∈ ℝ )
131 125 130 readdcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ℝ )
132 elicc2 ⊢ ( ( ( 𝐴 − 𝑋 ) ∈ ℝ ∧ ( 𝐵 − 𝑋 ) ∈ ℝ ) → ( 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝐵 − 𝑋 ) ) ) )
133 126 127 132 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝐵 − 𝑋 ) ) ) )
134 128 133 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑡 ∈ ℝ ∧ ( 𝐴 − 𝑋 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝐵 − 𝑋 ) ) )
135 134 simp2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) ≤ 𝑡 )
136 123 125 130 lesubadd2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( ( 𝐴 − 𝑋 ) ≤ 𝑡 ↔ 𝐴 ≤ ( 𝑋 + 𝑡 ) ) )
137 135 136 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝐴 ≤ ( 𝑋 + 𝑡 ) )
138 134 simp3d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑡 ≤ ( 𝐵 − 𝑋 ) )
139 125 130 124 leaddsub2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( ( 𝑋 + 𝑡 ) ≤ 𝐵 ↔ 𝑡 ≤ ( 𝐵 − 𝑋 ) ) )
140 138 139 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ≤ 𝐵 )
141 123 124 131 137 140 eliccd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ( 𝐴 [,] 𝐵 ) )
142 113 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
143 141 142 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ dom 𝐹 )
144 122 143 116 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ran 𝐹 )
145 121 144 sseldd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ℂ )
146 80 83 145 itgioo ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) (,) ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
147 12 119 146 3eqtrrd ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ⨜ [ ( 𝐴 − 𝑋 ) → ( 𝐵 − 𝑋 ) ] ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
148 nfv ⊢ Ⅎ 𝑥 𝜑
149 2 3 4 5 limcicciooub ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) = ( 𝐹 limℂ 𝐵 ) )
150 7 149 eleqtrrd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) )
151 2 3 4 5 limciccioolb ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) = ( 𝐹 limℂ 𝐴 ) )
152 8 151 eleqtrrd ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐴 ) )
153 148 1 2 3 6 150 152 cncfiooicc ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
154 2 3 10 9 153 itgsbtaddcnst ⊢ ( 𝜑 → ⨜ [ ( 𝐴 − 𝑋 ) → ( 𝐵 − 𝑋 ) ] ( 𝐺 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ⨜ [ 𝐴 → 𝐵 ] ( 𝐺 ‘ 𝑠 ) d 𝑠 )
155 10 ditgpos ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( 𝐺 ‘ 𝑠 ) d 𝑠 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑠 ) d 𝑠 )
156 fveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑡 ) )
157 156 cbvitgv ⊢ ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑠 ) d 𝑠 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑡 ) d 𝑡
158 1 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) ) )
159 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝐴 ∈ ℝ )
160 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑡 ∈ ( 𝐴 (,) 𝐵 ) )
161 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝐴 ∈ ℝ* )
162 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝐵 ∈ ℝ* )
163 elioo2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 < 𝑡 ∧ 𝑡 < 𝐵 ) ) )
164 161 162 163 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 < 𝑡 ∧ 𝑡 < 𝐵 ) ) )
165 160 164 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ( 𝑡 ∈ ℝ ∧ 𝐴 < 𝑡 ∧ 𝑡 < 𝐵 ) )
166 165 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝐴 < 𝑡 )
167 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 = 𝑡 )
168 166 167 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝐴 < 𝑥 )
169 159 168 gtned ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 ≠ 𝐴 )
170 169 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ¬ 𝑥 = 𝐴 )
171 170 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) )
172 165 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑡 ∈ ℝ )
173 167 172 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 ∈ ℝ )
174 165 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑡 < 𝐵 )
175 167 174 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 < 𝐵 )
176 173 175 ltned ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 ≠ 𝐵 )
177 176 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ¬ 𝑥 = 𝐵 )
178 177 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) )
179 167 160 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
180 179 64 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
181 fveq2 ⊢ ( 𝑥 = 𝑡 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑡 ) )
182 181 adantl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑡 ) )
183 180 182 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑡 ) )
184 171 178 183 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑥 = 𝑡 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑡 ) )
185 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
186 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑡 ∈ ( 𝐴 (,) 𝐵 ) )
187 185 186 sselid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑡 ∈ ( 𝐴 [,] 𝐵 ) )
188 110 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → Fun 𝐹 )
189 113 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
190 187 189 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑡 ∈ dom 𝐹 )
191 fvelrn ⊢ ( ( Fun 𝐹 ∧ 𝑡 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑡 ) ∈ ran 𝐹 )
192 188 190 191 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ran 𝐹 )
193 158 184 187 192 fvmptd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
194 193 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
195 157 194 eqtrid ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑠 ) d 𝑠 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
196 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
197 2 3 196 itgioo ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
198 155 195 197 3eqtrd ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( 𝐺 ‘ 𝑠 ) d 𝑠 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
199 147 154 198 3eqtrrd ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )