Step | Hyp | Ref
| Expression |
1 | | prfi 8946 |
. . 3
⊢ {ran
𝑄, ∪ ran 𝐼} ∈ Fin |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → {ran 𝑄, ∪ ran 𝐼} ∈ Fin) |
3 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) |
4 | | fourierdlem70.q |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
5 | | ovex 7246 |
. . . . . . . . . . 11
⊢
(0...𝑀) ∈
V |
6 | | fex 7042 |
. . . . . . . . . . 11
⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ V) → 𝑄 ∈ V) |
7 | 4, 5, 6 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ V) |
8 | | rnexg 7682 |
. . . . . . . . . 10
⊢ (𝑄 ∈ V → ran 𝑄 ∈ V) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝑄 ∈ V) |
10 | | fzofi 13547 |
. . . . . . . . . . . 12
⊢
(0..^𝑀) ∈
Fin |
11 | | fourierdlem70.i |
. . . . . . . . . . . . 13
⊢ 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
12 | 11 | rnmptfi 42380 |
. . . . . . . . . . . 12
⊢
((0..^𝑀) ∈ Fin
→ ran 𝐼 ∈
Fin) |
13 | 10, 12 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ran 𝐼 ∈ Fin |
14 | 13 | elexi 3427 |
. . . . . . . . . 10
⊢ ran 𝐼 ∈ V |
15 | 14 | uniex 7529 |
. . . . . . . . 9
⊢ ∪ ran 𝐼 ∈ V |
16 | | uniprg 4836 |
. . . . . . . . 9
⊢ ((ran
𝑄 ∈ V ∧ ∪ ran 𝐼 ∈ V) → ∪ {ran 𝑄, ∪ ran 𝐼} = (ran 𝑄 ∪ ∪ ran
𝐼)) |
17 | 9, 15, 16 | sylancl 589 |
. . . . . . . 8
⊢ (𝜑 → ∪ {ran 𝑄, ∪ ran 𝐼} = (ran 𝑄 ∪ ∪ ran
𝐼)) |
18 | 17 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → ∪ {ran
𝑄, ∪ ran 𝐼} = (ran 𝑄 ∪ ∪ ran
𝐼)) |
19 | 3, 18 | eleqtrd 2840 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) |
20 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ
↑m (0...𝑦))
∣ (((𝑣‘0) =
𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))}) = (𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑m
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))}) |
21 | | fourierdlem70.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
22 | | reex 10820 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
23 | 22, 5 | elmap 8552 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
↔ 𝑄:(0...𝑀)⟶ℝ) |
24 | 4, 23 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) |
25 | | fourierdlem70.q0 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
26 | | fourierdlem70.qm |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) |
27 | 25, 26 | jca 515 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) |
28 | | fourierdlem70.qlt |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
29 | 28 | ralrimiva 3105 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
30 | 24, 27, 29 | jca32 519 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
31 | 20 | fourierdlem2 43325 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ ((𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑m
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))})‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
32 | 21, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 ∈ ((𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑m
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))})‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
33 | 30, 32 | mpbird 260 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ((𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑m
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))})‘𝑀)) |
34 | 20, 21, 33 | fourierdlem15 43338 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) |
35 | 34 | frnd 6553 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵)) |
36 | 35 | sselda 3901 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ (𝐴[,]𝐵)) |
37 | 36 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ (𝐴[,]𝐵)) |
38 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝜑) |
39 | | elunnel1 4064 |
. . . . . . . . 9
⊢ ((𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ ∪ ran
𝐼) |
40 | 39 | adantll 714 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ ∪ ran
𝐼) |
41 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝑠 ∈ ∪ ran 𝐼) |
42 | 11 | funmpt2 6419 |
. . . . . . . . . . 11
⊢ Fun 𝐼 |
43 | | elunirn 7064 |
. . . . . . . . . . 11
⊢ (Fun
𝐼 → (𝑠 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖))) |
44 | 42, 43 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → (𝑠 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖))) |
45 | 41, 44 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → ∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖)) |
46 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ dom 𝐼) |
47 | | ovex 7246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V |
48 | 47, 11 | dmmpti 6522 |
. . . . . . . . . . . . . . . . . 18
⊢ dom 𝐼 = (0..^𝑀) |
49 | 46, 48 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ (0..^𝑀)) |
50 | 11 | fvmpt2 6829 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑀) ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
51 | 49, 47, 50 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ dom 𝐼 → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
52 | 51 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
53 | | ioossicc 13021 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) |
54 | | fourierdlem70.a |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ ℝ) |
55 | 54 | rexrd 10883 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
56 | 55 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝐴 ∈
ℝ*) |
57 | | fourierdlem70.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ ℝ) |
58 | 57 | rexrd 10883 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
59 | 58 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝐵 ∈
ℝ*) |
60 | 34 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) |
61 | 49 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝑖 ∈ (0..^𝑀)) |
62 | 56, 59, 60, 61 | fourierdlem8 43331 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵)) |
63 | 53, 62 | sstrid 3912 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵)) |
64 | 52, 63 | eqsstrd 3939 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ⊆ (𝐴[,]𝐵)) |
65 | 64 | 3adant3 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ (𝐼‘𝑖)) → (𝐼‘𝑖) ⊆ (𝐴[,]𝐵)) |
66 | | simp3 1140 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ (𝐼‘𝑖)) → 𝑠 ∈ (𝐼‘𝑖)) |
67 | 65, 66 | sseldd 3902 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ (𝐼‘𝑖)) → 𝑠 ∈ (𝐴[,]𝐵)) |
68 | 67 | 3exp 1121 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ dom 𝐼 → (𝑠 ∈ (𝐼‘𝑖) → 𝑠 ∈ (𝐴[,]𝐵)))) |
69 | 68 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → (𝑖 ∈ dom 𝐼 → (𝑠 ∈ (𝐼‘𝑖) → 𝑠 ∈ (𝐴[,]𝐵)))) |
70 | 69 | rexlimdv 3202 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → (∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖) → 𝑠 ∈ (𝐴[,]𝐵))) |
71 | 45, 70 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝑠 ∈ (𝐴[,]𝐵)) |
72 | 38, 40, 71 | syl2anc 587 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ (𝐴[,]𝐵)) |
73 | 37, 72 | pm2.61dan 813 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) → 𝑠 ∈ (𝐴[,]𝐵)) |
74 | 19, 73 | syldan 594 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → 𝑠 ∈ (𝐴[,]𝐵)) |
75 | | fourierdlem70.f |
. . . . . 6
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
76 | 75 | ffvelrnda 6904 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑠) ∈ ℝ) |
77 | 74, 76 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → (𝐹‘𝑠) ∈ ℝ) |
78 | 77 | recnd 10861 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → (𝐹‘𝑠) ∈ ℂ) |
79 | 78 | abscld 15000 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → (abs‘(𝐹‘𝑠)) ∈ ℝ) |
80 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → 𝑤 = ran 𝑄) |
81 | 4 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ) |
82 | | fzfid 13546 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → (0...𝑀) ∈ Fin) |
83 | | rnffi 42384 |
. . . . . . 7
⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin) |
84 | 81, 82, 83 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → ran 𝑄 ∈ Fin) |
85 | 80, 84 | eqeltrd 2838 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → 𝑤 ∈ Fin) |
86 | 85 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ 𝑤 = ran 𝑄) → 𝑤 ∈ Fin) |
87 | 75 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
88 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝜑) |
89 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ 𝑤) |
90 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤) → 𝑤 = ran 𝑄) |
91 | 89, 90 | eleqtrd 2840 |
. . . . . . . . . . 11
⊢ ((𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ ran 𝑄) |
92 | 91 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ ran 𝑄) |
93 | 88, 92, 36 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ (𝐴[,]𝐵)) |
94 | 87, 93 | ffvelrnd 6905 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → (𝐹‘𝑠) ∈ ℝ) |
95 | 94 | recnd 10861 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → (𝐹‘𝑠) ∈ ℂ) |
96 | 95 | abscld 15000 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → (abs‘(𝐹‘𝑠)) ∈ ℝ) |
97 | 96 | ralrimiva 3105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ∈ ℝ) |
98 | 97 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ 𝑤 = ran 𝑄) → ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ∈ ℝ) |
99 | | fimaxre3 11778 |
. . . 4
⊢ ((𝑤 ∈ Fin ∧ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) |
100 | 86, 98, 99 | syl2anc 587 |
. . 3
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ 𝑤 = ran 𝑄) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) |
101 | | simpll 767 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ ¬ 𝑤 = ran 𝑄) → 𝜑) |
102 | | neqne 2948 |
. . . . . 6
⊢ (¬
𝑤 = ran 𝑄 → 𝑤 ≠ ran 𝑄) |
103 | | elprn1 42849 |
. . . . . 6
⊢ ((𝑤 ∈ {ran 𝑄, ∪ ran 𝐼} ∧ 𝑤 ≠ ran 𝑄) → 𝑤 = ∪ ran 𝐼) |
104 | 102, 103 | sylan2 596 |
. . . . 5
⊢ ((𝑤 ∈ {ran 𝑄, ∪ ran 𝐼} ∧ ¬ 𝑤 = ran 𝑄) → 𝑤 = ∪ ran 𝐼) |
105 | 104 | adantll 714 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ ¬ 𝑤 = ran 𝑄) → 𝑤 = ∪ ran 𝐼) |
106 | 10, 12 | mp1i 13 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ran 𝐼 ∈ Fin) |
107 | | ax-resscn 10786 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
108 | 107 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ⊆
ℂ) |
109 | 75, 108 | fssd 6563 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
110 | 109 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
111 | 71 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝑠 ∈ (𝐴[,]𝐵)) |
112 | 110, 111 | ffvelrnd 6905 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → (𝐹‘𝑠) ∈ ℂ) |
113 | 112 | abscld 15000 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → (abs‘(𝐹‘𝑠)) ∈ ℝ) |
114 | 47, 11 | fnmpti 6521 |
. . . . . . . . . 10
⊢ 𝐼 Fn (0..^𝑀) |
115 | | fvelrnb 6773 |
. . . . . . . . . 10
⊢ (𝐼 Fn (0..^𝑀) → (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡)) |
116 | 114, 115 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
117 | 116 | biimpi 219 |
. . . . . . . 8
⊢ (𝑡 ∈ ran 𝐼 → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
118 | 117 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) |
119 | 4 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
120 | | elfzofz 13258 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
121 | 120 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
122 | 119, 121 | ffvelrnd 6905 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
123 | | fzofzp1 13339 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
124 | 123 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
125 | 119, 124 | ffvelrnd 6905 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
126 | | fourierdlem70.fcn |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
127 | | fourierdlem70.l |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
128 | | fourierdlem70.r |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
129 | 122, 125,
126, 127, 128 | cncfioobd 43113 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏) |
130 | | fvres 6736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠) = (𝐹‘𝑠)) |
131 | 130 | fveq2d 6721 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) = (abs‘(𝐹‘𝑠))) |
132 | 131 | breq1d 5063 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
133 | 132 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
134 | 133 | ralbidva 3117 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
135 | 134 | rexbidv 3216 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
136 | 129, 135 | mpbid 235 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏) |
137 | 136 | 3adant3 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏) |
138 | 47, 50 | mpan2 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (0..^𝑀) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
139 | 138 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖)) |
140 | 139 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖)) |
141 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (𝐼‘𝑖) = 𝑡) |
142 | 140, 141 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡) |
143 | 142 | raleqdv 3325 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
144 | 143 | rexbidv 3216 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
145 | 144 | 3adant1 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
146 | 137, 145 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏) |
147 | 146 | 3exp 1121 |
. . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏))) |
148 | 147 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏))) |
149 | 148 | rexlimdv 3202 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) |
150 | 118, 149 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏) |
151 | 150 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏) |
152 | | eqimss 3957 |
. . . . . 6
⊢ (𝑤 = ∪
ran 𝐼 → 𝑤 ⊆ ∪ ran 𝐼) |
153 | 152 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → 𝑤 ⊆ ∪ ran
𝐼) |
154 | 106, 113,
151, 153 | ssfiunibd 42521 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) |
155 | 101, 105,
154 | syl2anc 587 |
. . 3
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ ¬ 𝑤 = ran 𝑄) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) |
156 | 100, 155 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) |
157 | 21 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑀 ∈ ℕ) |
158 | 4 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ) |
159 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (𝐴[,]𝐵)) |
160 | 25 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 = (𝑄‘0)) |
161 | 26 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 = (𝑄‘𝑀)) |
162 | 160, 161 | oveq12d 7231 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀))) |
163 | 162 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀))) |
164 | 159, 163 | eleqtrd 2840 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) |
165 | 164 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) |
166 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ¬ 𝑡 ∈ ran 𝑄) |
167 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗)) |
168 | 167 | breq1d 5063 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < 𝑡 ↔ (𝑄‘𝑗) < 𝑡)) |
169 | 168 | cbvrabv 3402 |
. . . . . . . . . . . . 13
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝑡} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑡} |
170 | 169 | supeq1i 9063 |
. . . . . . . . . . . 12
⊢
sup({𝑘 ∈
(0..^𝑀) ∣ (𝑄‘𝑘) < 𝑡}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑡}, ℝ, < ) |
171 | 157, 158,
165, 166, 170 | fourierdlem25 43348 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
172 | 138 | eleq2d 2823 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0..^𝑀) → (𝑡 ∈ (𝐼‘𝑖) ↔ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
173 | 172 | rexbiia 3169 |
. . . . . . . . . . 11
⊢
(∃𝑖 ∈
(0..^𝑀)𝑡 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
174 | 171, 173 | sylibr 237 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑡 ∈ (𝐼‘𝑖)) |
175 | 48 | eqcomi 2746 |
. . . . . . . . . . 11
⊢
(0..^𝑀) = dom 𝐼 |
176 | 175 | rexeqi 3324 |
. . . . . . . . . 10
⊢
(∃𝑖 ∈
(0..^𝑀)𝑡 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖)) |
177 | 174, 176 | sylib 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖)) |
178 | | elunirn 7064 |
. . . . . . . . . 10
⊢ (Fun
𝐼 → (𝑡 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖))) |
179 | 42, 178 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → (𝑡 ∈ ∪ ran
𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖))) |
180 | 177, 179 | mpbird 260 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑡 ∈ ∪ ran
𝐼) |
181 | 180 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (¬ 𝑡 ∈ ran 𝑄 → 𝑡 ∈ ∪ ran
𝐼)) |
182 | 181 | orrd 863 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ ran 𝑄 ∨ 𝑡 ∈ ∪ ran
𝐼)) |
183 | | elun 4063 |
. . . . . 6
⊢ (𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼) ↔ (𝑡 ∈ ran 𝑄 ∨ 𝑡 ∈ ∪ ran
𝐼)) |
184 | 182, 183 | sylibr 237 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) |
185 | 184 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑡 ∈ (𝐴[,]𝐵)𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) |
186 | | dfss3 3888 |
. . . 4
⊢ ((𝐴[,]𝐵) ⊆ (ran 𝑄 ∪ ∪ ran
𝐼) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) |
187 | 185, 186 | sylibr 237 |
. . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (ran 𝑄 ∪ ∪ ran
𝐼)) |
188 | 187, 17 | sseqtrrd 3942 |
. 2
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ {ran
𝑄, ∪ ran 𝐼}) |
189 | 2, 79, 156, 188 | ssfiunibd 42521 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑠 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑠)) ≤ 𝑥) |