Proof of Theorem fourierdlem114
| Step | Hyp | Ref
| Expression |
| 1 | | fourierdlem114.f |
. 2
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
| 2 | | fourierdlem114.t |
. 2
⊢ 𝑇 = (2 ·
π) |
| 3 | | fourierdlem114.per |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
| 4 | | fourierdlem114.x |
. 2
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 5 | | fourierdlem114.l |
. 2
⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) |
| 6 | | fourierdlem114.r |
. 2
⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) |
| 7 | | fourierdlem114.p |
. 2
⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
| 8 | | fourierdlem114.m |
. . 3
⊢ 𝑀 = ((♯‘𝐻) − 1) |
| 9 | | 2z 12649 |
. . . . . 6
⊢ 2 ∈
ℤ |
| 10 | 9 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℤ) |
| 11 | | fourierdlem114.h |
. . . . . . . 8
⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) |
| 12 | | tpfi 9365 |
. . . . . . . . . 10
⊢ {-π,
π, (𝐸‘𝑋)} ∈ Fin |
| 13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ∈ Fin) |
| 14 | | pire 26500 |
. . . . . . . . . . . . . . 15
⊢ π
∈ ℝ |
| 15 | 14 | renegcli 11570 |
. . . . . . . . . . . . . 14
⊢ -π
∈ ℝ |
| 16 | 15 | rexri 11319 |
. . . . . . . . . . . . 13
⊢ -π
∈ ℝ* |
| 17 | 14 | rexri 11319 |
. . . . . . . . . . . . 13
⊢ π
∈ ℝ* |
| 18 | | negpilt0 45292 |
. . . . . . . . . . . . . . 15
⊢ -π
< 0 |
| 19 | | pipos 26502 |
. . . . . . . . . . . . . . 15
⊢ 0 <
π |
| 20 | | 0re 11263 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
| 21 | 15, 20, 14 | lttri 11387 |
. . . . . . . . . . . . . . 15
⊢ ((-π
< 0 ∧ 0 < π) → -π < π) |
| 22 | 18, 19, 21 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ -π
< π |
| 23 | 15, 14, 22 | ltleii 11384 |
. . . . . . . . . . . . 13
⊢ -π
≤ π |
| 24 | | prunioo 13521 |
. . . . . . . . . . . . 13
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ -π
≤ π) → ((-π(,)π) ∪ {-π, π}) =
(-π[,]π)) |
| 25 | 16, 17, 23, 24 | mp3an 1463 |
. . . . . . . . . . . 12
⊢
((-π(,)π) ∪ {-π, π}) = (-π[,]π) |
| 26 | 25 | difeq1i 4122 |
. . . . . . . . . . 11
⊢
(((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = ((-π[,]π) ∖ dom 𝐺) |
| 27 | | difundir 4291 |
. . . . . . . . . . 11
⊢
(((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖
dom 𝐺)) |
| 28 | 26, 27 | eqtr3i 2767 |
. . . . . . . . . 10
⊢
((-π[,]π) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖
dom 𝐺)) |
| 29 | | fourierdlem114.dmdv |
. . . . . . . . . . 11
⊢ (𝜑 → ((-π(,)π) ∖
dom 𝐺) ∈
Fin) |
| 30 | | prfi 9363 |
. . . . . . . . . . . 12
⊢ {-π,
π} ∈ Fin |
| 31 | | diffi 9215 |
. . . . . . . . . . . 12
⊢ ({-π,
π} ∈ Fin → ({-π, π} ∖ dom 𝐺) ∈ Fin) |
| 32 | 30, 31 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → ({-π, π} ∖ dom
𝐺) ∈
Fin) |
| 33 | | unfi 9211 |
. . . . . . . . . . 11
⊢
((((-π(,)π) ∖ dom 𝐺) ∈ Fin ∧ ({-π, π} ∖
dom 𝐺) ∈ Fin) →
(((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin) |
| 34 | 29, 32, 33 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (((-π(,)π) ∖
dom 𝐺) ∪ ({-π, π}
∖ dom 𝐺)) ∈
Fin) |
| 35 | 28, 34 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝜑 → ((-π[,]π) ∖
dom 𝐺) ∈
Fin) |
| 36 | | unfi 9211 |
. . . . . . . . 9
⊢ (({-π,
π, (𝐸‘𝑋)} ∈ Fin ∧
((-π[,]π) ∖ dom 𝐺) ∈ Fin) → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin) |
| 37 | 13, 35, 36 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin) |
| 38 | 11, 37 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ Fin) |
| 39 | | hashcl 14395 |
. . . . . . 7
⊢ (𝐻 ∈ Fin →
(♯‘𝐻) ∈
ℕ0) |
| 40 | 38, 39 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐻) ∈
ℕ0) |
| 41 | 40 | nn0zd 12639 |
. . . . 5
⊢ (𝜑 → (♯‘𝐻) ∈
ℤ) |
| 42 | 15, 22 | ltneii 11374 |
. . . . . . 7
⊢ -π
≠ π |
| 43 | | hashprg 14434 |
. . . . . . . 8
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ) → (-π ≠ π ↔
(♯‘{-π, π}) = 2)) |
| 44 | 15, 14, 43 | mp2an 692 |
. . . . . . 7
⊢ (-π
≠ π ↔ (♯‘{-π, π}) = 2) |
| 45 | 42, 44 | mpbi 230 |
. . . . . 6
⊢
(♯‘{-π, π}) = 2 |
| 46 | 12 | elexi 3503 |
. . . . . . . . . 10
⊢ {-π,
π, (𝐸‘𝑋)} ∈ V |
| 47 | | ovex 7464 |
. . . . . . . . . . 11
⊢
(-π[,]π) ∈ V |
| 48 | | difexg 5329 |
. . . . . . . . . . 11
⊢
((-π[,]π) ∈ V → ((-π[,]π) ∖ dom 𝐺) ∈ V) |
| 49 | 47, 48 | ax-mp 5 |
. . . . . . . . . 10
⊢
((-π[,]π) ∖ dom 𝐺) ∈ V |
| 50 | 46, 49 | unex 7764 |
. . . . . . . . 9
⊢ ({-π,
π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖
dom 𝐺)) ∈
V |
| 51 | 11, 50 | eqeltri 2837 |
. . . . . . . 8
⊢ 𝐻 ∈ V |
| 52 | | negex 11506 |
. . . . . . . . . . 11
⊢ -π
∈ V |
| 53 | 52 | tpid1 4768 |
. . . . . . . . . 10
⊢ -π
∈ {-π, π, (𝐸‘𝑋)} |
| 54 | 14 | elexi 3503 |
. . . . . . . . . . 11
⊢ π
∈ V |
| 55 | 54 | tpid2 4770 |
. . . . . . . . . 10
⊢ π
∈ {-π, π, (𝐸‘𝑋)} |
| 56 | | prssi 4821 |
. . . . . . . . . 10
⊢ ((-π
∈ {-π, π, (𝐸‘𝑋)} ∧ π ∈ {-π, π, (𝐸‘𝑋)}) → {-π, π} ⊆ {-π,
π, (𝐸‘𝑋)}) |
| 57 | 53, 55, 56 | mp2an 692 |
. . . . . . . . 9
⊢ {-π,
π} ⊆ {-π, π, (𝐸‘𝑋)} |
| 58 | | ssun1 4178 |
. . . . . . . . . 10
⊢ {-π,
π, (𝐸‘𝑋)} ⊆ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) |
| 59 | 58, 11 | sseqtrri 4033 |
. . . . . . . . 9
⊢ {-π,
π, (𝐸‘𝑋)} ⊆ 𝐻 |
| 60 | 57, 59 | sstri 3993 |
. . . . . . . 8
⊢ {-π,
π} ⊆ 𝐻 |
| 61 | | hashss 14448 |
. . . . . . . 8
⊢ ((𝐻 ∈ V ∧ {-π, π}
⊆ 𝐻) →
(♯‘{-π, π}) ≤ (♯‘𝐻)) |
| 62 | 51, 60, 61 | mp2an 692 |
. . . . . . 7
⊢
(♯‘{-π, π}) ≤ (♯‘𝐻) |
| 63 | 62 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (♯‘{-π,
π}) ≤ (♯‘𝐻)) |
| 64 | 45, 63 | eqbrtrrid 5179 |
. . . . 5
⊢ (𝜑 → 2 ≤
(♯‘𝐻)) |
| 65 | | eluz2 12884 |
. . . . 5
⊢
((♯‘𝐻)
∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧
(♯‘𝐻) ∈
ℤ ∧ 2 ≤ (♯‘𝐻))) |
| 66 | 10, 41, 64, 65 | syl3anbrc 1344 |
. . . 4
⊢ (𝜑 → (♯‘𝐻) ∈
(ℤ≥‘2)) |
| 67 | | uz2m1nn 12965 |
. . . 4
⊢
((♯‘𝐻)
∈ (ℤ≥‘2) → ((♯‘𝐻) − 1) ∈
ℕ) |
| 68 | 66, 67 | syl 17 |
. . 3
⊢ (𝜑 → ((♯‘𝐻) − 1) ∈
ℕ) |
| 69 | 8, 68 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 70 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → -π ∈
ℝ) |
| 71 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → π ∈
ℝ) |
| 72 | | negpitopissre 26582 |
. . . . . . . . . . . 12
⊢
(-π(,]π) ⊆ ℝ |
| 73 | 22 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → -π <
π) |
| 74 | | picn 26501 |
. . . . . . . . . . . . . . . 16
⊢ π
∈ ℂ |
| 75 | 74 | 2timesi 12404 |
. . . . . . . . . . . . . . 15
⊢ (2
· π) = (π + π) |
| 76 | 74, 74 | subnegi 11588 |
. . . . . . . . . . . . . . 15
⊢ (π
− -π) = (π + π) |
| 77 | 75, 2, 76 | 3eqtr4i 2775 |
. . . . . . . . . . . . . 14
⊢ 𝑇 = (π −
-π) |
| 78 | | fourierdlem114.e |
. . . . . . . . . . . . . 14
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))) |
| 79 | 70, 71, 73, 77, 78 | fourierdlem4 46126 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸:ℝ⟶(-π(,]π)) |
| 80 | 79, 4 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π(,]π)) |
| 81 | 72, 80 | sselid 3981 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ) |
| 82 | 70, 71, 81 | 3jca 1129 |
. . . . . . . . . 10
⊢ (𝜑 → (-π ∈ ℝ
∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ)) |
| 83 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐸‘𝑋) ∈ V |
| 84 | 52, 54, 83 | tpss 4837 |
. . . . . . . . . 10
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ) ↔ {-π, π,
(𝐸‘𝑋)} ⊆ ℝ) |
| 85 | 82, 84 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ ℝ) |
| 86 | | iccssre 13469 |
. . . . . . . . . . 11
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆
ℝ) |
| 87 | 15, 14, 86 | mp2an 692 |
. . . . . . . . . 10
⊢
(-π[,]π) ⊆ ℝ |
| 88 | | ssdifss 4140 |
. . . . . . . . . 10
⊢
((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ dom 𝐺) ⊆
ℝ) |
| 89 | 87, 88 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ((-π[,]π) ∖
dom 𝐺) ⊆
ℝ) |
| 90 | 85, 89 | unssd 4192 |
. . . . . . . 8
⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆
ℝ) |
| 91 | 11, 90 | eqsstrid 4022 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ⊆ ℝ) |
| 92 | | fourierdlem114.q |
. . . . . . 7
⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻)) |
| 93 | 38, 91, 92, 8 | fourierdlem36 46158 |
. . . . . 6
⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻)) |
| 94 | | isof1o 7343 |
. . . . . 6
⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–1-1-onto→𝐻) |
| 95 | | f1of 6848 |
. . . . . 6
⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)⟶𝐻) |
| 96 | 93, 94, 95 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻) |
| 97 | 96, 91 | fssd 6753 |
. . . 4
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
| 98 | | reex 11246 |
. . . . 5
⊢ ℝ
∈ V |
| 99 | | ovex 7464 |
. . . . 5
⊢
(0...𝑀) ∈
V |
| 100 | 98, 99 | elmap 8911 |
. . . 4
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
↔ 𝑄:(0...𝑀)⟶ℝ) |
| 101 | 97, 100 | sylibr 234 |
. . 3
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) |
| 102 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (0 =
𝑖 → (𝑄‘0) = (𝑄‘𝑖)) |
| 103 | 102 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) = (𝑄‘𝑖)) |
| 104 | 97 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
| 105 | 104 | leidd 11829 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑖)) |
| 106 | 105 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘𝑖) ≤ (𝑄‘𝑖)) |
| 107 | 103, 106 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖)) |
| 108 | | elfzelz 13564 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ) |
| 109 | 108 | zred 12722 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ) |
| 110 | 109 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ∈ ℝ) |
| 111 | | elfzle1 13567 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖) |
| 112 | 111 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 ≤ 𝑖) |
| 113 | | neqne 2948 |
. . . . . . . . . . . . 13
⊢ (¬ 0
= 𝑖 → 0 ≠ 𝑖) |
| 114 | 113 | necomd 2996 |
. . . . . . . . . . . 12
⊢ (¬ 0
= 𝑖 → 𝑖 ≠ 0) |
| 115 | 114 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ≠ 0) |
| 116 | 110, 112,
115 | ne0gt0d 11398 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 < 𝑖) |
| 117 | | nnssnn0 12529 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
⊆ ℕ0 |
| 118 | | nn0uz 12920 |
. . . . . . . . . . . . . . . . 17
⊢
ℕ0 = (ℤ≥‘0) |
| 119 | 117, 118 | sseqtri 4032 |
. . . . . . . . . . . . . . . 16
⊢ ℕ
⊆ (ℤ≥‘0) |
| 120 | 119, 69 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
| 121 | | eluzfz1 13571 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) |
| 122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
| 123 | 96, 122 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄‘0) ∈ 𝐻) |
| 124 | 91, 123 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) |
| 125 | 124 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ∈ ℝ) |
| 126 | 104 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘𝑖) ∈ ℝ) |
| 127 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 0 < 𝑖) |
| 128 | 93 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 𝑄 Isom < , < ((0...𝑀), 𝐻)) |
| 129 | 122 | anim1i 615 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) |
| 130 | 129 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) |
| 131 | | isorel 7346 |
. . . . . . . . . . . . 13
⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖))) |
| 132 | 128, 130,
131 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖))) |
| 133 | 127, 132 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) < (𝑄‘𝑖)) |
| 134 | 125, 126,
133 | ltled 11409 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖)) |
| 135 | 116, 134 | syldan 591 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖)) |
| 136 | 107, 135 | pm2.61dan 813 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖)) |
| 137 | 136 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ (𝑄‘𝑖)) |
| 138 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘𝑖) = -π) |
| 139 | 137, 138 | breqtrd 5169 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ -π) |
| 140 | 70 | rexrd 11311 |
. . . . . . . 8
⊢ (𝜑 → -π ∈
ℝ*) |
| 141 | 71 | rexrd 11311 |
. . . . . . . 8
⊢ (𝜑 → π ∈
ℝ*) |
| 142 | | lbicc2 13504 |
. . . . . . . . . . . . . 14
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ -π
≤ π) → -π ∈ (-π[,]π)) |
| 143 | 16, 17, 23, 142 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢ -π
∈ (-π[,]π) |
| 144 | 143 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → -π ∈
(-π[,]π)) |
| 145 | | ubicc2 13505 |
. . . . . . . . . . . . . 14
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ -π
≤ π) → π ∈ (-π[,]π)) |
| 146 | 16, 17, 23, 145 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢ π
∈ (-π[,]π) |
| 147 | 146 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → π ∈
(-π[,]π)) |
| 148 | | iocssicc 13477 |
. . . . . . . . . . . . 13
⊢
(-π(,]π) ⊆ (-π[,]π) |
| 149 | 148, 80 | sselid 3981 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π[,]π)) |
| 150 | | tpssi 4838 |
. . . . . . . . . . . 12
⊢ ((-π
∈ (-π[,]π) ∧ π ∈ (-π[,]π) ∧ (𝐸‘𝑋) ∈ (-π[,]π)) → {-π,
π, (𝐸‘𝑋)} ⊆
(-π[,]π)) |
| 151 | 144, 147,
149, 150 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π)) |
| 152 | | difssd 4137 |
. . . . . . . . . . 11
⊢ (𝜑 → ((-π[,]π) ∖
dom 𝐺) ⊆
(-π[,]π)) |
| 153 | 151, 152 | unssd 4192 |
. . . . . . . . . 10
⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆
(-π[,]π)) |
| 154 | 11, 153 | eqsstrid 4022 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ⊆ (-π[,]π)) |
| 155 | 154, 123 | sseldd 3984 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘0) ∈
(-π[,]π)) |
| 156 | | iccgelb 13443 |
. . . . . . . 8
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ (𝑄‘0) ∈ (-π[,]π))
→ -π ≤ (𝑄‘0)) |
| 157 | 140, 141,
155, 156 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → -π ≤ (𝑄‘0)) |
| 158 | 157 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ≤ (𝑄‘0)) |
| 159 | 124 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ∈ ℝ) |
| 160 | 15 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ∈
ℝ) |
| 161 | 159, 160 | letri3d 11403 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → ((𝑄‘0) = -π ↔ ((𝑄‘0) ≤ -π ∧ -π ≤ (𝑄‘0)))) |
| 162 | 139, 158,
161 | mpbir2and 713 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) = -π) |
| 163 | 59, 53 | sselii 3980 |
. . . . . . 7
⊢ -π
∈ 𝐻 |
| 164 | | f1ofo 6855 |
. . . . . . . . 9
⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)–onto→𝐻) |
| 165 | 94, 164 | syl 17 |
. . . . . . . 8
⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–onto→𝐻) |
| 166 | | forn 6823 |
. . . . . . . 8
⊢ (𝑄:(0...𝑀)–onto→𝐻 → ran 𝑄 = 𝐻) |
| 167 | 93, 165, 166 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ran 𝑄 = 𝐻) |
| 168 | 163, 167 | eleqtrrid 2848 |
. . . . . 6
⊢ (𝜑 → -π ∈ ran 𝑄) |
| 169 | | ffn 6736 |
. . . . . . 7
⊢ (𝑄:(0...𝑀)⟶𝐻 → 𝑄 Fn (0...𝑀)) |
| 170 | | fvelrnb 6969 |
. . . . . . 7
⊢ (𝑄 Fn (0...𝑀) → (-π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π)) |
| 171 | 96, 169, 170 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (-π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π)) |
| 172 | 168, 171 | mpbid 232 |
. . . . 5
⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π) |
| 173 | 162, 172 | r19.29a 3162 |
. . . 4
⊢ (𝜑 → (𝑄‘0) = -π) |
| 174 | 59, 55 | sselii 3980 |
. . . . . . 7
⊢ π
∈ 𝐻 |
| 175 | 174, 167 | eleqtrrid 2848 |
. . . . . 6
⊢ (𝜑 → π ∈ ran 𝑄) |
| 176 | | fvelrnb 6969 |
. . . . . . 7
⊢ (𝑄 Fn (0...𝑀) → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π)) |
| 177 | 96, 169, 176 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π)) |
| 178 | 175, 177 | mpbid 232 |
. . . . 5
⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π) |
| 179 | 96, 154 | fssd 6753 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π)) |
| 180 | | eluzfz2 13572 |
. . . . . . . . . . 11
⊢ (𝑀 ∈
(ℤ≥‘0) → 𝑀 ∈ (0...𝑀)) |
| 181 | 120, 180 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
| 182 | 179, 181 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘𝑀) ∈ (-π[,]π)) |
| 183 | | iccleub 13442 |
. . . . . . . . 9
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ (𝑄‘𝑀) ∈ (-π[,]π)) → (𝑄‘𝑀) ≤ π) |
| 184 | 140, 141,
182, 183 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘𝑀) ≤ π) |
| 185 | 184 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ≤ π) |
| 186 | | id 22 |
. . . . . . . . . 10
⊢ ((𝑄‘𝑖) = π → (𝑄‘𝑖) = π) |
| 187 | 186 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝑄‘𝑖) = π → π = (𝑄‘𝑖)) |
| 188 | 187 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π = (𝑄‘𝑖)) |
| 189 | 105 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑖)) |
| 190 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀)) |
| 191 | 190 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) = (𝑄‘𝑀)) |
| 192 | 189, 191 | breqtrd 5169 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀)) |
| 193 | 109 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ∈ ℝ) |
| 194 | | elfzel2 13562 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ) |
| 195 | 194 | zred 12722 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ) |
| 196 | 195 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ∈ ℝ) |
| 197 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀) |
| 198 | 197 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ≤ 𝑀) |
| 199 | | neqne 2948 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑖 = 𝑀 → 𝑖 ≠ 𝑀) |
| 200 | 199 | necomd 2996 |
. . . . . . . . . . . . 13
⊢ (¬
𝑖 = 𝑀 → 𝑀 ≠ 𝑖) |
| 201 | 200 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ≠ 𝑖) |
| 202 | 193, 196,
198, 201 | leneltd 11415 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 < 𝑀) |
| 203 | 104 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ∈ ℝ) |
| 204 | 87, 182 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ) |
| 205 | 204 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑀) ∈ ℝ) |
| 206 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑖 < 𝑀) |
| 207 | 93 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑄 Isom < , < ((0...𝑀), 𝐻)) |
| 208 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀)) |
| 209 | 181 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (0...𝑀)) |
| 210 | 208, 209 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀))) |
| 211 | 210 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀))) |
| 212 | | isorel 7346 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀))) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀))) |
| 213 | 207, 211,
212 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀))) |
| 214 | 206, 213 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) < (𝑄‘𝑀)) |
| 215 | 203, 205,
214 | ltled 11409 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀)) |
| 216 | 202, 215 | syldan 591 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀)) |
| 217 | 192, 216 | pm2.61dan 813 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀)) |
| 218 | 217 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑖) ≤ (𝑄‘𝑀)) |
| 219 | 188, 218 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ≤ (𝑄‘𝑀)) |
| 220 | 204 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ∈ ℝ) |
| 221 | 14 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ∈
ℝ) |
| 222 | 220, 221 | letri3d 11403 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → ((𝑄‘𝑀) = π ↔ ((𝑄‘𝑀) ≤ π ∧ π ≤ (𝑄‘𝑀)))) |
| 223 | 185, 219,
222 | mpbir2and 713 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) = π) |
| 224 | 223 | rexlimdv3a 3159 |
. . . . 5
⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π → (𝑄‘𝑀) = π)) |
| 225 | 178, 224 | mpd 15 |
. . . 4
⊢ (𝜑 → (𝑄‘𝑀) = π) |
| 226 | | elfzoelz 13699 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ) |
| 227 | 226 | zred 12722 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ) |
| 228 | 227 | ltp1d 12198 |
. . . . . . 7
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1)) |
| 229 | 228 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 < (𝑖 + 1)) |
| 230 | | elfzofz 13715 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
| 231 | | fzofzp1 13803 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
| 232 | 230, 231 | jca 511 |
. . . . . . 7
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀))) |
| 233 | | isorel 7346 |
. . . . . . 7
⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀))) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
| 234 | 93, 232, 233 | syl2an 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
| 235 | 229, 234 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
| 236 | 235 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
| 237 | 173, 225,
236 | jca31 514 |
. . 3
⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
| 238 | 7 | fourierdlem2 46124 |
. . . 4
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
| 239 | 69, 238 | syl 17 |
. . 3
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
| 240 | 101, 237,
239 | mpbir2and 713 |
. 2
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
| 241 | | fourierdlem114.g |
. . . . 5
⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) |
| 242 | 241 | reseq1i 5993 |
. . . 4
⊢ (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 243 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈
ℝ*) |
| 244 | 17 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈
ℝ*) |
| 245 | 179 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π)) |
| 246 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀)) |
| 247 | 243, 244,
245, 246 | fourierdlem27 46149 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆
(-π(,)π)) |
| 248 | 247 | resabs1d 6026 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
| 249 | 242, 248 | eqtr2id 2790 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
| 250 | | fourierdlem114.gcn |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) |
| 251 | 250, 7, 69, 240, 11, 167 | fourierdlem38 46160 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
| 252 | 249, 251 | eqeltrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
| 253 | 249 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
| 254 | 250 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺 ∈ (dom 𝐺–cn→ℂ)) |
| 255 | | fourierdlem114.rlim |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) |
| 256 | 255 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) |
| 257 | | fourierdlem114.llim |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) |
| 258 | 257 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) |
| 259 | 93 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 Isom < , < ((0...𝑀), 𝐻)) |
| 260 | 259, 94, 95 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶𝐻) |
| 261 | 81 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐸‘𝑋) ∈ ℝ) |
| 262 | 259, 165,
166 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran 𝑄 = 𝐻) |
| 263 | 254, 256,
258, 259, 260, 246, 235, 247, 261, 11, 262 | fourierdlem46 46167 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) ≠ ∅ ∧ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) ≠ ∅)) |
| 264 | 263 | simpld 494 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) ≠ ∅) |
| 265 | 253, 264 | eqnetrd 3008 |
. 2
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) ≠ ∅) |
| 266 | 249 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
| 267 | 263 | simprd 495 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) ≠ ∅) |
| 268 | 266, 267 | eqnetrd 3008 |
. 2
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) ≠ ∅) |
| 269 | | fourierdlem114.a |
. 2
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦
(∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) |
| 270 | | fourierdlem114.b |
. 2
⊢ 𝐵 = (𝑛 ∈ ℕ ↦
(∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) |
| 271 | | fourierdlem114.s |
. 2
⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) |
| 272 | 83 | tpid3 4773 |
. . . . 5
⊢ (𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)} |
| 273 | | elun1 4182 |
. . . . 5
⊢ ((𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)} → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) |
| 274 | 272, 273 | mp1i 13 |
. . . 4
⊢ (𝜑 → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) |
| 275 | 274, 11 | eleqtrrdi 2852 |
. . 3
⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐻) |
| 276 | 275, 167 | eleqtrrd 2844 |
. 2
⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄) |
| 277 | 1, 2, 3, 4, 5, 6, 7, 69, 240, 252, 265, 268, 269, 270, 271, 78, 276 | fourierdlem113 46234 |
1
⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) |