Proof of Theorem fourierdlem37
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3969 |
. . . 4
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ (0..^𝑀) |
2 | | ltso 10799 |
. . . . . 6
⊢ < Or
ℝ |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → < Or
ℝ) |
4 | | fzfi 13431 |
. . . . . . 7
⊢
(0...𝑀) ∈
Fin |
5 | | fzossfz 13147 |
. . . . . . . 8
⊢
(0..^𝑀) ⊆
(0...𝑀) |
6 | 1, 5 | sstri 3886 |
. . . . . . 7
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ (0...𝑀) |
7 | | ssfi 8772 |
. . . . . . 7
⊢
(((0...𝑀) ∈ Fin
∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ (0...𝑀)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ∈ Fin) |
8 | 4, 6, 7 | mp2an 692 |
. . . . . 6
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ∈ Fin |
9 | 8 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ∈ Fin) |
10 | | 0zd 12074 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℤ) |
11 | | fourierdlem37.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℕ) |
12 | 11 | nnzd 12167 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | 11 | nngt0d 11765 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝑀) |
14 | | fzolb 13135 |
. . . . . . . . 9
⊢ (0 ∈
(0..^𝑀) ↔ (0 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 0 < 𝑀)) |
15 | 10, 12, 13, 14 | syl3anbrc 1344 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ (0..^𝑀)) |
16 | 15 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ (0..^𝑀)) |
17 | | fourierdlem37.q |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
18 | | fourierdlem37.p |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
19 | 18 | fourierdlem2 43192 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
20 | 11, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
21 | 17, 20 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
22 | 21 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
23 | 22 | simplld 768 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
24 | 18, 11, 17 | fourierdlem11 43201 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) |
25 | 24 | simp1d 1143 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) |
26 | 23, 25 | eqeltrd 2833 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) |
27 | 26, 23 | eqled 10821 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄‘0) ≤ 𝐴) |
28 | 27 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ 𝐴) |
29 | | iftrue 4420 |
. . . . . . . . . . . 12
⊢ ((𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = 𝐴) |
30 | 29 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ ((𝐸‘𝑥) = 𝐵 → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
31 | 30 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
32 | 28, 31 | breqtrd 5056 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
33 | 26 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ∈ ℝ) |
34 | 25 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ) |
35 | 34 | rexrd 10769 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈
ℝ*) |
36 | 24 | simp2d 1144 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ ℝ) |
37 | 36 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ) |
38 | | iocssre 12901 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴(,]𝐵) ⊆
ℝ) |
39 | 35, 37, 38 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ) |
40 | 24 | simp3d 1145 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 < 𝐵) |
41 | | fourierdlem37.t |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = (𝐵 − 𝐴) |
42 | | fourierdlem37.e |
. . . . . . . . . . . . . . 15
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
43 | 25, 36, 40, 41, 42 | fourierdlem4 43194 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵)) |
44 | 43 | ffvelrnda 6861 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵)) |
45 | 39, 44 | sseldd 3878 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ ℝ) |
46 | 23 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) = 𝐴) |
47 | | elioc2 12884 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵))) |
48 | 35, 37, 47 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵))) |
49 | 44, 48 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵)) |
50 | 49 | simp2d 1144 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝐸‘𝑥)) |
51 | 46, 50 | eqbrtrd 5052 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) < (𝐸‘𝑥)) |
52 | 33, 45, 51 | ltled 10866 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐸‘𝑥)) |
53 | 52 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ (𝐸‘𝑥)) |
54 | | iffalse 4423 |
. . . . . . . . . . . 12
⊢ (¬
(𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = (𝐸‘𝑥)) |
55 | 54 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (¬
(𝐸‘𝑥) = 𝐵 → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
56 | 55 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
57 | 53, 56 | breqtrd 5056 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
58 | 32, 57 | pm2.61dan 813 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
59 | | fourierdlem37.l |
. . . . . . . . . 10
⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) |
60 | 59 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))) |
61 | | eqeq1 2742 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐸‘𝑥) → (𝑦 = 𝐵 ↔ (𝐸‘𝑥) = 𝐵)) |
62 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐸‘𝑥) → 𝑦 = (𝐸‘𝑥)) |
63 | 61, 62 | ifbieq2d 4440 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐸‘𝑥) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
64 | 63 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 = (𝐸‘𝑥)) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
65 | 34, 45 | ifcld 4460 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) ∈ ℝ) |
66 | 60, 64, 44, 65 | fvmptd 6782 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐿‘(𝐸‘𝑥)) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
67 | 58, 66 | breqtrrd 5058 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥))) |
68 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0)) |
69 | 68 | breq1d 5040 |
. . . . . . . 8
⊢ (𝑖 = 0 → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥)) ↔ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥)))) |
70 | 69 | elrab 3588 |
. . . . . . 7
⊢ (0 ∈
{𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥)))) |
71 | 16, 67, 70 | sylanbrc 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) |
72 | 71 | ne0d 4224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅) |
73 | | fzssz 13000 |
. . . . . . . . 9
⊢
(0...𝑀) ⊆
ℤ |
74 | 5, 73 | sstri 3886 |
. . . . . . . 8
⊢
(0..^𝑀) ⊆
ℤ |
75 | | zssre 12069 |
. . . . . . . 8
⊢ ℤ
⊆ ℝ |
76 | 74, 75 | sstri 3886 |
. . . . . . 7
⊢
(0..^𝑀) ⊆
ℝ |
77 | 1, 76 | sstri 3886 |
. . . . . 6
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ ℝ |
78 | 77 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ ℝ) |
79 | | fisupcl 9006 |
. . . . 5
⊢ (( <
Or ℝ ∧ ({𝑖 ∈
(0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ∈ Fin ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ ℝ)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) |
80 | 3, 9, 72, 78, 79 | syl13anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) |
81 | 1, 80 | sseldi 3875 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ (0..^𝑀)) |
82 | | fourierdlem37.i |
. . 3
⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )) |
83 | 81, 82 | fmptd 6888 |
. 2
⊢ (𝜑 → 𝐼:ℝ⟶(0..^𝑀)) |
84 | 80 | ex 416 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})) |
85 | 83, 84 | jca 515 |
1
⊢ (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}))) |