| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem69.f | . . . 4
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) | 
| 2 |  | fourierdlem69.q | . . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) | 
| 3 |  | fourierdlem69.m | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 4 |  | fourierdlem69.p | . . . . . . . . . . . 12
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) | 
| 5 | 4 | fourierdlem2 46124 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 6 | 3, 5 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 7 | 2, 6 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) | 
| 8 | 7 | simprd 495 | . . . . . . . 8
⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) | 
| 9 | 8 | simpld 494 | . . . . . . 7
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) | 
| 10 | 9 | simpld 494 | . . . . . 6
⊢ (𝜑 → (𝑄‘0) = 𝐴) | 
| 11 | 9 | simprd 495 | . . . . . 6
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) | 
| 12 | 10, 11 | oveq12d 7449 | . . . . 5
⊢ (𝜑 → ((𝑄‘0)[,](𝑄‘𝑀)) = (𝐴[,]𝐵)) | 
| 13 | 12 | feq2d 6722 | . . . 4
⊢ (𝜑 → (𝐹:((𝑄‘0)[,](𝑄‘𝑀))⟶ℂ ↔ 𝐹:(𝐴[,]𝐵)⟶ℂ)) | 
| 14 | 1, 13 | mpbird 257 | . . 3
⊢ (𝜑 → 𝐹:((𝑄‘0)[,](𝑄‘𝑀))⟶ℂ) | 
| 15 | 14 | feqmptd 6977 | . 2
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀)) ↦ (𝐹‘𝑥))) | 
| 16 |  | nfv 1914 | . . 3
⊢
Ⅎ𝑥𝜑 | 
| 17 |  | 0zd 12625 | . . 3
⊢ (𝜑 → 0 ∈
ℤ) | 
| 18 |  | nnuz 12921 | . . . . 5
⊢ ℕ =
(ℤ≥‘1) | 
| 19 |  | 1e0p1 12775 | . . . . . 6
⊢ 1 = (0 +
1) | 
| 20 | 19 | fveq2i 6909 | . . . . 5
⊢
(ℤ≥‘1) = (ℤ≥‘(0 +
1)) | 
| 21 | 18, 20 | eqtri 2765 | . . . 4
⊢ ℕ =
(ℤ≥‘(0 + 1)) | 
| 22 | 3, 21 | eleqtrdi 2851 | . . 3
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(0 +
1))) | 
| 23 | 7 | simpld 494 | . . . . 5
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) | 
| 24 |  | elmapi 8889 | . . . . 5
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
→ 𝑄:(0...𝑀)⟶ℝ) | 
| 25 | 23, 24 | syl 17 | . . . 4
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) | 
| 26 | 25 | ffvelcdmda 7104 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ) | 
| 27 | 8 | simprd 495 | . . . 4
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) | 
| 28 | 27 | r19.21bi 3251 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) | 
| 29 | 1 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝐹:(𝐴[,]𝐵)⟶ℂ) | 
| 30 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) | 
| 31 | 10 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝑄‘0) = 𝐴) | 
| 32 | 11 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝑄‘𝑀) = 𝐵) | 
| 33 | 31, 32 | oveq12d 7449 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → ((𝑄‘0)[,](𝑄‘𝑀)) = (𝐴[,]𝐵)) | 
| 34 | 30, 33 | eleqtrd 2843 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 35 | 29, 34 | ffvelcdmd 7105 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝐹‘𝑥) ∈ ℂ) | 
| 36 | 25 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) | 
| 37 |  | elfzofz 13715 | . . . . . 6
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) | 
| 38 | 37 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) | 
| 39 | 36, 38 | ffvelcdmd 7105 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) | 
| 40 |  | fzofzp1 13803 | . . . . . 6
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) | 
| 41 | 40 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) | 
| 42 | 36, 41 | ffvelcdmd 7105 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) | 
| 43 | 1 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:(𝐴[,]𝐵)⟶ℂ) | 
| 44 |  | ioossicc 13473 | . . . . . . . 8
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) | 
| 45 | 4, 3, 2 | fourierdlem11 46133 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) | 
| 46 | 45 | simp1d 1143 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 47 | 46 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 48 | 47 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈
ℝ*) | 
| 49 | 45 | simp2d 1144 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 50 | 49 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 51 | 50 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐵 ∈
ℝ*) | 
| 52 | 4, 3, 2 | fourierdlem15 46137 | . . . . . . . . . 10
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) | 
| 53 | 52 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) | 
| 54 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀)) | 
| 55 | 48, 51, 53, 54 | fourierdlem8 46130 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵)) | 
| 56 | 44, 55 | sstrid 3995 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵)) | 
| 57 | 43, 56 | feqresmpt 6978 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥))) | 
| 58 |  | fourierdlem69.fcn | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) | 
| 59 | 57, 58 | eqeltrrd 2842 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) | 
| 60 |  | fourierdlem69.l | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) | 
| 61 | 57 | oveq1d 7446 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) = ((𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) limℂ (𝑄‘(𝑖 + 1)))) | 
| 62 | 60, 61 | eleqtrd 2843 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) limℂ (𝑄‘(𝑖 + 1)))) | 
| 63 |  | fourierdlem69.r | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) | 
| 64 | 57 | oveq1d 7446 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) = ((𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) limℂ (𝑄‘𝑖))) | 
| 65 | 63, 64 | eleqtrd 2843 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) limℂ (𝑄‘𝑖))) | 
| 66 | 39, 42, 59, 62, 65 | iblcncfioo 45993 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) ∈
𝐿1) | 
| 67 | 43 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝐹:(𝐴[,]𝐵)⟶ℂ) | 
| 68 | 55 | sselda 3983 | . . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 69 | 67, 68 | ffvelcdmd 7105 | . . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑥) ∈ ℂ) | 
| 70 | 39, 42, 66, 69 | ibliooicc 45986 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) ∈
𝐿1) | 
| 71 | 16, 17, 22, 26, 28, 35, 70 | iblspltprt 45988 | . 2
⊢ (𝜑 → (𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀)) ↦ (𝐹‘𝑥)) ∈
𝐿1) | 
| 72 | 15, 71 | eqeltrd 2841 | 1
⊢ (𝜑 → 𝐹 ∈
𝐿1) |