Step | Hyp | Ref
| Expression |
1 | | iblsplit.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ) |
2 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ 𝑈 ↦ 𝐶) = (𝑥 ∈ 𝑈 ↦ 𝐶) |
3 | 1, 2 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶):𝑈⟶ℂ) |
4 | | ssun1 3738 |
. . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
5 | | iblsplit.2 |
. . . . . 6
⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) |
6 | 4, 5 | syl5sseqr 3617 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
7 | 6 | resmptd 5371 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
8 | | iblsplit.4 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈
𝐿1) |
9 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) |
10 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 / (i↑𝑦))) = (ℜ‘(𝐶 / (i↑𝑦)))) |
11 | 6 | sseld 3567 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑈)) |
12 | 11 | imdistani 722 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜑 ∧ 𝑥 ∈ 𝑈)) |
13 | 12, 1 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
14 | 9, 10, 13 | isibl2 23339 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ))) |
15 | 8, 14 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ)) |
16 | 15 | simpld 474 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) |
17 | 7, 16 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐴) ∈ MblFn) |
18 | | ssun2 3739 |
. . . . . 6
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
19 | 18, 5 | syl5sseqr 3617 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
20 | 19 | resmptd 5371 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
21 | | iblsplit.5 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈
𝐿1) |
22 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) |
23 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑦))) = (ℜ‘(𝐶 / (i↑𝑦)))) |
24 | 19 | sseld 3567 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈)) |
25 | 24 | imdistani 722 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜑 ∧ 𝑥 ∈ 𝑈)) |
26 | 25, 1 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ) |
27 | 22, 23, 26 | isibl2 23339 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ))) |
28 | 21, 27 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑦 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑦)))), (ℜ‘(𝐶 / (i↑𝑦))), 0))) ∈ ℝ)) |
29 | 28 | simpld 474 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn) |
30 | 20, 29 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ↾ 𝐵) ∈ MblFn) |
31 | 5 | eqcomd 2616 |
. . 3
⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝑈) |
32 | 3, 17, 30, 31 | mbfres2cn 38850 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶) ∈ MblFn) |
33 | 16, 13 | mbfdm2 23211 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ dom vol) |
34 | 33 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝐴 ∈ dom vol) |
35 | 29, 26 | mbfdm2 23211 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ dom vol) |
36 | 35 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝐵 ∈ dom vol) |
37 | | iblsplit.1 |
. . . . . 6
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) |
38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (vol*‘(𝐴 ∩ 𝐵)) = 0) |
39 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝑈 = (𝐴 ∪ 𝐵)) |
40 | 1 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ) |
41 | | ax-icn 9874 |
. . . . . . . . . . . . . 14
⊢ i ∈
ℂ |
42 | 41 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → i ∈
ℂ) |
43 | | elfznn0 12302 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℕ0) |
44 | 42, 43 | expcld 12870 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...3) →
(i↑𝑘) ∈
ℂ) |
45 | 44 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (i↑𝑘) ∈ ℂ) |
46 | 41 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → i ∈ ℂ) |
47 | | ine0 10344 |
. . . . . . . . . . . . 13
⊢ i ≠
0 |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → i ≠ 0) |
49 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℤ) |
50 | 49 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → 𝑘 ∈ ℤ) |
51 | 46, 48, 50 | expne0d 12876 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (i↑𝑘) ≠ 0) |
52 | 40, 45, 51 | divcld 10680 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (𝐶 / (i↑𝑘)) ∈ ℂ) |
53 | 52 | recld 13782 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ) |
54 | 53 | rexrd 9968 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (ℜ‘(𝐶 / (i↑𝑘))) ∈
ℝ*) |
55 | 54 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → (ℜ‘(𝐶 / (i↑𝑘))) ∈
ℝ*) |
56 | | simpr 476 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) |
57 | | pnfge 11840 |
. . . . . . . 8
⊢
((ℜ‘(𝐶 /
(i↑𝑘))) ∈
ℝ* → (ℜ‘(𝐶 / (i↑𝑘))) ≤ +∞) |
58 | 55, 57 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → (ℜ‘(𝐶 / (i↑𝑘))) ≤ +∞) |
59 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
60 | | pnfxr 9971 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
61 | | elicc1 12090 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
((ℜ‘(𝐶 /
(i↑𝑘))) ∈
(0[,]+∞) ↔ ((ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ* ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))) ∧
(ℜ‘(𝐶 /
(i↑𝑘))) ≤
+∞))) |
62 | 59, 60, 61 | mp2an 704 |
. . . . . . 7
⊢
((ℜ‘(𝐶 /
(i↑𝑘))) ∈
(0[,]+∞) ↔ ((ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ* ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))) ∧
(ℜ‘(𝐶 /
(i↑𝑘))) ≤
+∞)) |
63 | 55, 56, 58, 62 | syl3anbrc 1239 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → (ℜ‘(𝐶 / (i↑𝑘))) ∈ (0[,]+∞)) |
64 | | 0e0iccpnf 12154 |
. . . . . . 7
⊢ 0 ∈
(0[,]+∞) |
65 | 64 | a1i 11 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) ∧ ¬ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))) → 0 ∈
(0[,]+∞)) |
66 | 63, 65 | ifclda 4070 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈
(0[,]+∞)) |
67 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) |
68 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) |
69 | | ifan 4084 |
. . . . . 6
⊢ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝑈, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) |
70 | 69 | mpteq2i 4669 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝑈 ∧ 0 ≤
(ℜ‘(𝐶 /
(i↑𝑘)))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) |
71 | | ifan 4084 |
. . . . . . . . . 10
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) |
72 | 71 | eqcomi 2619 |
. . . . . . . . 9
⊢ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) |
73 | 72 | mpteq2i 4669 |
. . . . . . . 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 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) |
76 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
77 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) |
78 | 76, 77, 13 | isibl2 23339 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ))) |
79 | 8, 78 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)) |
80 | 79 | simprd 478 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
81 | 80 | r19.21bi 2916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
82 | 75, 81 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0)))
∈ ℝ) |
83 | | ifan 4084 |
. . . . . . . . 9
⊢ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) |
84 | 83 | eqcomi 2619 |
. . . . . . . 8
⊢ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) |
85 | 84 | mpteq2i 4669 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) |
86 | 85 | fveq2i 6106 |
. . . . . 6
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
87 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
88 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) |
89 | 87, 88, 26 | isibl2 23339 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ))) |
90 | 21, 89 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)) |
91 | 90 | simprd 478 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
92 | 91 | r19.21bi 2916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
93 | 86, 92 | syl5eqel 2692 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0)))
∈ ℝ) |
94 | 34, 36, 38, 39, 66, 67, 68, 70, 82, 93 | itg2split 23322 |
. . . 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 9948 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))) +
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐵, if(0 ≤
(ℜ‘(𝐶 /
(i↑𝑘))),
(ℜ‘(𝐶 /
(i↑𝑘))), 0), 0))))
∈ ℝ) |
96 | 94, 95 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
97 | 96 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ) |
98 | | eqidd 2611 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) |
99 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))) |
100 | 98, 99, 1 | isibl2 23339 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝑈 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ))) |
101 | 32, 97, 100 | mpbir2and 959 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ 𝐶) ∈
𝐿1) |