Step | Hyp | Ref
| Expression |
1 | | itgparts.b |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
2 | | cncff 22696 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
4 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) |
5 | 4 | fmpt 6381 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝑋(,)𝑌)𝐵 ∈ ℂ ↔ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
6 | 3, 5 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)𝐵 ∈ ℂ) |
7 | 6 | r19.21bi 2932 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ) |
8 | | ioossicc 12259 |
. . . . . . 7
⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) |
9 | 8 | sseli 3599 |
. . . . . 6
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌)) |
10 | | itgparts.c |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
11 | | cncff 22696 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶):(𝑋[,]𝑌)⟶ℂ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶):(𝑋[,]𝑌)⟶ℂ) |
13 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) |
14 | 13 | fmpt 6381 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(𝑋[,]𝑌)𝐶 ∈ ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶):(𝑋[,]𝑌)⟶ℂ) |
15 | 12, 14 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐶 ∈ ℂ) |
16 | 15 | r19.21bi 2932 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐶 ∈ ℂ) |
17 | 9, 16 | sylan2 491 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐶 ∈ ℂ) |
18 | 7, 17 | mulcld 10060 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐵 · 𝐶) ∈ ℂ) |
19 | | itgparts.bc |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐵 · 𝐶)) ∈
𝐿1) |
20 | 18, 19 | itgcl 23550 |
. . 3
⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥 ∈ ℂ) |
21 | | itgparts.a |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
22 | | cncff 22696 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶ℂ) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶ℂ) |
24 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) |
25 | 24 | fmpt 6381 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(𝑋[,]𝑌)𝐴 ∈ ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶ℂ) |
26 | 23, 25 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ ℂ) |
27 | 26 | r19.21bi 2932 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ) |
28 | 9, 27 | sylan2 491 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ ℂ) |
29 | | itgparts.d |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
30 | | cncff 22696 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷):(𝑋(,)𝑌)⟶ℂ) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷):(𝑋(,)𝑌)⟶ℂ) |
32 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) |
33 | 32 | fmpt 6381 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝑋(,)𝑌)𝐷 ∈ ℂ ↔ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷):(𝑋(,)𝑌)⟶ℂ) |
34 | 31, 33 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)𝐷 ∈ ℂ) |
35 | 34 | r19.21bi 2932 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ ℂ) |
36 | 28, 35 | mulcld 10060 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐴 · 𝐷) ∈ ℂ) |
37 | | itgparts.ad |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐴 · 𝐷)) ∈
𝐿1) |
38 | 36, 37 | itgcl 23550 |
. . 3
⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐴 · 𝐷) d𝑥 ∈ ℂ) |
39 | 20, 38 | pncan2d 10394 |
. 2
⊢ (𝜑 → ((∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥 + ∫(𝑋(,)𝑌)(𝐴 · 𝐷) d𝑥) − ∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥) = ∫(𝑋(,)𝑌)(𝐴 · 𝐷) d𝑥) |
40 | 18, 19, 36, 37 | itgadd 23591 |
. . . 4
⊢ (𝜑 → ∫(𝑋(,)𝑌)((𝐵 · 𝐶) + (𝐴 · 𝐷)) d𝑥 = (∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥 + ∫(𝑋(,)𝑌)(𝐴 · 𝐷) d𝑥)) |
41 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝑡 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑥) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑡)) |
42 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑥) |
43 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥ℝ |
44 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥
D |
45 | | nfmpt1 4747 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)) |
46 | 43, 44, 45 | nfov 6676 |
. . . . . . . 8
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))) |
47 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑡 |
48 | 46, 47 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑡) |
49 | 41, 42, 48 | cbvitg 23542 |
. . . . . 6
⊢
∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑡) d𝑡 |
50 | | itgparts.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℝ) |
51 | | itgparts.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℝ) |
52 | | itgparts.le |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
53 | | ax-resscn 9993 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
54 | 53 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) |
55 | | iccssre 12255 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ) |
56 | 50, 51, 55 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
57 | 27, 16 | mulcld 10060 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 · 𝐶) ∈ ℂ) |
58 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
59 | 58 | tgioo2 22606 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
60 | | iccntr 22624 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌)) |
61 | 50, 51, 60 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌)) |
62 | 54, 56, 57, 59, 58, 61 | dvmptntr 23734 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐴 · 𝐶)))) |
63 | | reelprrecn 10028 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
64 | 63 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
65 | 54, 56, 27, 59, 58, 61 | dvmptntr 23734 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴))) |
66 | | itgparts.da |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
67 | 65, 66 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
68 | 54, 56, 16, 59, 58, 61 | dvmptntr 23734 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶))) |
69 | | itgparts.dc |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷)) |
70 | 68, 69 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷)) |
71 | 64, 28, 7, 67, 17, 35, 70 | dvmptmul 23724 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐴 · 𝐶))) = (𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐷 · 𝐴)))) |
72 | 35, 28 | mulcomd 10061 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (𝐷 · 𝐴) = (𝐴 · 𝐷)) |
73 | 72 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝐵 · 𝐶) + (𝐷 · 𝐴)) = ((𝐵 · 𝐶) + (𝐴 · 𝐷))) |
74 | 73 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐷 · 𝐴))) = (𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐴 · 𝐷)))) |
75 | 62, 71, 74 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))) = (𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐴 · 𝐷)))) |
76 | 58 | addcn 22668 |
. . . . . . . . . 10
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
77 | 76 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
78 | | resmpt 5449 |
. . . . . . . . . . . 12
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶)) |
79 | 8, 78 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶) |
80 | | rescncf 22700 |
. . . . . . . . . . . 12
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))) |
81 | 8, 10, 80 | mpsyl 68 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
82 | 79, 81 | syl5eqelr 2706 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
83 | 1, 82 | mulcncf 23215 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐵 · 𝐶)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
84 | | resmpt 5449 |
. . . . . . . . . . . 12
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) |
85 | 8, 84 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴) |
86 | | rescncf 22700 |
. . . . . . . . . . . 12
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))) |
87 | 8, 21, 86 | mpsyl 68 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
88 | 85, 87 | syl5eqelr 2706 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
89 | 88, 29 | mulcncf 23215 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐴 · 𝐷)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
90 | 58, 77, 83, 89 | cncfmpt2f 22717 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐴 · 𝐷))) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
91 | 75, 90 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
92 | 18, 19, 36, 37 | ibladd 23587 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐴 · 𝐷))) ∈
𝐿1) |
93 | 75, 92 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))) ∈
𝐿1) |
94 | 21, 10 | mulcncf 23215 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
95 | 50, 51, 52, 91, 93, 94 | ftc2 23807 |
. . . . . 6
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑋))) |
96 | 49, 95 | syl5eq 2668 |
. . . . 5
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑥) d𝑥 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑋))) |
97 | 75 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐴 · 𝐷)))‘𝑥)) |
98 | 97 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐴 · 𝐷)))‘𝑥)) |
99 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝑥 ∈ (𝑋(,)𝑌)) |
100 | | ovex 6678 |
. . . . . . . 8
⊢ ((𝐵 · 𝐶) + (𝐴 · 𝐷)) ∈ V |
101 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐴 · 𝐷))) = (𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐴 · 𝐷))) |
102 | 101 | fvmpt2 6291 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ∧ ((𝐵 · 𝐶) + (𝐴 · 𝐷)) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐴 · 𝐷)))‘𝑥) = ((𝐵 · 𝐶) + (𝐴 · 𝐷))) |
103 | 99, 100, 102 | sylancl 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ ((𝐵 · 𝐶) + (𝐴 · 𝐷)))‘𝑥) = ((𝐵 · 𝐶) + (𝐴 · 𝐷))) |
104 | 98, 103 | eqtrd 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑥) = ((𝐵 · 𝐶) + (𝐴 · 𝐷))) |
105 | 104 | itgeq2dv 23548 |
. . . . 5
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)((𝐵 · 𝐶) + (𝐴 · 𝐷)) d𝑥) |
106 | 50 | rexrd 10089 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
107 | 51 | rexrd 10089 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
108 | | ubicc2 12289 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌)) |
109 | 106, 107,
52, 108 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌)) |
110 | | ovex 6678 |
. . . . . . . . 9
⊢ (𝐴 · 𝐶) ∈ V |
111 | 110 | csbex 4793 |
. . . . . . . 8
⊢
⦋𝑌 /
𝑥⦌(𝐴 · 𝐶) ∈ V |
112 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶)) |
113 | 112 | fvmpts 6285 |
. . . . . . . 8
⊢ ((𝑌 ∈ (𝑋[,]𝑌) ∧ ⦋𝑌 / 𝑥⦌(𝐴 · 𝐶) ∈ V) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑌) = ⦋𝑌 / 𝑥⦌(𝐴 · 𝐶)) |
114 | 109, 111,
113 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑌) = ⦋𝑌 / 𝑥⦌(𝐴 · 𝐶)) |
115 | | itgparts.f |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝐴 · 𝐶) = 𝐹) |
116 | 51, 115 | csbied 3560 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌(𝐴 · 𝐶) = 𝐹) |
117 | 114, 116 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑌) = 𝐹) |
118 | | lbicc2 12288 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌)) |
119 | 106, 107,
52, 118 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌)) |
120 | 110 | csbex 4793 |
. . . . . . . 8
⊢
⦋𝑋 /
𝑥⦌(𝐴 · 𝐶) ∈ V |
121 | 112 | fvmpts 6285 |
. . . . . . . 8
⊢ ((𝑋 ∈ (𝑋[,]𝑌) ∧ ⦋𝑋 / 𝑥⦌(𝐴 · 𝐶) ∈ V) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑋) = ⦋𝑋 / 𝑥⦌(𝐴 · 𝐶)) |
122 | 119, 120,
121 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑋) = ⦋𝑋 / 𝑥⦌(𝐴 · 𝐶)) |
123 | | itgparts.e |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝐴 · 𝐶) = 𝐸) |
124 | 50, 123 | csbied 3560 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌(𝐴 · 𝐶) = 𝐸) |
125 | 122, 124 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑋) = 𝐸) |
126 | 117, 125 | oveq12d 6668 |
. . . . 5
⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ (𝐴 · 𝐶))‘𝑋)) = (𝐹 − 𝐸)) |
127 | 96, 105, 126 | 3eqtr3d 2664 |
. . . 4
⊢ (𝜑 → ∫(𝑋(,)𝑌)((𝐵 · 𝐶) + (𝐴 · 𝐷)) d𝑥 = (𝐹 − 𝐸)) |
128 | 40, 127 | eqtr3d 2658 |
. . 3
⊢ (𝜑 → (∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥 + ∫(𝑋(,)𝑌)(𝐴 · 𝐷) d𝑥) = (𝐹 − 𝐸)) |
129 | 128 | oveq1d 6665 |
. 2
⊢ (𝜑 → ((∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥 + ∫(𝑋(,)𝑌)(𝐴 · 𝐷) d𝑥) − ∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥) = ((𝐹 − 𝐸) − ∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥)) |
130 | 39, 129 | eqtr3d 2658 |
1
⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐴 · 𝐷) d𝑥 = ((𝐹 − 𝐸) − ∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥)) |