Step | Hyp | Ref
| Expression |
1 | | prfi 8235 |
. . 3
⊢ {ran
𝑄, ∪ ran 𝐼} ∈ Fin |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → {ran 𝑄, ∪ ran 𝐼} ∈ Fin) |
3 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) |
4 | | fourierdlem70.q |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
5 | | ovex 6678 |
. . . . . . . . . . 11
⊢
(0...𝑀) ∈
V |
6 | | fex 6490 |
. . . . . . . . . . 11
⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ V) → 𝑄 ∈ V) |
7 | 4, 5, 6 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ V) |
8 | | rnexg 7098 |
. . . . . . . . . 10
⊢ (𝑄 ∈ V → ran 𝑄 ∈ V) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝑄 ∈ V) |
10 | | fzofi 12773 |
. . . . . . . . . . . 12
⊢
(0..^𝑀) ∈
Fin |
11 | | fourierdlem70.i |
. . . . . . . . . . . . 13
⊢ 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
12 | 11 | rnmptfi 39351 |
. . . . . . . . . . . 12
⊢
((0..^𝑀) ∈ Fin
→ ran 𝐼 ∈
Fin) |
13 | 10, 12 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ran 𝐼 ∈ Fin |
14 | 13 | elexi 3213 |
. . . . . . . . . 10
⊢ ran 𝐼 ∈ V |
15 | 14 | uniex 6953 |
. . . . . . . . 9
⊢ ∪ ran 𝐼 ∈ V |
16 | | uniprg 4450 |
. . . . . . . . 9
⊢ ((ran
𝑄 ∈ V ∧ ∪ ran 𝐼 ∈ V) → ∪ {ran 𝑄, ∪ ran 𝐼} = (ran 𝑄 ∪ ∪ ran
𝐼)) |
17 | 9, 15, 16 | sylancl 694 |
. . . . . . . 8
⊢ (𝜑 → ∪ {ran 𝑄, ∪ ran 𝐼} = (ran 𝑄 ∪ ∪ ran
𝐼)) |
18 | 17 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → ∪ {ran
𝑄, ∪ ran 𝐼} = (ran 𝑄 ∪ ∪ ran
𝐼)) |
19 | 3, 18 | eleqtrd 2703 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) |
20 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ
↑𝑚 (0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))}) = (𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑𝑚
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))}) |
21 | | fourierdlem70.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
22 | | reex 10027 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
23 | 22, 5 | elmap 7886 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (ℝ
↑𝑚 (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ) |
24 | 4, 23 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑𝑚
(0...𝑀))) |
25 | | fourierdlem70.q0 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
26 | | fourierdlem70.qm |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) |
27 | 25, 26 | jca 554 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) |
28 | | fourierdlem70.qlt |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
29 | 28 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
30 | 24, 27, 29 | jca32 558 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
31 | 20 | fourierdlem2 40326 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ ((𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑𝑚
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))})‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
32 | 21, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 ∈ ((𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑𝑚
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))})‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
33 | 30, 32 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ((𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑𝑚
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))})‘𝑀)) |
34 | 20, 21, 33 | fourierdlem15 40339 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) |
35 | | frn 6053 |
. . . . . . . . . 10
⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → ran 𝑄 ⊆ (𝐴[,]𝐵)) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵)) |
37 | 36 | sselda 3603 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ (𝐴[,]𝐵)) |
38 | 37 | adantlr 751 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ (𝐴[,]𝐵)) |
39 | | simpll 790 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝜑) |
40 | | elunnel1 3754 |
. . . . . . . . 9
⊢ ((𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ ∪ ran
𝐼) |
41 | 40 | adantll 750 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ ∪ ran
𝐼) |
42 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝑠 ∈ ∪ ran 𝐼) |
43 | 11 | funmpt2 5927 |
. . . . . . . . . . 11
⊢ Fun 𝐼 |
44 | | elunirn 6509 |
. . . . . . . . . . 11
⊢ (Fun
𝐼 → (𝑠 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖))) |
45 | 43, 44 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → (𝑠 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖))) |
46 | 42, 45 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → ∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖)) |
47 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ dom 𝐼) |
48 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V |
49 | 48, 11 | dmmpti 6023 |
. . . . . . . . . . . . . . . . . 18
⊢ dom 𝐼 = (0..^𝑀) |
50 | 47, 49 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ (0..^𝑀)) |
51 | 11 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑀) ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
52 | 50, 48, 51 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ dom 𝐼 → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
54 | | ioossicc 12259 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) |
55 | | fourierdlem70.a |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ ℝ) |
56 | 55 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝐴 ∈
ℝ*) |
58 | | fourierdlem70.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ ℝ) |
59 | 58 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝐵 ∈
ℝ*) |
61 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) |
62 | 50 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝑖 ∈ (0..^𝑀)) |
63 | 57, 60, 61, 62 | fourierdlem8 40332 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵)) |
64 | 54, 63 | syl5ss 3614 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵)) |
65 | 53, 64 | eqsstrd 3639 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ⊆ (𝐴[,]𝐵)) |
66 | 65 | 3adant3 1081 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ (𝐼‘𝑖)) → (𝐼‘𝑖) ⊆ (𝐴[,]𝐵)) |
67 | | simp3 1063 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ (𝐼‘𝑖)) → 𝑠 ∈ (𝐼‘𝑖)) |
68 | 66, 67 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ (𝐼‘𝑖)) → 𝑠 ∈ (𝐴[,]𝐵)) |
69 | 68 | 3exp 1264 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ dom 𝐼 → (𝑠 ∈ (𝐼‘𝑖) → 𝑠 ∈ (𝐴[,]𝐵)))) |
70 | 69 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → (𝑖 ∈ dom 𝐼 → (𝑠 ∈ (𝐼‘𝑖) → 𝑠 ∈ (𝐴[,]𝐵)))) |
71 | 70 | rexlimdv 3030 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → (∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖) → 𝑠 ∈ (𝐴[,]𝐵))) |
72 | 46, 71 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝑠 ∈ (𝐴[,]𝐵)) |
73 | 39, 41, 72 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ (𝐴[,]𝐵)) |
74 | 38, 73 | pm2.61dan 832 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) → 𝑠 ∈ (𝐴[,]𝐵)) |
75 | 19, 74 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → 𝑠 ∈ (𝐴[,]𝐵)) |
76 | | fourierdlem70.f |
. . . . . 6
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
77 | 76 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑠) ∈ ℝ) |
78 | 75, 77 | syldan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → (𝐹‘𝑠) ∈ ℝ) |
79 | 78 | recnd 10068 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → (𝐹‘𝑠) ∈ ℂ) |
80 | 79 | abscld 14175 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → (abs‘(𝐹‘𝑠)) ∈ ℝ) |
81 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → 𝑤 = ran 𝑄) |
82 | 4 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ) |
83 | | fzfid 12772 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → (0...𝑀) ∈ Fin) |
84 | | rnffi 39356 |
. . . . . . 7
⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin) |
85 | 82, 83, 84 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → ran 𝑄 ∈ Fin) |
86 | 81, 85 | eqeltrd 2701 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → 𝑤 ∈ Fin) |
87 | 86 | adantlr 751 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ 𝑤 = ran 𝑄) → 𝑤 ∈ Fin) |
88 | 76 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
89 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝜑) |
90 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ 𝑤) |
91 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤) → 𝑤 = ran 𝑄) |
92 | 90, 91 | eleqtrd 2703 |
. . . . . . . . . . 11
⊢ ((𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ ran 𝑄) |
93 | 92 | adantll 750 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ ran 𝑄) |
94 | 89, 93, 37 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ (𝐴[,]𝐵)) |
95 | 88, 94 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → (𝐹‘𝑠) ∈ ℝ) |
96 | 95 | recnd 10068 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → (𝐹‘𝑠) ∈ ℂ) |
97 | 96 | abscld 14175 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → (abs‘(𝐹‘𝑠)) ∈ ℝ) |
98 | 97 | ralrimiva 2966 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ∈ ℝ) |
99 | 98 | adantlr 751 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ 𝑤 = ran 𝑄) → ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ∈ ℝ) |
100 | | fimaxre3 10970 |
. . . 4
⊢ ((𝑤 ∈ Fin ∧ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) |
101 | 87, 99, 100 | syl2anc 693 |
. . 3
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ 𝑤 = ran 𝑄) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) |
102 | | simpll 790 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ ¬ 𝑤 = ran 𝑄) → 𝜑) |
103 | | neqne 2802 |
. . . . . 6
⊢ (¬
𝑤 = ran 𝑄 → 𝑤 ≠ ran 𝑄) |
104 | | elprn1 39865 |
. . . . . 6
⊢ ((𝑤 ∈ {ran 𝑄, ∪ ran 𝐼} ∧ 𝑤 ≠ ran 𝑄) → 𝑤 = ∪ ran 𝐼) |
105 | 103, 104 | sylan2 491 |
. . . . 5
⊢ ((𝑤 ∈ {ran 𝑄, ∪ ran 𝐼} ∧ ¬ 𝑤 = ran 𝑄) → 𝑤 = ∪ ran 𝐼) |
106 | 105 | adantll 750 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ ¬ 𝑤 = ran 𝑄) → 𝑤 = ∪ ran 𝐼) |
107 | 10, 12 | mp1i 13 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ran 𝐼 ∈ Fin) |
108 | | ax-resscn 9993 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
109 | 108 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ⊆
ℂ) |
110 | 76, 109 | fssd 6057 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
111 | 110 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
112 | 72 | adantlr 751 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝑠 ∈ (𝐴[,]𝐵)) |
113 | 111, 112 | ffvelrnd 6360 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → (𝐹‘𝑠) ∈ ℂ) |
114 | 113 | abscld 14175 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → (abs‘(𝐹‘𝑠)) ∈ ℝ) |
115 | 48, 11 | fnmpti 6022 |
. . . . . . . . . 10
⊢ 𝐼 Fn (0..^𝑀) |
116 | | fvelrnb 6243 |
. . . . . . . . . 10
⊢ (𝐼 Fn (0..^𝑀) → (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡)) |
117 | 115, 116 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
118 | 117 | biimpi 206 |
. . . . . . . 8
⊢ (𝑡 ∈ ran 𝐼 → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
119 | 118 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
120 | 4 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
121 | | elfzofz 12485 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
122 | 121 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
123 | 120, 122 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
124 | | fzofzp1 12565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
125 | 124 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
126 | 120, 125 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
127 | | fourierdlem70.fcn |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
128 | | fourierdlem70.l |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
129 | | fourierdlem70.r |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
130 | 123, 126,
127, 128, 129 | cncfioobd 40110 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏) |
131 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠) = (𝐹‘𝑠)) |
132 | 131 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) = (abs‘(𝐹‘𝑠))) |
133 | 132 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
134 | 133 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
135 | 134 | ralbidva 2985 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
136 | 135 | rexbidv 3052 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
137 | 130, 136 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏) |
138 | 137 | 3adant3 1081 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏) |
139 | 48, 51 | mpan2 707 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (0..^𝑀) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
140 | 139 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖)) |
141 | 140 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖)) |
142 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (𝐼‘𝑖) = 𝑡) |
143 | 141, 142 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡) |
144 | 143 | raleqdv 3144 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
145 | 144 | rexbidv 3052 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
146 | 145 | 3adant1 1079 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
147 | 138, 146 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏) |
148 | 147 | 3exp 1264 |
. . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏))) |
149 | 148 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏))) |
150 | 149 | rexlimdv 3030 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
151 | 119, 150 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏) |
152 | 151 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏) |
153 | | eqimss 3657 |
. . . . . 6
⊢ (𝑤 = ∪
ran 𝐼 → 𝑤 ⊆ ∪ ran 𝐼) |
154 | 153 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → 𝑤 ⊆ ∪ ran
𝐼) |
155 | 107, 114,
152, 154 | ssfiunibd 39523 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) |
156 | 102, 106,
155 | syl2anc 693 |
. . 3
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ ¬ 𝑤 = ran 𝑄) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) |
157 | 101, 156 | pm2.61dan 832 |
. 2
⊢ ((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) |
158 | 21 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑀 ∈ ℕ) |
159 | 4 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ) |
160 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (𝐴[,]𝐵)) |
161 | 25 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 = (𝑄‘0)) |
162 | 26 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 = (𝑄‘𝑀)) |
163 | 161, 162 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀))) |
164 | 163 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀))) |
165 | 160, 164 | eleqtrd 2703 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) |
166 | 165 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) |
167 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ¬ 𝑡 ∈ ran 𝑄) |
168 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗)) |
169 | 168 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < 𝑡 ↔ (𝑄‘𝑗) < 𝑡)) |
170 | 169 | cbvrabv 3199 |
. . . . . . . . . . . . 13
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝑡} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑡} |
171 | 170 | supeq1i 8353 |
. . . . . . . . . . . 12
⊢
sup({𝑘 ∈
(0..^𝑀) ∣ (𝑄‘𝑘) < 𝑡}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑡}, ℝ, < ) |
172 | 158, 159,
166, 167, 171 | fourierdlem25 40349 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
173 | 139 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0..^𝑀) → (𝑡 ∈ (𝐼‘𝑖) ↔ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
174 | 173 | rexbiia 3040 |
. . . . . . . . . . 11
⊢
(∃𝑖 ∈
(0..^𝑀)𝑡 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
175 | 172, 174 | sylibr 224 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑡 ∈ (𝐼‘𝑖)) |
176 | 49 | eqcomi 2631 |
. . . . . . . . . . 11
⊢
(0..^𝑀) = dom 𝐼 |
177 | 176 | rexeqi 3143 |
. . . . . . . . . 10
⊢
(∃𝑖 ∈
(0..^𝑀)𝑡 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖)) |
178 | 175, 177 | sylib 208 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖)) |
179 | | elunirn 6509 |
. . . . . . . . . 10
⊢ (Fun
𝐼 → (𝑡 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖))) |
180 | 43, 179 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → (𝑡 ∈ ∪ ran
𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖))) |
181 | 178, 180 | mpbird 247 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑡 ∈ ∪ ran
𝐼) |
182 | 181 | ex 450 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (¬ 𝑡 ∈ ran 𝑄 → 𝑡 ∈ ∪ ran
𝐼)) |
183 | 182 | orrd 393 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ ran 𝑄 ∨ 𝑡 ∈ ∪ ran
𝐼)) |
184 | | elun 3753 |
. . . . . 6
⊢ (𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼) ↔ (𝑡 ∈ ran 𝑄 ∨ 𝑡 ∈ ∪ ran
𝐼)) |
185 | 183, 184 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) |
186 | 185 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑡 ∈ (𝐴[,]𝐵)𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) |
187 | | dfss3 3592 |
. . . 4
⊢ ((𝐴[,]𝐵) ⊆ (ran 𝑄 ∪ ∪ ran
𝐼) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) |
188 | 186, 187 | sylibr 224 |
. . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (ran 𝑄 ∪ ∪ ran
𝐼)) |
189 | 188, 17 | sseqtr4d 3642 |
. 2
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ {ran
𝑄, ∪ ran 𝐼}) |
190 | 2, 80, 157, 189 | ssfiunibd 39523 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑠 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑠)) ≤ 𝑥) |