Proof of Theorem itgadd
Step | Hyp | Ref
| Expression |
1 | | itgadd.2 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
2 | | iblmbf 24520 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
4 | | itgadd.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
5 | 3, 4 | mbfmptcl 24389 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
6 | | itgadd.4 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈
𝐿1) |
7 | | iblmbf 24520 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) |
9 | | itgadd.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
10 | 8, 9 | mbfmptcl 24389 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
11 | 5, 10 | readdd 14664 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 + 𝐶)) = ((ℜ‘𝐵) + (ℜ‘𝐶))) |
12 | 11 | itgeq2dv 24534 |
. . . . 5
⊢ (𝜑 → ∫𝐴(ℜ‘(𝐵 + 𝐶)) d𝑥 = ∫𝐴((ℜ‘𝐵) + (ℜ‘𝐶)) d𝑥) |
13 | 5 | recld 14644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ) |
14 | 5 | iblcn 24551 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1))) |
15 | 1, 14 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1)) |
16 | 15 | simpld 498 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈
𝐿1) |
17 | 10 | recld 14644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐶) ∈ ℝ) |
18 | 10 | iblcn 24551 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)) ∈
𝐿1))) |
19 | 6, 18 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)) ∈
𝐿1)) |
20 | 19 | simpld 498 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)) ∈
𝐿1) |
21 | 13, 16, 17, 20, 13, 17 | itgaddlem2 24576 |
. . . . 5
⊢ (𝜑 → ∫𝐴((ℜ‘𝐵) + (ℜ‘𝐶)) d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + ∫𝐴(ℜ‘𝐶) d𝑥)) |
22 | 12, 21 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → ∫𝐴(ℜ‘(𝐵 + 𝐶)) d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + ∫𝐴(ℜ‘𝐶) d𝑥)) |
23 | 5, 10 | imaddd 14665 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘(𝐵 + 𝐶)) = ((ℑ‘𝐵) + (ℑ‘𝐶))) |
24 | 23 | itgeq2dv 24534 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴(ℑ‘(𝐵 + 𝐶)) d𝑥 = ∫𝐴((ℑ‘𝐵) + (ℑ‘𝐶)) d𝑥) |
25 | 5 | imcld 14645 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ) |
26 | 15 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1) |
27 | 10 | imcld 14645 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐶) ∈ ℝ) |
28 | 19 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)) ∈
𝐿1) |
29 | 25, 26, 27, 28, 25, 27 | itgaddlem2 24576 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴((ℑ‘𝐵) + (ℑ‘𝐶)) d𝑥 = (∫𝐴(ℑ‘𝐵) d𝑥 + ∫𝐴(ℑ‘𝐶) d𝑥)) |
30 | 24, 29 | eqtrd 2773 |
. . . . . 6
⊢ (𝜑 → ∫𝐴(ℑ‘(𝐵 + 𝐶)) d𝑥 = (∫𝐴(ℑ‘𝐵) d𝑥 + ∫𝐴(ℑ‘𝐶) d𝑥)) |
31 | 30 | oveq2d 7187 |
. . . . 5
⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐵 + 𝐶)) d𝑥) = (i · (∫𝐴(ℑ‘𝐵) d𝑥 + ∫𝐴(ℑ‘𝐶) d𝑥))) |
32 | | ax-icn 10675 |
. . . . . . 7
⊢ i ∈
ℂ |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝜑 → i ∈
ℂ) |
34 | 25, 26 | itgcl 24536 |
. . . . . 6
⊢ (𝜑 → ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) |
35 | 27, 28 | itgcl 24536 |
. . . . . 6
⊢ (𝜑 → ∫𝐴(ℑ‘𝐶) d𝑥 ∈ ℂ) |
36 | 33, 34, 35 | adddid 10744 |
. . . . 5
⊢ (𝜑 → (i · (∫𝐴(ℑ‘𝐵) d𝑥 + ∫𝐴(ℑ‘𝐶) d𝑥)) = ((i · ∫𝐴(ℑ‘𝐵) d𝑥) + (i · ∫𝐴(ℑ‘𝐶) d𝑥))) |
37 | 31, 36 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐵 + 𝐶)) d𝑥) = ((i · ∫𝐴(ℑ‘𝐵) d𝑥) + (i · ∫𝐴(ℑ‘𝐶) d𝑥))) |
38 | 22, 37 | oveq12d 7189 |
. . 3
⊢ (𝜑 → (∫𝐴(ℜ‘(𝐵 + 𝐶)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐵 + 𝐶)) d𝑥)) = ((∫𝐴(ℜ‘𝐵) d𝑥 + ∫𝐴(ℜ‘𝐶) d𝑥) + ((i · ∫𝐴(ℑ‘𝐵) d𝑥) + (i · ∫𝐴(ℑ‘𝐶) d𝑥)))) |
39 | 13, 16 | itgcl 24536 |
. . . 4
⊢ (𝜑 → ∫𝐴(ℜ‘𝐵) d𝑥 ∈ ℂ) |
40 | 17, 20 | itgcl 24536 |
. . . 4
⊢ (𝜑 → ∫𝐴(ℜ‘𝐶) d𝑥 ∈ ℂ) |
41 | | mulcl 10700 |
. . . . 5
⊢ ((i
∈ ℂ ∧ ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) → (i ·
∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ) |
42 | 32, 34, 41 | sylancr 590 |
. . . 4
⊢ (𝜑 → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ) |
43 | | mulcl 10700 |
. . . . 5
⊢ ((i
∈ ℂ ∧ ∫𝐴(ℑ‘𝐶) d𝑥 ∈ ℂ) → (i ·
∫𝐴(ℑ‘𝐶) d𝑥) ∈ ℂ) |
44 | 32, 35, 43 | sylancr 590 |
. . . 4
⊢ (𝜑 → (i · ∫𝐴(ℑ‘𝐶) d𝑥) ∈ ℂ) |
45 | 39, 40, 42, 44 | add4d 10947 |
. . 3
⊢ (𝜑 → ((∫𝐴(ℜ‘𝐵) d𝑥 + ∫𝐴(ℜ‘𝐶) d𝑥) + ((i · ∫𝐴(ℑ‘𝐵) d𝑥) + (i · ∫𝐴(ℑ‘𝐶) d𝑥))) = ((∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)) + (∫𝐴(ℜ‘𝐶) d𝑥 + (i · ∫𝐴(ℑ‘𝐶) d𝑥)))) |
46 | 38, 45 | eqtrd 2773 |
. 2
⊢ (𝜑 → (∫𝐴(ℜ‘(𝐵 + 𝐶)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐵 + 𝐶)) d𝑥)) = ((∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)) + (∫𝐴(ℜ‘𝐶) d𝑥 + (i · ∫𝐴(ℑ‘𝐶) d𝑥)))) |
47 | | ovexd 7206 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ V) |
48 | 4, 1, 9, 6 | ibladd 24573 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈
𝐿1) |
49 | 47, 48 | itgcnval 24552 |
. 2
⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴(ℜ‘(𝐵 + 𝐶)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐵 + 𝐶)) d𝑥))) |
50 | 4, 1 | itgcnval 24552 |
. . 3
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) |
51 | 9, 6 | itgcnval 24552 |
. . 3
⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = (∫𝐴(ℜ‘𝐶) d𝑥 + (i · ∫𝐴(ℑ‘𝐶) d𝑥))) |
52 | 50, 51 | oveq12d 7189 |
. 2
⊢ (𝜑 → (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥) = ((∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)) + (∫𝐴(ℜ‘𝐶) d𝑥 + (i · ∫𝐴(ℑ‘𝐶) d𝑥)))) |
53 | 46, 49, 52 | 3eqtr4d 2783 |
1
⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥)) |