| Step | Hyp | Ref
| Expression |
| 1 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝐹‘𝑥) ∈ V |
| 2 | | c0ex 11255 |
. . . . . . . . . 10
⊢ 0 ∈
V |
| 3 | 1, 2 | ifex 4576 |
. . . . . . . . 9
⊢ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ V |
| 4 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
| 5 | 4 | fvmpt2 7027 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥) = if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
| 6 | 3, 5 | mpan2 691 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥) = if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
| 7 | 6 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
| 8 | 7 | rneqd 5949 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
| 9 | 8 | supeq1d 9486 |
. . . . 5
⊢ (𝑥 ∈ ℝ → sup(ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
| 10 | 9 | mpteq2ia 5245 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ sup(ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < )) = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
| 11 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑦sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < ) |
| 12 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥ℕ |
| 13 | | nfmpt1 5250 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
| 14 | 12, 13 | nfmpt 5249 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
| 15 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑚 |
| 16 | 14, 15 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) |
| 17 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑦 |
| 18 | 16, 17 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑥(((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) |
| 19 | 12, 18 | nfmpt 5249 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) |
| 20 | 19 | nfrn 5963 |
. . . . . 6
⊢
Ⅎ𝑥ran
(𝑚 ∈ ℕ ↦
(((𝑛 ∈ ℕ ↦
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) |
| 21 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥ℝ |
| 22 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥
< |
| 23 | 20, 21, 22 | nfsup 9491 |
. . . . 5
⊢
Ⅎ𝑥sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < ) |
| 24 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦)) |
| 25 | 24 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦))) |
| 26 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑥) ≤ 𝑛 ↔ (𝐹‘𝑥) ≤ 𝑚)) |
| 27 | 26 | ifbid 4549 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
| 28 | 27 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
| 29 | 28 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
| 30 | 29 | cbvmptv 5255 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
| 31 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) = (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
| 32 | | reex 11246 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
| 33 | 32 | mptex 7243 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∈ V |
| 34 | 28, 31, 33 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
| 35 | 34 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
| 36 | 35 | mpteq2ia 5245 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
| 37 | 30, 36 | eqtr4i 2768 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑦)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)) |
| 38 | 25, 37 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦))) |
| 39 | 38 | rneqd 5949 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)) = ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦))) |
| 40 | 39 | supeq1d 9486 |
. . . . 5
⊢ (𝑥 = 𝑦 → sup(ran (𝑛 ∈ ℕ ↦ ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < ) = sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )) |
| 41 | 11, 23, 40 | cbvmpt 5253 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ sup(ran
(𝑛 ∈ ℕ ↦
((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑥)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran (𝑚 ∈ ℕ ↦ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )) |
| 42 | 10, 41 | eqtr3i 2767 |
. . 3
⊢ (𝑥 ∈ ℝ ↦ sup(ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) = (𝑦 ∈ ℝ ↦ sup(ran
(𝑚 ∈ ℕ ↦
(((𝑛 ∈ ℕ ↦
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦)), ℝ, < )) |
| 43 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
| 44 | 43 | breq1d 5153 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑚 ↔ (𝐹‘𝑦) ≤ 𝑚)) |
| 45 | 44, 43 | ifbieq1d 4550 |
. . . . . 6
⊢ (𝑥 = 𝑦 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
| 46 | 45 | cbvmptv 5255 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
| 47 | 34 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
| 48 | | nnre 12273 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
| 49 | 48 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ) |
| 50 | 49 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑚 ∈ ℝ*) |
| 51 | | elioopnf 13483 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℝ*
→ ((𝐹‘𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 < (𝐹‘𝑦)))) |
| 52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹‘𝑦) ∈ (𝑚(,)+∞) ↔ ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 < (𝐹‘𝑦)))) |
| 53 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
| 54 | | itg2cn.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
| 55 | 54 | ffnd 6737 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn ℝ) |
| 56 | 55 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → 𝐹 Fn ℝ) |
| 57 | | elpreima 7078 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn ℝ → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑦) ∈ (𝑚(,)+∞)))) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ (𝑦 ∈ ℝ ∧ (𝐹‘𝑦) ∈ (𝑚(,)+∞)))) |
| 59 | 53, 58 | mpbirand 707 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ (𝐹‘𝑦) ∈ (𝑚(,)+∞))) |
| 60 | | rge0ssre 13496 |
. . . . . . . . . . . . . 14
⊢
(0[,)+∞) ⊆ ℝ |
| 61 | | fss 6752 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ) |
| 62 | 54, 60, 61 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
| 63 | 62 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹:ℝ⟶ℝ) |
| 64 | 63 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) |
| 65 | 64 | biantrurd 532 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑚 < (𝐹‘𝑦) ↔ ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 < (𝐹‘𝑦)))) |
| 66 | 52, 59, 65 | 3bitr4d 311 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ 𝑚 < (𝐹‘𝑦))) |
| 67 | 66 | notbid 318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)) ↔ ¬ 𝑚 < (𝐹‘𝑦))) |
| 68 | | eldif 3961 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ (𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)))) |
| 69 | 68 | baib 535 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)))) |
| 70 | 69 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ ¬ 𝑦 ∈ (◡𝐹 “ (𝑚(,)+∞)))) |
| 71 | 64, 49 | lenltd 11407 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝐹‘𝑦) ≤ 𝑚 ↔ ¬ 𝑚 < (𝐹‘𝑦))) |
| 72 | 67, 70, 71 | 3bitr4d 311 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↔ (𝐹‘𝑦) ≤ 𝑚)) |
| 73 | 72 | ifbid 4549 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) = if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0)) |
| 74 | 73 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) = (𝑦 ∈ ℝ ↦ if((𝐹‘𝑦) ≤ 𝑚, (𝐹‘𝑦), 0))) |
| 75 | 46, 47, 74 | 3eqtr4a 2803 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0))) |
| 76 | | difss 4136 |
. . . . . 6
⊢ (ℝ
∖ (◡𝐹 “ (𝑚(,)+∞))) ⊆
ℝ |
| 77 | 76 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (ℝ ∖
(◡𝐹 “ (𝑚(,)+∞))) ⊆
ℝ) |
| 78 | | rembl 25575 |
. . . . . 6
⊢ ℝ
∈ dom vol |
| 79 | 78 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ℝ ∈ dom
vol) |
| 80 | | fvex 6919 |
. . . . . . 7
⊢ (𝐹‘𝑦) ∈ V |
| 81 | 80, 2 | ifex 4576 |
. . . . . 6
⊢ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) ∈ V |
| 82 | 81 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) ∈ V) |
| 83 | | eldifn 4132 |
. . . . . . 7
⊢ (𝑦 ∈ (ℝ ∖
(ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) → ¬ 𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) |
| 84 | 83 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖
(◡𝐹 “ (𝑚(,)+∞))))) → ¬ 𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) |
| 85 | 84 | iffalsed 4536 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ (ℝ ∖ (ℝ ∖
(◡𝐹 “ (𝑚(,)+∞))))) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) = 0) |
| 86 | | iftrue 4531 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) → if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0) = (𝐹‘𝑦)) |
| 87 | 86 | mpteq2ia 5245 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) = (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ (𝐹‘𝑦)) |
| 88 | | resmpt 6055 |
. . . . . . . . 9
⊢ ((ℝ
∖ (◡𝐹 “ (𝑚(,)+∞))) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ (𝐹‘𝑦))) |
| 89 | 76, 88 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) = (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ (𝐹‘𝑦)) |
| 90 | 87, 89 | eqtr4i 2768 |
. . . . . . 7
⊢ (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) = ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) |
| 91 | 54 | feqmptd 6977 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦))) |
| 92 | | itg2cn.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ MblFn) |
| 93 | 91, 92 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn) |
| 94 | | mbfima 25665 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) →
(◡𝐹 “ (𝑚(,)+∞)) ∈ dom
vol) |
| 95 | 92, 62, 94 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ (𝑚(,)+∞)) ∈ dom
vol) |
| 96 | | cmmbl 25569 |
. . . . . . . . 9
⊢ ((◡𝐹 “ (𝑚(,)+∞)) ∈ dom vol → (ℝ
∖ (◡𝐹 “ (𝑚(,)+∞))) ∈ dom
vol) |
| 97 | 95, 96 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ∈ dom
vol) |
| 98 | | mbfres 25679 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ∈ MblFn ∧ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ∈ dom vol) → ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) ∈
MblFn) |
| 99 | 93, 97, 98 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝐹‘𝑦)) ↾ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞)))) ∈
MblFn) |
| 100 | 90, 99 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) ∈ MblFn) |
| 101 | 100 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))) ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) ∈ MblFn) |
| 102 | 77, 79, 82, 85, 101 | mbfss 25681 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (ℝ ∖ (◡𝐹 “ (𝑚(,)+∞))), (𝐹‘𝑦), 0)) ∈ MblFn) |
| 103 | 75, 102 | eqeltrd 2841 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) ∈ MblFn) |
| 104 | 54 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
| 105 | | 0e0icopnf 13498 |
. . . . . 6
⊢ 0 ∈
(0[,)+∞) |
| 106 | | ifcl 4571 |
. . . . . 6
⊢ (((𝐹‘𝑥) ∈ (0[,)+∞) ∧ 0 ∈
(0[,)+∞)) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ (0[,)+∞)) |
| 107 | 104, 105,
106 | sylancl 586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ (0[,)+∞)) |
| 108 | 107 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ (0[,)+∞)) |
| 109 | 47, 108 | fmpt3d 7136 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚):ℝ⟶(0[,)+∞)) |
| 110 | | elrege0 13494 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
| 111 | 104, 110 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
| 112 | 111 | simpld 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
| 113 | 112 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
| 114 | 113 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ∈ ℝ) |
| 115 | 114 | leidd 11829 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ≤ (𝐹‘𝑥)) |
| 116 | | iftrue 4531 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ≤ 𝑚 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
| 117 | 116 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
| 118 | 48 | ad3antlr 731 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → 𝑚 ∈ ℝ) |
| 119 | | peano2re 11434 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℝ → (𝑚 + 1) ∈
ℝ) |
| 120 | 118, 119 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝑚 + 1) ∈ ℝ) |
| 121 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ≤ 𝑚) |
| 122 | 118 | lep1d 12199 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → 𝑚 ≤ (𝑚 + 1)) |
| 123 | 114, 118,
120, 121, 122 | letrd 11418 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → (𝐹‘𝑥) ≤ (𝑚 + 1)) |
| 124 | 123 | iftrued 4533 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
| 125 | 115, 117,
124 | 3brtr4d 5175 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
| 126 | | iffalse 4534 |
. . . . . . . . 9
⊢ (¬
(𝐹‘𝑥) ≤ 𝑚 → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = 0) |
| 127 | 126 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = 0) |
| 128 | 111 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥)) |
| 129 | | 0le0 12367 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
| 130 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑥) = if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
| 131 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (0 =
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) → (0 ≤ 0 ↔ 0 ≤
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
| 132 | 130, 131 | ifboth 4565 |
. . . . . . . . . . 11
⊢ ((0 ≤
(𝐹‘𝑥) ∧ 0 ≤ 0) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
| 133 | 128, 129,
132 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
| 134 | 133 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
| 135 | 134 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹‘𝑥) ≤ 𝑚) → 0 ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
| 136 | 127, 135 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐹‘𝑥) ≤ 𝑚) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
| 137 | 125, 136 | pm2.61dan 813 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
| 138 | 137 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
| 139 | 1, 2 | ifex 4576 |
. . . . . . 7
⊢ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) ∈ V |
| 140 | 139 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0) ∈ V) |
| 141 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
| 142 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
| 143 | 79, 108, 140, 141, 142 | ofrfval2 7718 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
| 144 | 138, 143 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
| 145 | | peano2nn 12278 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℕ) |
| 146 | 145 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ) |
| 147 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑛 = (𝑚 + 1) → ((𝐹‘𝑥) ≤ 𝑛 ↔ (𝐹‘𝑥) ≤ (𝑚 + 1))) |
| 148 | 147 | ifbid 4549 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) |
| 149 | 148 | mpteq2dv 5244 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
| 150 | 32 | mptex 7243 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0)) ∈ V |
| 151 | 149, 31, 150 | fvmpt 7016 |
. . . . 5
⊢ ((𝑚 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
| 152 | 146, 151 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘(𝑚 + 1)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ (𝑚 + 1), (𝐹‘𝑥), 0))) |
| 153 | 144, 47, 152 | 3brtr4d 5175 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) ∘r ≤ ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘(𝑚 + 1))) |
| 154 | 62 | ffvelcdmda 7104 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) |
| 155 | 34 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))) |
| 156 | 155 | fveq1d 6908 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
| 157 | 112 | leidd 11829 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ (𝐹‘𝑥)) |
| 158 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑥) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))) |
| 159 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢ (0 =
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))) |
| 160 | 158, 159 | ifboth 4565 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
| 161 | 157, 128,
160 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
| 162 | 161 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
| 163 | 162 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
| 164 | 32 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ℝ ∈
V) |
| 165 | 1, 2 | ifex 4576 |
. . . . . . . . . . . 12
⊢ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ V |
| 166 | 165 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ∈ V) |
| 167 | 54 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
| 168 | 167 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
| 169 | 164, 166,
113, 141, 168 | ofrfval2 7718 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))) |
| 170 | 163, 169 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘r ≤ 𝐹) |
| 171 | 166 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)):ℝ⟶V) |
| 172 | 171 | ffnd 6737 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) Fn ℝ) |
| 173 | 55 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹 Fn ℝ) |
| 174 | | inidm 4227 |
. . . . . . . . . 10
⊢ (ℝ
∩ ℝ) = ℝ |
| 175 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) = ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦)) |
| 176 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
| 177 | 172, 173,
164, 164, 174, 175, 176 | ofrfval 7707 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) ∘r ≤ 𝐹 ↔ ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦))) |
| 178 | 170, 177 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑦 ∈ ℝ ((𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦)) |
| 179 | 178 | r19.21bi 3251 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦)) |
| 180 | 179 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0))‘𝑦) ≤ (𝐹‘𝑦)) |
| 181 | 156, 180 | eqbrtrd 5165 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦)) |
| 182 | 181 | ralrimiva 3146 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦)) |
| 183 | | brralrspcev 5203 |
. . . 4
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ (𝐹‘𝑦)) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧) |
| 184 | 154, 182,
183 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)‘𝑦) ≤ 𝑧) |
| 185 | 28 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
| 186 | 185 | cbvmptv 5255 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = (𝑚 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
| 187 | 34 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ →
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚)) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
| 188 | 187 | mpteq2ia 5245 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))) = (𝑚 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)))) |
| 189 | 186, 188 | eqtr4i 2768 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = (𝑚 ∈ ℕ ↦
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))) |
| 190 | 189 | rneqi 5948 |
. . . 4
⊢ ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))) = ran (𝑚 ∈ ℕ ↦
(∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))) |
| 191 | 190 | supeq1i 9487 |
. . 3
⊢ sup(ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) =
sup(ran (𝑚 ∈ ℕ
↦ (∫2‘((𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))‘𝑚))), ℝ*, <
) |
| 192 | 42, 103, 109, 153, 184, 191 | itg2mono 25788 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ))) = sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, <
)) |
| 193 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) |
| 194 | 27, 193, 165 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
| 195 | 194 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
| 196 | 161 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)) |
| 197 | 195, 196 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥)) |
| 198 | 197 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥)) |
| 199 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ V) |
| 200 | 199 | fmpttd 7135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)):ℕ⟶V) |
| 201 | 200 | ffnd 6737 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ) |
| 202 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑤 = ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) → (𝑤 ≤ (𝐹‘𝑥) ↔ ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥))) |
| 203 | 202 | ralrn 7108 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥))) |
| 204 | 201, 203 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥) ↔ ∀𝑚 ∈ ℕ ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ≤ (𝐹‘𝑥))) |
| 205 | 198, 204 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥)) |
| 206 | 112 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑥) ∈ ℝ) |
| 207 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 208 | | ifcl 4571 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ ℝ) |
| 209 | 206, 207,
208 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℕ) → if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0) ∈ ℝ) |
| 210 | 209 | fmpttd 7135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥),
0)):ℕ⟶ℝ) |
| 211 | 210 | frnd 6744 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ) |
| 212 | | 1nn 12277 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
| 213 | 193, 209 | dmmptd 6713 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ℕ) |
| 214 | 212, 213 | eleqtrrid 2848 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ dom (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
| 215 | | n0i 4340 |
. . . . . . . . . 10
⊢ (1 ∈
dom (𝑛 ∈ ℕ
↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) → ¬ dom (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅) |
| 216 | | dm0rn0 5935 |
. . . . . . . . . . 11
⊢ (dom
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅) |
| 217 | 216 | necon3bbii 2988 |
. . . . . . . . . 10
⊢ (¬
dom (𝑛 ∈ ℕ
↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) = ∅ ↔ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅) |
| 218 | 215, 217 | sylib 218 |
. . . . . . . . 9
⊢ (1 ∈
dom (𝑛 ∈ ℕ
↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) → ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅) |
| 219 | 214, 218 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅) |
| 220 | | brralrspcev 5203 |
. . . . . . . . 9
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) |
| 221 | 112, 205,
220 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) |
| 222 | | suprleub 12234 |
. . . . . . . 8
⊢ (((ran
(𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ⊆ ℝ ∧ ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ 𝑧) ∧ (𝐹‘𝑥) ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥))) |
| 223 | 211, 219,
221, 112, 222 | syl31anc 1375 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥) ↔ ∀𝑤 ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))𝑤 ≤ (𝐹‘𝑥))) |
| 224 | 205, 223 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥)) |
| 225 | | arch 12523 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ ℝ → ∃𝑚 ∈ ℕ (𝐹‘𝑥) < 𝑚) |
| 226 | 112, 225 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑚 ∈ ℕ (𝐹‘𝑥) < 𝑚) |
| 227 | 194 | ad2antrl 728 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0)) |
| 228 | | ltle 11349 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝐹‘𝑥) < 𝑚 → (𝐹‘𝑥) ≤ 𝑚)) |
| 229 | 112, 48, 228 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℕ) → ((𝐹‘𝑥) < 𝑚 → (𝐹‘𝑥) ≤ 𝑚)) |
| 230 | 229 | impr 454 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → (𝐹‘𝑥) ≤ 𝑚) |
| 231 | 230 | iftrued 4533 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → if((𝐹‘𝑥) ≤ 𝑚, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
| 232 | 227, 231 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) = (𝐹‘𝑥)) |
| 233 | 201 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ) |
| 234 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → 𝑚 ∈ ℕ) |
| 235 | | fnfvelrn 7100 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)) Fn ℕ ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
| 236 | 233, 234,
235 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → ((𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))‘𝑚) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
| 237 | 232, 236 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑚 ∈ ℕ ∧ (𝐹‘𝑥) < 𝑚)) → (𝐹‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
| 238 | 226, 237 | rexlimddv 3161 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0))) |
| 239 | 211, 219,
221, 238 | suprubd 12230 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) |
| 240 | 211, 219,
221 | suprcld 12231 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ∈
ℝ) |
| 241 | 240, 112 | letri3d 11403 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) = (𝐹‘𝑥) ↔ (sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) ≤ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ≤ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )))) |
| 242 | 224, 239,
241 | mpbir2and 713 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ) = (𝐹‘𝑥)) |
| 243 | 242 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
| 244 | 243, 167 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦
if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < )) = 𝐹) |
| 245 | 244 | fveq2d 6910 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)), ℝ, < ))) =
(∫2‘𝐹)) |
| 246 | 192, 245 | eqtr3d 2779 |
1
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝑥
∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) =
(∫2‘𝐹)) |