Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  iblabsnclem Structured version   Visualization version   GIF version

Theorem iblabsnclem 33786
Description: Lemma for iblabsnc 33787; cf. iblabslem 23793. (Contributed by Brendan Leahy, 7-Nov-2017.)
Hypotheses
Ref Expression
iblabsnc.1 ((𝜑𝑥𝐴) → 𝐵𝑉)
iblabsnc.2 (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)
iblabsnclem.1 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐹𝐵)), 0))
iblabsnclem.2 (𝜑 → (𝑥𝐴 ↦ (𝐹𝐵)) ∈ 𝐿1)
iblabsnclem.3 ((𝜑𝑥𝐴) → (𝐹𝐵) ∈ ℝ)
Assertion
Ref Expression
iblabsnclem (𝜑 → (𝐺 ∈ MblFn ∧ (∫2𝐺) ∈ ℝ))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝐺(𝑥)   𝑉(𝑥)

Proof of Theorem iblabsnclem
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 iblabsnclem.1 . . 3 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐹𝐵)), 0))
2 iblabsnclem.2 . . . . . . . 8 (𝜑 → (𝑥𝐴 ↦ (𝐹𝐵)) ∈ 𝐿1)
3 iblabsnclem.3 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐹𝐵) ∈ ℝ)
43iblrelem 23756 . . . . . . . 8 (𝜑 → ((𝑥𝐴 ↦ (𝐹𝐵)) ∈ 𝐿1 ↔ ((𝑥𝐴 ↦ (𝐹𝐵)) ∈ MblFn ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0))) ∈ ℝ)))
52, 4mpbid 222 . . . . . . 7 (𝜑 → ((𝑥𝐴 ↦ (𝐹𝐵)) ∈ MblFn ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0))) ∈ ℝ))
65simp1d 1137 . . . . . 6 (𝜑 → (𝑥𝐴 ↦ (𝐹𝐵)) ∈ MblFn)
76, 3mbfdm2 23604 . . . . 5 (𝜑𝐴 ∈ dom vol)
8 mblss 23499 . . . . 5 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
97, 8syl 17 . . . 4 (𝜑𝐴 ⊆ ℝ)
10 rembl 23508 . . . . 5 ℝ ∈ dom vol
1110a1i 11 . . . 4 (𝜑 → ℝ ∈ dom vol)
123recnd 10260 . . . . . 6 ((𝜑𝑥𝐴) → (𝐹𝐵) ∈ ℂ)
1312abscld 14374 . . . . 5 ((𝜑𝑥𝐴) → (abs‘(𝐹𝐵)) ∈ ℝ)
14 0re 10232 . . . . 5 0 ∈ ℝ
15 ifcl 4274 . . . . 5 (((abs‘(𝐹𝐵)) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥𝐴, (abs‘(𝐹𝐵)), 0) ∈ ℝ)
1613, 14, 15sylancl 697 . . . 4 ((𝜑𝑥𝐴) → if(𝑥𝐴, (abs‘(𝐹𝐵)), 0) ∈ ℝ)
17 eldifn 3876 . . . . . 6 (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥𝐴)
1817adantl 473 . . . . 5 ((𝜑𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥𝐴)
19 iffalse 4239 . . . . 5 𝑥𝐴 → if(𝑥𝐴, (abs‘(𝐹𝐵)), 0) = 0)
2018, 19syl 17 . . . 4 ((𝜑𝑥 ∈ (ℝ ∖ 𝐴)) → if(𝑥𝐴, (abs‘(𝐹𝐵)), 0) = 0)
21 iftrue 4236 . . . . . 6 (𝑥𝐴 → if(𝑥𝐴, (abs‘(𝐹𝐵)), 0) = (abs‘(𝐹𝐵)))
2221mpteq2ia 4892 . . . . 5 (𝑥𝐴 ↦ if(𝑥𝐴, (abs‘(𝐹𝐵)), 0)) = (𝑥𝐴 ↦ (abs‘(𝐹𝐵)))
23 eqid 2760 . . . . . . 7 (𝑥𝐴 ↦ (abs‘(𝐹𝐵))) = (𝑥𝐴 ↦ (abs‘(𝐹𝐵)))
2413, 23fmptd 6548 . . . . . 6 (𝜑 → (𝑥𝐴 ↦ (abs‘(𝐹𝐵))):𝐴⟶ℝ)
2513adantlr 753 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → (abs‘(𝐹𝐵)) ∈ ℝ)
2625biantrurd 530 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → (𝑦 < (abs‘(𝐹𝐵)) ↔ ((abs‘(𝐹𝐵)) ∈ ℝ ∧ 𝑦 < (abs‘(𝐹𝐵)))))
273adantlr 753 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → (𝐹𝐵) ∈ ℝ)
28 simplr 809 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → 𝑦 ∈ ℝ)
2927, 28absled 14368 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((abs‘(𝐹𝐵)) ≤ 𝑦 ↔ (-𝑦 ≤ (𝐹𝐵) ∧ (𝐹𝐵) ≤ 𝑦)))
3029notbid 307 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → (¬ (abs‘(𝐹𝐵)) ≤ 𝑦 ↔ ¬ (-𝑦 ≤ (𝐹𝐵) ∧ (𝐹𝐵) ≤ 𝑦)))
3128, 25ltnled 10376 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → (𝑦 < (abs‘(𝐹𝐵)) ↔ ¬ (abs‘(𝐹𝐵)) ≤ 𝑦))
32 renegcl 10536 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
3332rexrd 10281 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ → -𝑦 ∈ ℝ*)
3433ad2antlr 765 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → -𝑦 ∈ ℝ*)
35 elioomnf 12461 . . . . . . . . . . . . . . 15 (-𝑦 ∈ ℝ* → ((𝐹𝐵) ∈ (-∞(,)-𝑦) ↔ ((𝐹𝐵) ∈ ℝ ∧ (𝐹𝐵) < -𝑦)))
3634, 35syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((𝐹𝐵) ∈ (-∞(,)-𝑦) ↔ ((𝐹𝐵) ∈ ℝ ∧ (𝐹𝐵) < -𝑦)))
3727biantrurd 530 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((𝐹𝐵) < -𝑦 ↔ ((𝐹𝐵) ∈ ℝ ∧ (𝐹𝐵) < -𝑦)))
3828renegcld 10649 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → -𝑦 ∈ ℝ)
3927, 38ltnled 10376 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((𝐹𝐵) < -𝑦 ↔ ¬ -𝑦 ≤ (𝐹𝐵)))
4036, 37, 393bitr2d 296 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((𝐹𝐵) ∈ (-∞(,)-𝑦) ↔ ¬ -𝑦 ≤ (𝐹𝐵)))
41 rexr 10277 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ → 𝑦 ∈ ℝ*)
4241ad2antlr 765 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → 𝑦 ∈ ℝ*)
43 elioopnf 12460 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ* → ((𝐹𝐵) ∈ (𝑦(,)+∞) ↔ ((𝐹𝐵) ∈ ℝ ∧ 𝑦 < (𝐹𝐵))))
4442, 43syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((𝐹𝐵) ∈ (𝑦(,)+∞) ↔ ((𝐹𝐵) ∈ ℝ ∧ 𝑦 < (𝐹𝐵))))
4527biantrurd 530 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → (𝑦 < (𝐹𝐵) ↔ ((𝐹𝐵) ∈ ℝ ∧ 𝑦 < (𝐹𝐵))))
4628, 27ltnled 10376 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → (𝑦 < (𝐹𝐵) ↔ ¬ (𝐹𝐵) ≤ 𝑦))
4744, 45, 463bitr2d 296 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((𝐹𝐵) ∈ (𝑦(,)+∞) ↔ ¬ (𝐹𝐵) ≤ 𝑦))
4840, 47orbi12d 748 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → (((𝐹𝐵) ∈ (-∞(,)-𝑦) ∨ (𝐹𝐵) ∈ (𝑦(,)+∞)) ↔ (¬ -𝑦 ≤ (𝐹𝐵) ∨ ¬ (𝐹𝐵) ≤ 𝑦)))
49 ianor 510 . . . . . . . . . . . 12 (¬ (-𝑦 ≤ (𝐹𝐵) ∧ (𝐹𝐵) ≤ 𝑦) ↔ (¬ -𝑦 ≤ (𝐹𝐵) ∨ ¬ (𝐹𝐵) ≤ 𝑦))
5048, 49syl6bbr 278 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → (((𝐹𝐵) ∈ (-∞(,)-𝑦) ∨ (𝐹𝐵) ∈ (𝑦(,)+∞)) ↔ ¬ (-𝑦 ≤ (𝐹𝐵) ∧ (𝐹𝐵) ≤ 𝑦)))
5130, 31, 503bitr4rd 301 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → (((𝐹𝐵) ∈ (-∞(,)-𝑦) ∨ (𝐹𝐵) ∈ (𝑦(,)+∞)) ↔ 𝑦 < (abs‘(𝐹𝐵))))
52 elioopnf 12460 . . . . . . . . . . 11 (𝑦 ∈ ℝ* → ((abs‘(𝐹𝐵)) ∈ (𝑦(,)+∞) ↔ ((abs‘(𝐹𝐵)) ∈ ℝ ∧ 𝑦 < (abs‘(𝐹𝐵)))))
5342, 52syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((abs‘(𝐹𝐵)) ∈ (𝑦(,)+∞) ↔ ((abs‘(𝐹𝐵)) ∈ ℝ ∧ 𝑦 < (abs‘(𝐹𝐵)))))
5426, 51, 533bitr4rd 301 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((abs‘(𝐹𝐵)) ∈ (𝑦(,)+∞) ↔ ((𝐹𝐵) ∈ (-∞(,)-𝑦) ∨ (𝐹𝐵) ∈ (𝑦(,)+∞))))
5554rabbidva 3328 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → {𝑥𝐴 ∣ (abs‘(𝐹𝐵)) ∈ (𝑦(,)+∞)} = {𝑥𝐴 ∣ ((𝐹𝐵) ∈ (-∞(,)-𝑦) ∨ (𝐹𝐵) ∈ (𝑦(,)+∞))})
5623mptpreima 5789 . . . . . . . 8 ((𝑥𝐴 ↦ (abs‘(𝐹𝐵))) “ (𝑦(,)+∞)) = {𝑥𝐴 ∣ (abs‘(𝐹𝐵)) ∈ (𝑦(,)+∞)}
57 eqid 2760 . . . . . . . . . . 11 (𝑥𝐴 ↦ (𝐹𝐵)) = (𝑥𝐴 ↦ (𝐹𝐵))
5857mptpreima 5789 . . . . . . . . . 10 ((𝑥𝐴 ↦ (𝐹𝐵)) “ (-∞(,)-𝑦)) = {𝑥𝐴 ∣ (𝐹𝐵) ∈ (-∞(,)-𝑦)}
5957mptpreima 5789 . . . . . . . . . 10 ((𝑥𝐴 ↦ (𝐹𝐵)) “ (𝑦(,)+∞)) = {𝑥𝐴 ∣ (𝐹𝐵) ∈ (𝑦(,)+∞)}
6058, 59uneq12i 3908 . . . . . . . . 9 (((𝑥𝐴 ↦ (𝐹𝐵)) “ (-∞(,)-𝑦)) ∪ ((𝑥𝐴 ↦ (𝐹𝐵)) “ (𝑦(,)+∞))) = ({𝑥𝐴 ∣ (𝐹𝐵) ∈ (-∞(,)-𝑦)} ∪ {𝑥𝐴 ∣ (𝐹𝐵) ∈ (𝑦(,)+∞)})
61 unrab 4041 . . . . . . . . 9 ({𝑥𝐴 ∣ (𝐹𝐵) ∈ (-∞(,)-𝑦)} ∪ {𝑥𝐴 ∣ (𝐹𝐵) ∈ (𝑦(,)+∞)}) = {𝑥𝐴 ∣ ((𝐹𝐵) ∈ (-∞(,)-𝑦) ∨ (𝐹𝐵) ∈ (𝑦(,)+∞))}
6260, 61eqtri 2782 . . . . . . . 8 (((𝑥𝐴 ↦ (𝐹𝐵)) “ (-∞(,)-𝑦)) ∪ ((𝑥𝐴 ↦ (𝐹𝐵)) “ (𝑦(,)+∞))) = {𝑥𝐴 ∣ ((𝐹𝐵) ∈ (-∞(,)-𝑦) ∨ (𝐹𝐵) ∈ (𝑦(,)+∞))}
6355, 56, 623eqtr4g 2819 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑥𝐴 ↦ (abs‘(𝐹𝐵))) “ (𝑦(,)+∞)) = (((𝑥𝐴 ↦ (𝐹𝐵)) “ (-∞(,)-𝑦)) ∪ ((𝑥𝐴 ↦ (𝐹𝐵)) “ (𝑦(,)+∞))))
64 iblmbf 23733 . . . . . . . . . 10 ((𝑥𝐴 ↦ (𝐹𝐵)) ∈ 𝐿1 → (𝑥𝐴 ↦ (𝐹𝐵)) ∈ MblFn)
652, 64syl 17 . . . . . . . . 9 (𝜑 → (𝑥𝐴 ↦ (𝐹𝐵)) ∈ MblFn)
663, 57fmptd 6548 . . . . . . . . 9 (𝜑 → (𝑥𝐴 ↦ (𝐹𝐵)):𝐴⟶ℝ)
67 mbfima 23598 . . . . . . . . . 10 (((𝑥𝐴 ↦ (𝐹𝐵)) ∈ MblFn ∧ (𝑥𝐴 ↦ (𝐹𝐵)):𝐴⟶ℝ) → ((𝑥𝐴 ↦ (𝐹𝐵)) “ (-∞(,)-𝑦)) ∈ dom vol)
68 mbfima 23598 . . . . . . . . . 10 (((𝑥𝐴 ↦ (𝐹𝐵)) ∈ MblFn ∧ (𝑥𝐴 ↦ (𝐹𝐵)):𝐴⟶ℝ) → ((𝑥𝐴 ↦ (𝐹𝐵)) “ (𝑦(,)+∞)) ∈ dom vol)
69 unmbl 23505 . . . . . . . . . 10 ((((𝑥𝐴 ↦ (𝐹𝐵)) “ (-∞(,)-𝑦)) ∈ dom vol ∧ ((𝑥𝐴 ↦ (𝐹𝐵)) “ (𝑦(,)+∞)) ∈ dom vol) → (((𝑥𝐴 ↦ (𝐹𝐵)) “ (-∞(,)-𝑦)) ∪ ((𝑥𝐴 ↦ (𝐹𝐵)) “ (𝑦(,)+∞))) ∈ dom vol)
7067, 68, 69syl2anc 696 . . . . . . . . 9 (((𝑥𝐴 ↦ (𝐹𝐵)) ∈ MblFn ∧ (𝑥𝐴 ↦ (𝐹𝐵)):𝐴⟶ℝ) → (((𝑥𝐴 ↦ (𝐹𝐵)) “ (-∞(,)-𝑦)) ∪ ((𝑥𝐴 ↦ (𝐹𝐵)) “ (𝑦(,)+∞))) ∈ dom vol)
7165, 66, 70syl2anc 696 . . . . . . . 8 (𝜑 → (((𝑥𝐴 ↦ (𝐹𝐵)) “ (-∞(,)-𝑦)) ∪ ((𝑥𝐴 ↦ (𝐹𝐵)) “ (𝑦(,)+∞))) ∈ dom vol)
7271adantr 472 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → (((𝑥𝐴 ↦ (𝐹𝐵)) “ (-∞(,)-𝑦)) ∪ ((𝑥𝐴 ↦ (𝐹𝐵)) “ (𝑦(,)+∞))) ∈ dom vol)
7363, 72eqeltrd 2839 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → ((𝑥𝐴 ↦ (abs‘(𝐹𝐵))) “ (𝑦(,)+∞)) ∈ dom vol)
74 elioomnf 12461 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ* → ((abs‘(𝐹𝐵)) ∈ (-∞(,)𝑦) ↔ ((abs‘(𝐹𝐵)) ∈ ℝ ∧ (abs‘(𝐹𝐵)) < 𝑦)))
7542, 74syl 17 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((abs‘(𝐹𝐵)) ∈ (-∞(,)𝑦) ↔ ((abs‘(𝐹𝐵)) ∈ ℝ ∧ (abs‘(𝐹𝐵)) < 𝑦)))
7625biantrurd 530 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((abs‘(𝐹𝐵)) < 𝑦 ↔ ((abs‘(𝐹𝐵)) ∈ ℝ ∧ (abs‘(𝐹𝐵)) < 𝑦)))
7727, 28absltd 14367 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((abs‘(𝐹𝐵)) < 𝑦 ↔ (-𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦)))
7875, 76, 773bitr2d 296 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((abs‘(𝐹𝐵)) ∈ (-∞(,)𝑦) ↔ (-𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦)))
7927biantrurd 530 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((-𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦) ↔ ((𝐹𝐵) ∈ ℝ ∧ (-𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦))))
8078, 79bitrd 268 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((abs‘(𝐹𝐵)) ∈ (-∞(,)𝑦) ↔ ((𝐹𝐵) ∈ ℝ ∧ (-𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦))))
81 3anass 1081 . . . . . . . . . . 11 (((𝐹𝐵) ∈ ℝ ∧ -𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦) ↔ ((𝐹𝐵) ∈ ℝ ∧ (-𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦)))
8280, 81syl6bbr 278 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((abs‘(𝐹𝐵)) ∈ (-∞(,)𝑦) ↔ ((𝐹𝐵) ∈ ℝ ∧ -𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦)))
83 elioo2 12409 . . . . . . . . . . . 12 ((-𝑦 ∈ ℝ*𝑦 ∈ ℝ*) → ((𝐹𝐵) ∈ (-𝑦(,)𝑦) ↔ ((𝐹𝐵) ∈ ℝ ∧ -𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦)))
8433, 41, 83syl2anc 696 . . . . . . . . . . 11 (𝑦 ∈ ℝ → ((𝐹𝐵) ∈ (-𝑦(,)𝑦) ↔ ((𝐹𝐵) ∈ ℝ ∧ -𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦)))
8584ad2antlr 765 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((𝐹𝐵) ∈ (-𝑦(,)𝑦) ↔ ((𝐹𝐵) ∈ ℝ ∧ -𝑦 < (𝐹𝐵) ∧ (𝐹𝐵) < 𝑦)))
8682, 85bitr4d 271 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐴) → ((abs‘(𝐹𝐵)) ∈ (-∞(,)𝑦) ↔ (𝐹𝐵) ∈ (-𝑦(,)𝑦)))
8786rabbidva 3328 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → {𝑥𝐴 ∣ (abs‘(𝐹𝐵)) ∈ (-∞(,)𝑦)} = {𝑥𝐴 ∣ (𝐹𝐵) ∈ (-𝑦(,)𝑦)})
8823mptpreima 5789 . . . . . . . 8 ((𝑥𝐴 ↦ (abs‘(𝐹𝐵))) “ (-∞(,)𝑦)) = {𝑥𝐴 ∣ (abs‘(𝐹𝐵)) ∈ (-∞(,)𝑦)}
8957mptpreima 5789 . . . . . . . 8 ((𝑥𝐴 ↦ (𝐹𝐵)) “ (-𝑦(,)𝑦)) = {𝑥𝐴 ∣ (𝐹𝐵) ∈ (-𝑦(,)𝑦)}
9087, 88, 893eqtr4g 2819 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑥𝐴 ↦ (abs‘(𝐹𝐵))) “ (-∞(,)𝑦)) = ((𝑥𝐴 ↦ (𝐹𝐵)) “ (-𝑦(,)𝑦)))
91 mbfima 23598 . . . . . . . . 9 (((𝑥𝐴 ↦ (𝐹𝐵)) ∈ MblFn ∧ (𝑥𝐴 ↦ (𝐹𝐵)):𝐴⟶ℝ) → ((𝑥𝐴 ↦ (𝐹𝐵)) “ (-𝑦(,)𝑦)) ∈ dom vol)
9265, 66, 91syl2anc 696 . . . . . . . 8 (𝜑 → ((𝑥𝐴 ↦ (𝐹𝐵)) “ (-𝑦(,)𝑦)) ∈ dom vol)
9392adantr 472 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((𝑥𝐴 ↦ (𝐹𝐵)) “ (-𝑦(,)𝑦)) ∈ dom vol)
9490, 93eqeltrd 2839 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → ((𝑥𝐴 ↦ (abs‘(𝐹𝐵))) “ (-∞(,)𝑦)) ∈ dom vol)
9524, 7, 73, 94ismbf2d 23607 . . . . 5 (𝜑 → (𝑥𝐴 ↦ (abs‘(𝐹𝐵))) ∈ MblFn)
9622, 95syl5eqel 2843 . . . 4 (𝜑 → (𝑥𝐴 ↦ if(𝑥𝐴, (abs‘(𝐹𝐵)), 0)) ∈ MblFn)
979, 11, 16, 20, 96mbfss 23612 . . 3 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐹𝐵)), 0)) ∈ MblFn)
981, 97syl5eqel 2843 . 2 (𝜑𝐺 ∈ MblFn)
99 reex 10219 . . . . . . . . 9 ℝ ∈ V
10099a1i 11 . . . . . . . 8 (𝜑 → ℝ ∈ V)
101 ifan 4278 . . . . . . . . . 10 if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0) = if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0)
102 ifcl 4274 . . . . . . . . . . . . 13 (((𝐹𝐵) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0) ∈ ℝ)
1033, 14, 102sylancl 697 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0) ∈ ℝ)
104 max1 12209 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ) → 0 ≤ if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0))
10514, 3, 104sylancr 698 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 0 ≤ if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0))
106 elrege0 12471 . . . . . . . . . . . 12 (if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0)))
107103, 105, 106sylanbrc 701 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0) ∈ (0[,)+∞))
108 0e0icopnf 12475 . . . . . . . . . . . 12 0 ∈ (0[,)+∞)
109108a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,)+∞))
110107, 109ifclda 4264 . . . . . . . . . 10 (𝜑 → if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) ∈ (0[,)+∞))
111101, 110syl5eqel 2843 . . . . . . . . 9 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0) ∈ (0[,)+∞))
112111adantr 472 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0) ∈ (0[,)+∞))
113 ifan 4278 . . . . . . . . . 10 if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0) = if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0)
1143renegcld 10649 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → -(𝐹𝐵) ∈ ℝ)
115 ifcl 4274 . . . . . . . . . . . . 13 ((-(𝐹𝐵) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0) ∈ ℝ)
116114, 14, 115sylancl 697 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0) ∈ ℝ)
117 max1 12209 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ -(𝐹𝐵) ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0))
11814, 114, 117sylancr 698 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 0 ≤ if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0))
119 elrege0 12471 . . . . . . . . . . . 12 (if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0)))
120116, 118, 119sylanbrc 701 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0) ∈ (0[,)+∞))
121120, 109ifclda 4264 . . . . . . . . . 10 (𝜑 → if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0) ∈ (0[,)+∞))
122113, 121syl5eqel 2843 . . . . . . . . 9 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0) ∈ (0[,)+∞))
123122adantr 472 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0) ∈ (0[,)+∞))
124 eqidd 2761 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)))
125 eqidd 2761 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)))
126100, 112, 123, 124, 125offval2 7079 . . . . . . 7 (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0))) = (𝑥 ∈ ℝ ↦ (if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0) + if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0))))
127101, 113oveq12i 6825 . . . . . . . . 9 (if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0) + if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)) = (if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) + if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0))
128 max0add 14249 . . . . . . . . . . . . 13 ((𝐹𝐵) ∈ ℝ → (if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0) + if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0)) = (abs‘(𝐹𝐵)))
1293, 128syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0) + if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0)) = (abs‘(𝐹𝐵)))
130 iftrue 4236 . . . . . . . . . . . . . 14 (𝑥𝐴 → if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) = if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0))
131130adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) = if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0))
132 iftrue 4236 . . . . . . . . . . . . . 14 (𝑥𝐴 → if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0) = if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0))
133132adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0) = if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0))
134131, 133oveq12d 6831 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) + if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0)) = (if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0) + if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0)))
13521adantl 473 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → if(𝑥𝐴, (abs‘(𝐹𝐵)), 0) = (abs‘(𝐹𝐵)))
136129, 134, 1353eqtr4d 2804 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) + if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0)) = if(𝑥𝐴, (abs‘(𝐹𝐵)), 0))
137136ex 449 . . . . . . . . . 10 (𝜑 → (𝑥𝐴 → (if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) + if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0)) = if(𝑥𝐴, (abs‘(𝐹𝐵)), 0)))
138 00id 10403 . . . . . . . . . . 11 (0 + 0) = 0
139 iffalse 4239 . . . . . . . . . . . 12 𝑥𝐴 → if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) = 0)
140 iffalse 4239 . . . . . . . . . . . 12 𝑥𝐴 → if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0) = 0)
141139, 140oveq12d 6831 . . . . . . . . . . 11 𝑥𝐴 → (if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) + if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0)) = (0 + 0))
142138, 141, 193eqtr4a 2820 . . . . . . . . . 10 𝑥𝐴 → (if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) + if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0)) = if(𝑥𝐴, (abs‘(𝐹𝐵)), 0))
143137, 142pm2.61d1 171 . . . . . . . . 9 (𝜑 → (if(𝑥𝐴, if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0), 0) + if(𝑥𝐴, if(0 ≤ -(𝐹𝐵), -(𝐹𝐵), 0), 0)) = if(𝑥𝐴, (abs‘(𝐹𝐵)), 0))
144127, 143syl5eq 2806 . . . . . . . 8 (𝜑 → (if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0) + if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)) = if(𝑥𝐴, (abs‘(𝐹𝐵)), 0))
145144mpteq2dv 4897 . . . . . . 7 (𝜑 → (𝑥 ∈ ℝ ↦ (if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0) + if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐹𝐵)), 0)))
146126, 145eqtrd 2794 . . . . . 6 (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐹𝐵)), 0)))
147146, 1syl6reqr 2813 . . . . 5 (𝜑𝐺 = ((𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0))))
148147fveq2d 6356 . . . 4 (𝜑 → (∫2𝐺) = (∫2‘((𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)))))
149111adantr 472 . . . . . 6 ((𝜑𝑥𝐴) → if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0) ∈ (0[,)+∞))
150101, 139syl5eq 2806 . . . . . . 7 𝑥𝐴 → if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0) = 0)
15118, 150syl 17 . . . . . 6 ((𝜑𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0) = 0)
152 ibar 526 . . . . . . . . 9 (𝑥𝐴 → (0 ≤ (𝐹𝐵) ↔ (𝑥𝐴 ∧ 0 ≤ (𝐹𝐵))))
153152ifbid 4252 . . . . . . . 8 (𝑥𝐴 → if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0) = if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0))
154153mpteq2ia 4892 . . . . . . 7 (𝑥𝐴 ↦ if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0)) = (𝑥𝐴 ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0))
1553, 6mbfpos 23617 . . . . . . 7 (𝜑 → (𝑥𝐴 ↦ if(0 ≤ (𝐹𝐵), (𝐹𝐵), 0)) ∈ MblFn)
156154, 155syl5eqelr 2844 . . . . . 6 (𝜑 → (𝑥𝐴 ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)) ∈ MblFn)
1579, 11, 149, 151, 156mbfss 23612 . . . . 5 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)) ∈ MblFn)
158 eqid 2760 . . . . . 6 (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0))
159112, 158fmptd 6548 . . . . 5 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)):ℝ⟶(0[,)+∞))
1605simp2d 1138 . . . . 5 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0))) ∈ ℝ)
161 eqid 2760 . . . . . 6 (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0))
162123, 161fmptd 6548 . . . . 5 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)):ℝ⟶(0[,)+∞))
1635simp3d 1139 . . . . 5 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0))) ∈ ℝ)
164157, 159, 160, 162, 163itg2addnc 33777 . . . 4 (𝜑 → (∫2‘((𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)))) = ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)))))
165148, 164eqtrd 2794 . . 3 (𝜑 → (∫2𝐺) = ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)))))
166160, 163readdcld 10261 . . 3 (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (𝐹𝐵)), (𝐹𝐵), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ -(𝐹𝐵)), -(𝐹𝐵), 0)))) ∈ ℝ)
167165, 166eqeltrd 2839 . 2 (𝜑 → (∫2𝐺) ∈ ℝ)
16898, 167jca 555 1 (𝜑 → (𝐺 ∈ MblFn ∧ (∫2𝐺) ∈ ℝ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1632  wcel 2139  {crab 3054  Vcvv 3340  cdif 3712  cun 3713  wss 3715  ifcif 4230   class class class wbr 4804  cmpt 4881  ccnv 5265  dom cdm 5266  cima 5269  wf 6045  cfv 6049  (class class class)co 6813  𝑓 cof 7060  cr 10127  0cc0 10128   + caddc 10131  +∞cpnf 10263  -∞cmnf 10264  *cxr 10265   < clt 10266  cle 10267  -cneg 10459  (,)cioo 12368  [,)cico 12370  abscabs 14173  volcvol 23432  MblFncmbf 23582  2citg2 23584  𝐿1cibl 23585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-disj 4773  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-ofr 7063  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fi 8482  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-z 11570  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ioo 12372  df-ico 12374  df-icc 12375  df-fz 12520  df-fzo 12660  df-fl 12787  df-seq 12996  df-exp 13055  df-hash 13312  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-clim 14418  df-sum 14616  df-rest 16285  df-topgen 16306  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-top 20901  df-topon 20918  df-bases 20952  df-cmp 21392  df-ovol 23433  df-vol 23434  df-mbf 23587  df-itg1 23588  df-itg2 23589  df-ibl 23590  df-0p 23636
This theorem is referenced by:  iblabsnc  33787  iblmulc2nc  33788
  Copyright terms: Public domain W3C validator