Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem82 Structured version   Visualization version   GIF version

Theorem fourierdlem82 42761
 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.)
Hypotheses
Ref Expression
fourierdlem82.1 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
fourierdlem82.2 (𝜑𝐴 ∈ ℝ)
fourierdlem82.3 (𝜑𝐵 ∈ ℝ)
fourierdlem82.4 (𝜑𝐴 < 𝐵)
fourierdlem82.5 (𝜑𝐹:(𝐴[,]𝐵)⟶ℂ)
fourierdlem82.6 (𝜑 → (𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
fourierdlem82.7 (𝜑𝐿 ∈ (𝐹 lim 𝐵))
fourierdlem82.8 (𝜑𝑅 ∈ (𝐹 lim 𝐴))
fourierdlem82.9 (𝜑𝑋 ∈ ℝ)
Assertion
Ref Expression
fourierdlem82 (𝜑 → ∫(𝐴[,]𝐵)(𝐹𝑡) d𝑡 = ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
Distinct variable groups:   𝑡,𝐴,𝑥   𝑡,𝐵,𝑥   𝑥,𝐹   𝑡,𝐺   𝑥,𝐿   𝑥,𝑅   𝑡,𝑋,𝑥   𝜑,𝑡,𝑥
Allowed substitution hints:   𝑅(𝑡)   𝐹(𝑡)   𝐺(𝑥)   𝐿(𝑡)

Proof of Theorem fourierdlem82
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem82.2 . . . . 5 (𝜑𝐴 ∈ ℝ)
2 fourierdlem82.3 . . . . 5 (𝜑𝐵 ∈ ℝ)
3 fourierdlem82.9 . . . . 5 (𝜑𝑋 ∈ ℝ)
4 fourierdlem82.4 . . . . . 6 (𝜑𝐴 < 𝐵)
51, 2, 4ltled 10786 . . . . 5 (𝜑𝐴𝐵)
61, 2, 3, 5lesub1dd 11254 . . . 4 (𝜑 → (𝐴𝑋) ≤ (𝐵𝑋))
76ditgpos 24466 . . 3 (𝜑 → ⨜[(𝐴𝑋) → (𝐵𝑋)](𝐺‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐴𝑋)(,)(𝐵𝑋))(𝐺‘(𝑋 + 𝑡)) d𝑡)
8 fourierdlem82.1 . . . . . . 7 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
9 iftrue 4456 . . . . . . . . . . . 12 (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = 𝑅)
109adantl 485 . . . . . . . . . . 11 ((𝜑𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = 𝑅)
11 iftrue 4456 . . . . . . . . . . . 12 (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = 𝑅)
1211adantl 485 . . . . . . . . . . 11 ((𝜑𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = 𝑅)
1310, 12eqtr4d 2862 . . . . . . . . . 10 ((𝜑𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
1413adantlr 714 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
15 iffalse 4459 . . . . . . . . . . . . 13 𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))
16 iftrue 4456 . . . . . . . . . . . . 13 (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = 𝐿)
1715, 16sylan9eq 2879 . . . . . . . . . . . 12 ((¬ 𝑥 = 𝐴𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = 𝐿)
1817adantll 713 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = 𝐿)
19 iffalse 4459 . . . . . . . . . . . . 13 𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
20 iftrue 4456 . . . . . . . . . . . . 13 (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = 𝐿)
2119, 20sylan9eq 2879 . . . . . . . . . . . 12 ((¬ 𝑥 = 𝐴𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = 𝐿)
2221adantll 713 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = 𝐿)
2318, 22eqtr4d 2862 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
24 iffalse 4459 . . . . . . . . . . . 12 𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))
2524adantl 485 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))
2615ad2antlr 726 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))
27 iffalse 4459 . . . . . . . . . . . . 13 𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = (𝐹𝑥))
2827adantl 485 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = (𝐹𝑥))
2919ad2antlr 726 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))
301rexrd 10689 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ*)
3130ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 ∈ ℝ*)
322rexrd 10689 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℝ*)
3332ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ*)
341adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
352adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
36 simpr 488 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
37 eliccre 42073 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
3834, 35, 36, 37syl3anc 1368 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
3938ad2antrr 725 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ℝ)
401ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝐴 ∈ ℝ)
4138adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ ℝ)
42 elicc2 12799 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
4334, 35, 42syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
4436, 43mpbid 235 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵))
4544simp2d 1140 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐴𝑥)
4645adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝐴𝑥)
47 neqne 3022 . . . . . . . . . . . . . . . . 17 𝑥 = 𝐴𝑥𝐴)
4847adantl 485 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝑥𝐴)
4940, 41, 46, 48leneltd 10792 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝐴 < 𝑥)
5049adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 < 𝑥)
5138adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ℝ)
522ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ)
5344simp3d 1141 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝑥𝐵)
5453adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝑥𝐵)
55 nesym 3070 . . . . . . . . . . . . . . . . . 18 (𝐵𝑥 ↔ ¬ 𝑥 = 𝐵)
5655biimpri 231 . . . . . . . . . . . . . . . . 17 𝑥 = 𝐵𝐵𝑥)
5756adantl 485 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝐵𝑥)
5851, 52, 54, 57leneltd 10792 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 < 𝐵)
5958adantlr 714 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 < 𝐵)
6031, 33, 39, 50, 59eliood 42066 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴(,)𝐵))
61 fvres 6680 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴(,)𝐵) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹𝑥))
6260, 61syl 17 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹𝑥))
6328, 29, 623eqtr4d 2869 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))
6425, 26, 633eqtr4d 2869 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
6523, 64pm2.61dan 812 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
6614, 65pm2.61dan 812 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))))
6766mpteq2dva 5147 . . . . . . 7 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))))
688, 67syl5eq 2871 . . . . . 6 (𝜑𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))))
6968adantr 484 . . . . 5 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)))))
70 eqeq1 2828 . . . . . . 7 (𝑥 = (𝑋 + 𝑡) → (𝑥 = 𝐴 ↔ (𝑋 + 𝑡) = 𝐴))
71 eqeq1 2828 . . . . . . . 8 (𝑥 = (𝑋 + 𝑡) → (𝑥 = 𝐵 ↔ (𝑋 + 𝑡) = 𝐵))
72 fveq2 6661 . . . . . . . 8 (𝑥 = (𝑋 + 𝑡) → (𝐹𝑥) = (𝐹‘(𝑋 + 𝑡)))
7371, 72ifbieq2d 4475 . . . . . . 7 (𝑥 = (𝑋 + 𝑡) → if(𝑥 = 𝐵, 𝐿, (𝐹𝑥)) = if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡))))
7470, 73ifbieq2d 4475 . . . . . 6 (𝑥 = (𝑋 + 𝑡) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = if((𝑋 + 𝑡) = 𝐴, 𝑅, if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡)))))
751adantr 484 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → 𝐴 ∈ ℝ)
76 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → 𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋)))
771, 3resubcld 11066 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝑋) ∈ ℝ)
7877rexrd 10689 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝑋) ∈ ℝ*)
7978adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝐴𝑋) ∈ ℝ*)
802, 3resubcld 11066 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝑋) ∈ ℝ)
8180rexrd 10689 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵𝑋) ∈ ℝ*)
8281adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝐵𝑋) ∈ ℝ*)
83 elioo2 12776 . . . . . . . . . . . . . 14 (((𝐴𝑋) ∈ ℝ* ∧ (𝐵𝑋) ∈ ℝ*) → (𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋)) ↔ (𝑡 ∈ ℝ ∧ (𝐴𝑋) < 𝑡𝑡 < (𝐵𝑋))))
8479, 82, 83syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋)) ↔ (𝑡 ∈ ℝ ∧ (𝐴𝑋) < 𝑡𝑡 < (𝐵𝑋))))
8576, 84mpbid 235 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝑡 ∈ ℝ ∧ (𝐴𝑋) < 𝑡𝑡 < (𝐵𝑋)))
8685simp2d 1140 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝐴𝑋) < 𝑡)
873adantr 484 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → 𝑋 ∈ ℝ)
8885simp1d 1139 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → 𝑡 ∈ ℝ)
8975, 87, 88ltsubadd2d 11236 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → ((𝐴𝑋) < 𝑡𝐴 < (𝑋 + 𝑡)))
9086, 89mpbid 235 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → 𝐴 < (𝑋 + 𝑡))
9175, 90gtned 10773 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝑋 + 𝑡) ≠ 𝐴)
9291neneqd 3019 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → ¬ (𝑋 + 𝑡) = 𝐴)
9392iffalsed 4461 . . . . . . 7 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → if((𝑋 + 𝑡) = 𝐴, 𝑅, if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡)))) = if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡))))
9487, 88readdcld 10668 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝑋 + 𝑡) ∈ ℝ)
9585simp3d 1141 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → 𝑡 < (𝐵𝑋))
962adantr 484 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → 𝐵 ∈ ℝ)
9787, 88, 96ltaddsub2d 11239 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → ((𝑋 + 𝑡) < 𝐵𝑡 < (𝐵𝑋)))
9895, 97mpbird 260 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝑋 + 𝑡) < 𝐵)
9994, 98ltned 10774 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝑋 + 𝑡) ≠ 𝐵)
10099neneqd 3019 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → ¬ (𝑋 + 𝑡) = 𝐵)
101100iffalsed 4461 . . . . . . 7 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡))) = (𝐹‘(𝑋 + 𝑡)))
10293, 101eqtrd 2859 . . . . . 6 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → if((𝑋 + 𝑡) = 𝐴, 𝑅, if((𝑋 + 𝑡) = 𝐵, 𝐿, (𝐹‘(𝑋 + 𝑡)))) = (𝐹‘(𝑋 + 𝑡)))
10374, 102sylan9eqr 2881 . . . . 5 (((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) ∧ 𝑥 = (𝑋 + 𝑡)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹𝑥))) = (𝐹‘(𝑋 + 𝑡)))
10475, 94, 90ltled 10786 . . . . . 6 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → 𝐴 ≤ (𝑋 + 𝑡))
10594, 96, 98ltled 10786 . . . . . 6 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝑋 + 𝑡) ≤ 𝐵)
10675, 96, 94, 104, 105eliccd 42072 . . . . 5 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝑋 + 𝑡) ∈ (𝐴[,]𝐵))
107 fourierdlem82.5 . . . . . . . 8 (𝜑𝐹:(𝐴[,]𝐵)⟶ℂ)
108107ffund 6507 . . . . . . 7 (𝜑 → Fun 𝐹)
109108adantr 484 . . . . . 6 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → Fun 𝐹)
110107fdmd 6513 . . . . . . . . 9 (𝜑 → dom 𝐹 = (𝐴[,]𝐵))
111110eqcomd 2830 . . . . . . . 8 (𝜑 → (𝐴[,]𝐵) = dom 𝐹)
112111adantr 484 . . . . . . 7 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝐴[,]𝐵) = dom 𝐹)
113106, 112eleqtrd 2918 . . . . . 6 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝑋 + 𝑡) ∈ dom 𝐹)
114 fvelrn 6835 . . . . . 6 ((Fun 𝐹 ∧ (𝑋 + 𝑡) ∈ dom 𝐹) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
115109, 113, 114syl2anc 587 . . . . 5 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
11669, 103, 106, 115fvmptd 6766 . . . 4 ((𝜑𝑡 ∈ ((𝐴𝑋)(,)(𝐵𝑋))) → (𝐺‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
117116itgeq2dv 24392 . . 3 (𝜑 → ∫((𝐴𝑋)(,)(𝐵𝑋))(𝐺‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐴𝑋)(,)(𝐵𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
118107frnd 6510 . . . . . 6 (𝜑 → ran 𝐹 ⊆ ℂ)
119118adantr 484 . . . . 5 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → ran 𝐹 ⊆ ℂ)
120108adantr 484 . . . . . 6 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → Fun 𝐹)
1211adantr 484 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝐴 ∈ ℝ)
1222adantr 484 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝐵 ∈ ℝ)
1233adantr 484 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑋 ∈ ℝ)
12477adantr 484 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐴𝑋) ∈ ℝ)
12580adantr 484 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐵𝑋) ∈ ℝ)
126 simpr 488 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋)))
127 eliccre 42073 . . . . . . . . . 10 (((𝐴𝑋) ∈ ℝ ∧ (𝐵𝑋) ∈ ℝ ∧ 𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑡 ∈ ℝ)
128124, 125, 126, 127syl3anc 1368 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑡 ∈ ℝ)
129123, 128readdcld 10668 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝑋 + 𝑡) ∈ ℝ)
130 elicc2 12799 . . . . . . . . . . . 12 (((𝐴𝑋) ∈ ℝ ∧ (𝐵𝑋) ∈ ℝ) → (𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋)) ↔ (𝑡 ∈ ℝ ∧ (𝐴𝑋) ≤ 𝑡𝑡 ≤ (𝐵𝑋))))
131124, 125, 130syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋)) ↔ (𝑡 ∈ ℝ ∧ (𝐴𝑋) ≤ 𝑡𝑡 ≤ (𝐵𝑋))))
132126, 131mpbid 235 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝑡 ∈ ℝ ∧ (𝐴𝑋) ≤ 𝑡𝑡 ≤ (𝐵𝑋)))
133132simp2d 1140 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐴𝑋) ≤ 𝑡)
134121, 123, 128lesubadd2d 11237 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → ((𝐴𝑋) ≤ 𝑡𝐴 ≤ (𝑋 + 𝑡)))
135133, 134mpbid 235 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝐴 ≤ (𝑋 + 𝑡))
136132simp3d 1141 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑡 ≤ (𝐵𝑋))
137123, 128, 122leaddsub2d 11240 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → ((𝑋 + 𝑡) ≤ 𝐵𝑡 ≤ (𝐵𝑋)))
138136, 137mpbird 260 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝑋 + 𝑡) ≤ 𝐵)
139121, 122, 129, 135, 138eliccd 42072 . . . . . . 7 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝑋 + 𝑡) ∈ (𝐴[,]𝐵))
140111adantr 484 . . . . . . 7 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐴[,]𝐵) = dom 𝐹)
141139, 140eleqtrd 2918 . . . . . 6 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝑋 + 𝑡) ∈ dom 𝐹)
142120, 141, 114syl2anc 587 . . . . 5 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
143119, 142sseldd 3954 . . . 4 ((𝜑𝑡 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
14477, 80, 143itgioo 24426 . . 3 (𝜑 → ∫((𝐴𝑋)(,)(𝐵𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
1457, 117, 1443eqtrrd 2864 . 2 (𝜑 → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ⨜[(𝐴𝑋) → (𝐵𝑋)](𝐺‘(𝑋 + 𝑡)) d𝑡)
146 nfv 1916 . . . 4 𝑥𝜑
147 fourierdlem82.6 . . . 4 (𝜑 → (𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
148 fourierdlem82.7 . . . . 5 (𝜑𝐿 ∈ (𝐹 lim 𝐵))
1491, 2, 4, 107limcicciooub 42210 . . . . 5 (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) lim 𝐵) = (𝐹 lim 𝐵))
150148, 149eleqtrrd 2919 . . . 4 (𝜑𝐿 ∈ ((𝐹 ↾ (𝐴(,)𝐵)) lim 𝐵))
151 fourierdlem82.8 . . . . 5 (𝜑𝑅 ∈ (𝐹 lim 𝐴))
1521, 2, 4, 107limciccioolb 42194 . . . . 5 (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) lim 𝐴) = (𝐹 lim 𝐴))
153151, 152eleqtrrd 2919 . . . 4 (𝜑𝑅 ∈ ((𝐹 ↾ (𝐴(,)𝐵)) lim 𝐴))
154146, 8, 1, 2, 147, 150, 153cncfiooicc 42467 . . 3 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
1551, 2, 5, 3, 154itgsbtaddcnst 42555 . 2 (𝜑 → ⨜[(𝐴𝑋) → (𝐵𝑋)](𝐺‘(𝑋 + 𝑡)) d𝑡 = ⨜[𝐴𝐵](𝐺𝑠) d𝑠)
1565ditgpos 24466 . . 3 (𝜑 → ⨜[𝐴𝐵](𝐺𝑠) d𝑠 = ∫(𝐴(,)𝐵)(𝐺𝑠) d𝑠)
157 fveq2 6661 . . . . 5 (𝑠 = 𝑡 → (𝐺𝑠) = (𝐺𝑡))
158157cbvitgv 24387 . . . 4 ∫(𝐴(,)𝐵)(𝐺𝑠) d𝑠 = ∫(𝐴(,)𝐵)(𝐺𝑡) d𝑡
1598a1i 11 . . . . . 6 ((𝜑𝑡 ∈ (𝐴(,)𝐵)) → 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))))
1601ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝐴 ∈ ℝ)
161 simplr 768 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑡 ∈ (𝐴(,)𝐵))
16230ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝐴 ∈ ℝ*)
16332ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝐵 ∈ ℝ*)
164 elioo2 12776 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑡 ∈ (𝐴(,)𝐵) ↔ (𝑡 ∈ ℝ ∧ 𝐴 < 𝑡𝑡 < 𝐵)))
165162, 163, 164syl2anc 587 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → (𝑡 ∈ (𝐴(,)𝐵) ↔ (𝑡 ∈ ℝ ∧ 𝐴 < 𝑡𝑡 < 𝐵)))
166161, 165mpbid 235 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → (𝑡 ∈ ℝ ∧ 𝐴 < 𝑡𝑡 < 𝐵))
167166simp2d 1140 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝐴 < 𝑡)
168 simpr 488 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥 = 𝑡)
169167, 168breqtrrd 5080 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝐴 < 𝑥)
170160, 169gtned 10773 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥𝐴)
171170neneqd 3019 . . . . . . . 8 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → ¬ 𝑥 = 𝐴)
172171iffalsed 4461 . . . . . . 7 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))
173166simp1d 1139 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑡 ∈ ℝ)
174168, 173eqeltrd 2916 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥 ∈ ℝ)
175166simp3d 1141 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑡 < 𝐵)
176168, 175eqbrtrd 5074 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥 < 𝐵)
177174, 176ltned 10774 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥𝐵)
178177neneqd 3019 . . . . . . . 8 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → ¬ 𝑥 = 𝐵)
179178iffalsed 4461 . . . . . . 7 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))
180168, 161eqeltrd 2916 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → 𝑥 ∈ (𝐴(,)𝐵))
181180, 61syl 17 . . . . . . . 8 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹𝑥))
182 fveq2 6661 . . . . . . . . 9 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
183182adantl 485 . . . . . . . 8 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → (𝐹𝑥) = (𝐹𝑡))
184181, 183eqtrd 2859 . . . . . . 7 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹𝑡))
185172, 179, 1843eqtrd 2863 . . . . . 6 (((𝜑𝑡 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑡) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = (𝐹𝑡))
186 ioossicc 12820 . . . . . . 7 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
187 simpr 488 . . . . . . 7 ((𝜑𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ (𝐴(,)𝐵))
188186, 187sseldi 3951 . . . . . 6 ((𝜑𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ (𝐴[,]𝐵))
189108adantr 484 . . . . . . 7 ((𝜑𝑡 ∈ (𝐴(,)𝐵)) → Fun 𝐹)
190111adantr 484 . . . . . . . 8 ((𝜑𝑡 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) = dom 𝐹)
191188, 190eleqtrd 2918 . . . . . . 7 ((𝜑𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ dom 𝐹)
192 fvelrn 6835 . . . . . . 7 ((Fun 𝐹𝑡 ∈ dom 𝐹) → (𝐹𝑡) ∈ ran 𝐹)
193189, 191, 192syl2anc 587 . . . . . 6 ((𝜑𝑡 ∈ (𝐴(,)𝐵)) → (𝐹𝑡) ∈ ran 𝐹)
194159, 185, 188, 193fvmptd 6766 . . . . 5 ((𝜑𝑡 ∈ (𝐴(,)𝐵)) → (𝐺𝑡) = (𝐹𝑡))
195194itgeq2dv 24392 . . . 4 (𝜑 → ∫(𝐴(,)𝐵)(𝐺𝑡) d𝑡 = ∫(𝐴(,)𝐵)(𝐹𝑡) d𝑡)
196158, 195syl5eq 2871 . . 3 (𝜑 → ∫(𝐴(,)𝐵)(𝐺𝑠) d𝑠 = ∫(𝐴(,)𝐵)(𝐹𝑡) d𝑡)
197107ffvelrnda 6842 . . . 4 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (𝐹𝑡) ∈ ℂ)
1981, 2, 197itgioo 24426 . . 3 (𝜑 → ∫(𝐴(,)𝐵)(𝐹𝑡) d𝑡 = ∫(𝐴[,]𝐵)(𝐹𝑡) d𝑡)
199156, 196, 1983eqtrd 2863 . 2 (𝜑 → ⨜[𝐴𝐵](𝐺𝑠) d𝑠 = ∫(𝐴[,]𝐵)(𝐹𝑡) d𝑡)
200145, 155, 1993eqtrrd 2864 1 (𝜑 → ∫(𝐴[,]𝐵)(𝐹𝑡) d𝑡 = ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   ≠ wne 3014   ⊆ wss 3919  ifcif 4450   class class class wbr 5052   ↦ cmpt 5132  dom cdm 5542  ran crn 5543   ↾ cres 5544  Fun wfun 6337  ⟶wf 6339  ‘cfv 6343  (class class class)co 7149  ℂcc 10533  ℝcr 10534   + caddc 10538  ℝ*cxr 10672   < clt 10673   ≤ cle 10674   − cmin 10868  (,)cioo 12735  [,]cicc 12738  –cn→ccncf 23488  ∫citg 24229  ⨜cdit 24456   limℂ climc 24472 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cc 9855  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613  ax-addf 10614  ax-mulf 10615 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-symdif 4204  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-disj 5018  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-ofr 7404  df-om 7575  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-omul 8103  df-er 8285  df-map 8404  df-pm 8405  df-ixp 8458  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fsupp 8831  df-fi 8872  df-sup 8903  df-inf 8904  df-oi 8971  df-dju 9327  df-card 9365  df-acn 9368  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-n0 11895  df-z 11979  df-dec 12096  df-uz 12241  df-q 12346  df-rp 12387  df-xneg 12504  df-xadd 12505  df-xmul 12506  df-ioo 12739  df-ioc 12740  df-ico 12741  df-icc 12742  df-fz 12895  df-fzo 13038  df-fl 13166  df-mod 13242  df-seq 13374  df-exp 13435  df-hash 13696  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-limsup 14828  df-clim 14845  df-rlim 14846  df-sum 15043  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-starv 16580  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-unif 16588  df-hom 16589  df-cco 16590  df-rest 16696  df-topn 16697  df-0g 16715  df-gsum 16716  df-topgen 16717  df-pt 16718  df-prds 16721  df-xrs 16775  df-qtop 16780  df-imas 16781  df-xps 16783  df-mre 16857  df-mrc 16858  df-acs 16860  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-submnd 17957  df-mulg 18225  df-cntz 18447  df-cmn 18908  df-psmet 20090  df-xmet 20091  df-met 20092  df-bl 20093  df-mopn 20094  df-fbas 20095  df-fg 20096  df-cnfld 20099  df-top 21506  df-topon 21523  df-topsp 21545  df-bases 21558  df-cld 21631  df-ntr 21632  df-cls 21633  df-nei 21710  df-lp 21748  df-perf 21749  df-cn 21839  df-cnp 21840  df-haus 21927  df-cmp 21999  df-tx 22174  df-hmeo 22367  df-fil 22458  df-fm 22550  df-flim 22551  df-flf 22552  df-xms 22934  df-ms 22935  df-tms 22936  df-cncf 23490  df-ovol 24075  df-vol 24076  df-mbf 24230  df-itg1 24231  df-itg2 24232  df-ibl 24233  df-itg 24234  df-0p 24281  df-ditg 24457  df-limc 24476  df-dv 24477 This theorem is referenced by:  fourierdlem93  42772
 Copyright terms: Public domain W3C validator