Step | Hyp | Ref
| Expression |
1 | | prfi 8639 |
. . . 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 7048 |
. . . . . . . . . . . . 13
⊢
(0...𝑀) ∈
V |
9 | 8 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0...𝑀) ∈ V) |
10 | | fex 6855 |
. . . . . . . . . . . 12
⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ V) → 𝑄 ∈ V) |
11 | 7, 9, 10 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ V) |
12 | | rnexg 7470 |
. . . . . . . . . . 11
⊢ (𝑄 ∈ V → ran 𝑄 ∈ V) |
13 | | inex1g 5114 |
. . . . . . . . . . 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 7048 |
. . . . . . . . . . . . . . 15
⊢
(0..^𝑀) ∈
V |
18 | 17 | mptex 6852 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ V |
19 | 16, 18 | eqeltri 2879 |
. . . . . . . . . . . . 13
⊢ 𝐼 ∈ V |
20 | 19 | rnex 7473 |
. . . . . . . . . . . 12
⊢ ran 𝐼 ∈ V |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐼 ∈ V) |
22 | | uniexg 7325 |
. . . . . . . . . . 11
⊢ (ran
𝐼 ∈ V → ∪ ran 𝐼 ∈ V) |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran 𝐼 ∈ V) |
24 | 23 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → ∪ ran 𝐼 ∈ V) |
25 | | uniprg 4759 |
. . . . . . . . 9
⊢ (((ran
𝑄 ∩ dom 𝐹) ∈ V ∧ ∪ ran 𝐼 ∈ V) → ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
26 | 15, 24, 25 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
27 | 6, 26 | eleqtrd 2885 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
28 | | elinel2 4094 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ran 𝑄 ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹) |
29 | 28 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹) |
30 | | simpll 763 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝜑) |
31 | | elunnel1 4047 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ ∪ ran
𝐼) |
32 | 31 | adantll 710 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ ∪ ran
𝐼) |
33 | 16 | funmpt2 6264 |
. . . . . . . . . . . . 13
⊢ Fun 𝐼 |
34 | | elunirn 6875 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐼 → (𝑥 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖))) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖)) |
36 | 35 | biimpi 217 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ ran 𝐼 → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖)) |
37 | 36 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖)) |
38 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ dom 𝐼) |
39 | | ovex 7048 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V |
40 | 39, 16 | dmmpti 6360 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom 𝐼 = (0..^𝑀) |
41 | 38, 40 | syl6eleq 2893 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ (0..^𝑀)) |
42 | 41 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝑖 ∈ (0..^𝑀)) |
43 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V) |
44 | 16 | fvmpt2 6645 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑀) ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
45 | 42, 43, 44 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
46 | | fourierdlem71.fcn |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
47 | | cncff 23184 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ) |
48 | | fdm 6390 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
50 | 41, 49 | sylan2 592 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
51 | | ssdmres 5757 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
52 | 50, 51 | sylibr 235 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹) |
53 | 45, 52 | eqsstrd 3926 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ⊆ dom 𝐹) |
54 | 53 | 3adant3 1125 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) → (𝐼‘𝑖) ⊆ dom 𝐹) |
55 | | simp3 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) → 𝑥 ∈ (𝐼‘𝑖)) |
56 | 54, 55 | sseldd 3890 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) → 𝑥 ∈ dom 𝐹) |
57 | 56 | 3exp 1112 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑖 ∈ dom 𝐼 → (𝑥 ∈ (𝐼‘𝑖) → 𝑥 ∈ dom 𝐹))) |
58 | 57 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → (𝑖 ∈ dom 𝐼 → (𝑥 ∈ (𝐼‘𝑖) → 𝑥 ∈ dom 𝐹))) |
59 | 58 | rexlimdv 3246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖) → 𝑥 ∈ dom 𝐹)) |
60 | 37, 59 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → 𝑥 ∈ dom 𝐹) |
61 | 30, 32, 60 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹) |
62 | 29, 61 | pm2.61dan 809 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) → 𝑥 ∈ dom 𝐹) |
63 | 5, 27, 62 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → 𝑥 ∈ dom 𝐹) |
64 | 4, 63 | ffvelrnd 6717 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → (𝐹‘𝑥) ∈ ℝ) |
65 | 64 | recnd 10515 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) → (𝐹‘𝑥) ∈ ℂ) |
66 | 65 | abscld 14630 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) →
(abs‘(𝐹‘𝑥)) ∈
ℝ) |
67 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = (ran 𝑄 ∩ dom 𝐹)) |
68 | | fzfid 13191 |
. . . . . . . . . 10
⊢ (𝜑 → (0...𝑀) ∈ Fin) |
69 | | rnffi 40971 |
. . . . . . . . . 10
⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin) |
70 | 7, 68, 69 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝑄 ∈ Fin) |
71 | | infi 8588 |
. . . . . . . . 9
⊢ (ran
𝑄 ∈ Fin → (ran
𝑄 ∩ dom 𝐹) ∈ Fin) |
72 | 70, 71 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ran 𝑄 ∩ dom 𝐹) ∈ Fin) |
73 | 72 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → (ran 𝑄 ∩ dom 𝐹) ∈ Fin) |
74 | 67, 73 | eqeltrd 2883 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 ∈ Fin) |
75 | | simpll 763 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥 ∈ 𝑤) → 𝜑) |
76 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ 𝑤) |
77 | | simpl 483 |
. . . . . . . . . 10
⊢ ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥 ∈ 𝑤) → 𝑤 = (ran 𝑄 ∩ dom 𝐹)) |
78 | 76, 77 | eleqtrd 2885 |
. . . . . . . . 9
⊢ ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) |
79 | 78 | adantll 710 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) |
80 | 3 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝐹:dom 𝐹⟶ℝ) |
81 | 28 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹) |
82 | 80, 81 | ffvelrnd 6717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (𝐹‘𝑥) ∈ ℝ) |
83 | 82 | recnd 10515 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (𝐹‘𝑥) ∈ ℂ) |
84 | 83 | abscld 14630 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
85 | 75, 79, 84 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥 ∈ 𝑤) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
86 | 85 | ralrimiva 3149 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ∈ ℝ) |
87 | | fimaxre3 11435 |
. . . . . 6
⊢ ((𝑤 ∈ Fin ∧ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
88 | 74, 86, 87 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
89 | 88 | adantlr 711 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
90 | | simpll 763 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝜑) |
91 | | neqne 2992 |
. . . . . . 7
⊢ (¬
𝑤 = (ran 𝑄 ∩ dom 𝐹) → 𝑤 ≠ (ran 𝑄 ∩ dom 𝐹)) |
92 | | elprn1 41456 |
. . . . . . 7
⊢ ((𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} ∧ 𝑤 ≠ (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ∪ ran 𝐼) |
93 | 91, 92 | sylan2 592 |
. . . . . 6
⊢ ((𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ∪ ran 𝐼) |
94 | 93 | adantll 710 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ∪ ran 𝐼) |
95 | | fzofi 13192 |
. . . . . . . 8
⊢
(0..^𝑀) ∈
Fin |
96 | 16 | rnmptfi 40967 |
. . . . . . . 8
⊢
((0..^𝑀) ∈ Fin
→ ran 𝐼 ∈
Fin) |
97 | 95, 96 | ax-mp 5 |
. . . . . . 7
⊢ ran 𝐼 ∈ Fin |
98 | 97 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ran 𝐼 ∈ Fin) |
99 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → 𝐹:dom 𝐹⟶ℝ) |
100 | 99, 60 | ffvelrnd 6717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → (𝐹‘𝑥) ∈ ℝ) |
101 | 100 | recnd 10515 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran
𝐼) → (𝐹‘𝑥) ∈ ℂ) |
102 | 101 | adantlr 711 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑥 ∈ ∪ ran
𝐼) → (𝐹‘𝑥) ∈ ℂ) |
103 | 102 | abscld 14630 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑥 ∈ ∪ ran
𝐼) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
104 | 39, 16 | fnmpti 6359 |
. . . . . . . . . . 11
⊢ 𝐼 Fn (0..^𝑀) |
105 | | fvelrnb 6594 |
. . . . . . . . . . 11
⊢ (𝐼 Fn (0..^𝑀) → (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡)) |
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
107 | 106 | biimpi 217 |
. . . . . . . . 9
⊢ (𝑡 ∈ ran 𝐼 → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
108 | 107 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
109 | 7 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
110 | | elfzofz 12903 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
111 | 110 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
112 | 109, 111 | ffvelrnd 6717 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
113 | | fzofzp1 12984 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
114 | 113 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
115 | 109, 114 | ffvelrnd 6717 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
116 | | fourierdlem71.l |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
117 | | fourierdlem71.r |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
118 | 112, 115,
46, 116, 117 | cncfioobd 41721 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏) |
119 | 118 | 3adant3 1125 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏) |
120 | | fvres 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥) = (𝐹‘𝑥)) |
121 | 120 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) = (abs‘(𝐹‘𝑥))) |
122 | 121 | breq1d 4972 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
123 | 122 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
124 | 123 | ralbidva 3163 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
125 | 124 | rexbidv 3260 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
126 | 125 | 3adant3 1125 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
127 | 39, 44 | mpan2 687 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (0..^𝑀) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
128 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼‘𝑖) = 𝑡 → (𝐼‘𝑖) = 𝑡) |
129 | 127, 128 | sylan9req 2852 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡) |
130 | 129 | 3adant1 1123 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡) |
131 | 130 | raleqdv 3375 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
132 | 131 | rexbidv 3260 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
133 | 126, 132 | bitrd 280 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
134 | 119, 133 | mpbid 233 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏) |
135 | 134 | 3exp 1112 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏))) |
136 | 135 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏))) |
137 | 136 | rexlimdv 3246 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)) |
138 | 108, 137 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏) |
139 | 138 | adantlr 711 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏) |
140 | | eqimss 3944 |
. . . . . . 7
⊢ (𝑤 = ∪
ran 𝐼 → 𝑤 ⊆ ∪ ran 𝐼) |
141 | 140 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → 𝑤 ⊆ ∪ ran
𝐼) |
142 | 98, 103, 139, 141 | ssfiunibd 41117 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
143 | 90, 94, 142 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
144 | 89, 143 | pm2.61dan 809 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
145 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ran 𝑄) |
146 | | elinel2 4094 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹) |
147 | 146 | ad2antlr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ dom 𝐹) |
148 | 145, 147 | elind 4092 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) |
149 | | elun1 4073 |
. . . . . . . 8
⊢ (𝑥 ∈ (ran 𝑄 ∩ dom 𝐹) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
150 | 148, 149 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
151 | | fourierdlem71.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℕ) |
152 | 151 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑀 ∈ ℕ) |
153 | 7 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ) |
154 | | elinel1 4093 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹) → 𝑥 ∈ (𝐴[,]𝐵)) |
155 | 154 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ (𝐴[,]𝐵)) |
156 | | fourierdlem71.q0 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
157 | 156 | eqcomd 2801 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 = (𝑄‘0)) |
158 | 157 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝐴 = (𝑄‘0)) |
159 | | fourierdlem71.10 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) |
160 | 159 | eqcomd 2801 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 = (𝑄‘𝑀)) |
161 | 160 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝐵 = (𝑄‘𝑀)) |
162 | 158, 161 | oveq12d 7034 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀))) |
163 | 155, 162 | eleqtrd 2885 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) |
164 | 163 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) |
165 | | simpr 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ¬ 𝑥 ∈ ran 𝑄) |
166 | | fveq2 6538 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗)) |
167 | 166 | breq1d 4972 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < 𝑥 ↔ (𝑄‘𝑗) < 𝑥)) |
168 | 167 | cbvrabv 3434 |
. . . . . . . . . . . 12
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝑥} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑥} |
169 | 168 | supeq1i 8757 |
. . . . . . . . . . 11
⊢
sup({𝑘 ∈
(0..^𝑀) ∣ (𝑄‘𝑘) < 𝑥}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑥}, ℝ, < ) |
170 | 152, 153,
164, 165, 169 | fourierdlem25 41959 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
171 | 41 | ad2antrl 724 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → 𝑖 ∈ (0..^𝑀)) |
172 | | simprr 769 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → 𝑥 ∈ (𝐼‘𝑖)) |
173 | 171, 127 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
174 | 172, 173 | eleqtrd 2885 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
175 | 171, 174 | jca 512 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
176 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0..^𝑀)) |
177 | 176, 40 | syl6eleqr 2894 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ dom 𝐼) |
178 | 177 | ad2antrl 724 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑖 ∈ dom 𝐼) |
179 | | simprr 769 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
180 | 127 | eqcomd 2801 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖)) |
181 | 180 | ad2antrl 724 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖)) |
182 | 179, 181 | eleqtrd 2885 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑥 ∈ (𝐼‘𝑖)) |
183 | 178, 182 | jca 512 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) |
184 | 175, 183 | impbida 797 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) ↔ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))) |
185 | 184 | rexbidv2 3258 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
186 | 185 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
187 | 170, 186 | mpbird 258 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖)) |
188 | 187, 35 | sylibr 235 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ∪ ran
𝐼) |
189 | | elun2 4074 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ ran 𝐼 → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
190 | 188, 189 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
191 | 150, 190 | pm2.61dan 809 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
192 | 191 | ralrimiva 3149 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
193 | | dfss3 3878 |
. . . . 5
⊢ (((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼) ↔ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
194 | 192, 193 | sylibr 235 |
. . . 4
⊢ (𝜑 → ((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
195 | 14, 23, 25 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran
𝐼)) |
196 | 194, 195 | sseqtr4d 3929 |
. . 3
⊢ (𝜑 → ((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ∪ {(ran
𝑄 ∩ dom 𝐹), ∪
ran 𝐼}) |
197 | 2, 66, 144, 196 | ssfiunibd 41117 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) |
198 | | nfv 1892 |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
199 | | nfra1 3186 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 |
200 | 198, 199 | nfan 1881 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) |
201 | | fourierdlem71.dmf |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝐹 ⊆ ℝ) |
202 | 201 | sselda 3889 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ ℝ) |
203 | | fourierdlem71.b |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ ℝ) |
204 | 203 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐵 ∈ ℝ) |
205 | 204, 202 | resubcld 10916 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐵 − 𝑥) ∈ ℝ) |
206 | | fourierdlem71.t |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 = (𝐵 − 𝐴) |
207 | | fourierdlem71.a |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐴 ∈ ℝ) |
208 | 203, 207 | resubcld 10916 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
209 | 206, 208 | syl5eqel 2887 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ∈ ℝ) |
210 | 209 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝑇 ∈ ℝ) |
211 | | fourierdlem71.altb |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 < 𝐵) |
212 | 207, 203 | posdifd 11075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
213 | 211, 212 | mpbid 233 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
214 | 213, 206 | syl6breqr 5004 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 𝑇) |
215 | 214 | gt0ne0d 11052 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ≠ 0) |
216 | 215 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝑇 ≠ 0) |
217 | 205, 210,
216 | redivcld 11316 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ) |
218 | 217 | flcld 13018 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) |
219 | 218 | zred 11936 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ) |
220 | 219, 210 | remulcld 10517 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ) |
221 | 202, 220 | readdcld 10516 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) |
222 | | fourierdlem71.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
223 | 222 | fvmpt2 6645 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
224 | 202, 221,
223 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
225 | 224 | fveq2d 6542 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘(𝐸‘𝑥)) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))) |
226 | | fvex 6551 |
. . . . . . . . . . . 12
⊢
(⌊‘((𝐵
− 𝑥) / 𝑇)) ∈ V |
227 | | eleq1 2870 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)) |
228 | 227 | anbi2d 628 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) ↔ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ))) |
229 | | oveq1 7023 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) |
230 | 229 | oveq2d 7032 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
231 | 230 | fveq2d 6542 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))) |
232 | 231 | eqeq1d 2797 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))) |
233 | 228, 232 | imbi12d 346 |
. . . . . . . . . . . 12
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) ↔ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))) |
234 | | fourierdlem71.fxpt |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) |
235 | 226, 233,
234 | vtocl 3502 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)) |
236 | 218, 235 | mpdan 683 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)) |
237 | 225, 236 | eqtr2d 2832 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘(𝐸‘𝑥))) |
238 | 237 | fveq2d 6542 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐸‘𝑥)))) |
239 | 238 | adantlr 711 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐸‘𝑥)))) |
240 | | fveq2 6538 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤)) |
241 | 240 | fveq2d 6542 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘𝑤))) |
242 | 241 | breq1d 4972 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → ((abs‘(𝐹‘𝑥)) ≤ 𝑦 ↔ (abs‘(𝐹‘𝑤)) ≤ 𝑦)) |
243 | 242 | cbvralv 3403 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 ↔ ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦) |
244 | 243 | biimpi 217 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 → ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦) |
245 | 244 | ad2antlr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦) |
246 | | iocssicc 12675 |
. . . . . . . . . . 11
⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵) |
247 | 207 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐴 ∈ ℝ) |
248 | 211 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐴 < 𝐵) |
249 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
250 | | oveq2 7024 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐵 − 𝑥) = (𝐵 − 𝑦)) |
251 | 250 | oveq1d 7031 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑦) / 𝑇)) |
252 | 251 | fveq2d 6542 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑦) / 𝑇))) |
253 | 252 | oveq1d 7031 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇)) |
254 | 249, 253 | oveq12d 7034 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑦 + ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇))) |
255 | 254 | cbvmptv 5061 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇))) |
256 | 222, 255 | eqtri 2819 |
. . . . . . . . . . . . 13
⊢ 𝐸 = (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇))) |
257 | 247, 204,
248, 206, 256 | fourierdlem4 41938 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐸:ℝ⟶(𝐴(,]𝐵)) |
258 | 257, 202 | ffvelrnd 6717 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵)) |
259 | 246, 258 | sseldi 3887 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ (𝐴[,]𝐵)) |
260 | 230 | eleq1d 2867 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹 ↔ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)) |
261 | 228, 260 | imbi12d 346 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹) ↔ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹))) |
262 | | fourierdlem71.xpt |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹) |
263 | 226, 261,
262 | vtocl 3502 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹) |
264 | 218, 263 | mpdan 683 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹) |
265 | 224, 264 | eqeltrd 2883 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ dom 𝐹) |
266 | 259, 265 | elind 4092 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) |
267 | 266 | adantlr 711 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) |
268 | | fveq2 6538 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝐸‘𝑥) → (𝐹‘𝑤) = (𝐹‘(𝐸‘𝑥))) |
269 | 268 | fveq2d 6542 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐸‘𝑥) → (abs‘(𝐹‘𝑤)) = (abs‘(𝐹‘(𝐸‘𝑥)))) |
270 | 269 | breq1d 4972 |
. . . . . . . . 9
⊢ (𝑤 = (𝐸‘𝑥) → ((abs‘(𝐹‘𝑤)) ≤ 𝑦 ↔ (abs‘(𝐹‘(𝐸‘𝑥))) ≤ 𝑦)) |
271 | 270 | rspccva 3558 |
. . . . . . . 8
⊢
((∀𝑤 ∈
((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦 ∧ (𝐸‘𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → (abs‘(𝐹‘(𝐸‘𝑥))) ≤ 𝑦) |
272 | 245, 267,
271 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘(𝐸‘𝑥))) ≤ 𝑦) |
273 | 239, 272 | eqbrtrd 4984 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘𝑥)) ≤ 𝑦) |
274 | 273 | ex 413 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) → (𝑥 ∈ dom 𝐹 → (abs‘(𝐹‘𝑥)) ≤ 𝑦)) |
275 | 200, 274 | ralrimi 3183 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) → ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦) |
276 | 275 | ex 413 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 → ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦)) |
277 | 276 | reximdv 3236 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦)) |
278 | 197, 277 | mpd 15 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦) |