Step | Hyp | Ref
| Expression |
1 | | fvex 6461 |
. . . . . . . . . 10
⊢ (𝐹‘𝑥) ∈ V |
2 | | c0ex 10372 |
. . . . . . . . . 10
⊢ 0 ∈
V |
3 | 1, 2 | ifex 4355 |
. . . . . . . . 9
⊢ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ V |
4 | | eqid 2778 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
5 | 4 | fvmpt2 6554 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥) = if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
6 | 3, 5 | mpan2 681 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥) = if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
7 | 6 | mpteq2dv 4982 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
8 | 7 | rneqd 5600 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
9 | 8 | supeq1d 8642 |
. . . . 5
⊢ (𝑥 ∈ ℝ → sup(ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
10 | 9 | mpteq2ia 4977 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ sup(ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < )) = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
11 | | nfcv 2934 |
. . . . 5
⊢
Ⅎ𝑦sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < ) |
12 | | nfcv 2934 |
. . . . . . . 8
⊢
Ⅎ𝑥ℕ |
13 | | nfmpt1 4984 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
14 | 12, 13 | nfmpt 4983 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
15 | | nfcv 2934 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑚 |
16 | 14, 15 | nffv 6458 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) |
17 | | nfcv 2934 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑦 |
18 | 16, 17 | nffv 6458 |
. . . . . . . 8
⊢
Ⅎ𝑥(((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) |
19 | 12, 18 | nfmpt 4983 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) |
20 | 19 | nfrn 5616 |
. . . . . 6
⊢
Ⅎ𝑥ran
(𝑚 ∈ ℕ ↦
(((𝑛 ∈ ℕ ↦
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) |
21 | | nfcv 2934 |
. . . . . 6
⊢
Ⅎ𝑥ℝ |
22 | | nfcv 2934 |
. . . . . 6
⊢
Ⅎ𝑥
< |
23 | 20, 21, 22 | nfsup 8647 |
. . . . 5
⊢
Ⅎ𝑥sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ) |
24 | | fveq2 6448 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦)) |
25 | 24 | mpteq2dv 4982 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦))) |
26 | | breq2 4892 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑥) ≤ 𝑛 ↔ (𝐹‘𝑥) ≤ 𝑚)) |
27 | 26 | ifbid 4329 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
28 | 27 | mpteq2dv 4982 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
29 | 28 | fveq1d 6450 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
30 | 29 | cbvmptv 4987 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
31 | | eqid 2778 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) = (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
32 | | reex 10365 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
33 | 32 | mptex 6760 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∈ V |
34 | 28, 31, 33 | fvmpt 6544 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
35 | 34 | fveq1d 6450 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
36 | 35 | mpteq2ia 4977 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
37 | 30, 36 | eqtr4i 2805 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) |
38 | 25, 37 | syl6eq 2830 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦))) |
39 | 38 | rneqd 5600 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦))) |
40 | 39 | supeq1d 8642 |
. . . . 5
⊢ (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )) |
41 | 11, 23, 40 | cbvmpt 4986 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ sup(ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )) |
42 | 10, 41 | eqtr3i 2804 |
. . 3
⊢ (𝑥 ∈ ℝ ↦ sup(ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran
(𝑚 ∈ ℕ ↦
(((𝑛 ∈ ℕ ↦
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )) |
43 | | fveq2 6448 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
44 | 43 | breq1d 4898 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑚 ↔ (𝐹‘𝑦) ≤ 𝑚)) |
45 | 44, 43 | ifbieq1d 4330 |
. . . . . 6
⊢ (𝑥 = 𝑦 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
46 | 45 | cbvmptv 4987 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
47 | 34 | adantl 475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
48 | | nnre 11386 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
49 | 48 | ad2antlr 717 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ) |
50 | 49 | rexrd 10428 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ*) |
51 | | elioopnf 12584 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℝ*
→ ((𝐹‘𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 < (𝐹‘𝑦)))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹‘𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 < (𝐹‘𝑦)))) |
53 | | itg2cn.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
54 | 53 | ffnd 6294 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn ℝ) |
55 | 54 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝐹 Fn ℝ) |
56 | | elpreima 6602 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn ℝ → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑦) ∈ (𝑚(,)+∞)))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑦) ∈ (𝑚(,)+∞)))) |
58 | | simpr 479 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
59 | 58 | biantrurd 528 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹‘𝑦) ∈ (𝑚(,)+∞) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑦) ∈ (𝑚(,)+∞)))) |
60 | 57, 59 | bitr4d 274 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ (𝐹‘𝑦) ∈ (𝑚(,)+∞))) |
61 | | rge0ssre 12598 |
. . . . . . . . . . . . . 14
⊢
(0[,)+∞) ⊆ ℝ |
62 | | fss 6306 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ) |
63 | 53, 61, 62 | sylancl 580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
64 | 63 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹:ℝ⟶ℝ) |
65 | 64 | ffvelrnda 6625 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) |
66 | 65 | biantrurd 528 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑚 < (𝐹‘𝑦) ↔ ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 < (𝐹‘𝑦)))) |
67 | 52, 60, 66 | 3bitr4d 303 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ 𝑚 < (𝐹‘𝑦))) |
68 | 67 | notbid 310 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ ¬ 𝑚 < (𝐹‘𝑦))) |
69 | | eldif 3802 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)))) |
70 | 69 | baib 531 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)))) |
71 | 70 | adantl 475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)))) |
72 | 65, 49 | lenltd 10524 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹‘𝑦) ≤ 𝑚 ↔ ¬ 𝑚 < (𝐹‘𝑦))) |
73 | 68, 71, 72 | 3bitr4d 303 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ (𝐹‘𝑦) ≤ 𝑚)) |
74 | 73 | ifbid 4329 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) = if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
75 | 74 | mpteq2dva 4981 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0))) |
76 | 46, 47, 75 | 3eqtr4a 2840 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0))) |
77 | | difss 3960 |
. . . . . 6
⊢ (ℝ
∖ (◡𝐹 “ (𝑚(,)+∞))) ⊆
ℝ |
78 | 77 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (ℝ ∖
(◡𝐹 “ (𝑚(,)+∞))) ⊆
ℝ) |
79 | | rembl 23748 |
. . . . . 6
⊢ ℝ
∈ dom vol |
80 | 79 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ℝ ∈ dom
vol) |
81 | | fvex 6461 |
. . . . . . 7
⊢ (𝐹‘𝑦) ∈ V |
82 | 81, 2 | ifex 4355 |
. . . . . 6
⊢ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) ∈ V |
83 | 82 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) ∈ V) |
84 | | eldifn 3956 |
. . . . . . 7
⊢ (𝑦 ∈ (ℝ ∖
(ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) → ¬ 𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) |
85 | 84 | adantl 475 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖
(◡𝐹 “ (𝑚(,)+∞))))) → ¬ 𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) |
86 | 85 | iffalsed 4318 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖
(◡𝐹 “ (𝑚(,)+∞))))) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) = 0) |
87 | | iftrue 4313 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) = (𝐹‘𝑦)) |
88 | 87 | mpteq2ia 4977 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) = (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ (𝐹‘𝑦)) |
89 | | resmpt 5701 |
. . . . . . . . 9
⊢ ((ℝ
∖ (◡𝐹 “ (𝑚(,)+∞))) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ (𝐹‘𝑦))) |
90 | 77, 89 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ (𝐹‘𝑦)) |
91 | 88, 90 | eqtr4i 2805 |
. . . . . . 7
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) = ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) |
92 | 53 | feqmptd 6511 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦))) |
93 | | itg2cn.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ MblFn) |
94 | 92, 93 | eqeltrrd 2860 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn) |
95 | | mbfima 23838 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) →
(◡𝐹 “ (𝑚(,)+∞)) ∈ dom
vol) |
96 | 93, 63, 95 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ (𝑚(,)+∞)) ∈ dom
vol) |
97 | | cmmbl 23742 |
. . . . . . . . 9
⊢ ((◡𝐹 “ (𝑚(,)+∞)) ∈ dom vol → (ℝ
∖ (◡𝐹 “ (𝑚(,)+∞))) ∈ dom
vol) |
98 | 96, 97 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ∈ dom
vol) |
99 | | mbfres 23852 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn ∧ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ∈ dom vol) → ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) ∈
MblFn) |
100 | 94, 98, 99 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) ∈
MblFn) |
101 | 91, 100 | syl5eqel 2863 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) ∈ MblFn) |
102 | 101 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) ∈ MblFn) |
103 | 78, 80, 83, 86, 102 | mbfss 23854 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) ∈ MblFn) |
104 | 76, 103 | eqeltrd 2859 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) ∈ MblFn) |
105 | 53 | ffvelrnda 6625 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
106 | | 0e0icopnf 12600 |
. . . . . . 7
⊢ 0 ∈
(0[,)+∞) |
107 | | ifcl 4351 |
. . . . . . 7
⊢ (((𝐹‘𝑥) ∈ (0[,)+∞) ∧ 0 ∈
(0[,)+∞)) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ (0[,)+∞)) |
108 | 105, 106,
107 | sylancl 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ (0[,)+∞)) |
109 | 108 | adantlr 705 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ (0[,)+∞)) |
110 | 109 | fmpttd 6651 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥),
0)):ℝ⟶(0[,)+∞)) |
111 | 47 | feq1d 6278 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚):ℝ⟶(0[,)+∞) ↔ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥),
0)):ℝ⟶(0[,)+∞))) |
112 | 110, 111 | mpbird 249 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚):ℝ⟶(0[,)+∞)) |
113 | | elrege0 12596 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
114 | 105, 113 | sylib 210 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
115 | 114 | simpld 490 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
116 | 115 | adantlr 705 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
117 | 116 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ∈ ℝ) |
118 | 117 | leidd 10943 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ≤ (𝐹‘𝑥)) |
119 | | iftrue 4313 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ≤ 𝑚 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
120 | 119 | adantl 475 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
121 | 48 | ad3antlr 721 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → 𝑚 ∈ ℝ) |
122 | | peano2re 10551 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℝ → (𝑚 + 1) ∈
ℝ) |
123 | 121, 122 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝑚 + 1) ∈ ℝ) |
124 | | simpr 479 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ≤ 𝑚) |
125 | 121 | lep1d 11311 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → 𝑚 ≤ (𝑚 + 1)) |
126 | 117, 121,
123, 124, 125 | letrd 10535 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ≤ (𝑚 + 1)) |
127 | 126 | iftrued 4315 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
128 | 118, 120,
127 | 3brtr4d 4920 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
129 | | iffalse 4316 |
. . . . . . . . 9
⊢ (¬
(𝐹‘𝑥) ≤ 𝑚 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = 0) |
130 | 129 | adantl 475 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = 0) |
131 | 114 | simprd 491 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥)) |
132 | | 0le0 11487 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
133 | | breq2 4892 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑥) = if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
134 | | breq2 4892 |
. . . . . . . . . . . 12
⊢ (0 =
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) → (0 ≤ 0 ↔ 0 ≤
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
135 | 133, 134 | ifboth 4345 |
. . . . . . . . . . 11
⊢ ((0 ≤
(𝐹‘𝑥) ∧ 0 ≤ 0) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
136 | 131, 132,
135 | sylancl 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
137 | 136 | adantlr 705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
138 | 137 | adantr 474 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹‘𝑥) ≤ 𝑚) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
139 | 130, 138 | eqbrtrd 4910 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
140 | 128, 139 | pm2.61dan 803 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
141 | 140 | ralrimiva 3148 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
142 | 1, 2 | ifex 4355 |
. . . . . . 7
⊢ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) ∈ V |
143 | 142 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) ∈ V) |
144 | | eqidd 2779 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
145 | | eqidd 2779 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
146 | 80, 109, 143, 144, 145 | ofrfval2 7194 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
147 | 141, 146 | mpbird 249 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
148 | | peano2nn 11392 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℕ) |
149 | 148 | adantl 475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ) |
150 | | breq2 4892 |
. . . . . . . 8
⊢ (𝑛 = (𝑚 + 1) → ((𝐹‘𝑥) ≤ 𝑛 ↔ (𝐹‘𝑥) ≤ (𝑚 + 1))) |
151 | 150 | ifbid 4329 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
152 | 151 | mpteq2dv 4982 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
153 | 32 | mptex 6760 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) ∈ V |
154 | 152, 31, 153 | fvmpt 6544 |
. . . . 5
⊢ ((𝑚 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
155 | 149, 154 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
156 | 147, 47, 155 | 3brtr4d 4920 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) ∘𝑟 ≤ ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘(𝑚 + 1))) |
157 | 63 | ffvelrnda 6625 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) |
158 | 34 | adantl 475 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
159 | 158 | fveq1d 6450 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
160 | 115 | leidd 10943 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ (𝐹‘𝑥)) |
161 | | breq1 4891 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑥) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))) |
162 | | breq1 4891 |
. . . . . . . . . . . . . 14
⊢ (0 =
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))) |
163 | 161, 162 | ifboth 4345 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
164 | 160, 131,
163 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
165 | 164 | adantlr 705 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
166 | 165 | ralrimiva 3148 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
167 | 32 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ℝ ∈
V) |
168 | 1, 2 | ifex 4355 |
. . . . . . . . . . . 12
⊢ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ V |
169 | 168 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ V) |
170 | 53 | feqmptd 6511 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
171 | 170 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
172 | 167, 169,
116, 144, 171 | ofrfval2 7194 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))) |
173 | 166, 172 | mpbird 249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘𝑟 ≤ 𝐹) |
174 | 169 | fmpttd 6651 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)):ℝ⟶V) |
175 | 174 | ffnd 6294 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) Fn ℝ) |
176 | 54 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹 Fn ℝ) |
177 | | inidm 4043 |
. . . . . . . . . 10
⊢ (ℝ
∩ ℝ) = ℝ |
178 | | eqidd 2779 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
179 | | eqidd 2779 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
180 | 175, 176,
167, 167, 177, 178, 179 | ofrfval 7184 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘𝑟 ≤ 𝐹 ↔ ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦))) |
181 | 173, 180 | mpbid 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦)) |
182 | 181 | r19.21bi 3114 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦)) |
183 | 182 | an32s 642 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦)) |
184 | 159, 183 | eqbrtrd 4910 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦)) |
185 | 184 | ralrimiva 3148 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦)) |
186 | | brralrspcev 4948 |
. . . 4
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦)) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧) |
187 | 157, 185,
186 | syl2anc 579 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧) |
188 | 28 | fveq2d 6452 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
189 | 188 | cbvmptv 4987 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = (𝑚 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
190 | 34 | fveq2d 6452 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ →
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
191 | 190 | mpteq2ia 4977 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))) = (𝑚 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
192 | 189, 191 | eqtr4i 2805 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = (𝑚 ∈ ℕ ↦
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))) |
193 | 192 | rneqi 5599 |
. . . 4
⊢ ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = ran (𝑚 ∈ ℕ ↦
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))) |
194 | 193 | supeq1i 8643 |
. . 3
⊢ sup(ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) =
sup(ran (𝑚 ∈ ℕ
↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))), ℝ*, <
) |
195 | 42, 104, 112, 156, 187, 194 | itg2mono 23961 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ))) = sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, <
)) |
196 | | eqid 2778 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
197 | 27, 196, 168 | fvmpt 6544 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
198 | 197 | adantl 475 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
199 | 164 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
200 | 198, 199 | eqbrtrd 4910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥)) |
201 | 200 | ralrimiva 3148 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥)) |
202 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ V) |
203 | 202 | fmpttd 6651 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)):ℕ⟶V) |
204 | 203 | ffnd 6294 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ) |
205 | | breq1 4891 |
. . . . . . . . . 10
⊢ (𝑤 = ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) → (𝑤 ≤ (𝐹‘𝑥) ↔ ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥))) |
206 | 205 | ralrn 6628 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥))) |
207 | 204, 206 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥))) |
208 | 201, 207 | mpbird 249 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥)) |
209 | 115 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑥) ∈ ℝ) |
210 | | 0re 10380 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
211 | | ifcl 4351 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ ℝ) |
212 | 209, 210,
211 | sylancl 580 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ ℝ) |
213 | 212 | fmpttd 6651 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥),
0)):ℕ⟶ℝ) |
214 | 213 | frnd 6300 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ) |
215 | | 1nn 11391 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
216 | 196, 212 | dmmptd 6272 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ℕ) |
217 | 215, 216 | syl5eleqr 2866 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
218 | | n0i 4148 |
. . . . . . . . . 10
⊢ (1 ∈
dom (𝑛 ∈ ℕ
↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) → ¬ dom (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅) |
219 | | dm0rn0 5589 |
. . . . . . . . . . 11
⊢ (dom
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅) |
220 | 219 | necon3bbii 3016 |
. . . . . . . . . 10
⊢ (¬
dom (𝑛 ∈ ℕ
↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅) |
221 | 218, 220 | sylib 210 |
. . . . . . . . 9
⊢ (1 ∈
dom (𝑛 ∈ ℕ
↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) → ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅) |
222 | 217, 221 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅) |
223 | | brralrspcev 4948 |
. . . . . . . . 9
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) |
224 | 115, 208,
223 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) |
225 | | suprleub 11347 |
. . . . . . . 8
⊢ (((ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) ∧ (𝐹‘𝑥) ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥))) |
226 | 214, 222,
224, 115, 225 | syl31anc 1441 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥))) |
227 | 208, 226 | mpbird 249 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥)) |
228 | | arch 11643 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ ℝ → ∃𝑚 ∈ ℕ (𝐹‘𝑥) < 𝑚) |
229 | 115, 228 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑚 ∈ ℕ (𝐹‘𝑥) < 𝑚) |
230 | 197 | ad2antrl 718 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
231 | | ltle 10467 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝐹‘𝑥) < 𝑚 → (𝐹‘𝑥) ≤ 𝑚)) |
232 | 115, 48, 231 | syl2an 589 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝐹‘𝑥) < 𝑚 → (𝐹‘𝑥) ≤ 𝑚)) |
233 | 232 | impr 448 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → (𝐹‘𝑥) ≤ 𝑚) |
234 | 233 | iftrued 4315 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
235 | 230, 234 | eqtrd 2814 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = (𝐹‘𝑥)) |
236 | 204 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ) |
237 | | simprl 761 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → 𝑚 ∈ ℕ) |
238 | | fnfvelrn 6622 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
239 | 236, 237,
238 | syl2anc 579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
240 | 235, 239 | eqeltrrd 2860 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → (𝐹‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
241 | 229, 240 | rexlimddv 3218 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
242 | | suprub 11342 |
. . . . . . 7
⊢ (((ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) ∧ (𝐹‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) → (𝐹‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
243 | 214, 222,
224, 241, 242 | syl31anc 1441 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
244 | | suprcl 11341 |
. . . . . . . 8
⊢ ((ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ∈
ℝ) |
245 | 214, 222,
224, 244 | syl3anc 1439 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ∈
ℝ) |
246 | 245, 115 | letri3d 10520 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) = (𝐹‘𝑥) ↔ (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )))) |
247 | 227, 243,
246 | mpbir2and 703 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) = (𝐹‘𝑥)) |
248 | 247 | mpteq2dva 4981 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
249 | 248, 170 | eqtr4d 2817 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) = 𝐹) |
250 | 249 | fveq2d 6452 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ))) =
(∫2‘𝐹)) |
251 | 195, 250 | eqtr3d 2816 |
1
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) =
(∫2‘𝐹)) |