Step | Hyp | Ref
| Expression |
1 | | prfi 8781 |
. . . 4
⊢ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼} ∈
Fin |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} ∈ Fin) |
3 | | fourierdlem71.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ) |
4 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → 𝐹:dom 𝐹⟶ℝ) |
5 | | simpl 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → 𝜑) |
6 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) |
7 | | fourierdlem71.q |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
8 | | ovex 7178 |
. . . . . . . . . . . . 13
⊢
(0...𝑀) ∈
V |
9 | 8 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0...𝑀) ∈ V) |
10 | | fex 6980 |
. . . . . . . . . . . 12
⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ V) → 𝑄 ∈ V) |
11 | 7, 9, 10 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ V) |
12 | | rnexg 7603 |
. . . . . . . . . . 11
⊢ (𝑄 ∈ V → ran 𝑄 ∈ V) |
13 | | inex1g 5214 |
. . . . . . . . . . 11
⊢ (ran
𝑄 ∈ V → (ran
𝑄 ∩ dom 𝐹) ∈ V) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (ran 𝑄 ∩ dom 𝐹) ∈ V) |
15 | 14 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → (ran 𝑄 ∩ dom 𝐹) ∈ V) |
16 | | fourierdlem71.i |
. . . . . . . . . . . . . 14
⊢ 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
17 | | ovex 7178 |
. . . . . . . . . . . . . . 15
⊢
(0..^𝑀) ∈
V |
18 | 17 | mptex 6977 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ V |
19 | 16, 18 | eqeltri 2906 |
. . . . . . . . . . . . 13
⊢ 𝐼 ∈ V |
20 | 19 | rnex 7606 |
. . . . . . . . . . . 12
⊢ ran 𝐼 ∈ V |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐼 ∈ V) |
22 | 21 | uniexd 7457 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran 𝐼 ∈ V) |
23 | 22 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → ∪ ran 𝐼 ∈ V) |
24 | | uniprg 4844 |
. . . . . . . . 9
⊢ (((ran
𝑄 ∩ dom 𝐹) ∈ V ∧ ∪ ran 𝐼 ∈ V) → ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
25 | 15, 23, 24 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
26 | 6, 25 | eleqtrd 2912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
27 | | elinel2 4170 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ran 𝑄 ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹) |
28 | 27 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹) |
29 | | simpll 763 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝜑) |
30 | | elunnel1 4123 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ ∪ ran
𝐼) |
31 | 30 | adantll 710 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ ∪ ran
𝐼) |
32 | 16 | funmpt2 6387 |
. . . . . . . . . . . . 13
⊢ Fun 𝐼 |
33 | | elunirn 7001 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐼 → (𝑥 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖))) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖)) |
35 | 34 | biimpi 217 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ ran 𝐼 → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖)) |
36 | 35 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖)) |
37 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ dom 𝐼) |
38 | | ovex 7178 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V |
39 | 38, 16 | dmmpti 6485 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom 𝐼 = (0..^𝑀) |
40 | 37, 39 | eleqtrdi 2920 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ (0..^𝑀)) |
41 | 40 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝑖 ∈ (0..^𝑀)) |
42 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V) |
43 | 16 | fvmpt2 6771 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑀) ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
44 | 41, 42, 43 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
45 | | fourierdlem71.fcn |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
46 | | cncff 23428 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ) |
47 | | fdm 6515 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
48 | 45, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
49 | 40, 48 | sylan2 592 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
50 | | ssdmres 5869 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
51 | 49, 50 | sylibr 235 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹) |
52 | 44, 51 | eqsstrd 4002 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ⊆ dom 𝐹) |
53 | 52 | 3adant3 1124 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) → (𝐼‘𝑖) ⊆ dom 𝐹) |
54 | | simp3 1130 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) → 𝑥 ∈ (𝐼‘𝑖)) |
55 | 53, 54 | sseldd 3965 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) → 𝑥 ∈ dom 𝐹) |
56 | 55 | 3exp 1111 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑖 ∈ dom 𝐼 → (𝑥 ∈ (𝐼‘𝑖) → 𝑥 ∈ dom 𝐹))) |
57 | 56 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → (𝑖 ∈ dom 𝐼 → (𝑥 ∈ (𝐼‘𝑖) → 𝑥 ∈ dom 𝐹))) |
58 | 57 | rexlimdv 3280 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖) → 𝑥 ∈ dom 𝐹)) |
59 | 36, 58 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → 𝑥 ∈ dom 𝐹) |
60 | 29, 31, 59 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹) |
61 | 28, 60 | pm2.61dan 809 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) → 𝑥 ∈ dom 𝐹) |
62 | 5, 26, 61 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → 𝑥 ∈ dom 𝐹) |
63 | 4, 62 | ffvelrnd 6844 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → (𝐹‘𝑥) ∈ ℝ) |
64 | 63 | recnd 10657 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → (𝐹‘𝑥) ∈ ℂ) |
65 | 64 | abscld 14784 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) →
(abs‘(𝐹‘𝑥)) ∈
ℝ) |
66 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = (ran 𝑄 ∩ dom 𝐹)) |
67 | | fzfid 13329 |
. . . . . . . . . 10
⊢ (𝜑 → (0...𝑀) ∈ Fin) |
68 | | rnffi 41307 |
. . . . . . . . . 10
⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin) |
69 | 7, 67, 68 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝑄 ∈ Fin) |
70 | | infi 8730 |
. . . . . . . . 9
⊢ (ran
𝑄 ∈ Fin → (ran
𝑄 ∩ dom 𝐹) ∈ Fin) |
71 | 69, 70 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ran 𝑄 ∩ dom 𝐹) ∈ Fin) |
72 | 71 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → (ran 𝑄 ∩ dom 𝐹) ∈ Fin) |
73 | 66, 72 | eqeltrd 2910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 ∈ Fin) |
74 | | simpll 763 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥 ∈ 𝑤) → 𝜑) |
75 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ 𝑤) |
76 | | simpl 483 |
. . . . . . . . . 10
⊢ ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥 ∈ 𝑤) → 𝑤 = (ran 𝑄 ∩ dom 𝐹)) |
77 | 75, 76 | eleqtrd 2912 |
. . . . . . . . 9
⊢ ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) |
78 | 77 | adantll 710 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) |
79 | 3 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝐹:dom 𝐹⟶ℝ) |
80 | 27 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹) |
81 | 79, 80 | ffvelrnd 6844 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (𝐹‘𝑥) ∈ ℝ) |
82 | 81 | recnd 10657 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (𝐹‘𝑥) ∈ ℂ) |
83 | 82 | abscld 14784 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
84 | 74, 78, 83 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥 ∈ 𝑤) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
85 | 84 | ralrimiva 3179 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ∈ ℝ) |
86 | | fimaxre3 11575 |
. . . . . 6
⊢ ((𝑤 ∈ Fin ∧ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
87 | 73, 85, 86 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
88 | 87 | adantlr 711 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
89 | | simpll 763 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝜑) |
90 | | neqne 3021 |
. . . . . . 7
⊢ (¬
𝑤 = (ran 𝑄 ∩ dom 𝐹) → 𝑤 ≠ (ran 𝑄 ∩ dom 𝐹)) |
91 | | elprn1 41790 |
. . . . . . 7
⊢ ((𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} ∧ 𝑤 ≠ (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ∪ ran 𝐼) |
92 | 90, 91 | sylan2 592 |
. . . . . 6
⊢ ((𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ∪ ran 𝐼) |
93 | 92 | adantll 710 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ∪ ran 𝐼) |
94 | | fzofi 13330 |
. . . . . . . 8
⊢
(0..^𝑀) ∈
Fin |
95 | 16 | rnmptfi 41303 |
. . . . . . . 8
⊢
((0..^𝑀) ∈ Fin
→ ran 𝐼 ∈
Fin) |
96 | 94, 95 | ax-mp 5 |
. . . . . . 7
⊢ ran 𝐼 ∈ Fin |
97 | 96 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ran 𝐼 ∈ Fin) |
98 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → 𝐹:dom 𝐹⟶ℝ) |
99 | 98, 59 | ffvelrnd 6844 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → (𝐹‘𝑥) ∈ ℝ) |
100 | 99 | recnd 10657 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → (𝐹‘𝑥) ∈ ℂ) |
101 | 100 | adantlr 711 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑥 ∈ ∪ ran
𝐼) → (𝐹‘𝑥) ∈ ℂ) |
102 | 101 | abscld 14784 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑥 ∈ ∪ ran
𝐼) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
103 | 38, 16 | fnmpti 6484 |
. . . . . . . . . . 11
⊢ 𝐼 Fn (0..^𝑀) |
104 | | fvelrnb 6719 |
. . . . . . . . . . 11
⊢ (𝐼 Fn (0..^𝑀) → (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡)) |
105 | 103, 104 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
106 | 105 | biimpi 217 |
. . . . . . . . 9
⊢ (𝑡 ∈ ran 𝐼 → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
107 | 106 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
108 | 7 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
109 | | elfzofz 13041 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
110 | 109 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
111 | 108, 110 | ffvelrnd 6844 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
112 | | fzofzp1 13122 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
113 | 112 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
114 | 108, 113 | ffvelrnd 6844 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
115 | | fourierdlem71.l |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
116 | | fourierdlem71.r |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
117 | 111, 114,
45, 115, 116 | cncfioobd 42056 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏) |
118 | 117 | 3adant3 1124 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏) |
119 | | fvres 6682 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥) = (𝐹‘𝑥)) |
120 | 119 | fveq2d 6667 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) = (abs‘(𝐹‘𝑥))) |
121 | 120 | breq1d 5067 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
122 | 121 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
123 | 122 | ralbidva 3193 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
124 | 123 | rexbidv 3294 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
125 | 124 | 3adant3 1124 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
126 | 38, 43 | mpan2 687 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (0..^𝑀) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
127 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼‘𝑖) = 𝑡 → (𝐼‘𝑖) = 𝑡) |
128 | 126, 127 | sylan9req 2874 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡) |
129 | 128 | 3adant1 1122 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡) |
130 | 129 | raleqdv 3413 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
131 | 130 | rexbidv 3294 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
132 | 125, 131 | bitrd 280 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
133 | 118, 132 | mpbid 233 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏) |
134 | 133 | 3exp 1111 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏))) |
135 | 134 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏))) |
136 | 135 | rexlimdv 3280 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
137 | 107, 136 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏) |
138 | 137 | adantlr 711 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏) |
139 | | eqimss 4020 |
. . . . . . 7
⊢ (𝑤 = ∪
ran 𝐼 → 𝑤 ⊆ ∪ ran 𝐼) |
140 | 139 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → 𝑤 ⊆ ∪ ran
𝐼) |
141 | 97, 102, 138, 140 | ssfiunibd 41452 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
142 | 89, 93, 141 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
143 | 88, 142 | pm2.61dan 809 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
144 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ran 𝑄) |
145 | | elinel2 4170 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹) |
146 | 145 | ad2antlr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ dom 𝐹) |
147 | 144, 146 | elind 4168 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) |
148 | | elun1 4149 |
. . . . . . . 8
⊢ (𝑥 ∈ (ran 𝑄 ∩ dom 𝐹) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
149 | 147, 148 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
150 | | fourierdlem71.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℕ) |
151 | 150 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑀 ∈ ℕ) |
152 | 7 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ) |
153 | | elinel1 4169 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹) → 𝑥 ∈ (𝐴[,]𝐵)) |
154 | 153 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ (𝐴[,]𝐵)) |
155 | | fourierdlem71.q0 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
156 | 155 | eqcomd 2824 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 = (𝑄‘0)) |
157 | 156 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝐴 = (𝑄‘0)) |
158 | | fourierdlem71.10 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) |
159 | 158 | eqcomd 2824 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 = (𝑄‘𝑀)) |
160 | 159 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝐵 = (𝑄‘𝑀)) |
161 | 157, 160 | oveq12d 7163 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀))) |
162 | 154, 161 | eleqtrd 2912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) |
163 | 162 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) |
164 | | simpr 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ¬ 𝑥 ∈ ran 𝑄) |
165 | | fveq2 6663 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗)) |
166 | 165 | breq1d 5067 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < 𝑥 ↔ (𝑄‘𝑗) < 𝑥)) |
167 | 166 | cbvrabv 3489 |
. . . . . . . . . . . 12
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝑥} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑥} |
168 | 167 | supeq1i 8899 |
. . . . . . . . . . 11
⊢
sup({𝑘 ∈
(0..^𝑀) ∣ (𝑄‘𝑘) < 𝑥}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑥}, ℝ, < ) |
169 | 151, 152,
163, 164, 168 | fourierdlem25 42294 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
170 | 40 | ad2antrl 724 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → 𝑖 ∈ (0..^𝑀)) |
171 | | simprr 769 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → 𝑥 ∈ (𝐼‘𝑖)) |
172 | 170, 126 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
173 | 171, 172 | eleqtrd 2912 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
174 | 170, 173 | jca 512 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
175 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0..^𝑀)) |
176 | 175, 39 | eleqtrrdi 2921 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ dom 𝐼) |
177 | 176 | ad2antrl 724 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑖 ∈ dom 𝐼) |
178 | | simprr 769 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
179 | 126 | eqcomd 2824 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖)) |
180 | 179 | ad2antrl 724 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖)) |
181 | 178, 180 | eleqtrd 2912 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑥 ∈ (𝐼‘𝑖)) |
182 | 177, 181 | jca 512 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) |
183 | 174, 182 | impbida 797 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) ↔ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))) |
184 | 183 | rexbidv2 3292 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
185 | 184 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
186 | 169, 185 | mpbird 258 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖)) |
187 | 186, 34 | sylibr 235 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ∪ ran
𝐼) |
188 | | elun2 4150 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ ran 𝐼 → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
189 | 187, 188 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
190 | 149, 189 | pm2.61dan 809 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
191 | 190 | ralrimiva 3179 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
192 | | dfss3 3953 |
. . . . 5
⊢ (((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼) ↔ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
193 | 191, 192 | sylibr 235 |
. . . 4
⊢ (𝜑 → ((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
194 | 14, 22, 24 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
195 | 193, 194 | sseqtrrd 4005 |
. . 3
⊢ (𝜑 → ((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) |
196 | 2, 65, 143, 195 | ssfiunibd 41452 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) |
197 | | nfv 1906 |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
198 | | nfra1 3216 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 |
199 | 197, 198 | nfan 1891 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) |
200 | | fourierdlem71.dmf |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝐹 ⊆ ℝ) |
201 | 200 | sselda 3964 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ ℝ) |
202 | | fourierdlem71.b |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ ℝ) |
203 | 202 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐵 ∈ ℝ) |
204 | 203, 201 | resubcld 11056 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐵 − 𝑥) ∈ ℝ) |
205 | | fourierdlem71.t |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 = (𝐵 − 𝐴) |
206 | | fourierdlem71.a |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐴 ∈ ℝ) |
207 | 202, 206 | resubcld 11056 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
208 | 205, 207 | eqeltrid 2914 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ∈ ℝ) |
209 | 208 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝑇 ∈ ℝ) |
210 | | fourierdlem71.altb |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 < 𝐵) |
211 | 206, 202 | posdifd 11215 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
212 | 210, 211 | mpbid 233 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
213 | 212, 205 | breqtrrdi 5099 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 𝑇) |
214 | 213 | gt0ne0d 11192 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ≠ 0) |
215 | 214 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝑇 ≠ 0) |
216 | 204, 209,
215 | redivcld 11456 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ) |
217 | 216 | flcld 13156 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) |
218 | 217 | zred 12075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ) |
219 | 218, 209 | remulcld 10659 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ) |
220 | 201, 219 | readdcld 10658 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) |
221 | | fourierdlem71.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
222 | 221 | fvmpt2 6771 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
223 | 201, 220,
222 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
224 | 223 | fveq2d 6667 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘(𝐸‘𝑥)) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))) |
225 | | fvex 6676 |
. . . . . . . . . . . 12
⊢
(⌊‘((𝐵
− 𝑥) / 𝑇)) ∈ V |
226 | | eleq1 2897 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)) |
227 | 226 | anbi2d 628 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) ↔ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ))) |
228 | | oveq1 7152 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) |
229 | 228 | oveq2d 7161 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
230 | 229 | fveq2d 6667 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))) |
231 | 230 | eqeq1d 2820 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))) |
232 | 227, 231 | imbi12d 346 |
. . . . . . . . . . . 12
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) ↔ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))) |
233 | | fourierdlem71.fxpt |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) |
234 | 225, 232,
233 | vtocl 3557 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)) |
235 | 217, 234 | mpdan 683 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)) |
236 | 224, 235 | eqtr2d 2854 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘(𝐸‘𝑥))) |
237 | 236 | fveq2d 6667 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐸‘𝑥)))) |
238 | 237 | adantlr 711 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐸‘𝑥)))) |
239 | | fveq2 6663 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤)) |
240 | 239 | fveq2d 6667 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘𝑤))) |
241 | 240 | breq1d 5067 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → ((abs‘(𝐹‘𝑥)) ≤ 𝑦 ↔ (abs‘(𝐹‘𝑤)) ≤ 𝑦)) |
242 | 241 | cbvralvw 3447 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 ↔ ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦) |
243 | 242 | biimpi 217 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 → ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦) |
244 | 243 | ad2antlr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦) |
245 | | iocssicc 12813 |
. . . . . . . . . . 11
⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵) |
246 | 206 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐴 ∈ ℝ) |
247 | 210 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐴 < 𝐵) |
248 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
249 | | oveq2 7153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐵 − 𝑥) = (𝐵 − 𝑦)) |
250 | 249 | oveq1d 7160 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑦) / 𝑇)) |
251 | 250 | fveq2d 6667 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑦) / 𝑇))) |
252 | 251 | oveq1d 7160 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇)) |
253 | 248, 252 | oveq12d 7163 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑦 + ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇))) |
254 | 253 | cbvmptv 5160 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇))) |
255 | 221, 254 | eqtri 2841 |
. . . . . . . . . . . . 13
⊢ 𝐸 = (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇))) |
256 | 246, 203,
247, 205, 255 | fourierdlem4 42273 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐸:ℝ⟶(𝐴(,]𝐵)) |
257 | 256, 201 | ffvelrnd 6844 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵)) |
258 | 245, 257 | sseldi 3962 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ (𝐴[,]𝐵)) |
259 | 229 | eleq1d 2894 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹 ↔ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)) |
260 | 227, 259 | imbi12d 346 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹) ↔ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹))) |
261 | | fourierdlem71.xpt |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹) |
262 | 225, 260,
261 | vtocl 3557 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹) |
263 | 217, 262 | mpdan 683 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹) |
264 | 223, 263 | eqeltrd 2910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ dom 𝐹) |
265 | 258, 264 | elind 4168 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) |
266 | 265 | adantlr 711 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) |
267 | | fveq2 6663 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝐸‘𝑥) → (𝐹‘𝑤) = (𝐹‘(𝐸‘𝑥))) |
268 | 267 | fveq2d 6667 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐸‘𝑥) → (abs‘(𝐹‘𝑤)) = (abs‘(𝐹‘(𝐸‘𝑥)))) |
269 | 268 | breq1d 5067 |
. . . . . . . . 9
⊢ (𝑤 = (𝐸‘𝑥) → ((abs‘(𝐹‘𝑤)) ≤ 𝑦 ↔ (abs‘(𝐹‘(𝐸‘𝑥))) ≤ 𝑦)) |
270 | 269 | rspccva 3619 |
. . . . . . . 8
⊢
((∀𝑤 ∈
((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦 ∧ (𝐸‘𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → (abs‘(𝐹‘(𝐸‘𝑥))) ≤ 𝑦) |
271 | 244, 266,
270 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘(𝐸‘𝑥))) ≤ 𝑦) |
272 | 238, 271 | eqbrtrd 5079 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
273 | 272 | ex 413 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) → (𝑥 ∈ dom 𝐹 → (abs‘(𝐹‘𝑥)) ≤ 𝑦)) |
274 | 199, 273 | ralrimi 3213 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) → ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦) |
275 | 274 | ex 413 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 → ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦)) |
276 | 275 | reximdv 3270 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦)) |
277 | 196, 276 | mpd 15 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦) |