Step | Hyp | Ref
| Expression |
1 | | fvex 6201 |
. . . . . . . . . 10
⊢ (𝐹‘𝑥) ∈ V |
2 | | c0ex 10034 |
. . . . . . . . . 10
⊢ 0 ∈
V |
3 | 1, 2 | ifex 4156 |
. . . . . . . . 9
⊢ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ V |
4 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
5 | 4 | fvmpt2 6291 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥) = if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
6 | 3, 5 | mpan2 707 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥) = if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
7 | 6 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
8 | 7 | rneqd 5353 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
9 | 8 | supeq1d 8352 |
. . . . 5
⊢ (𝑥 ∈ ℝ → sup(ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
10 | 9 | mpteq2ia 4740 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ sup(ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < )) = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
11 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑦sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < ) |
12 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥ℕ |
13 | | nfmpt1 4747 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
14 | 12, 13 | nfmpt 4746 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
15 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑚 |
16 | 14, 15 | nffv 6198 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) |
17 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑦 |
18 | 16, 17 | nffv 6198 |
. . . . . . . 8
⊢
Ⅎ𝑥(((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) |
19 | 12, 18 | nfmpt 4746 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) |
20 | 19 | nfrn 5368 |
. . . . . 6
⊢
Ⅎ𝑥ran
(𝑚 ∈ ℕ ↦
(((𝑛 ∈ ℕ ↦
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) |
21 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑥ℝ |
22 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑥
< |
23 | 20, 21, 22 | nfsup 8357 |
. . . . 5
⊢
Ⅎ𝑥sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ) |
24 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦)) |
25 | 24 | mpteq2dv 4745 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦))) |
26 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑥) ≤ 𝑛 ↔ (𝐹‘𝑥) ≤ 𝑚)) |
27 | 26 | ifbid 4108 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
28 | 27 | mpteq2dv 4745 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
29 | 28 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
30 | 29 | cbvmptv 4750 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
31 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) = (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
32 | | reex 10027 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
33 | 32 | mptex 6486 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∈ V |
34 | 28, 31, 33 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
35 | 34 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
36 | 35 | mpteq2ia 4740 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
37 | 30, 36 | eqtr4i 2647 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) |
38 | 25, 37 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦))) |
39 | 38 | rneqd 5353 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦))) |
40 | 39 | supeq1d 8352 |
. . . . 5
⊢ (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )) |
41 | 11, 23, 40 | cbvmpt 4749 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ sup(ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )) |
42 | 10, 41 | eqtr3i 2646 |
. . 3
⊢ (𝑥 ∈ ℝ ↦ sup(ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran
(𝑚 ∈ ℕ ↦
(((𝑛 ∈ ℕ ↦
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )) |
43 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
44 | 43 | breq1d 4663 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑚 ↔ (𝐹‘𝑦) ≤ 𝑚)) |
45 | 44, 43 | ifbieq1d 4109 |
. . . . . 6
⊢ (𝑥 = 𝑦 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
46 | 45 | cbvmptv 4750 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
47 | 34 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
48 | | nnre 11027 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
49 | 48 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ) |
50 | 49 | rexrd 10089 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ*) |
51 | | elioopnf 12267 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℝ*
→ ((𝐹‘𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 < (𝐹‘𝑦)))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹‘𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 < (𝐹‘𝑦)))) |
53 | | itg2cn.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
54 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℝ⟶(0[,)+∞)
→ 𝐹 Fn
ℝ) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn ℝ) |
56 | 55 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝐹 Fn ℝ) |
57 | | elpreima 6337 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn ℝ → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑦) ∈ (𝑚(,)+∞)))) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑦) ∈ (𝑚(,)+∞)))) |
59 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
60 | 59 | biantrurd 529 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹‘𝑦) ∈ (𝑚(,)+∞) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑦) ∈ (𝑚(,)+∞)))) |
61 | 58, 60 | bitr4d 271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ (𝐹‘𝑦) ∈ (𝑚(,)+∞))) |
62 | | rge0ssre 12280 |
. . . . . . . . . . . . . 14
⊢
(0[,)+∞) ⊆ ℝ |
63 | | fss 6056 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ) |
64 | 53, 62, 63 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
65 | 64 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹:ℝ⟶ℝ) |
66 | 65 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) |
67 | 66 | biantrurd 529 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑚 < (𝐹‘𝑦) ↔ ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 < (𝐹‘𝑦)))) |
68 | 52, 61, 67 | 3bitr4d 300 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ 𝑚 < (𝐹‘𝑦))) |
69 | 68 | notbid 308 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ ¬ 𝑚 < (𝐹‘𝑦))) |
70 | | eldif 3584 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)))) |
71 | 70 | baib 944 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)))) |
72 | 71 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)))) |
73 | 66, 49 | lenltd 10183 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹‘𝑦) ≤ 𝑚 ↔ ¬ 𝑚 < (𝐹‘𝑦))) |
74 | 69, 72, 73 | 3bitr4d 300 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ (𝐹‘𝑦) ≤ 𝑚)) |
75 | 74 | ifbid 4108 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) = if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
76 | 75 | mpteq2dva 4744 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0))) |
77 | 46, 47, 76 | 3eqtr4a 2682 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0))) |
78 | | difss 3737 |
. . . . . 6
⊢ (ℝ
∖ (◡𝐹 “ (𝑚(,)+∞))) ⊆
ℝ |
79 | 78 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (ℝ ∖
(◡𝐹 “ (𝑚(,)+∞))) ⊆
ℝ) |
80 | | rembl 23308 |
. . . . . 6
⊢ ℝ
∈ dom vol |
81 | 80 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ℝ ∈ dom
vol) |
82 | | fvex 6201 |
. . . . . . 7
⊢ (𝐹‘𝑦) ∈ V |
83 | 82, 2 | ifex 4156 |
. . . . . 6
⊢ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) ∈ V |
84 | 83 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) ∈ V) |
85 | | eldifn 3733 |
. . . . . . 7
⊢ (𝑦 ∈ (ℝ ∖
(ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) → ¬ 𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) |
86 | 85 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖
(◡𝐹 “ (𝑚(,)+∞))))) → ¬ 𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) |
87 | 86 | iffalsed 4097 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖
(◡𝐹 “ (𝑚(,)+∞))))) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) = 0) |
88 | | iftrue 4092 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) = (𝐹‘𝑦)) |
89 | 88 | mpteq2ia 4740 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) = (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ (𝐹‘𝑦)) |
90 | | resmpt 5449 |
. . . . . . . . 9
⊢ ((ℝ
∖ (◡𝐹 “ (𝑚(,)+∞))) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ (𝐹‘𝑦))) |
91 | 78, 90 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ (𝐹‘𝑦)) |
92 | 89, 91 | eqtr4i 2647 |
. . . . . . 7
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) = ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) |
93 | 53 | feqmptd 6249 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦))) |
94 | | itg2cn.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ MblFn) |
95 | 93, 94 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn) |
96 | | mbfima 23399 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) →
(◡𝐹 “ (𝑚(,)+∞)) ∈ dom
vol) |
97 | 94, 64, 96 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ (𝑚(,)+∞)) ∈ dom
vol) |
98 | | cmmbl 23302 |
. . . . . . . . 9
⊢ ((◡𝐹 “ (𝑚(,)+∞)) ∈ dom vol → (ℝ
∖ (◡𝐹 “ (𝑚(,)+∞))) ∈ dom
vol) |
99 | 97, 98 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ∈ dom
vol) |
100 | | mbfres 23411 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn ∧ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ∈ dom vol) → ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) ∈
MblFn) |
101 | 95, 99, 100 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) ∈
MblFn) |
102 | 92, 101 | syl5eqel 2705 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) ∈ MblFn) |
103 | 102 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) ∈ MblFn) |
104 | 79, 81, 84, 87, 103 | mbfss 23413 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) ∈ MblFn) |
105 | 77, 104 | eqeltrd 2701 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) ∈ MblFn) |
106 | 53 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
107 | | 0e0icopnf 12282 |
. . . . . . 7
⊢ 0 ∈
(0[,)+∞) |
108 | | ifcl 4130 |
. . . . . . 7
⊢ (((𝐹‘𝑥) ∈ (0[,)+∞) ∧ 0 ∈
(0[,)+∞)) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ (0[,)+∞)) |
109 | 106, 107,
108 | sylancl 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ (0[,)+∞)) |
110 | 109 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ (0[,)+∞)) |
111 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
112 | 110, 111 | fmptd 6385 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥),
0)):ℝ⟶(0[,)+∞)) |
113 | 47 | feq1d 6030 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚):ℝ⟶(0[,)+∞) ↔ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥),
0)):ℝ⟶(0[,)+∞))) |
114 | 112, 113 | mpbird 247 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚):ℝ⟶(0[,)+∞)) |
115 | | elrege0 12278 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
116 | 106, 115 | sylib 208 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
117 | 116 | simpld 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
118 | 117 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
119 | 118 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ∈ ℝ) |
120 | 119 | leidd 10594 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ≤ (𝐹‘𝑥)) |
121 | | iftrue 4092 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ≤ 𝑚 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
122 | 121 | adantl 482 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
123 | 48 | ad3antlr 767 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → 𝑚 ∈ ℝ) |
124 | | peano2re 10209 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℝ → (𝑚 + 1) ∈
ℝ) |
125 | 123, 124 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝑚 + 1) ∈ ℝ) |
126 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ≤ 𝑚) |
127 | 123 | lep1d 10955 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → 𝑚 ≤ (𝑚 + 1)) |
128 | 119, 123,
125, 126, 127 | letrd 10194 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ≤ (𝑚 + 1)) |
129 | 128 | iftrued 4094 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
130 | 120, 122,
129 | 3brtr4d 4685 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
131 | | iffalse 4095 |
. . . . . . . . 9
⊢ (¬
(𝐹‘𝑥) ≤ 𝑚 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = 0) |
132 | 131 | adantl 482 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = 0) |
133 | 116 | simprd 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥)) |
134 | | 0le0 11110 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
135 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑥) = if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
136 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ (0 =
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) → (0 ≤ 0 ↔ 0 ≤
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
137 | 135, 136 | ifboth 4124 |
. . . . . . . . . . 11
⊢ ((0 ≤
(𝐹‘𝑥) ∧ 0 ≤ 0) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
138 | 133, 134,
137 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
139 | 138 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
140 | 139 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹‘𝑥) ≤ 𝑚) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
141 | 132, 140 | eqbrtrd 4675 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
142 | 130, 141 | pm2.61dan 832 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
143 | 142 | ralrimiva 2966 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
144 | 1, 2 | ifex 4156 |
. . . . . . 7
⊢ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) ∈ V |
145 | 144 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) ∈ V) |
146 | | eqidd 2623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
147 | | eqidd 2623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
148 | 81, 110, 145, 146, 147 | ofrfval2 6915 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
149 | 143, 148 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
150 | | peano2nn 11032 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℕ) |
151 | 150 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ) |
152 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑛 = (𝑚 + 1) → ((𝐹‘𝑥) ≤ 𝑛 ↔ (𝐹‘𝑥) ≤ (𝑚 + 1))) |
153 | 152 | ifbid 4108 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
154 | 153 | mpteq2dv 4745 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
155 | 32 | mptex 6486 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) ∈ V |
156 | 154, 31, 155 | fvmpt 6282 |
. . . . 5
⊢ ((𝑚 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
157 | 151, 156 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
158 | 149, 47, 157 | 3brtr4d 4685 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) ∘𝑟 ≤ ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘(𝑚 + 1))) |
159 | 64 | ffvelrnda 6359 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) |
160 | 34 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
161 | 160 | fveq1d 6193 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
162 | 117 | leidd 10594 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ (𝐹‘𝑥)) |
163 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑥) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))) |
164 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢ (0 =
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))) |
165 | 163, 164 | ifboth 4124 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
166 | 162, 133,
165 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
167 | 166 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
168 | 167 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
169 | 32 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ℝ ∈
V) |
170 | 1, 2 | ifex 4156 |
. . . . . . . . . . . 12
⊢ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ V |
171 | 170 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ V) |
172 | 53 | feqmptd 6249 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
173 | 172 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
174 | 169, 171,
118, 146, 173 | ofrfval2 6915 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))) |
175 | 168, 174 | mpbird 247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘𝑟 ≤ 𝐹) |
176 | 171, 111 | fmptd 6385 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)):ℝ⟶V) |
177 | | ffn 6045 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)):ℝ⟶V → (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) Fn ℝ) |
178 | 176, 177 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) Fn ℝ) |
179 | 55 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹 Fn ℝ) |
180 | | inidm 3822 |
. . . . . . . . . 10
⊢ (ℝ
∩ ℝ) = ℝ |
181 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
182 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
183 | 178, 179,
169, 169, 180, 181, 182 | ofrfval 6905 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘𝑟 ≤ 𝐹 ↔ ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦))) |
184 | 175, 183 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦)) |
185 | 184 | r19.21bi 2932 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦)) |
186 | 185 | an32s 846 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦)) |
187 | 161, 186 | eqbrtrd 4675 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦)) |
188 | 187 | ralrimiva 2966 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦)) |
189 | | breq2 4657 |
. . . . . 6
⊢ (𝑧 = (𝐹‘𝑦) → ((((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧 ↔ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦))) |
190 | 189 | ralbidv 2986 |
. . . . 5
⊢ (𝑧 = (𝐹‘𝑦) → (∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧 ↔ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦))) |
191 | 190 | rspcev 3309 |
. . . 4
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦)) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧) |
192 | 159, 188,
191 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧) |
193 | 28 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
194 | 193 | cbvmptv 4750 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = (𝑚 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
195 | 34 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ →
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
196 | 195 | mpteq2ia 4740 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))) = (𝑚 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
197 | 194, 196 | eqtr4i 2647 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = (𝑚 ∈ ℕ ↦
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))) |
198 | 197 | rneqi 5352 |
. . . 4
⊢ ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = ran (𝑚 ∈ ℕ ↦
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))) |
199 | 198 | supeq1i 8353 |
. . 3
⊢ sup(ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) =
sup(ran (𝑚 ∈ ℕ
↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))), ℝ*, <
) |
200 | 42, 105, 114, 158, 192, 199 | itg2mono 23520 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ))) = sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, <
)) |
201 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
202 | 27, 201, 170 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
203 | 202 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
204 | 166 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
205 | 203, 204 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥)) |
206 | 205 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥)) |
207 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ V) |
208 | 207, 201 | fmptd 6385 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)):ℕ⟶V) |
209 | | ffn 6045 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)):ℕ⟶V → (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ) |
210 | 208, 209 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ) |
211 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑤 = ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) → (𝑤 ≤ (𝐹‘𝑥) ↔ ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥))) |
212 | 211 | ralrn 6362 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥))) |
213 | 210, 212 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥))) |
214 | 206, 213 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥)) |
215 | 117 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑥) ∈ ℝ) |
216 | | 0re 10040 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
217 | | ifcl 4130 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ ℝ) |
218 | 215, 216,
217 | sylancl 694 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ ℝ) |
219 | 218, 201 | fmptd 6385 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥),
0)):ℕ⟶ℝ) |
220 | | frn 6053 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)):ℕ⟶ℝ → ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ) |
221 | 219, 220 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ) |
222 | | 1nn 11031 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
223 | 201, 218 | dmmptd 6024 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ℕ) |
224 | 222, 223 | syl5eleqr 2708 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
225 | | n0i 3920 |
. . . . . . . . . 10
⊢ (1 ∈
dom (𝑛 ∈ ℕ
↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) → ¬ dom (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅) |
226 | | dm0rn0 5342 |
. . . . . . . . . . 11
⊢ (dom
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅) |
227 | 226 | necon3bbii 2841 |
. . . . . . . . . 10
⊢ (¬
dom (𝑛 ∈ ℕ
↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅) |
228 | 225, 227 | sylib 208 |
. . . . . . . . 9
⊢ (1 ∈
dom (𝑛 ∈ ℕ
↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) → ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅) |
229 | 224, 228 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅) |
230 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘𝑥) → (𝑤 ≤ 𝑧 ↔ 𝑤 ≤ (𝐹‘𝑥))) |
231 | 230 | ralbidv 2986 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐹‘𝑥) → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧 ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥))) |
232 | 231 | rspcev 3309 |
. . . . . . . . 9
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) |
233 | 117, 214,
232 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) |
234 | | suprleub 10989 |
. . . . . . . 8
⊢ (((ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) ∧ (𝐹‘𝑥) ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥))) |
235 | 221, 229,
233, 117, 234 | syl31anc 1329 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥))) |
236 | 214, 235 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥)) |
237 | | arch 11289 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ ℝ → ∃𝑚 ∈ ℕ (𝐹‘𝑥) < 𝑚) |
238 | 117, 237 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑚 ∈ ℕ (𝐹‘𝑥) < 𝑚) |
239 | 202 | ad2antrl 764 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
240 | | ltle 10126 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝐹‘𝑥) < 𝑚 → (𝐹‘𝑥) ≤ 𝑚)) |
241 | 117, 48, 240 | syl2an 494 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝐹‘𝑥) < 𝑚 → (𝐹‘𝑥) ≤ 𝑚)) |
242 | 241 | impr 649 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → (𝐹‘𝑥) ≤ 𝑚) |
243 | 242 | iftrued 4094 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
244 | 239, 243 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = (𝐹‘𝑥)) |
245 | 210 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ) |
246 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → 𝑚 ∈ ℕ) |
247 | | fnfvelrn 6356 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
248 | 245, 246,
247 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
249 | 244, 248 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → (𝐹‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
250 | 238, 249 | rexlimddv 3035 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
251 | | suprub 10984 |
. . . . . . 7
⊢ (((ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) ∧ (𝐹‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) → (𝐹‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
252 | 221, 229,
233, 250, 251 | syl31anc 1329 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
253 | | suprcl 10983 |
. . . . . . . 8
⊢ ((ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) → sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ∈
ℝ) |
254 | 221, 229,
233, 253 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ∈
ℝ) |
255 | 254, 117 | letri3d 10179 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) = (𝐹‘𝑥) ↔ (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )))) |
256 | 236, 252,
255 | mpbir2and 957 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) = (𝐹‘𝑥)) |
257 | 256 | mpteq2dva 4744 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
258 | 257, 172 | eqtr4d 2659 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) = 𝐹) |
259 | 258 | fveq2d 6195 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ))) =
(∫2‘𝐹)) |
260 | 200, 259 | eqtr3d 2658 |
1
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) =
(∫2‘𝐹)) |