Step | Hyp | Ref
| Expression |
1 | | iblsplit.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ) |
2 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ 𝑈 ↦ 𝐶) = (𝑥 ∈ 𝑈 ↦ 𝐶) |
3 | 1, 2 | fmptd 6385 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶):𝑈⟶ℂ) |
4 | | ssun1 3776 |
. . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
5 | | iblsplit.2 |
. . . . . 6
⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) |
6 | 4, 5 | syl5sseqr 3654 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
7 | 6 | resmptd 5452 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
8 | | iblsplit.4 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈
𝐿1) |
9 | | eqidd 2623 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) |
10 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 / (i↑𝑦))) = (ℜ‘(𝐶 / (i↑𝑦)))) |
11 | 6 | sseld 3602 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑈)) |
12 | 11 | imdistani 726 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜑 ∧ 𝑥 ∈ 𝑈)) |
13 | 12, 1 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
14 | 9, 10, 13 | isibl2 23533 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ))) |
15 | 8, 14 | mpbid 222 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ)) |
16 | 15 | simpld 475 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) |
17 | 7, 16 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐴) ∈ MblFn) |
18 | | ssun2 3777 |
. . . . . 6
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
19 | 18, 5 | syl5sseqr 3654 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
20 | 19 | resmptd 5452 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
21 | | iblsplit.5 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈
𝐿1) |
22 | | eqidd 2623 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) |
23 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑦))) = (ℜ‘(𝐶 / (i↑𝑦)))) |
24 | 19 | sseld 3602 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈)) |
25 | 24 | imdistani 726 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜑 ∧ 𝑥 ∈ 𝑈)) |
26 | 25, 1 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ) |
27 | 22, 23, 26 | isibl2 23533 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ))) |
28 | 21, 27 | mpbid 222 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ)) |
29 | 28 | simpld 475 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn) |
30 | 20, 29 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐵) ∈ MblFn) |
31 | 5 | eqcomd 2628 |
. . 3
⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝑈) |
32 | 3, 17, 30, 31 | mbfres2cn 40174 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶) ∈ MblFn) |
33 | 16, 13 | mbfdm2 23405 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ dom vol) |
34 | 33 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝐴 ∈ dom vol) |
35 | 29, 26 | mbfdm2 23405 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ dom vol) |
36 | 35 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝐵 ∈ dom vol) |
37 | | iblsplit.1 |
. . . . . 6
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) |
38 | 37 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (vol*‘(𝐴 ∩ 𝐵)) = 0) |
39 | 5 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝑈 = (𝐴 ∪ 𝐵)) |
40 | 1 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ) |
41 | | ax-icn 9995 |
. . . . . . . . . . . . . 14
⊢ i ∈
ℂ |
42 | 41 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → i ∈
ℂ) |
43 | | elfznn0 12433 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℕ0) |
44 | 42, 43 | expcld 13008 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...3) →
(i↑𝑘) ∈
ℂ) |
45 | 44 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (i↑𝑘) ∈ ℂ) |
46 | 41 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → i ∈ ℂ) |
47 | | ine0 10465 |
. . . . . . . . . . . . 13
⊢ i ≠
0 |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → i ≠ 0) |
49 | | elfzelz 12342 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℤ) |
50 | 49 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → 𝑘 ∈ ℤ) |
51 | 46, 48, 50 | expne0d 13014 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (i↑𝑘) ≠ 0) |
52 | 40, 45, 51 | divcld 10801 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (𝐶 / (i↑𝑘)) ∈ ℂ) |
53 | 52 | recld 13934 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ) |
54 | 53 | rexrd 10089 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (ℜ‘(𝐶 / (i↑𝑘))) ∈
ℝ*) |
55 | 54 | adantr 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → (ℜ‘(𝐶 / (i↑𝑘))) ∈
ℝ*) |
56 | | simpr 477 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) |
57 | | pnfge 11964 |
. . . . . . . 8
⊢
((ℜ‘(𝐶 /
(i↑𝑘))) ∈
ℝ* → (ℜ‘(𝐶 / (i↑𝑘))) ≤ +∞) |
58 | 55, 57 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → (ℜ‘(𝐶 / (i↑𝑘))) ≤ +∞) |
59 | | 0xr 10086 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
60 | | pnfxr 10092 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
61 | | elicc1 12219 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
((ℜ‘(𝐶 /
(i↑𝑘))) ∈
(0[,]+∞) ↔ ((ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ* ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))) ∧
(ℜ‘(𝐶 /
(i↑𝑘))) ≤
+∞))) |
62 | 59, 60, 61 | mp2an 708 |
. . . . . . 7
⊢
((ℜ‘(𝐶 /
(i↑𝑘))) ∈
(0[,]+∞) ↔ ((ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ* ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))) ∧
(ℜ‘(𝐶 /
(i↑𝑘))) ≤
+∞)) |
63 | 55, 56, 58, 62 | syl3anbrc 1246 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → (ℜ‘(𝐶 / (i↑𝑘))) ∈ (0[,]+∞)) |
64 | | 0e0iccpnf 12283 |
. . . . . . 7
⊢ 0 ∈
(0[,]+∞) |
65 | 64 | a1i 11 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ ¬ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → 0 ∈
(0[,]+∞)) |
66 | 63, 65 | ifclda 4120 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈
(0[,]+∞)) |
67 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) |
68 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) |
69 | | ifan 4134 |
. . . . . 6
⊢ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝑈, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) |
70 | 69 | mpteq2i 4741 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝑈 ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘)))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) |
71 | | ifan 4134 |
. . . . . . . . . 10
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) |
72 | 71 | eqcomi 2631 |
. . . . . . . . 9
⊢ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) |
73 | 72 | mpteq2i 4741 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
74 | 73 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
75 | 74 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) |
76 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
77 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) |
78 | 76, 77, 13 | isibl2 23533 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ))) |
79 | 8, 78 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)) |
80 | 79 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
81 | 80 | r19.21bi 2932 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
82 | 75, 81 | eqeltrd 2701 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0)))
∈ ℝ) |
83 | | ifan 4134 |
. . . . . . . . 9
⊢ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) |
84 | 83 | eqcomi 2631 |
. . . . . . . 8
⊢ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) |
85 | 84 | mpteq2i 4741 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
86 | 85 | fveq2i 6194 |
. . . . . 6
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
87 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
88 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) |
89 | 87, 88, 26 | isibl2 23533 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ))) |
90 | 21, 89 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)) |
91 | 90 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
92 | 91 | r19.21bi 2932 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
93 | 86, 92 | syl5eqel 2705 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0)))
∈ ℝ) |
94 | 34, 36, 38, 39, 66, 67, 68, 70, 82, 93 | itg2split 23516 |
. . . 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))))) |
95 | 82, 93 | readdcld 10069 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))) +
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0))))
∈ ℝ) |
96 | 94, 95 | eqeltrd 2701 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
97 | 96 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
98 | | eqidd 2623 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
99 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) |
100 | 98, 99, 1 | isibl2 23533 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝑈 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ))) |
101 | 32, 97, 100 | mpbir2and 957 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶) ∈
𝐿1) |