| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem92.a | . . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 2 | 1 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 0 < 𝑇) → 𝐴 ∈ ℝ) | 
| 3 |  | fourierdlem92.b | . . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 4 | 3 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 0 < 𝑇) → 𝐵 ∈ ℝ) | 
| 5 |  | fourierdlem92.p | . . 3
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) | 
| 6 |  | fourierdlem92.m | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 7 | 6 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 0 < 𝑇) → 𝑀 ∈ ℕ) | 
| 8 |  | fourierdlem92.t | . . . . 5
⊢ (𝜑 → 𝑇 ∈ ℝ) | 
| 9 | 8 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ) | 
| 10 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑇) → 0 < 𝑇) | 
| 11 | 9, 10 | elrpd 13074 | . . 3
⊢ ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈
ℝ+) | 
| 12 |  | fourierdlem92.q | . . . 4
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) | 
| 13 | 12 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 0 < 𝑇) → 𝑄 ∈ (𝑃‘𝑀)) | 
| 14 |  | fourierdlem92.fper | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) | 
| 15 | 14 | adantlr 715 | . . 3
⊢ (((𝜑 ∧ 0 < 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) | 
| 16 |  | fveq2 6906 | . . . . 5
⊢ (𝑗 = 𝑖 → (𝑄‘𝑗) = (𝑄‘𝑖)) | 
| 17 | 16 | oveq1d 7446 | . . . 4
⊢ (𝑗 = 𝑖 → ((𝑄‘𝑗) + 𝑇) = ((𝑄‘𝑖) + 𝑇)) | 
| 18 | 17 | cbvmptv 5255 | . . 3
⊢ (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) + 𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) + 𝑇)) | 
| 19 |  | fourierdlem92.f | . . . 4
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) | 
| 20 | 19 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 0 < 𝑇) → 𝐹:ℝ⟶ℂ) | 
| 21 |  | fourierdlem92.cncf | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) | 
| 22 | 21 | adantlr 715 | . . 3
⊢ (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) | 
| 23 |  | fourierdlem92.r | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) | 
| 24 | 23 | adantlr 715 | . . 3
⊢ (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) | 
| 25 |  | fourierdlem92.l | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) | 
| 26 | 25 | adantlr 715 | . . 3
⊢ (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) | 
| 27 |  | eqeq1 2741 | . . . . 5
⊢ (𝑦 = 𝑥 → (𝑦 = (𝑄‘𝑖) ↔ 𝑥 = (𝑄‘𝑖))) | 
| 28 |  | eqeq1 2741 | . . . . . 6
⊢ (𝑦 = 𝑥 → (𝑦 = (𝑄‘(𝑖 + 1)) ↔ 𝑥 = (𝑄‘(𝑖 + 1)))) | 
| 29 |  | fveq2 6906 | . . . . . 6
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) | 
| 30 | 28, 29 | ifbieq2d 4552 | . . . . 5
⊢ (𝑦 = 𝑥 → if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑦)) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) | 
| 31 | 27, 30 | ifbieq2d 4552 | . . . 4
⊢ (𝑦 = 𝑥 → if(𝑦 = (𝑄‘𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑦))) = if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)))) | 
| 32 | 31 | cbvmptv 5255 | . . 3
⊢ (𝑦 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑦 = (𝑄‘𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑦)))) = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)))) | 
| 33 |  | eqid 2737 | . . 3
⊢ (𝑥 ∈ (((𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) + 𝑇))‘𝑖)[,]((𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) + 𝑇))‘(𝑖 + 1))) ↦ ((𝑦 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑦 = (𝑄‘𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑦))))‘(𝑥 − 𝑇))) = (𝑥 ∈ (((𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) + 𝑇))‘𝑖)[,]((𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) + 𝑇))‘(𝑖 + 1))) ↦ ((𝑦 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑦 = (𝑄‘𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑦))))‘(𝑥 − 𝑇))) | 
| 34 | 2, 4, 5, 7, 11, 13, 15, 18, 20, 22, 24, 26, 32, 33 | fourierdlem81 46202 | . 2
⊢ ((𝜑 ∧ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | 
| 35 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑇 = 0) → 𝑇 = 0) | 
| 36 | 35 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑇 = 0) → (𝐴 + 𝑇) = (𝐴 + 0)) | 
| 37 | 1 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 38 | 37 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑇 = 0) → 𝐴 ∈ ℂ) | 
| 39 | 38 | addridd 11461 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑇 = 0) → (𝐴 + 0) = 𝐴) | 
| 40 | 36, 39 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑇 = 0) → (𝐴 + 𝑇) = 𝐴) | 
| 41 | 35 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑇 = 0) → (𝐵 + 𝑇) = (𝐵 + 0)) | 
| 42 | 3 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 43 | 42 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑇 = 0) → 𝐵 ∈ ℂ) | 
| 44 | 43 | addridd 11461 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑇 = 0) → (𝐵 + 0) = 𝐵) | 
| 45 | 41, 44 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑇 = 0) → (𝐵 + 𝑇) = 𝐵) | 
| 46 | 40, 45 | oveq12d 7449 | . . . . 5
⊢ ((𝜑 ∧ 𝑇 = 0) → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = (𝐴[,]𝐵)) | 
| 47 | 46 | itgeq1d 45972 | . . . 4
⊢ ((𝜑 ∧ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | 
| 48 | 47 | adantlr 715 | . . 3
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | 
| 49 |  | simpll 767 | . . . 4
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝜑) | 
| 50 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 𝑇 = 0) | 
| 51 |  | simplr 769 | . . . . . . 7
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 0 < 𝑇) | 
| 52 |  | ioran 986 | . . . . . . 7
⊢ (¬
(𝑇 = 0 ∨ 0 < 𝑇) ↔ (¬ 𝑇 = 0 ∧ ¬ 0 < 𝑇)) | 
| 53 | 50, 51, 52 | sylanbrc 583 | . . . . . 6
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ (𝑇 = 0 ∨ 0 < 𝑇)) | 
| 54 | 49, 8 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 ∈ ℝ) | 
| 55 |  | 0red 11264 | . . . . . . 7
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 ∈
ℝ) | 
| 56 | 54, 55 | lttrid 11399 | . . . . . 6
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ ¬ (𝑇 = 0 ∨ 0 < 𝑇))) | 
| 57 | 53, 56 | mpbird 257 | . . . . 5
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 < 0) | 
| 58 | 54 | lt0neg1d 11832 | . . . . 5
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ 0 < -𝑇)) | 
| 59 | 57, 58 | mpbid 232 | . . . 4
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 < -𝑇) | 
| 60 | 1, 8 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + 𝑇) ∈ ℝ) | 
| 61 | 60 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + 𝑇) ∈ ℂ) | 
| 62 | 8 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℂ) | 
| 63 | 61, 62 | negsubd 11626 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 𝑇) + -𝑇) = ((𝐴 + 𝑇) − 𝑇)) | 
| 64 | 37, 62 | pncand 11621 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴) | 
| 65 | 63, 64 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝜑 → ((𝐴 + 𝑇) + -𝑇) = 𝐴) | 
| 66 | 3, 8 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 + 𝑇) ∈ ℝ) | 
| 67 | 66 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐵 + 𝑇) ∈ ℂ) | 
| 68 | 67, 62 | negsubd 11626 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇)) | 
| 69 | 42, 62 | pncand 11621 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵) | 
| 70 | 68, 69 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝜑 → ((𝐵 + 𝑇) + -𝑇) = 𝐵) | 
| 71 | 65, 70 | oveq12d 7449 | . . . . . . . 8
⊢ (𝜑 → (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)) = (𝐴[,]𝐵)) | 
| 72 | 71 | eqcomd 2743 | . . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) = (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))) | 
| 73 | 72 | itgeq1d 45972 | . . . . . 6
⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹‘𝑥) d𝑥) | 
| 74 | 73 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 0 < -𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹‘𝑥) d𝑥) | 
| 75 | 1 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 0 < -𝑇) → 𝐴 ∈ ℝ) | 
| 76 | 8 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 0 < -𝑇) → 𝑇 ∈ ℝ) | 
| 77 | 75, 76 | readdcld 11290 | . . . . . 6
⊢ ((𝜑 ∧ 0 < -𝑇) → (𝐴 + 𝑇) ∈ ℝ) | 
| 78 | 3 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 0 < -𝑇) → 𝐵 ∈ ℝ) | 
| 79 | 78, 76 | readdcld 11290 | . . . . . 6
⊢ ((𝜑 ∧ 0 < -𝑇) → (𝐵 + 𝑇) ∈ ℝ) | 
| 80 |  | eqid 2737 | . . . . . 6
⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ
↑m (0...𝑚))
∣ (((𝑝‘0) =
(𝐴 + 𝑇) ∧ (𝑝‘𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝‘𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) | 
| 81 | 6 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 0 < -𝑇) → 𝑀 ∈ ℕ) | 
| 82 | 76 | renegcld 11690 | . . . . . . 7
⊢ ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ) | 
| 83 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 0 < -𝑇) → 0 < -𝑇) | 
| 84 | 82, 83 | elrpd 13074 | . . . . . 6
⊢ ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈
ℝ+) | 
| 85 | 5 | fourierdlem2 46124 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 86 | 6, 85 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 87 | 12, 86 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) | 
| 88 | 87 | simpld 494 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) | 
| 89 |  | elmapi 8889 | . . . . . . . . . . . . . . 15
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
→ 𝑄:(0...𝑀)⟶ℝ) | 
| 90 | 88, 89 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) | 
| 91 | 90 | ffvelcdmda 7104 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ) | 
| 92 | 8 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑇 ∈ ℝ) | 
| 93 | 91, 92 | readdcld 11290 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑄‘𝑖) + 𝑇) ∈ ℝ) | 
| 94 |  | fourierdlem92.s | . . . . . . . . . . . 12
⊢ 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) + 𝑇)) | 
| 95 | 93, 94 | fmptd 7134 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆:(0...𝑀)⟶ℝ) | 
| 96 |  | reex 11246 | . . . . . . . . . . . . 13
⊢ ℝ
∈ V | 
| 97 | 96 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈
V) | 
| 98 |  | ovex 7464 | . . . . . . . . . . . . 13
⊢
(0...𝑀) ∈
V | 
| 99 | 98 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → (0...𝑀) ∈ V) | 
| 100 | 97, 99 | elmapd 8880 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑆 ∈ (ℝ ↑m
(0...𝑀)) ↔ 𝑆:(0...𝑀)⟶ℝ)) | 
| 101 | 95, 100 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ (ℝ ↑m
(0...𝑀))) | 
| 102 | 94 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) + 𝑇))) | 
| 103 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0)) | 
| 104 | 103 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 0 → ((𝑄‘𝑖) + 𝑇) = ((𝑄‘0) + 𝑇)) | 
| 105 | 104 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) + 𝑇) = ((𝑄‘0) + 𝑇)) | 
| 106 |  | 0zd 12625 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈
ℤ) | 
| 107 | 6 | nnzd 12640 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 108 |  | 0le0 12367 | . . . . . . . . . . . . . . 15
⊢ 0 ≤
0 | 
| 109 | 108 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ 0) | 
| 110 |  | nnnn0 12533 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) | 
| 111 | 110 | nn0ge0d 12590 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 0 ≤
𝑀) | 
| 112 | 6, 111 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ 𝑀) | 
| 113 | 106, 107,
106, 109, 112 | elfzd 13555 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ (0...𝑀)) | 
| 114 | 90, 113 | ffvelcdmd 7105 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) | 
| 115 | 114, 8 | readdcld 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘0) + 𝑇) ∈ ℝ) | 
| 116 | 102, 105,
113, 115 | fvmptd 7023 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘0) = ((𝑄‘0) + 𝑇)) | 
| 117 |  | simprll 779 | . . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ (ℝ
↑m (0...𝑀))
∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄‘0) = 𝐴) | 
| 118 | 87, 117 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄‘0) = 𝐴) | 
| 119 | 118 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑄‘0) + 𝑇) = (𝐴 + 𝑇)) | 
| 120 | 116, 119 | eqtrd 2777 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑆‘0) = (𝐴 + 𝑇)) | 
| 121 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀)) | 
| 122 | 121 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑀 → ((𝑄‘𝑖) + 𝑇) = ((𝑄‘𝑀) + 𝑇)) | 
| 123 | 122 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 = 𝑀) → ((𝑄‘𝑖) + 𝑇) = ((𝑄‘𝑀) + 𝑇)) | 
| 124 | 6 | nnnn0d 12587 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 125 |  | nn0uz 12920 | . . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) | 
| 126 | 124, 125 | eleqtrdi 2851 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) | 
| 127 |  | eluzfz2 13572 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘0) → 𝑀 ∈ (0...𝑀)) | 
| 128 | 126, 127 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) | 
| 129 | 90, 128 | ffvelcdmd 7105 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ) | 
| 130 | 129, 8 | readdcld 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘𝑀) + 𝑇) ∈ ℝ) | 
| 131 | 102, 123,
128, 130 | fvmptd 7023 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘𝑀) = ((𝑄‘𝑀) + 𝑇)) | 
| 132 |  | simprlr 780 | . . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ (ℝ
↑m (0...𝑀))
∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄‘𝑀) = 𝐵) | 
| 133 | 87, 132 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) | 
| 134 | 133 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑄‘𝑀) + 𝑇) = (𝐵 + 𝑇)) | 
| 135 | 131, 134 | eqtrd 2777 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑆‘𝑀) = (𝐵 + 𝑇)) | 
| 136 | 120, 135 | jca 511 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆‘𝑀) = (𝐵 + 𝑇))) | 
| 137 | 90 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) | 
| 138 |  | elfzofz 13715 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) | 
| 139 | 138 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) | 
| 140 | 137, 139 | ffvelcdmd 7105 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) | 
| 141 |  | fzofzp1 13803 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) | 
| 142 | 141 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) | 
| 143 | 137, 142 | ffvelcdmd 7105 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) | 
| 144 | 8 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℝ) | 
| 145 | 87 | simprrd 774 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) | 
| 146 | 145 | r19.21bi 3251 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) | 
| 147 | 140, 143,
144, 146 | ltadd1dd 11874 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑇) < ((𝑄‘(𝑖 + 1)) + 𝑇)) | 
| 148 | 140, 144 | readdcld 11290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑇) ∈ ℝ) | 
| 149 | 94 | fvmpt2 7027 | . . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑄‘𝑖) + 𝑇) ∈ ℝ) → (𝑆‘𝑖) = ((𝑄‘𝑖) + 𝑇)) | 
| 150 | 139, 148,
149 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑆‘𝑖) = ((𝑄‘𝑖) + 𝑇)) | 
| 151 | 94, 18 | eqtr4i 2768 | . . . . . . . . . . . . . 14
⊢ 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) + 𝑇)) | 
| 152 | 151 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) + 𝑇))) | 
| 153 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑖 + 1) → (𝑄‘𝑗) = (𝑄‘(𝑖 + 1))) | 
| 154 | 153 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑖 + 1) → ((𝑄‘𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇)) | 
| 155 | 154 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄‘𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇)) | 
| 156 | 143, 144 | readdcld 11290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ) | 
| 157 | 152, 155,
142, 156 | fvmptd 7023 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑆‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) + 𝑇)) | 
| 158 | 147, 150,
157 | 3brtr4d 5175 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))) | 
| 159 | 158 | ralrimiva 3146 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))) | 
| 160 | 101, 136,
159 | jca32 515 | . . . . . . . . 9
⊢ (𝜑 → (𝑆 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆‘𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) | 
| 161 |  | fourierdlem92.h | . . . . . . . . . . 11
⊢ 𝐻 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝‘𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) | 
| 162 | 161 | fourierdlem2 46124 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑆 ∈ (𝐻‘𝑀) ↔ (𝑆 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆‘𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) | 
| 163 | 6, 162 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝑆 ∈ (𝐻‘𝑀) ↔ (𝑆 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆‘𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) | 
| 164 | 160, 163 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ (𝐻‘𝑀)) | 
| 165 | 161 | fveq1i 6907 | . . . . . . . 8
⊢ (𝐻‘𝑀) = ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝‘𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀) | 
| 166 | 164, 165 | eleqtrdi 2851 | . . . . . . 7
⊢ (𝜑 → 𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝‘𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀)) | 
| 167 | 166 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 0 < -𝑇) → 𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝‘𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀)) | 
| 168 | 60 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ) | 
| 169 | 66 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ) | 
| 170 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) | 
| 171 |  | eliccre 45518 | . . . . . . . . . . . 12
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) | 
| 172 | 168, 169,
170, 171 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) | 
| 173 | 172 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ) | 
| 174 | 62 | negcld 11607 | . . . . . . . . . . 11
⊢ (𝜑 → -𝑇 ∈ ℂ) | 
| 175 | 174 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℂ) | 
| 176 | 173, 175 | addcld 11280 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℂ) | 
| 177 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝜑) | 
| 178 | 1 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ) | 
| 179 | 3 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ) | 
| 180 | 8 | renegcld 11690 | . . . . . . . . . . . . 13
⊢ (𝜑 → -𝑇 ∈ ℝ) | 
| 181 | 180 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℝ) | 
| 182 | 172, 181 | readdcld 11290 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℝ) | 
| 183 | 63, 64 | eqtr2d 2778 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 = ((𝐴 + 𝑇) + -𝑇)) | 
| 184 | 183 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) + -𝑇)) | 
| 185 | 168 | rexrd 11311 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈
ℝ*) | 
| 186 | 169 | rexrd 11311 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈
ℝ*) | 
| 187 |  | iccgelb 13443 | . . . . . . . . . . . . . 14
⊢ (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ* ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥) | 
| 188 | 185, 186,
170, 187 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥) | 
| 189 | 168, 172,
181, 188 | leadd1dd 11877 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) + -𝑇) ≤ (𝑥 + -𝑇)) | 
| 190 | 184, 189 | eqbrtrd 5165 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 + -𝑇)) | 
| 191 |  | iccleub 13442 | . . . . . . . . . . . . . 14
⊢ (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ* ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇)) | 
| 192 | 185, 186,
170, 191 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇)) | 
| 193 | 172, 169,
181, 192 | leadd1dd 11877 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ ((𝐵 + 𝑇) + -𝑇)) | 
| 194 | 169 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℂ) | 
| 195 | 62 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ) | 
| 196 | 194, 195 | negsubd 11626 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇)) | 
| 197 | 69 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵) | 
| 198 | 196, 197 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = 𝐵) | 
| 199 | 193, 198 | breqtrd 5169 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ 𝐵) | 
| 200 | 178, 179,
182, 190, 199 | eliccd 45517 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) | 
| 201 | 177, 200 | jca 511 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))) | 
| 202 |  | eleq1 2829 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 + -𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))) | 
| 203 | 202 | anbi2d 630 | . . . . . . . . . . 11
⊢ (𝑦 = (𝑥 + -𝑇) → ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))) | 
| 204 |  | oveq1 7438 | . . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 + -𝑇) → (𝑦 + 𝑇) = ((𝑥 + -𝑇) + 𝑇)) | 
| 205 | 204 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 + -𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥 + -𝑇) + 𝑇))) | 
| 206 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 + -𝑇) → (𝐹‘𝑦) = (𝐹‘(𝑥 + -𝑇))) | 
| 207 | 205, 206 | eqeq12d 2753 | . . . . . . . . . . 11
⊢ (𝑦 = (𝑥 + -𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦) ↔ (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))) | 
| 208 | 203, 207 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑦 = (𝑥 + -𝑇) → (((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)) ↔ ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))) | 
| 209 |  | eleq1 2829 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑦 ∈ (𝐴[,]𝐵))) | 
| 210 | 209 | anbi2d 630 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)))) | 
| 211 |  | oveq1 7438 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇)) | 
| 212 | 211 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇))) | 
| 213 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) | 
| 214 | 212, 213 | eqeq12d 2753 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))) | 
| 215 | 210, 214 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)))) | 
| 216 | 215, 14 | chvarvv 1998 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)) | 
| 217 | 208, 216 | vtoclg 3554 | . . . . . . . . 9
⊢ ((𝑥 + -𝑇) ∈ ℂ → ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))) | 
| 218 | 176, 201,
217 | sylc 65 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))) | 
| 219 | 173, 195 | negsubd 11626 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) = (𝑥 − 𝑇)) | 
| 220 | 219 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = ((𝑥 − 𝑇) + 𝑇)) | 
| 221 | 173, 195 | npcand 11624 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 − 𝑇) + 𝑇) = 𝑥) | 
| 222 | 220, 221 | eqtrd 2777 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = 𝑥) | 
| 223 | 222 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘𝑥)) | 
| 224 | 218, 223 | eqtr3d 2779 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹‘𝑥)) | 
| 225 | 224 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ 0 < -𝑇) ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹‘𝑥)) | 
| 226 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑗 = 𝑖 → (𝑆‘𝑗) = (𝑆‘𝑖)) | 
| 227 | 226 | oveq1d 7446 | . . . . . . 7
⊢ (𝑗 = 𝑖 → ((𝑆‘𝑗) + -𝑇) = ((𝑆‘𝑖) + -𝑇)) | 
| 228 | 227 | cbvmptv 5255 | . . . . . 6
⊢ (𝑗 ∈ (0...𝑀) ↦ ((𝑆‘𝑗) + -𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑆‘𝑖) + -𝑇)) | 
| 229 | 19 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 0 < -𝑇) → 𝐹:ℝ⟶ℂ) | 
| 230 | 19 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ) | 
| 231 |  | ioossre 13448 | . . . . . . . . . . 11
⊢ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ | 
| 232 | 231 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ) | 
| 233 | 230, 232 | feqresmpt 6978 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥))) | 
| 234 | 150, 157 | oveq12d 7449 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) = (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) | 
| 235 | 140, 143,
144 | iooshift 45535 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) | 
| 236 | 234, 235 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) | 
| 237 | 236 | mpteq1d 5237 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹‘𝑥))) | 
| 238 |  | simpll 767 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝜑) | 
| 239 |  | simplr 769 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑖 ∈ (0..^𝑀)) | 
| 240 | 235 | eleq2d 2827 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) ↔ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})) | 
| 241 | 240 | biimpar 477 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) | 
| 242 | 140 | rexrd 11311 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈
ℝ*) | 
| 243 | 242 | 3adant3 1133 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘𝑖) ∈
ℝ*) | 
| 244 | 143 | rexrd 11311 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈
ℝ*) | 
| 245 | 244 | 3adant3 1133 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈
ℝ*) | 
| 246 |  | elioore 13417 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) → 𝑥 ∈ ℝ) | 
| 247 | 246 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ) | 
| 248 | 8 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ) | 
| 249 | 247, 248 | resubcld 11691 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ) | 
| 250 | 249 | 3adant2 1132 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ) | 
| 251 | 140 | recnd 11289 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ) | 
| 252 | 62 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℂ) | 
| 253 | 251, 252 | pncand 11621 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) + 𝑇) − 𝑇) = (𝑄‘𝑖)) | 
| 254 | 253 | eqcomd 2743 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (((𝑄‘𝑖) + 𝑇) − 𝑇)) | 
| 255 | 254 | 3adant3 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘𝑖) = (((𝑄‘𝑖) + 𝑇) − 𝑇)) | 
| 256 | 148 | 3adant3 1133 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘𝑖) + 𝑇) ∈ ℝ) | 
| 257 | 247 | 3adant2 1132 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ) | 
| 258 | 8 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ) | 
| 259 | 148 | rexrd 11311 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑇) ∈
ℝ*) | 
| 260 | 259 | 3adant3 1133 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘𝑖) + 𝑇) ∈
ℝ*) | 
| 261 | 156 | rexrd 11311 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈
ℝ*) | 
| 262 | 261 | 3adant3 1133 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈
ℝ*) | 
| 263 |  | simp3 1139 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) | 
| 264 |  | ioogtlb 45508 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑄‘𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ* ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘𝑖) + 𝑇) < 𝑥) | 
| 265 | 260, 262,
263, 264 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘𝑖) + 𝑇) < 𝑥) | 
| 266 | 256, 257,
258, 265 | ltsub1dd 11875 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄‘𝑖) + 𝑇) − 𝑇) < (𝑥 − 𝑇)) | 
| 267 | 255, 266 | eqbrtrd 5165 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘𝑖) < (𝑥 − 𝑇)) | 
| 268 | 156 | 3adant3 1133 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ) | 
| 269 |  | iooltub 45523 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑄‘𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ* ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇)) | 
| 270 | 260, 262,
263, 269 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇)) | 
| 271 | 257, 268,
258, 270 | ltsub1dd 11875 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) < (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇)) | 
| 272 | 143 | recnd 11289 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ) | 
| 273 | 272, 252 | pncand 11621 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1))) | 
| 274 | 273 | 3adant3 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1))) | 
| 275 | 271, 274 | breqtrd 5169 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) < (𝑄‘(𝑖 + 1))) | 
| 276 | 243, 245,
250, 267, 275 | eliood 45511 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) | 
| 277 | 238, 239,
241, 276 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥 − 𝑇) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) | 
| 278 |  | fvres 6925 | . . . . . . . . . . . 12
⊢ ((𝑥 − 𝑇) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)) = (𝐹‘(𝑥 − 𝑇))) | 
| 279 | 277, 278 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)) = (𝐹‘(𝑥 − 𝑇))) | 
| 280 | 238, 241,
249 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥 − 𝑇) ∈ ℝ) | 
| 281 | 1 | 3ad2ant1 1134 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ∈ ℝ) | 
| 282 | 3 | 3ad2ant1 1134 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐵 ∈ ℝ) | 
| 283 | 64 | eqcomd 2743 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) | 
| 284 | 283 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) | 
| 285 | 60 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ) | 
| 286 | 1 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ) | 
| 287 | 1 | rexrd 11311 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 288 | 287 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈
ℝ*) | 
| 289 | 3 | rexrd 11311 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 290 | 289 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐵 ∈
ℝ*) | 
| 291 | 5, 6, 12 | fourierdlem15 46137 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) | 
| 292 | 291 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) | 
| 293 | 292, 139 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ (𝐴[,]𝐵)) | 
| 294 |  | iccgelb 13443 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝑄‘𝑖) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑄‘𝑖)) | 
| 295 | 288, 290,
293, 294 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ≤ (𝑄‘𝑖)) | 
| 296 | 286, 140,
144, 295 | leadd1dd 11877 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐴 + 𝑇) ≤ ((𝑄‘𝑖) + 𝑇)) | 
| 297 | 296 | 3adant3 1133 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ≤ ((𝑄‘𝑖) + 𝑇)) | 
| 298 | 285, 256,
257, 297, 265 | lelttrd 11419 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) < 𝑥) | 
| 299 | 285, 257,
258, 298 | ltsub1dd 11875 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) < (𝑥 − 𝑇)) | 
| 300 | 284, 299 | eqbrtrd 5165 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 < (𝑥 − 𝑇)) | 
| 301 | 281, 250,
300 | ltled 11409 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ≤ (𝑥 − 𝑇)) | 
| 302 | 143 | 3adant3 1133 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ) | 
| 303 | 292, 142 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵)) | 
| 304 |  | iccleub 13442 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵) | 
| 305 | 288, 290,
303, 304 | syl3anc 1373 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵) | 
| 306 | 305 | 3adant3 1133 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ≤ 𝐵) | 
| 307 | 250, 302,
282, 275, 306 | ltletrd 11421 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) < 𝐵) | 
| 308 | 250, 282,
307 | ltled 11409 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) ≤ 𝐵) | 
| 309 | 281, 282,
250, 301, 308 | eliccd 45517 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) | 
| 310 | 238, 239,
241, 309 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) | 
| 311 | 238, 310 | jca 511 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝜑 ∧ (𝑥 − 𝑇) ∈ (𝐴[,]𝐵))) | 
| 312 |  | eleq1 2829 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥 − 𝑇) ∈ (𝐴[,]𝐵))) | 
| 313 | 312 | anbi2d 630 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 − 𝑇) → ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)))) | 
| 314 |  | oveq1 7438 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑥 − 𝑇) → (𝑦 + 𝑇) = ((𝑥 − 𝑇) + 𝑇)) | 
| 315 | 314 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥 − 𝑇) + 𝑇))) | 
| 316 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 𝑇) → (𝐹‘𝑦) = (𝐹‘(𝑥 − 𝑇))) | 
| 317 | 315, 316 | eqeq12d 2753 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 − 𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦) ↔ (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘(𝑥 − 𝑇)))) | 
| 318 | 313, 317 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 − 𝑇) → (((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)) ↔ ((𝜑 ∧ (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘(𝑥 − 𝑇))))) | 
| 319 | 318, 216 | vtoclg 3554 | . . . . . . . . . . . 12
⊢ ((𝑥 − 𝑇) ∈ ℝ → ((𝜑 ∧ (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘(𝑥 − 𝑇)))) | 
| 320 | 280, 311,
319 | sylc 65 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘(𝑥 − 𝑇))) | 
| 321 | 241, 246 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ℝ) | 
| 322 |  | recn 11245 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) | 
| 323 | 322 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) | 
| 324 | 62 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ) | 
| 325 | 323, 324 | npcand 11624 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 − 𝑇) + 𝑇) = 𝑥) | 
| 326 | 325 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘𝑥)) | 
| 327 | 238, 321,
326 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘𝑥)) | 
| 328 | 279, 320,
327 | 3eqtr2rd 2784 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘𝑥) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))) | 
| 329 | 328 | mpteq2dva 5242 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))) | 
| 330 | 233, 237,
329 | 3eqtrd 2781 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))) | 
| 331 |  | ioosscn 13449 | . . . . . . . . . . 11
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ | 
| 332 | 331 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ) | 
| 333 |  | eqeq1 2741 | . . . . . . . . . . . . 13
⊢ (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇))) | 
| 334 | 333 | rexbidv 3179 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇))) | 
| 335 |  | oveq1 7438 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇)) | 
| 336 | 335 | eqeq2d 2748 | . . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇))) | 
| 337 | 336 | cbvrexvw 3238 | . . . . . . . . . . . 12
⊢
(∃𝑧 ∈
((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)) | 
| 338 | 334, 337 | bitrdi 287 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇))) | 
| 339 | 338 | cbvrabv 3447 | . . . . . . . . . 10
⊢ {𝑤 ∈ ℂ ∣
∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} | 
| 340 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))) | 
| 341 | 332, 252,
339, 21, 340 | cncfshift 45889 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))) ∈ ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ)) | 
| 342 | 236 | eqcomd 2743 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) | 
| 343 | 342 | oveq1d 7446 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ) = (((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ)) | 
| 344 | 341, 343 | eleqtrd 2843 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))) ∈ (((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ)) | 
| 345 | 330, 344 | eqeltrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ)) | 
| 346 | 345 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ)) | 
| 347 |  | ffdm 6765 | . . . . . . . . . . . 12
⊢ (𝐹:ℝ⟶ℂ →
(𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) | 
| 348 | 19, 347 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) | 
| 349 | 348 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) | 
| 350 | 349 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:dom 𝐹⟶ℂ) | 
| 351 |  | ioossre 13448 | . . . . . . . . . 10
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ | 
| 352 |  | fdm 6745 | . . . . . . . . . . 11
⊢ (𝐹:ℝ⟶ℂ →
dom 𝐹 =
ℝ) | 
| 353 | 230, 352 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom 𝐹 = ℝ) | 
| 354 | 351, 353 | sseqtrrid 4027 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹) | 
| 355 | 339 | eqcomi 2746 | . . . . . . . . 9
⊢ {𝑥 ∈ ℂ ∣
∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} | 
| 356 | 232, 342,
353 | 3sstr4d 4039 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ⊆ dom 𝐹) | 
| 357 | 339, 356 | eqsstrrid 4023 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} ⊆ dom 𝐹) | 
| 358 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑) | 
| 359 | 358, 287 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐴 ∈
ℝ*) | 
| 360 | 358, 289 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐵 ∈
ℝ*) | 
| 361 | 358, 291 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) | 
| 362 |  | simplr 769 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀)) | 
| 363 |  | ioossicc 13473 | . . . . . . . . . . . . 13
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) | 
| 364 | 363 | sseli 3979 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑧 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) | 
| 365 | 364 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) | 
| 366 | 359, 360,
361, 362, 365 | fourierdlem1 46123 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ (𝐴[,]𝐵)) | 
| 367 |  | eleq1 2829 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑧 ∈ (𝐴[,]𝐵))) | 
| 368 | 367 | anbi2d 630 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)))) | 
| 369 |  | oveq1 7438 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑥 + 𝑇) = (𝑧 + 𝑇)) | 
| 370 | 369 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑧 + 𝑇))) | 
| 371 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) | 
| 372 | 370, 371 | eqeq12d 2753 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑧 + 𝑇)) = (𝐹‘𝑧))) | 
| 373 | 368, 372 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹‘𝑧)))) | 
| 374 | 373, 14 | chvarvv 1998 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹‘𝑧)) | 
| 375 | 358, 366,
374 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑧 + 𝑇)) = (𝐹‘𝑧)) | 
| 376 | 350, 332,
354, 252, 355, 357, 375, 23 | limcperiod 45643 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) limℂ ((𝑄‘𝑖) + 𝑇))) | 
| 377 | 355, 342 | eqtrid 2789 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) | 
| 378 | 377 | reseq2d 5997 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) = (𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))) | 
| 379 | 150 | eqcomd 2743 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑇) = (𝑆‘𝑖)) | 
| 380 | 378, 379 | oveq12d 7449 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) limℂ ((𝑄‘𝑖) + 𝑇)) = ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) limℂ (𝑆‘𝑖))) | 
| 381 | 376, 380 | eleqtrd 2843 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) limℂ (𝑆‘𝑖))) | 
| 382 | 381 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) limℂ (𝑆‘𝑖))) | 
| 383 | 350, 332,
354, 252, 355, 357, 375, 25 | limcperiod 45643 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) limℂ ((𝑄‘(𝑖 + 1)) + 𝑇))) | 
| 384 | 157 | eqcomd 2743 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) = (𝑆‘(𝑖 + 1))) | 
| 385 | 378, 384 | oveq12d 7449 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) limℂ ((𝑄‘(𝑖 + 1)) + 𝑇)) = ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) limℂ (𝑆‘(𝑖 + 1)))) | 
| 386 | 383, 385 | eleqtrd 2843 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) limℂ (𝑆‘(𝑖 + 1)))) | 
| 387 | 386 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) limℂ (𝑆‘(𝑖 + 1)))) | 
| 388 |  | eqeq1 2741 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑦 = (𝑆‘𝑖) ↔ 𝑥 = (𝑆‘𝑖))) | 
| 389 |  | eqeq1 2741 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑦 = (𝑆‘(𝑖 + 1)) ↔ 𝑥 = (𝑆‘(𝑖 + 1)))) | 
| 390 | 389, 29 | ifbieq2d 4552 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹‘𝑦)) = if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) | 
| 391 | 388, 390 | ifbieq2d 4552 | . . . . . . 7
⊢ (𝑦 = 𝑥 → if(𝑦 = (𝑆‘𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹‘𝑦))) = if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)))) | 
| 392 | 391 | cbvmptv 5255 | . . . . . 6
⊢ (𝑦 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆‘𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹‘𝑦)))) = (𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)))) | 
| 393 |  | eqid 2737 | . . . . . 6
⊢ (𝑥 ∈ (((𝑗 ∈ (0...𝑀) ↦ ((𝑆‘𝑗) + -𝑇))‘𝑖)[,]((𝑗 ∈ (0...𝑀) ↦ ((𝑆‘𝑗) + -𝑇))‘(𝑖 + 1))) ↦ ((𝑦 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆‘𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹‘𝑦))))‘(𝑥 − -𝑇))) = (𝑥 ∈ (((𝑗 ∈ (0...𝑀) ↦ ((𝑆‘𝑗) + -𝑇))‘𝑖)[,]((𝑗 ∈ (0...𝑀) ↦ ((𝑆‘𝑗) + -𝑇))‘(𝑖 + 1))) ↦ ((𝑦 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆‘𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹‘𝑦))))‘(𝑥 − -𝑇))) | 
| 394 | 77, 79, 80, 81, 84, 167, 225, 228, 229, 346, 382, 387, 392, 393 | fourierdlem81 46202 | . . . . 5
⊢ ((𝜑 ∧ 0 < -𝑇) → ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥) | 
| 395 | 74, 394 | eqtr2d 2778 | . . . 4
⊢ ((𝜑 ∧ 0 < -𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | 
| 396 | 49, 59, 395 | syl2anc 584 | . . 3
⊢ (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | 
| 397 | 48, 396 | pm2.61dan 813 | . 2
⊢ ((𝜑 ∧ ¬ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | 
| 398 | 34, 397 | pm2.61dan 813 | 1
⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |