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