| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | iblsplit.3 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ) | 
| 2 | 1 | fmpttd 7134 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶):𝑈⟶ℂ) | 
| 3 |  | ssun1 4177 | . . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) | 
| 4 |  | iblsplit.2 | . . . . . 6
⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) | 
| 5 | 3, 4 | sseqtrrid 4026 | . . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑈) | 
| 6 | 5 | resmptd 6057 | . . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | 
| 7 |  | iblsplit.4 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈
𝐿1) | 
| 8 |  | eqidd 2737 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) | 
| 9 |  | eqidd 2737 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 / (i↑𝑦))) = (ℜ‘(𝐶 / (i↑𝑦)))) | 
| 10 | 5 | sseld 3981 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑈)) | 
| 11 | 10 | imdistani 568 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜑 ∧ 𝑥 ∈ 𝑈)) | 
| 12 | 11, 1 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) | 
| 13 | 8, 9, 12 | isibl2 25802 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ))) | 
| 14 | 7, 13 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ)) | 
| 15 | 14 | simpld 494 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) | 
| 16 | 6, 15 | eqeltrd 2840 | . . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐴) ∈ MblFn) | 
| 17 |  | ssun2 4178 | . . . . . 6
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) | 
| 18 | 17, 4 | sseqtrrid 4026 | . . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝑈) | 
| 19 | 18 | resmptd 6057 | . . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | 
| 20 |  | iblsplit.5 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈
𝐿1) | 
| 21 |  | eqidd 2737 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) | 
| 22 |  | eqidd 2737 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑦))) = (ℜ‘(𝐶 / (i↑𝑦)))) | 
| 23 | 18 | sseld 3981 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈)) | 
| 24 | 23 | imdistani 568 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜑 ∧ 𝑥 ∈ 𝑈)) | 
| 25 | 24, 1 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ) | 
| 26 | 21, 22, 25 | isibl2 25802 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ))) | 
| 27 | 20, 26 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ)) | 
| 28 | 27 | simpld 494 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn) | 
| 29 | 19, 28 | eqeltrd 2840 | . . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐵) ∈ MblFn) | 
| 30 | 4 | eqcomd 2742 | . . 3
⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝑈) | 
| 31 | 2, 16, 29, 30 | mbfres2cn 45978 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶) ∈ MblFn) | 
| 32 | 15, 12 | mbfdm2 25673 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ dom vol) | 
| 33 | 32 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝐴 ∈ dom vol) | 
| 34 | 28, 25 | mbfdm2 25673 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ dom vol) | 
| 35 | 34 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝐵 ∈ dom vol) | 
| 36 |  | iblsplit.1 | . . . . . 6
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) | 
| 37 | 36 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (vol*‘(𝐴 ∩ 𝐵)) = 0) | 
| 38 | 4 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝑈 = (𝐴 ∪ 𝐵)) | 
| 39 | 1 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ) | 
| 40 |  | ax-icn 11215 | . . . . . . . . . . . . . 14
⊢ i ∈
ℂ | 
| 41 | 40 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → i ∈
ℂ) | 
| 42 |  | elfznn0 13661 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℕ0) | 
| 43 | 41, 42 | expcld 14187 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...3) →
(i↑𝑘) ∈
ℂ) | 
| 44 | 43 | ad2antlr 727 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (i↑𝑘) ∈ ℂ) | 
| 45 | 40 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → i ∈ ℂ) | 
| 46 |  | ine0 11699 | . . . . . . . . . . . . 13
⊢ i ≠
0 | 
| 47 | 46 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → i ≠ 0) | 
| 48 |  | elfzelz 13565 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℤ) | 
| 49 | 48 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → 𝑘 ∈ ℤ) | 
| 50 | 45, 47, 49 | expne0d 14193 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (i↑𝑘) ≠ 0) | 
| 51 | 39, 44, 50 | divcld 12044 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (𝐶 / (i↑𝑘)) ∈ ℂ) | 
| 52 | 51 | recld 15234 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ) | 
| 53 | 52 | rexrd 11312 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (ℜ‘(𝐶 / (i↑𝑘))) ∈
ℝ*) | 
| 54 | 53 | adantr 480 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → (ℜ‘(𝐶 / (i↑𝑘))) ∈
ℝ*) | 
| 55 |  | simpr 484 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) | 
| 56 |  | pnfge 13173 | . . . . . . . 8
⊢
((ℜ‘(𝐶 /
(i↑𝑘))) ∈
ℝ* → (ℜ‘(𝐶 / (i↑𝑘))) ≤ +∞) | 
| 57 | 54, 56 | syl 17 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → (ℜ‘(𝐶 / (i↑𝑘))) ≤ +∞) | 
| 58 |  | 0xr 11309 | . . . . . . . 8
⊢ 0 ∈
ℝ* | 
| 59 |  | pnfxr 11316 | . . . . . . . 8
⊢ +∞
∈ ℝ* | 
| 60 |  | elicc1 13432 | . . . . . . . 8
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
((ℜ‘(𝐶 /
(i↑𝑘))) ∈
(0[,]+∞) ↔ ((ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ* ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))) ∧
(ℜ‘(𝐶 /
(i↑𝑘))) ≤
+∞))) | 
| 61 | 58, 59, 60 | mp2an 692 | . . . . . . 7
⊢
((ℜ‘(𝐶 /
(i↑𝑘))) ∈
(0[,]+∞) ↔ ((ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ* ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))) ∧
(ℜ‘(𝐶 /
(i↑𝑘))) ≤
+∞)) | 
| 62 | 54, 55, 57, 61 | syl3anbrc 1343 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → (ℜ‘(𝐶 / (i↑𝑘))) ∈ (0[,]+∞)) | 
| 63 |  | 0e0iccpnf 13500 | . . . . . . 7
⊢ 0 ∈
(0[,]+∞) | 
| 64 | 63 | a1i 11 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ ¬ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → 0 ∈
(0[,]+∞)) | 
| 65 | 62, 64 | ifclda 4560 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈
(0[,]+∞)) | 
| 66 |  | eqid 2736 | . . . . 5
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) | 
| 67 |  | eqid 2736 | . . . . 5
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) | 
| 68 |  | ifan 4578 | . . . . . 6
⊢ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝑈, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) | 
| 69 | 68 | mpteq2i 5246 | . . . . 5
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝑈 ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘)))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) | 
| 70 |  | ifan 4578 | . . . . . . . . . 10
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) | 
| 71 | 70 | eqcomi 2745 | . . . . . . . . 9
⊢ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) | 
| 72 | 71 | mpteq2i 5246 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) | 
| 73 | 72 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) | 
| 74 | 73 | fveq2d 6909 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) | 
| 75 |  | eqidd 2737 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) | 
| 76 |  | eqidd 2737 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) | 
| 77 | 75, 76, 12 | isibl2 25802 | . . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ))) | 
| 78 | 7, 77 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)) | 
| 79 | 78 | simprd 495 | . . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) | 
| 80 | 79 | r19.21bi 3250 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) | 
| 81 | 74, 80 | eqeltrd 2840 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0)))
∈ ℝ) | 
| 82 |  | ifan 4578 | . . . . . . . . 9
⊢ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) | 
| 83 | 82 | eqcomi 2745 | . . . . . . . 8
⊢ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) | 
| 84 | 83 | mpteq2i 5246 | . . . . . . 7
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) | 
| 85 | 84 | fveq2i 6908 | . . . . . 6
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) | 
| 86 |  | eqidd 2737 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) | 
| 87 |  | eqidd 2737 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) | 
| 88 | 86, 87, 25 | isibl2 25802 | . . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ))) | 
| 89 | 20, 88 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)) | 
| 90 | 89 | simprd 495 | . . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) | 
| 91 | 90 | r19.21bi 3250 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) | 
| 92 | 85, 91 | eqeltrid 2844 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0)))
∈ ℝ) | 
| 93 | 33, 35, 37, 38, 65, 66, 67, 69, 81, 92 | itg2split 25785 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) = ((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))) +
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0),
0))))) | 
| 94 | 81, 92 | readdcld 11291 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))) +
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0))))
∈ ℝ) | 
| 95 | 93, 94 | eqeltrd 2840 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) | 
| 96 | 95 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) | 
| 97 |  | eqidd 2737 | . . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) | 
| 98 |  | eqidd 2737 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) | 
| 99 | 97, 98, 1 | isibl2 25802 | . 2
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝑈 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ))) | 
| 100 | 31, 96, 99 | mpbir2and 713 | 1
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶) ∈
𝐿1) |