| Step | Hyp | Ref
| Expression |
| 1 | | iblss2.1 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| 2 | | iblss2.2 |
. . 3
⊢ (𝜑 → 𝐵 ∈ dom vol) |
| 3 | | iblss2.3 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
| 4 | | iblss2.4 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) |
| 5 | | iblss2.5 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈
𝐿1) |
| 6 | | iblmbf 25802 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) |
| 7 | 5, 6 | syl 17 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) |
| 8 | 1, 2, 3, 4, 7 | mbfss 25681 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn) |
| 9 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝐴 ⊆ 𝐵) |
| 10 | 9 | sselda 3983 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
| 11 | 10 | iftrued 4533 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
| 12 | | iftrue 4531 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
| 13 | 12 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
| 14 | 11, 13 | eqtr4d 2780 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) |
| 15 | | ifid 4566 |
. . . . . . . . 9
⊢ if(𝑥 ∈ 𝐵, 0, 0) = 0 |
| 16 | | simplll 775 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝜑) |
| 17 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
| 18 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ 𝐴) |
| 19 | 17, 18 | eldifd 3962 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (𝐵 ∖ 𝐴)) |
| 20 | 16, 19, 4 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝐶 = 0) |
| 21 | 20 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝐶 / (i↑𝑘)) = (0 / (i↑𝑘))) |
| 22 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ (0...3)) |
| 23 | | elfzelz 13564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℤ) |
| 24 | | ax-icn 11214 |
. . . . . . . . . . . . . . . . 17
⊢ i ∈
ℂ |
| 25 | | ine0 11698 |
. . . . . . . . . . . . . . . . 17
⊢ i ≠
0 |
| 26 | | expclz 14125 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ∈
ℂ) |
| 27 | | expne0i 14135 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ≠ 0) |
| 28 | 26, 27 | div0d 12042 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (0 / (i↑𝑘)) = 0) |
| 29 | 24, 25, 28 | mp3an12 1453 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℤ → (0 /
(i↑𝑘)) =
0) |
| 30 | 22, 23, 29 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (0 / (i↑𝑘)) = 0) |
| 31 | 21, 30 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝐶 / (i↑𝑘)) = 0) |
| 32 | 31 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘0)) |
| 33 | | re0 15191 |
. . . . . . . . . . . . 13
⊢
(ℜ‘0) = 0 |
| 34 | 32, 33 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑘))) = 0) |
| 35 | 34 | ifeq1d 4545 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), 0, 0)) |
| 36 | | ifid 4566 |
. . . . . . . . . . 11
⊢ if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))), 0, 0) =
0 |
| 37 | 35, 36 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = 0) |
| 38 | 37 | ifeq1da 4557 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if(𝑥 ∈ 𝐵, 0, 0)) |
| 39 | | iffalse 4534 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = 0) |
| 40 | 39 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = 0) |
| 41 | 15, 38, 40 | 3eqtr4a 2803 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) |
| 42 | 14, 41 | pm2.61dan 813 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) |
| 43 | | ifan 4579 |
. . . . . . 7
⊢ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) |
| 44 | | ifan 4579 |
. . . . . . 7
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) |
| 45 | 42, 43, 44 | 3eqtr4g 2802 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
| 46 | 45 | mpteq2dv 5244 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
| 47 | 46 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘)))),
(ℜ‘(𝐶 /
(i↑𝑘))),
0)))) |
| 48 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
| 49 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) |
| 50 | 48, 49, 5, 3 | iblitg 25803 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
| 51 | 23, 50 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
| 52 | 47, 51 | eqeltrd 2841 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
| 53 | 52 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
| 54 | | eqidd 2738 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
| 55 | | eqidd 2738 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) |
| 56 | | elun 4153 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐴))) |
| 57 | | undif2 4477 |
. . . . . . . 8
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
| 58 | | ssequn1 4186 |
. . . . . . . . 9
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) |
| 59 | 1, 58 | sylib 218 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝐵) |
| 60 | 57, 59 | eqtrid 2789 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) |
| 61 | 60 | eleq2d 2827 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐴)) ↔ 𝑥 ∈ 𝐵)) |
| 62 | 56, 61 | bitr3id 285 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ 𝑥 ∈ 𝐵)) |
| 63 | 62 | biimpar 477 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐴))) |
| 64 | 7, 3 | mbfmptcl 25671 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
| 65 | | 0cn 11253 |
. . . . . 6
⊢ 0 ∈
ℂ |
| 66 | 4, 65 | eqeltrdi 2849 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ ℂ) |
| 67 | 64, 66 | jaodan 960 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐴))) → 𝐶 ∈ ℂ) |
| 68 | 63, 67 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ) |
| 69 | 54, 55, 68 | isibl2 25801 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ))) |
| 70 | 8, 53, 69 | mpbir2and 713 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈
𝐿1) |