Proof of Theorem fourierdlem37
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . . 4
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ (0..^𝑀) |
2 | | ltso 10118 |
. . . . . 6
⊢ < Or
ℝ |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → < Or
ℝ) |
4 | | fzfi 12771 |
. . . . . . 7
⊢
(0...𝑀) ∈
Fin |
5 | | fzossfz 12488 |
. . . . . . . 8
⊢
(0..^𝑀) ⊆
(0...𝑀) |
6 | 1, 5 | sstri 3612 |
. . . . . . 7
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ (0...𝑀) |
7 | | ssfi 8180 |
. . . . . . 7
⊢
(((0...𝑀) ∈ Fin
∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ (0...𝑀)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ∈ Fin) |
8 | 4, 6, 7 | mp2an 708 |
. . . . . 6
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ∈ Fin |
9 | 8 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ∈ Fin) |
10 | | 0zd 11389 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℤ) |
11 | | fourierdlem37.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℕ) |
12 | 11 | nnzd 11481 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | 11 | nngt0d 11064 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝑀) |
14 | | fzolb 12476 |
. . . . . . . . 9
⊢ (0 ∈
(0..^𝑀) ↔ (0 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 0 < 𝑀)) |
15 | 10, 12, 13, 14 | syl3anbrc 1246 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ (0..^𝑀)) |
16 | 15 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ (0..^𝑀)) |
17 | | fourierdlem37.q |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
18 | | fourierdlem37.p |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
19 | 18 | fourierdlem2 40326 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
20 | 11, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
21 | 17, 20 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
22 | 21 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
23 | 22 | simplld 791 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
24 | 18, 11, 17 | fourierdlem11 40335 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) |
25 | 24 | simp1d 1073 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) |
26 | 23, 25 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) |
27 | 26, 23 | eqled 10140 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄‘0) ≤ 𝐴) |
28 | 27 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ 𝐴) |
29 | | iftrue 4092 |
. . . . . . . . . . . 12
⊢ ((𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = 𝐴) |
30 | 29 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ ((𝐸‘𝑥) = 𝐵 → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
31 | 30 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
32 | 28, 31 | breqtrd 4679 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
33 | 26 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ∈ ℝ) |
34 | 25 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ) |
35 | 34 | rexrd 10089 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈
ℝ*) |
36 | 24 | simp2d 1074 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ ℝ) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ) |
38 | | iocssre 12253 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴(,]𝐵) ⊆
ℝ) |
39 | 35, 37, 38 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ) |
40 | 24 | simp3d 1075 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 < 𝐵) |
41 | | fourierdlem37.t |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = (𝐵 − 𝐴) |
42 | | fourierdlem37.e |
. . . . . . . . . . . . . . 15
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
43 | 25, 36, 40, 41, 42 | fourierdlem4 40328 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵)) |
44 | 43 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵)) |
45 | 39, 44 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ ℝ) |
46 | 23 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) = 𝐴) |
47 | | elioc2 12236 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵))) |
48 | 35, 37, 47 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵))) |
49 | 44, 48 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵)) |
50 | 49 | simp2d 1074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝐸‘𝑥)) |
51 | 46, 50 | eqbrtrd 4675 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) < (𝐸‘𝑥)) |
52 | 33, 45, 51 | ltled 10185 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐸‘𝑥)) |
53 | 52 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ (𝐸‘𝑥)) |
54 | | iffalse 4095 |
. . . . . . . . . . . 12
⊢ (¬
(𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = (𝐸‘𝑥)) |
55 | 54 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ (¬
(𝐸‘𝑥) = 𝐵 → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
56 | 55 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
57 | 53, 56 | breqtrd 4679 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
58 | 32, 57 | pm2.61dan 832 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
59 | | fourierdlem37.l |
. . . . . . . . . 10
⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) |
60 | 59 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))) |
61 | | eqeq1 2626 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐸‘𝑥) → (𝑦 = 𝐵 ↔ (𝐸‘𝑥) = 𝐵)) |
62 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐸‘𝑥) → 𝑦 = (𝐸‘𝑥)) |
63 | 61, 62 | ifbieq2d 4111 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐸‘𝑥) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
64 | 63 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 = (𝐸‘𝑥)) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
65 | 34, 45 | ifcld 4131 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) ∈ ℝ) |
66 | 60, 64, 44, 65 | fvmptd 6288 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐿‘(𝐸‘𝑥)) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
67 | 58, 66 | breqtrrd 4681 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥))) |
68 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0)) |
69 | 68 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑖 = 0 → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥)) ↔ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥)))) |
70 | 69 | elrab 3363 |
. . . . . . 7
⊢ (0 ∈
{𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥)))) |
71 | 16, 67, 70 | sylanbrc 698 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) |
72 | | ne0i 3921 |
. . . . . 6
⊢ (0 ∈
{𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅) |
73 | 71, 72 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅) |
74 | | fzssz 12343 |
. . . . . . . . 9
⊢
(0...𝑀) ⊆
ℤ |
75 | 5, 74 | sstri 3612 |
. . . . . . . 8
⊢
(0..^𝑀) ⊆
ℤ |
76 | | zssre 11384 |
. . . . . . . 8
⊢ ℤ
⊆ ℝ |
77 | 75, 76 | sstri 3612 |
. . . . . . 7
⊢
(0..^𝑀) ⊆
ℝ |
78 | 1, 77 | sstri 3612 |
. . . . . 6
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ ℝ |
79 | 78 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ ℝ) |
80 | | fisupcl 8375 |
. . . . 5
⊢ (( <
Or ℝ ∧ ({𝑖 ∈
(0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ∈ Fin ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ⊆ ℝ)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) |
81 | 3, 9, 73, 79, 80 | syl13anc 1328 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) |
82 | 1, 81 | sseldi 3601 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ (0..^𝑀)) |
83 | | fourierdlem37.i |
. . 3
⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )) |
84 | 82, 83 | fmptd 6385 |
. 2
⊢ (𝜑 → 𝐼:ℝ⟶(0..^𝑀)) |
85 | 81 | ex 450 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})) |
86 | 84, 85 | jca 554 |
1
⊢ (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}))) |