Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. 2
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. 2
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | readdcl 9898 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) |
4 | 3 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ) |
5 | | itg2mono.3 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) |
6 | | rge0ssre 12151 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℝ |
7 | | fss 5969 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ ℝ) → (𝐹‘𝑛):ℝ⟶ℝ) |
8 | 5, 6, 7 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶ℝ) |
9 | | itg2mono.8 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐻 ∈ dom
∫1) |
10 | | itg2mono.7 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑇 ∈ (0(,)1)) |
11 | | 0xr 9965 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℝ* |
12 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ |
13 | 12 | rexri 9976 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℝ* |
14 | | elioo2 12087 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑇 ∈ (0(,)1) ↔ (𝑇 ∈ ℝ ∧ 0 <
𝑇 ∧ 𝑇 < 1))) |
15 | 11, 13, 14 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ (0(,)1) ↔ (𝑇 ∈ ℝ ∧ 0 <
𝑇 ∧ 𝑇 < 1)) |
16 | 10, 15 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1)) |
17 | 16 | simp1d 1066 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ∈ ℝ) |
18 | 17 | renegcld 10336 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → -𝑇 ∈ ℝ) |
19 | 9, 18 | i1fmulc 23276 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((ℝ × {-𝑇}) ∘𝑓
· 𝐻) ∈ dom
∫1) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ ×
{-𝑇})
∘𝑓 · 𝐻) ∈ dom
∫1) |
21 | | i1ff 23249 |
. . . . . . . . . . . . . . . 16
⊢
(((ℝ × {-𝑇}) ∘𝑓 ·
𝐻) ∈ dom
∫1 → ((ℝ × {-𝑇}) ∘𝑓 ·
𝐻):ℝ⟶ℝ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ ×
{-𝑇})
∘𝑓 · 𝐻):ℝ⟶ℝ) |
23 | | reex 9906 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
∈ V |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℝ ∈
V) |
25 | | inidm 3784 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
∩ ℝ) = ℝ |
26 | 4, 8, 22, 24, 24, 25 | off 6810 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)):ℝ⟶ℝ) |
27 | 26 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)):ℝ⟶ℝ) |
28 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)):ℝ⟶ℝ → ((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) Fn ℝ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) Fn ℝ) |
30 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) Fn ℝ → (𝑥 ∈ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)) ↔ (𝑥 ∈ ℝ ∧ (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ (-∞(,)0)))) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)) ↔ (𝑥 ∈ ℝ ∧ (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ (-∞(,)0)))) |
32 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
33 | 32 | biantrurd 528 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ (-∞(,)0) ↔ (𝑥 ∈ ℝ ∧ (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ (-∞(,)0)))) |
34 | 31, 33 | bitr4d 270 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)) ↔ (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ (-∞(,)0))) |
35 | 26 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ ℝ) |
36 | 35 | biantrurd 528 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) < 0 ↔ ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ ℝ ∧ (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) < 0))) |
37 | | elioomnf 12139 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℝ* → ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ (-∞(,)0) ↔ ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ ℝ ∧ (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) < 0))) |
38 | 11, 37 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ (-∞(,)0) ↔ ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ ℝ ∧ (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) < 0)) |
39 | 36, 38 | syl6rbbr 278 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) ∈ (-∞(,)0) ↔ (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) < 0)) |
40 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑛):ℝ⟶ℝ → (𝐹‘𝑛) Fn ℝ) |
41 | 8, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) Fn ℝ) |
42 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢
(((ℝ × {-𝑇}) ∘𝑓 ·
𝐻):ℝ⟶ℝ
→ ((ℝ × {-𝑇}) ∘𝑓 ·
𝐻) Fn
ℝ) |
43 | 22, 42 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ ×
{-𝑇})
∘𝑓 · 𝐻) Fn ℝ) |
44 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑥)) |
45 | 18 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → -𝑇 ∈ ℝ) |
46 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐻 ∈ dom ∫1
→ 𝐻:ℝ⟶ℝ) |
47 | 9, 46 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐻:ℝ⟶ℝ) |
48 | | ffn 5958 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐻:ℝ⟶ℝ →
𝐻 Fn
ℝ) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐻 Fn ℝ) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐻 Fn ℝ) |
51 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) = (𝐻‘𝑥)) |
52 | 24, 45, 50, 51 | ofc1 6818 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ ×
{-𝑇})
∘𝑓 · 𝐻)‘𝑥) = (-𝑇 · (𝐻‘𝑥))) |
53 | 17 | recnd 9947 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 ∈ ℂ) |
54 | 53 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ) |
55 | 47 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ) |
56 | 55 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ) |
57 | 56 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℂ) |
58 | 54, 57 | mulneg1d 10362 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (-𝑇 · (𝐻‘𝑥)) = -(𝑇 · (𝐻‘𝑥))) |
59 | 52, 58 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((ℝ ×
{-𝑇})
∘𝑓 · 𝐻)‘𝑥) = -(𝑇 · (𝐻‘𝑥))) |
60 | 41, 43, 24, 24, 25, 44, 59 | ofval 6804 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥)))) |
61 | 8 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) |
62 | 61 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑛)‘𝑥) ∈ ℂ) |
63 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ) |
64 | 63, 55 | remulcld 9949 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ) |
65 | 64 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ) |
66 | 65 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℂ) |
67 | 62, 66 | negsubd 10277 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛)‘𝑥) + -(𝑇 · (𝐻‘𝑥))) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥)))) |
68 | 60, 67 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) = (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥)))) |
69 | 68 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) < 0 ↔ (((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0)) |
70 | | 0red 9920 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ∈
ℝ) |
71 | 61, 65, 70 | ltsubaddd 10502 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛)‘𝑥) − (𝑇 · (𝐻‘𝑥))) < 0 ↔ ((𝐹‘𝑛)‘𝑥) < (0 + (𝑇 · (𝐻‘𝑥))))) |
72 | 66 | addid2d 10116 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (0 + (𝑇 · (𝐻‘𝑥))) = (𝑇 · (𝐻‘𝑥))) |
73 | 72 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑛)‘𝑥) < (0 + (𝑇 · (𝐻‘𝑥))) ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥)))) |
74 | 69, 71, 73 | 3bitrd 293 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻))‘𝑥) < 0 ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥)))) |
75 | 34, 39, 74 | 3bitrd 293 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)) ↔ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥)))) |
76 | 75 | notbid 307 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)) ↔ ¬
((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥)))) |
77 | | eldif 3550 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0))) ↔ (𝑥 ∈ ℝ ∧ ¬
𝑥 ∈ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “
(-∞(,)0)))) |
78 | 77 | baib 942 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0))) ↔ ¬
𝑥 ∈ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “
(-∞(,)0)))) |
79 | 78 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0))) ↔ ¬
𝑥 ∈ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “
(-∞(,)0)))) |
80 | 65, 61 | lenltd 10062 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ ¬ ((𝐹‘𝑛)‘𝑥) < (𝑇 · (𝐻‘𝑥)))) |
81 | 76, 79, 80 | 3bitr4d 299 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0))) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥))) |
82 | 81 | rabbi2dva 3783 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∩
(ℝ ∖ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)))) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)}) |
83 | | rembl 23115 |
. . . . . . 7
⊢ ℝ
∈ dom vol |
84 | | itg2mono.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn) |
85 | | i1fmbf 23248 |
. . . . . . . . . . 11
⊢
(((ℝ × {-𝑇}) ∘𝑓 ·
𝐻) ∈ dom
∫1 → ((ℝ × {-𝑇}) ∘𝑓 ·
𝐻) ∈
MblFn) |
86 | 20, 85 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ℝ ×
{-𝑇})
∘𝑓 · 𝐻) ∈ MblFn) |
87 | 84, 86 | mbfadd 23234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) ∈ MblFn) |
88 | | mbfima 23205 |
. . . . . . . . 9
⊢ ((((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) ∈ MblFn ∧ ((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)):ℝ⟶ℝ) → (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)) ∈ dom
vol) |
89 | 87, 26, 88 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)) ∈ dom
vol) |
90 | | cmmbl 23109 |
. . . . . . . 8
⊢ ((◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)) ∈ dom vol
→ (ℝ ∖ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0))) ∈ dom
vol) |
91 | 89, 90 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∖
(◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0))) ∈ dom
vol) |
92 | | inmbl 23117 |
. . . . . . 7
⊢ ((ℝ
∈ dom vol ∧ (ℝ ∖ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0))) ∈ dom vol)
→ (ℝ ∩ (ℝ ∖ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)))) ∈ dom
vol) |
93 | 83, 91, 92 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ℝ ∩
(ℝ ∖ (◡((𝐹‘𝑛) ∘𝑓 + ((ℝ
× {-𝑇})
∘𝑓 · 𝐻)) “ (-∞(,)0)))) ∈ dom
vol) |
94 | 82, 93 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} ∈ dom vol) |
95 | | itg2mono.11 |
. . . . 5
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)}) |
96 | 94, 95 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝐴:ℕ⟶dom vol) |
97 | | itg2mono.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1))) |
98 | 97 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1))) |
99 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗)) |
100 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1)) |
101 | 100 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑗 + 1))) |
102 | 99, 101 | breq12d 4596 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑗) ∘𝑟 ≤ (𝐹‘(𝑗 + 1)))) |
103 | 102 | cbvralv 3147 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛) ∘𝑟
≤ (𝐹‘(𝑛 + 1)) ↔ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘𝑟 ≤ (𝐹‘(𝑗 + 1))) |
104 | 98, 103 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗) ∘𝑟 ≤ (𝐹‘(𝑗 + 1))) |
105 | 104 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∘𝑟 ≤ (𝐹‘(𝑗 + 1))) |
106 | 5 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞)) |
107 | 99 | feq1d 5943 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑗):ℝ⟶(0[,)+∞))) |
108 | 107 | cbvralv 3147 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞)
↔ ∀𝑗 ∈
ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞)) |
109 | 106, 108 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝐹‘𝑗):ℝ⟶(0[,)+∞)) |
110 | 109 | r19.21bi 2916 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞)) |
111 | | ffn 5958 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑗):ℝ⟶(0[,)+∞) → (𝐹‘𝑗) Fn ℝ) |
112 | 110, 111 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) Fn ℝ) |
113 | | peano2nn 10909 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
114 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑗 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑗 + 1))) |
115 | 114 | feq1d 5943 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘(𝑗 +
1)):ℝ⟶(0[,)+∞))) |
116 | 115 | rspccva 3281 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞)
∧ (𝑗 + 1) ∈
ℕ) → (𝐹‘(𝑗 +
1)):ℝ⟶(0[,)+∞)) |
117 | 106, 113,
116 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 +
1)):ℝ⟶(0[,)+∞)) |
118 | | ffn 5958 |
. . . . . . . . . . 11
⊢ ((𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞) →
(𝐹‘(𝑗 + 1)) Fn
ℝ) |
119 | 117, 118 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 + 1)) Fn ℝ) |
120 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℝ ∈
V) |
121 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) = ((𝐹‘𝑗)‘𝑥)) |
122 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥)) |
123 | 112, 119,
120, 120, 25, 121, 122 | ofrfval 6803 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∘𝑟 ≤ (𝐹‘(𝑗 + 1)) ↔ ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))) |
124 | 105, 123 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) |
125 | 124 | r19.21bi 2916 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) |
126 | 17 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ) |
127 | 47 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐻:ℝ⟶ℝ) |
128 | 127 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ∈ ℝ) |
129 | 126, 128 | remulcld 9949 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ) |
130 | | fss 5969 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑗):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ ℝ) → (𝐹‘𝑗):ℝ⟶ℝ) |
131 | 110, 6, 130 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶ℝ) |
132 | 131 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ) |
133 | | fss 5969 |
. . . . . . . . . 10
⊢ (((𝐹‘(𝑗 + 1)):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ ℝ) → (𝐹‘(𝑗 +
1)):ℝ⟶ℝ) |
134 | 117, 6, 133 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝑗 +
1)):ℝ⟶ℝ) |
135 | 134 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ) |
136 | | letr 10010 |
. . . . . . . 8
⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ ((𝐹‘(𝑗 + 1))‘𝑥) ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))) |
137 | 129, 132,
135, 136 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) ∧ ((𝐹‘𝑗)‘𝑥) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))) |
138 | 125, 137 | mpan2d 706 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))) |
139 | 138 | ss2rabdv 3646 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ⊆ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)}) |
140 | 99 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑗)‘𝑥)) |
141 | 140 | breq2d 4595 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))) |
142 | 141 | rabbidv 3164 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}) |
143 | 23 | rabex 4740 |
. . . . . . 7
⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ∈ V |
144 | 142, 95, 143 | fvmpt 6191 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}) |
145 | 144 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}) |
146 | 113 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ) |
147 | 114 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑛 = (𝑗 + 1) → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘(𝑗 + 1))‘𝑥)) |
148 | 147 | breq2d 4595 |
. . . . . . . 8
⊢ (𝑛 = (𝑗 + 1) → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥))) |
149 | 148 | rabbidv 3164 |
. . . . . . 7
⊢ (𝑛 = (𝑗 + 1) → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)}) |
150 | 23 | rabex 4740 |
. . . . . . 7
⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)} ∈ V |
151 | 149, 95, 150 | fvmpt 6191 |
. . . . . 6
⊢ ((𝑗 + 1) ∈ ℕ →
(𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)}) |
152 | 146, 151 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘(𝑗 + 1)) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘(𝑗 + 1))‘𝑥)}) |
153 | 139, 145,
152 | 3sstr4d 3611 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ⊆ (𝐴‘(𝑗 + 1))) |
154 | 64 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ) |
155 | 55 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℝ) |
156 | 61 | an32s 842 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛)‘𝑥) ∈ ℝ) |
157 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) |
158 | 156, 157 | fmptd 6292 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ) |
159 | | frn 5966 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ) |
161 | | 1nn 10908 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℕ |
162 | 157, 156 | dmmptd 5937 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ℕ) |
163 | 161, 162 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))) |
164 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
dom (𝑛 ∈ ℕ
↦ ((𝐹‘𝑛)‘𝑥)) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅) |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅) |
166 | | dm0rn0 5263 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ∅) |
167 | 166 | necon3bii 2834 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅) |
168 | 165, 167 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅) |
169 | | itg2mono.5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
170 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)):ℕ⟶ℝ → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ) |
171 | 158, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ) |
172 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) → (𝑧 ≤ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦)) |
173 | 172 | ralrn 6270 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦)) |
174 | 171, 173 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦)) |
175 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
176 | 175 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑚)‘𝑥)) |
177 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘𝑚)‘𝑥) ∈ V |
178 | 176, 157,
177 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) = ((𝐹‘𝑚)‘𝑥)) |
179 | 178 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)) |
180 | 179 | ralbiia 2962 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑚 ∈
ℕ ((𝑛 ∈ ℕ
↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦) |
181 | 176 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → (((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦)) |
182 | 181 | cbvralv 3147 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑛 ∈
ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦 ↔ ∀𝑚 ∈ ℕ ((𝐹‘𝑚)‘𝑥) ≤ 𝑦) |
183 | 180, 182 | bitr4i 266 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑚 ∈
ℕ ((𝑛 ∈ ℕ
↦ ((𝐹‘𝑛)‘𝑥))‘𝑚) ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
184 | 174, 183 | syl6bb 275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)) |
185 | 184 | rexbidv 3034 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)) |
186 | 169, 185 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) |
187 | | suprcl 10862 |
. . . . . . . . . . . . . . . 16
⊢ ((ran
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈
ℝ) |
188 | 160, 168,
186, 187 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈
ℝ) |
189 | 188 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ∈
ℝ) |
190 | 16 | simp3d 1068 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 < 1) |
191 | 190 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 𝑇 < 1) |
192 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 𝑇 ∈ ℝ) |
193 | | 1red 9934 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 1 ∈ ℝ) |
194 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → 0 < (𝐻‘𝑥)) |
195 | | ltmul1 10752 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ ℝ ∧ 1 ∈
ℝ ∧ ((𝐻‘𝑥) ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 < 1 ↔ (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥)))) |
196 | 192, 193,
155, 194, 195 | syl112anc 1322 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 < 1 ↔ (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥)))) |
197 | 191, 196 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < (1 · (𝐻‘𝑥))) |
198 | 155 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ∈ ℂ) |
199 | 198 | mulid2d 9937 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (1 · (𝐻‘𝑥)) = (𝐻‘𝑥)) |
200 | 197, 199 | breqtrd 4609 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < (𝐻‘𝑥)) |
201 | | itg2mono.9 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐻 ∘𝑟 ≤ 𝐺) |
202 | | itg2mono.1 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
203 | 188, 202 | fmptd 6292 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
204 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺:ℝ⟶ℝ →
𝐺 Fn
ℝ) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐺 Fn ℝ) |
206 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ℝ ∈
V) |
207 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐻‘𝑦) = (𝐻‘𝑦)) |
208 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑛)‘𝑦)) |
209 | 208 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦))) |
210 | 209 | rneqd 5274 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) = ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦))) |
211 | 210 | supeq1d 8235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )) |
212 | | ltso 9997 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ < Or
ℝ |
213 | 212 | supex 8252 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ sup(ran
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑦)), ℝ, < ) ∈ V |
214 | 211, 202,
213 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )) |
215 | 214 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐺‘𝑦) = sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )) |
216 | 49, 205, 206, 206, 25, 207, 215 | ofrfval 6803 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐻 ∘𝑟 ≤ 𝐺 ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))) |
217 | 201, 216 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )) |
218 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) |
219 | 218, 211 | breq12d 4596 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < ))) |
220 | 219 | cbvralv 3147 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∀𝑦 ∈ ℝ (𝐻‘𝑦) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑦)), ℝ, < )) |
221 | 217, 220 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
222 | 221 | r19.21bi 2916 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
223 | 222 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝐻‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
224 | 154, 155,
189, 200, 223 | ltletrd 10076 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
225 | 160 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ⊆ ℝ) |
226 | 168 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅) |
227 | 186 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) |
228 | | suprlub 10864 |
. . . . . . . . . . . . . 14
⊢ (((ran
(𝑛 ∈ ℕ ↦
((𝐹‘𝑛)‘𝑥)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))𝑧 ≤ 𝑦) ∧ (𝑇 · (𝐻‘𝑥)) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤)) |
229 | 225, 226,
227, 154, 228 | syl31anc 1321 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ((𝑇 · (𝐻‘𝑥)) < sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤)) |
230 | 224, 229 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤) |
231 | 171 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ) |
232 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) → ((𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗))) |
233 | 232 | rexrn 6269 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)) Fn ℕ → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗))) |
234 | 231, 233 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗))) |
235 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑗)‘𝑥) ∈ V |
236 | 140, 157,
235 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) = ((𝐹‘𝑗)‘𝑥)) |
237 | 236 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → ((𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))) |
238 | 237 | rexbiia 3022 |
. . . . . . . . . . . . 13
⊢
(∃𝑗 ∈
ℕ (𝑇 · (𝐻‘𝑥)) < ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))‘𝑗) ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)) |
239 | 234, 238 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥))(𝑇 · (𝐻‘𝑥)) < 𝑤 ↔ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥))) |
240 | 230, 239 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥)) |
241 | 192, 155 | remulcld 9949 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ) |
242 | 241 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ) |
243 | 110 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):ℝ⟶(0[,)+∞)) |
244 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈ ℝ) |
245 | 243, 244 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞)) |
246 | | elrege0 12149 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑗)‘𝑥) ∈ (0[,)+∞) ↔ (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥))) |
247 | 245, 246 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥))) |
248 | 247 | simpld 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ) |
249 | 248 | adantlrr 753 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ) |
250 | | ltle 10005 |
. . . . . . . . . . . . 13
⊢ (((𝑇 · (𝐻‘𝑥)) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑥) ∈ ℝ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))) |
251 | 242, 249,
250 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) ∧ 𝑗 ∈ ℕ) → ((𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))) |
252 | 251 | reximdva 3000 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → (∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) < ((𝐹‘𝑗)‘𝑥) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥))) |
253 | 240, 252 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 0 < (𝐻‘𝑥))) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) |
254 | 253 | anassrs 678 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 0 < (𝐻‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) |
255 | 161 | ne0ii 3882 |
. . . . . . . . . . 11
⊢ ℕ
≠ ∅ |
256 | 64 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ) |
257 | 256 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ∈ ℝ) |
258 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 ∈
ℝ) |
259 | 247 | adantlrr 753 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (((𝐹‘𝑗)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑗)‘𝑥))) |
260 | 259 | simpld 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑥) ∈ ℝ) |
261 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑥) ≤ 0) |
262 | 55 | adantrr 749 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → (𝐻‘𝑥) ∈ ℝ) |
263 | 262 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑥) ∈ ℝ) |
264 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℝ) |
265 | 16 | simp2d 1067 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 < 𝑇) |
266 | 265 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 < 𝑇) |
267 | | lemul2 10755 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐻‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧
(𝑇 ∈ ℝ ∧ 0
< 𝑇)) → ((𝐻‘𝑥) ≤ 0 ↔ (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0))) |
268 | 263, 258,
264, 266, 267 | syl112anc 1322 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑥) ≤ 0 ↔ (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0))) |
269 | 261, 268 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ (𝑇 · 0)) |
270 | 264 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℂ) |
271 | 270 | mul01d 10114 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · 0) = 0) |
272 | 269, 271 | breqtrd 4609 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ 0) |
273 | 259 | simprd 478 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → 0 ≤ ((𝐹‘𝑗)‘𝑥)) |
274 | 257, 258,
260, 272, 273 | letrd 10073 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) ∧ 𝑗 ∈ ℕ) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) |
275 | 274 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) |
276 | | r19.2z 4012 |
. . . . . . . . . . 11
⊢ ((ℕ
≠ ∅ ∧ ∀𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) |
277 | 255, 275,
276 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐻‘𝑥) ≤ 0)) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) |
278 | 277 | anassrs 678 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐻‘𝑥) ≤ 0) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) |
279 | | 0red 9920 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈
ℝ) |
280 | 254, 278,
279, 55 | ltlecasei 10024 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) |
281 | 280 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) |
282 | | rabid2 3096 |
. . . . . . 7
⊢ (ℝ
= {𝑥 ∈ ℝ ∣
∃𝑗 ∈ ℕ
(𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)) |
283 | 281, 282 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → ℝ = {𝑥 ∈ ℝ ∣
∃𝑗 ∈ ℕ
(𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}) |
284 | | iunrab 4503 |
. . . . . 6
⊢ ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} = {𝑥 ∈ ℝ ∣ ∃𝑗 ∈ ℕ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)} |
285 | 283, 284 | syl6eqr 2662 |
. . . . 5
⊢ (𝜑 → ℝ = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}) |
286 | 145 | iuneq2dv 4478 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ 𝑗 ∈ ℕ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑗)‘𝑥)}) |
287 | | ffn 5958 |
. . . . . . 7
⊢ (𝐴:ℕ⟶dom vol →
𝐴 Fn
ℕ) |
288 | 96, 287 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴 Fn ℕ) |
289 | | fniunfv 6409 |
. . . . . 6
⊢ (𝐴 Fn ℕ → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴) |
290 | 288, 289 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (𝐴‘𝑗) = ∪ ran 𝐴) |
291 | 285, 286,
290 | 3eqtr2rd 2651 |
. . . 4
⊢ (𝜑 → ∪ ran 𝐴 = ℝ) |
292 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) |
293 | 96, 153, 291, 9, 292 | itg1climres 23287 |
. . 3
⊢ (𝜑 → (𝑗 ∈ ℕ ↦
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ⇝
(∫1‘𝐻)) |
294 | | nnex 10903 |
. . . . 5
⊢ ℕ
∈ V |
295 | 294 | mptex 6390 |
. . . 4
⊢ (𝑗 ∈ ℕ ↦ (𝑇 ·
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V |
296 | 295 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ∈ V) |
297 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘)) |
298 | 297 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑥 ∈ (𝐴‘𝑗) ↔ 𝑥 ∈ (𝐴‘𝑘))) |
299 | 298 | ifbid 4058 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0) = if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) |
300 | 299 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) |
301 | 300 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) |
302 | | eqid 2610 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ ↦
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑗 ∈ ℕ ↦
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) |
303 | | fvex 6113 |
. . . . . . 7
⊢
(∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ V |
304 | 301, 302,
303 | fvmpt 6191 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) |
305 | 304 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) |
306 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐻 ∈ dom
∫1) |
307 | 96 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ dom vol) |
308 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) |
309 | 308 | i1fres 23278 |
. . . . . . 7
⊢ ((𝐻 ∈ dom ∫1
∧ (𝐴‘𝑘) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom
∫1) |
310 | 306, 307,
309 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom
∫1) |
311 | | itg1cl 23258 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) ∈ dom ∫1 →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ) |
312 | 310, 311 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ ℝ) |
313 | 305, 312 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℝ) |
314 | 313 | recnd 9947 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘) ∈ ℂ) |
315 | 301 | oveq2d 6565 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))) |
316 | | eqid 2610 |
. . . . . 6
⊢ (𝑗 ∈ ℕ ↦ (𝑇 ·
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) = (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) |
317 | | ovex 6577 |
. . . . . 6
⊢ (𝑇 ·
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) ∈ V |
318 | 315, 316,
317 | fvmpt 6191 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (𝑇 ·
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))) |
319 | 304 | oveq2d 6565 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (𝑇 · ((𝑗 ∈ ℕ ↦
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘)) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))) |
320 | 318, 319 | eqtr4d 2647 |
. . . 4
⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ (𝑇 ·
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · ((𝑗 ∈ ℕ ↦
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘))) |
321 | 320 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · ((𝑗 ∈ ℕ ↦
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))‘𝑘))) |
322 | 1, 2, 293, 53, 296, 314, 321 | climmulc2 14215 |
. 2
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))))) ⇝ (𝑇 · (∫1‘𝐻))) |
323 | | icossicc 12131 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
324 | | fss 5969 |
. . . . . . 7
⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
325 | 5, 323, 324 | sylancl 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
326 | | itg2mono.10 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ ℝ) |
327 | 326 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ∈ ℝ) |
328 | | itg2cl 23305 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛):ℝ⟶(0[,]+∞) →
(∫2‘(𝐹‘𝑛)) ∈
ℝ*) |
329 | 325, 328 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ∈
ℝ*) |
330 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) |
331 | 329, 330 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ*) |
332 | | frn 5966 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ* →
ran (𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
333 | 331, 332 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
334 | 333 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
335 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(∫2‘(𝐹‘𝑛)) ∈ V |
336 | 335 | elabrex 6405 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))}) |
337 | 336 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ∈ {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))}) |
338 | 330 | rnmpt 5292 |
. . . . . . . . 9
⊢ ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = (∫2‘(𝐹‘𝑛))} |
339 | 337, 338 | syl6eleqr 2699 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) |
340 | | supxrub 12026 |
. . . . . . . 8
⊢ ((ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ* ∧
(∫2‘(𝐹‘𝑛)) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) → (∫2‘(𝐹‘𝑛)) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
)) |
341 | 334, 339,
340 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
)) |
342 | | itg2mono.6 |
. . . . . . 7
⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
) |
343 | 341, 342 | syl6breqr 4625 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ≤ 𝑆) |
344 | | itg2lecl 23311 |
. . . . . 6
⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ 𝑆 ∈ ℝ ∧
(∫2‘(𝐹‘𝑛)) ≤ 𝑆) → (∫2‘(𝐹‘𝑛)) ∈ ℝ) |
345 | 325, 327,
343, 344 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ∈ ℝ) |
346 | 345, 330 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ) |
347 | 325 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
348 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
349 | 348 | feq1d 5943 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,]+∞))) |
350 | 349 | cbvralv 3147 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞)
↔ ∀𝑘 ∈
ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞)) |
351 | 347, 350 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞)) |
352 | | peano2nn 10909 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
353 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
354 | 353 | feq1d 5943 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘):ℝ⟶(0[,]+∞) ↔ (𝐹‘(𝑛 +
1)):ℝ⟶(0[,]+∞))) |
355 | 354 | rspccva 3281 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
ℕ (𝐹‘𝑘):ℝ⟶(0[,]+∞)
∧ (𝑛 + 1) ∈
ℕ) → (𝐹‘(𝑛 +
1)):ℝ⟶(0[,]+∞)) |
356 | 351, 352,
355 | syl2an 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘(𝑛 +
1)):ℝ⟶(0[,]+∞)) |
357 | | itg2le 23312 |
. . . . . . . 8
⊢ (((𝐹‘𝑛):ℝ⟶(0[,]+∞) ∧ (𝐹‘(𝑛 + 1)):ℝ⟶(0[,]+∞) ∧
(𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1))) →
(∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1)))) |
358 | 325, 356,
97, 357 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1)))) |
359 | 358 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ℕ
(∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1)))) |
360 | 348 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘𝑘))) |
361 | | fvex 6113 |
. . . . . . . . . 10
⊢
(∫2‘(𝐹‘𝑘)) ∈ V |
362 | 360, 330,
361 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘))) |
363 | | peano2nn 10909 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
364 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑘 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑘 + 1))) |
365 | 364 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑘 + 1) → (∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘(𝑘 + 1)))) |
366 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(∫2‘(𝐹‘(𝑘 + 1))) ∈ V |
367 | 365, 330,
366 | fvmpt 6191 |
. . . . . . . . . 10
⊢ ((𝑘 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1)))) |
368 | 363, 367 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) = (∫2‘(𝐹‘(𝑘 + 1)))) |
369 | 362, 368 | breq12d 4596 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ (∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1))))) |
370 | 369 | ralbiia 2962 |
. . . . . . 7
⊢
(∀𝑘 ∈
ℕ ((𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ ∀𝑘 ∈ ℕ
(∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))) |
371 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1)) |
372 | 371 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1))) |
373 | 372 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (∫2‘(𝐹‘(𝑛 + 1))) = (∫2‘(𝐹‘(𝑘 + 1)))) |
374 | 360, 373 | breq12d 4596 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))) ↔
(∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1))))) |
375 | 374 | cbvralv 3147 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ (∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1))) ↔ ∀𝑘 ∈ ℕ
(∫2‘(𝐹‘𝑘)) ≤ (∫2‘(𝐹‘(𝑘 + 1)))) |
376 | 370, 375 | bitr4i 266 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ ((𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘(𝑘 + 1)) ↔ ∀𝑛 ∈ ℕ
(∫2‘(𝐹‘𝑛)) ≤ (∫2‘(𝐹‘(𝑛 + 1)))) |
377 | 359, 376 | sylibr 223 |
. . . . 5
⊢ (𝜑 → ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘(𝑘 + 1))) |
378 | 377 | r19.21bi 2916 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘(𝑘 + 1))) |
379 | 343 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℕ
(∫2‘(𝐹‘𝑛)) ≤ 𝑆) |
380 | 362 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)) |
381 | 380 | ralbiia 2962 |
. . . . . . . 8
⊢
(∀𝑘 ∈
ℕ ((𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ
(∫2‘(𝐹‘𝑘)) ≤ 𝑥) |
382 | 360 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑘)) ≤ 𝑥)) |
383 | 382 | cbvralv 3147 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ℕ (∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ
(∫2‘(𝐹‘𝑘)) ≤ 𝑥) |
384 | 381, 383 | bitr4i 266 |
. . . . . . 7
⊢
(∀𝑘 ∈
ℕ ((𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ
(∫2‘(𝐹‘𝑛)) ≤ 𝑥) |
385 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑥 = 𝑆 → ((∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ (∫2‘(𝐹‘𝑛)) ≤ 𝑆)) |
386 | 385 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = 𝑆 → (∀𝑛 ∈ ℕ
(∫2‘(𝐹‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ
(∫2‘(𝐹‘𝑛)) ≤ 𝑆)) |
387 | 384, 386 | syl5bb 271 |
. . . . . 6
⊢ (𝑥 = 𝑆 → (∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥 ↔ ∀𝑛 ∈ ℕ
(∫2‘(𝐹‘𝑛)) ≤ 𝑆)) |
388 | 387 | rspcev 3282 |
. . . . 5
⊢ ((𝑆 ∈ ℝ ∧
∀𝑛 ∈ ℕ
(∫2‘(𝐹‘𝑛)) ≤ 𝑆) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥) |
389 | 326, 379,
388 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥) |
390 | 1, 2, 346, 378, 389 | climsup 14248 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⇝ sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ, < )) |
391 | | frn 5966 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ) |
392 | 346, 391 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ) |
393 | 330, 329 | dmmptd 5937 |
. . . . . . 7
⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) = ℕ) |
394 | 255 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℕ ≠
∅) |
395 | 393, 394 | eqnetrd 2849 |
. . . . . 6
⊢ (𝜑 → dom (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ≠ ∅) |
396 | | dm0rn0 5263 |
. . . . . . 7
⊢ (dom
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) = ∅ ↔ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) = ∅) |
397 | 396 | necon3bii 2834 |
. . . . . 6
⊢ (dom
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ≠ ∅ ↔ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ≠ ∅) |
398 | 395, 397 | sylib 207 |
. . . . 5
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ≠ ∅) |
399 | 335, 330 | fnmpti 5935 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ |
400 | 399 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ) |
401 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑧 = ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) → (𝑧 ≤ 𝑥 ↔ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)) |
402 | 401 | ralrn 6270 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)) |
403 | 400, 402 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)) |
404 | 403 | rexbidv 3034 |
. . . . . 6
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ≤ 𝑥)) |
405 | 389, 404 | mpbird 246 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥) |
406 | | supxrre 12029 |
. . . . 5
⊢ ((ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))𝑧 ≤ 𝑥) → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, < ) = sup(ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ, < )) |
407 | 392, 398,
405, 406 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, < ) = sup(ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ, < )) |
408 | 342, 407 | syl5req 2657 |
. . 3
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ, < ) = 𝑆) |
409 | 390, 408 | breqtrd 4609 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⇝ 𝑆) |
410 | 17 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℝ) |
411 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐻 ∈ dom
∫1) |
412 | 96 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑗) ∈ dom vol) |
413 | 292 | i1fres 23278 |
. . . . . . 7
⊢ ((𝐻 ∈ dom ∫1
∧ (𝐴‘𝑗) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom
∫1) |
414 | 411, 412,
413 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom
∫1) |
415 | | itg1cl 23258 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)) ∈ dom ∫1 →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ) |
416 | 414, 415 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑗), (𝐻‘𝑥), 0))) ∈ ℝ) |
417 | 410, 416 | remulcld 9949 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))) ∈ ℝ) |
418 | 417, 316 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥),
0))))):ℕ⟶ℝ) |
419 | 418 | ffvelrnda 6267 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ∈ ℝ) |
420 | 346 | ffvelrnda 6267 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) ∈ ℝ) |
421 | 348 | feq1d 5943 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛):ℝ⟶(0[,)+∞) ↔ (𝐹‘𝑘):ℝ⟶(0[,)+∞))) |
422 | 421 | cbvralv 3147 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛):ℝ⟶(0[,)+∞)
↔ ∀𝑘 ∈
ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞)) |
423 | 106, 422 | sylib 207 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘):ℝ⟶(0[,)+∞)) |
424 | 423 | r19.21bi 2916 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):ℝ⟶(0[,)+∞)) |
425 | | fss 5969 |
. . . . 5
⊢ (((𝐹‘𝑘):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑘):ℝ⟶(0[,]+∞)) |
426 | 424, 323,
425 | sylancl 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):ℝ⟶(0[,]+∞)) |
427 | 23 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℝ ∈
V) |
428 | 17 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 ∈ ℝ) |
429 | 428 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ) |
430 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐻‘𝑥) ∈ V |
431 | | c0ex 9913 |
. . . . . . . . 9
⊢ 0 ∈
V |
432 | 430, 431 | ifex 4106 |
. . . . . . . 8
⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V |
433 | 432 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0) ∈ V) |
434 | | fconstmpt 5085 |
. . . . . . . 8
⊢ (ℝ
× {𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇) |
435 | 434 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℝ ×
{𝑇}) = (𝑥 ∈ ℝ ↦ 𝑇)) |
436 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) |
437 | 427, 429,
433, 435, 436 | offval2 6812 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ ×
{𝑇})
∘𝑓 · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) |
438 | | ovif2 6636 |
. . . . . . . 8
⊢ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0)) |
439 | 53 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 ∈ ℂ) |
440 | 439 | mul01d 10114 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · 0) = 0) |
441 | 440 | ifeq2d 4055 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), (𝑇 · 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) |
442 | 438, 441 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)) = if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) |
443 | 442 | mpteq2dv 4673 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ (𝑇 · if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) |
444 | 437, 443 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ ×
{𝑇})
∘𝑓 · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) |
445 | 310, 428 | i1fmulc 23276 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℝ ×
{𝑇})
∘𝑓 · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))) ∈ dom
∫1) |
446 | 444, 445 | eqeltrrd 2689 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom
∫1) |
447 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥))) |
448 | 447 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = (𝑇 · (𝐻‘𝑥))) |
449 | 348 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)‘𝑥) = ((𝐹‘𝑘)‘𝑥)) |
450 | 449 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → ((𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥) ↔ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))) |
451 | 450 | rabbidv 3164 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)}) |
452 | 23 | rabex 4740 |
. . . . . . . . . . . . 13
⊢ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ∈ V |
453 | 451, 95, 452 | fvmpt 6191 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)}) |
454 | 453 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴‘𝑘) = {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)}) |
455 | 454 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)})) |
456 | 455 | biimpa 500 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → 𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)}) |
457 | | rabid 3095 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} ↔ (𝑥 ∈ ℝ ∧ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥))) |
458 | 457 | simprbi 479 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)} → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)) |
459 | 456, 458 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑘)‘𝑥)) |
460 | 448, 459 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥)) |
461 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ (𝐴‘𝑘) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0) |
462 | 461 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) = 0) |
463 | 424 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞)) |
464 | | elrege0 12149 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞) ↔ (((𝐹‘𝑘)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑘)‘𝑥))) |
465 | 464 | simprbi 479 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑘)‘𝑥) ∈ (0[,)+∞) → 0 ≤ ((𝐹‘𝑘)‘𝑥)) |
466 | 463, 465 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘𝑘)‘𝑥)) |
467 | 466 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → 0 ≤ ((𝐹‘𝑘)‘𝑥)) |
468 | 462, 467 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (𝐴‘𝑘)) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥)) |
469 | 460, 468 | pm2.61dan 828 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥)) |
470 | 469 | ralrimiva 2949 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥)) |
471 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑇 · (𝐻‘𝑥)) ∈ V |
472 | 471, 431 | ifex 4106 |
. . . . . . 7
⊢ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V |
473 | 472 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ∈ V) |
474 | | fvex 6113 |
. . . . . . 7
⊢ ((𝐹‘𝑘)‘𝑥) ∈ V |
475 | 474 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑘)‘𝑥) ∈ V) |
476 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) |
477 | 424 | feqmptd 6159 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑥 ∈ ℝ ↦ ((𝐹‘𝑘)‘𝑥))) |
478 | 427, 473,
475, 476, 477 | ofrfval2 6813 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘𝑟 ≤
(𝐹‘𝑘) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0) ≤ ((𝐹‘𝑘)‘𝑥))) |
479 | 470, 478 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘𝑟 ≤
(𝐹‘𝑘)) |
480 | | itg2ub 23306 |
. . . 4
⊢ (((𝐹‘𝑘):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∈ dom ∫1 ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)) ∘𝑟 ≤
(𝐹‘𝑘)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) ≤ (∫2‘(𝐹‘𝑘))) |
481 | 426, 446,
479, 480 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0))) ≤ (∫2‘(𝐹‘𝑘))) |
482 | 318 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))) |
483 | 310, 428 | itg1mulc 23277 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(∫1‘((ℝ × {𝑇}) ∘𝑓 ·
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0))))) |
484 | 444 | fveq2d 6107 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(∫1‘((ℝ × {𝑇}) ∘𝑓 ·
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ (𝐴‘𝑘), (𝐻‘𝑥), 0)))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))) |
485 | 482, 483,
484 | 3eqtr2d 2650 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑘), (𝑇 · (𝐻‘𝑥)), 0)))) |
486 | 362 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘) = (∫2‘(𝐹‘𝑘))) |
487 | 481, 485,
486 | 3brtr4d 4615 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑇 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑗), (𝐻‘𝑥), 0)))))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘𝑘)) |
488 | 1, 2, 322, 409, 419, 420, 487 | climle 14218 |
1
⊢ (𝜑 → (𝑇 · (∫1‘𝐻)) ≤ 𝑆) |