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