Step | Hyp | Ref
| Expression |
1 | | fourierdlem82.2 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | fourierdlem82.3 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | fourierdlem82.9 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℝ) |
4 | | fourierdlem82.4 |
. . . . . 6
⊢ (𝜑 → 𝐴 < 𝐵) |
5 | 1, 2, 4 | ltled 10064 |
. . . . 5
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
6 | 1, 2, 3, 5 | lesub1dd 10522 |
. . . 4
⊢ (𝜑 → (𝐴 − 𝑋) ≤ (𝐵 − 𝑋)) |
7 | 6 | ditgpos 23426 |
. . 3
⊢ (𝜑 → ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐺‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐴 − 𝑋)(,)(𝐵 − 𝑋))(𝐺‘(𝑋 + 𝑡)) d𝑡) |
8 | | fourierdlem82.1 |
. . . . . . 7
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))) |
9 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = 𝑅) |
10 | 9 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = 𝑅) |
11 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝑅) |
12 | 11 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝑅) |
13 | 10, 12 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
14 | 13 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
15 | | iffalse 4045 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) |
16 | | iftrue 4042 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = 𝐿) |
17 | 15, 16 | sylan9eq 2664 |
. . . . . . . . . . . 12
⊢ ((¬
𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = 𝐿) |
18 | 17 | adantll 746 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = 𝐿) |
19 | | iffalse 4045 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) |
20 | | iftrue 4042 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = 𝐿) |
21 | 19, 20 | sylan9eq 2664 |
. . . . . . . . . . . 12
⊢ ((¬
𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝐿) |
22 | 21 | adantll 746 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝐿) |
23 | 18, 22 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
24 | | iffalse 4045 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) |
25 | 24 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) |
26 | 15 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) |
27 | | iffalse 4045 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥)) |
28 | 27 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥)) |
29 | 19 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) |
30 | 1 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
31 | 30 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 ∈
ℝ*) |
32 | 2 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
33 | 32 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈
ℝ*) |
34 | 1 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
35 | 2 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
36 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) |
37 | | eliccre 38575 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
38 | 34, 35, 36, 37 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
39 | 38 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ℝ) |
40 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝐴 ∈ ℝ) |
41 | 38 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ ℝ) |
42 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
43 | 34, 35, 42 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
44 | 36, 43 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
45 | 44 | simp2d 1067 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝐴 ≤ 𝑥) |
47 | | neqne 2790 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 = 𝐴 → 𝑥 ≠ 𝐴) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ≠ 𝐴) |
49 | 40, 41, 46, 48 | leneltd 10070 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝐴 < 𝑥) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 < 𝑥) |
51 | 38 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ℝ) |
52 | 2 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ) |
53 | 44 | simp3d 1068 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ≤ 𝐵) |
55 | | nesym 2838 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ≠ 𝑥 ↔ ¬ 𝑥 = 𝐵) |
56 | 55 | biimpri 217 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 = 𝐵 → 𝐵 ≠ 𝑥) |
57 | 56 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ≠ 𝑥) |
58 | 51, 52, 54, 57 | leneltd 10070 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 < 𝐵) |
59 | 58 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 < 𝐵) |
60 | 31, 33, 39, 50, 59 | eliood 38567 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴(,)𝐵)) |
61 | | fvres 6117 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹‘𝑥)) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹‘𝑥)) |
63 | 28, 29, 62 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) |
64 | 25, 26, 63 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
65 | 23, 64 | pm2.61dan 828 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
66 | 14, 65 | pm2.61dan 828 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
67 | 66 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))) |
68 | 8, 67 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))) |
69 | 68 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))) |
70 | | eqeq1 2614 |
. . . . . . 7
⊢ (𝑥 = (𝑋 + 𝑡) → (𝑥 = 𝐴 ↔ (𝑋 + 𝑡) = 𝐴)) |
71 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑥 = (𝑋 + 𝑡) → (𝑥 = 𝐵 ↔ (𝑋 + 𝑡) = 𝐵)) |
72 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = (𝑋 + 𝑡) → (𝐹‘𝑥) = (𝐹‘(𝑋 + 𝑡))) |
73 | 71, 72 | ifbieq2d 4061 |
. . . . . . 7
⊢ (𝑥 = (𝑋 + 𝑡) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡)))) |
74 | 70, 73 | ifbieq2d 4061 |
. . . . . 6
⊢ (𝑥 = (𝑋 + 𝑡) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if((𝑋 + 𝑡) = 𝐴, 𝑅, if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡))))) |
75 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → 𝐴 ∈ ℝ) |
76 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) |
77 | 1, 3 | resubcld 10337 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ) |
78 | 77 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 − 𝑋) ∈
ℝ*) |
79 | 78 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝐴 − 𝑋) ∈
ℝ*) |
80 | 2, 3 | resubcld 10337 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ) |
81 | 80 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 − 𝑋) ∈
ℝ*) |
82 | 81 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈
ℝ*) |
83 | | elioo2 12087 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 − 𝑋) ∈ ℝ* ∧ (𝐵 − 𝑋) ∈ ℝ*) → (𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ (𝐴 − 𝑋) < 𝑡 ∧ 𝑡 < (𝐵 − 𝑋)))) |
84 | 79, 82, 83 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ (𝐴 − 𝑋) < 𝑡 ∧ 𝑡 < (𝐵 − 𝑋)))) |
85 | 76, 84 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝑡 ∈ ℝ ∧ (𝐴 − 𝑋) < 𝑡 ∧ 𝑡 < (𝐵 − 𝑋))) |
86 | 85 | simp2d 1067 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝐴 − 𝑋) < 𝑡) |
87 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → 𝑋 ∈ ℝ) |
88 | 85 | simp1d 1066 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → 𝑡 ∈ ℝ) |
89 | 75, 87, 88 | ltsubadd2d 10504 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → ((𝐴 − 𝑋) < 𝑡 ↔ 𝐴 < (𝑋 + 𝑡))) |
90 | 86, 89 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → 𝐴 < (𝑋 + 𝑡)) |
91 | 75, 90 | gtned 10051 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝑋 + 𝑡) ≠ 𝐴) |
92 | 91 | neneqd 2787 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → ¬ (𝑋 + 𝑡) = 𝐴) |
93 | 92 | iffalsed 4047 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → if((𝑋 + 𝑡) = 𝐴, 𝑅, if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡)))) = if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡)))) |
94 | 87, 88 | readdcld 9948 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝑋 + 𝑡) ∈ ℝ) |
95 | 85 | simp3d 1068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → 𝑡 < (𝐵 − 𝑋)) |
96 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → 𝐵 ∈ ℝ) |
97 | 87, 88, 96 | ltaddsub2d 10507 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → ((𝑋 + 𝑡) < 𝐵 ↔ 𝑡 < (𝐵 − 𝑋))) |
98 | 95, 97 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝑋 + 𝑡) < 𝐵) |
99 | 94, 98 | ltned 10052 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝑋 + 𝑡) ≠ 𝐵) |
100 | 99 | neneqd 2787 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → ¬ (𝑋 + 𝑡) = 𝐵) |
101 | 100 | iffalsed 4047 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡))) = (𝐹‘(𝑋 + 𝑡))) |
102 | 93, 101 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → if((𝑋 + 𝑡) = 𝐴, 𝑅, if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡)))) = (𝐹‘(𝑋 + 𝑡))) |
103 | 74, 102 | sylan9eqr 2666 |
. . . . 5
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) ∧ 𝑥 = (𝑋 + 𝑡)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = (𝐹‘(𝑋 + 𝑡))) |
104 | 75, 94, 90 | ltled 10064 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → 𝐴 ≤ (𝑋 + 𝑡)) |
105 | 94, 96, 98 | ltled 10064 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝑋 + 𝑡) ≤ 𝐵) |
106 | 75, 96, 94, 104, 105 | eliccd 38573 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝑋 + 𝑡) ∈ (𝐴[,]𝐵)) |
107 | | fourierdlem82.5 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
108 | | ffun 5961 |
. . . . . . . 8
⊢ (𝐹:(𝐴[,]𝐵)⟶ℂ → Fun 𝐹) |
109 | 107, 108 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Fun 𝐹) |
110 | 109 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → Fun 𝐹) |
111 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝐹:(𝐴[,]𝐵)⟶ℂ → dom 𝐹 = (𝐴[,]𝐵)) |
112 | 107, 111 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = (𝐴[,]𝐵)) |
113 | 112 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝜑 → (𝐴[,]𝐵) = dom 𝐹) |
114 | 113 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝐴[,]𝐵) = dom 𝐹) |
115 | 106, 114 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝑋 + 𝑡) ∈ dom 𝐹) |
116 | | fvelrn 6260 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ (𝑋 + 𝑡) ∈ dom 𝐹) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹) |
117 | 110, 115,
116 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹) |
118 | 69, 103, 106, 117 | fvmptd 6197 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)(,)(𝐵 − 𝑋))) → (𝐺‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡))) |
119 | 118 | itgeq2dv 23354 |
. . 3
⊢ (𝜑 → ∫((𝐴 − 𝑋)(,)(𝐵 − 𝑋))(𝐺‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐴 − 𝑋)(,)(𝐵 − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
120 | | frn 5966 |
. . . . . . 7
⊢ (𝐹:(𝐴[,]𝐵)⟶ℂ → ran 𝐹 ⊆
ℂ) |
121 | 107, 120 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
122 | 121 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → ran 𝐹 ⊆ ℂ) |
123 | 109 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → Fun 𝐹) |
124 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐴 ∈ ℝ) |
125 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐵 ∈ ℝ) |
126 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑋 ∈ ℝ) |
127 | 77 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ∈ ℝ) |
128 | 80 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ) |
129 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
130 | | eliccre 38575 |
. . . . . . . . . 10
⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑡 ∈ ℝ) |
131 | 127, 128,
129, 130 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑡 ∈ ℝ) |
132 | 126, 131 | readdcld 9948 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑡) ∈ ℝ) |
133 | | elicc2 12109 |
. . . . . . . . . . . 12
⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ) → (𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ (𝐵 − 𝑋)))) |
134 | 127, 128,
133 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ (𝐵 − 𝑋)))) |
135 | 129, 134 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑡 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ (𝐵 − 𝑋))) |
136 | 135 | simp2d 1067 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ≤ 𝑡) |
137 | 124, 126,
131 | lesubadd2d 10505 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → ((𝐴 − 𝑋) ≤ 𝑡 ↔ 𝐴 ≤ (𝑋 + 𝑡))) |
138 | 136, 137 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐴 ≤ (𝑋 + 𝑡)) |
139 | 135 | simp3d 1068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑡 ≤ (𝐵 − 𝑋)) |
140 | 126, 131,
125 | leaddsub2d 10508 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → ((𝑋 + 𝑡) ≤ 𝐵 ↔ 𝑡 ≤ (𝐵 − 𝑋))) |
141 | 139, 140 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑡) ≤ 𝐵) |
142 | 124, 125,
132, 138, 141 | eliccd 38573 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑡) ∈ (𝐴[,]𝐵)) |
143 | 113 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴[,]𝐵) = dom 𝐹) |
144 | 142, 143 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑡) ∈ dom 𝐹) |
145 | 123, 144,
116 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹) |
146 | 122, 145 | sseldd 3569 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ) |
147 | 77, 80, 146 | itgioo 23388 |
. . 3
⊢ (𝜑 → ∫((𝐴 − 𝑋)(,)(𝐵 − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
148 | 7, 119, 147 | 3eqtrrd 2649 |
. 2
⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐺‘(𝑋 + 𝑡)) d𝑡) |
149 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑥𝜑 |
150 | | fourierdlem82.6 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
151 | | fourierdlem82.7 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) |
152 | 1, 2, 4, 107 | limcicciooub 38704 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵) = (𝐹 limℂ 𝐵)) |
153 | 151, 152 | eleqtrrd 2691 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵)) |
154 | | fourierdlem82.8 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴)) |
155 | 1, 2, 4, 107 | limciccioolb 38688 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐴) = (𝐹 limℂ 𝐴)) |
156 | 154, 155 | eleqtrrd 2691 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐴)) |
157 | 149, 8, 1, 2, 150, 153, 156 | cncfiooicc 38780 |
. . 3
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
158 | 1, 2, 5, 3, 157 | itgsbtaddcnst 38874 |
. 2
⊢ (𝜑 → ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐺‘(𝑋 + 𝑡)) d𝑡 = ⨜[𝐴 → 𝐵](𝐺‘𝑠) d𝑠) |
159 | 5 | ditgpos 23426 |
. . 3
⊢ (𝜑 → ⨜[𝐴 → 𝐵](𝐺‘𝑠) d𝑠 = ∫(𝐴(,)𝐵)(𝐺‘𝑠) d𝑠) |
160 | | fveq2 6103 |
. . . . 5
⊢ (𝑠 = 𝑡 → (𝐺‘𝑠) = (𝐺‘𝑡)) |
161 | 160 | cbvitgv 23349 |
. . . 4
⊢
∫(𝐴(,)𝐵)(𝐺‘𝑠) d𝑠 = ∫(𝐴(,)𝐵)(𝐺‘𝑡) d𝑡 |
162 | 8 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))) |
163 | 1 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝐴 ∈ ℝ) |
164 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑡 ∈ (𝐴(,)𝐵)) |
165 | 30 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝐴 ∈
ℝ*) |
166 | 32 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝐵 ∈
ℝ*) |
167 | | elioo2 12087 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑡 ∈ (𝐴(,)𝐵) ↔ (𝑡 ∈ ℝ ∧ 𝐴 < 𝑡 ∧ 𝑡 < 𝐵))) |
168 | 165, 166,
167 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → (𝑡 ∈ (𝐴(,)𝐵) ↔ (𝑡 ∈ ℝ ∧ 𝐴 < 𝑡 ∧ 𝑡 < 𝐵))) |
169 | 164, 168 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → (𝑡 ∈ ℝ ∧ 𝐴 < 𝑡 ∧ 𝑡 < 𝐵)) |
170 | 169 | simp2d 1067 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝐴 < 𝑡) |
171 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥 = 𝑡) |
172 | 170, 171 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝐴 < 𝑥) |
173 | 163, 172 | gtned 10051 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥 ≠ 𝐴) |
174 | 173 | neneqd 2787 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → ¬ 𝑥 = 𝐴) |
175 | 174 | iffalsed 4047 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) |
176 | 169 | simp1d 1066 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑡 ∈ ℝ) |
177 | 171, 176 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥 ∈ ℝ) |
178 | 169 | simp3d 1068 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑡 < 𝐵) |
179 | 171, 178 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥 < 𝐵) |
180 | 177, 179 | ltned 10052 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥 ≠ 𝐵) |
181 | 180 | neneqd 2787 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → ¬ 𝑥 = 𝐵) |
182 | 181 | iffalsed 4047 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) |
183 | 171, 164 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥 ∈ (𝐴(,)𝐵)) |
184 | 183, 61 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹‘𝑥)) |
185 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡)) |
186 | 185 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → (𝐹‘𝑥) = (𝐹‘𝑡)) |
187 | 184, 186 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹‘𝑡)) |
188 | 175, 182,
187 | 3eqtrd 2648 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = (𝐹‘𝑡)) |
189 | | ioossicc 12130 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
190 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ (𝐴(,)𝐵)) |
191 | 189, 190 | sseldi 3566 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ (𝐴[,]𝐵)) |
192 | 109 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → Fun 𝐹) |
193 | 113 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) = dom 𝐹) |
194 | 191, 193 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ dom 𝐹) |
195 | | fvelrn 6260 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑡 ∈ dom 𝐹) → (𝐹‘𝑡) ∈ ran 𝐹) |
196 | 192, 194,
195 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑡) ∈ ran 𝐹) |
197 | 162, 188,
191, 196 | fvmptd 6197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑡) = (𝐹‘𝑡)) |
198 | 197 | itgeq2dv 23354 |
. . . 4
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐺‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)(𝐹‘𝑡) d𝑡) |
199 | 161, 198 | syl5eq 2656 |
. . 3
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐺‘𝑠) d𝑠 = ∫(𝐴(,)𝐵)(𝐹‘𝑡) d𝑡) |
200 | 107 | ffvelrnda 6267 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑡) ∈ ℂ) |
201 | 1, 2, 200 | itgioo 23388 |
. . 3
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐹‘𝑡) d𝑡 = ∫(𝐴[,]𝐵)(𝐹‘𝑡) d𝑡) |
202 | 159, 199,
201 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → ⨜[𝐴 → 𝐵](𝐺‘𝑠) d𝑠 = ∫(𝐴[,]𝐵)(𝐹‘𝑡) d𝑡) |
203 | 148, 158,
202 | 3eqtrrd 2649 |
1
⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝐹‘𝑡) d𝑡 = ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |