Step | Hyp | Ref
| Expression |
1 | | itgsubst.le |
. . 3
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
2 | 1 | ditgpos 23620 |
. 2
⊢ (𝜑 → ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
3 | | itgsubst.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) |
4 | | itgsubst.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ℝ) |
5 | | ax-resscn 9993 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℂ) |
7 | | iccssre 12255 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ) |
8 | 3, 4, 7 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
9 | | itgsubst.cl2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁)) |
10 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) |
11 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) |
12 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐴 → (𝑀(,)𝑣) = (𝑀(,)𝐴)) |
13 | | itgeq1 23539 |
. . . . . . . . . . . . 13
⊢ ((𝑀(,)𝑣) = (𝑀(,)𝐴) → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
15 | 9, 10, 11, 14 | fmptco 6396 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
16 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) |
17 | 9, 16 | fmptd 6385 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)) |
18 | | ioossicc 12259 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
19 | | itgsubst.z |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑍 ∈
ℝ*) |
20 | | itgsubst.w |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑊 ∈
ℝ*) |
21 | | itgsubst.m |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊)) |
22 | | eliooord 12233 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊)) |
24 | 23 | simpld 475 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑍 < 𝑀) |
25 | | itgsubst.n |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊)) |
26 | | eliooord 12233 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊)) |
28 | 27 | simprd 479 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 < 𝑊) |
29 | | iccssioo 12242 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑍 ∈ ℝ*
∧ 𝑊 ∈
ℝ*) ∧ (𝑍 < 𝑀 ∧ 𝑁 < 𝑊)) → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊)) |
30 | 19, 20, 24, 28, 29 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊)) |
31 | 18, 30 | syl5ss 3614 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑍(,)𝑊)) |
32 | | ioossre 12235 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍(,)𝑊) ⊆ ℝ |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℝ) |
34 | 33, 5 | syl6ss 3615 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℂ) |
35 | 31, 34 | sstrd 3613 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℂ) |
36 | | itgsubst.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) |
37 | | cncffvrn 22701 |
. . . . . . . . . . . . . 14
⊢ (((𝑀(,)𝑁) ⊆ ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))) |
38 | 35, 36, 37 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))) |
39 | 17, 38 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁))) |
40 | 18 | sseli 3599 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ (𝑀(,)𝑁) → 𝑣 ∈ (𝑀[,]𝑁)) |
41 | 32, 25 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ ℝ) |
42 | 41 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
43 | 42 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑁 ∈
ℝ*) |
44 | 32, 21 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑀 ∈ ℝ) |
45 | | elicc2 12238 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))) |
46 | 44, 41, 45 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))) |
47 | 46 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)) |
48 | 47 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑣 ≤ 𝑁) |
49 | | iooss2 12211 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℝ*
∧ 𝑣 ≤ 𝑁) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁)) |
50 | 43, 48, 49 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁)) |
51 | 50 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝑢 ∈ (𝑀(,)𝑁)) |
52 | 31 | sselda 3603 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝑢 ∈ (𝑍(,)𝑊)) |
53 | | itgsubst.c |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ)) |
54 | | cncff 22696 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ) |
56 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) |
57 | 56 | fmpt 6381 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑢 ∈
(𝑍(,)𝑊)𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ) |
58 | 55, 57 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑢 ∈ (𝑍(,)𝑊)𝐶 ∈ ℂ) |
59 | 58 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑍(,)𝑊)) → 𝐶 ∈ ℂ) |
60 | 52, 59 | syldan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ) |
61 | 60 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ) |
62 | 51, 61 | syldan 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝐶 ∈ ℂ) |
63 | | ioombl 23333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀(,)𝑣) ∈ dom vol |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ∈ dom vol) |
65 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)) |
66 | | ioombl 23333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀(,)𝑁) ∈ dom vol |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀(,)𝑁) ∈ dom vol) |
68 | 30 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝑢 ∈ (𝑍(,)𝑊)) |
69 | 68, 59 | syldan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ) |
70 | 30 | resmptd 5452 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) = (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶)) |
71 | | rescncf 22700 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀[,]𝑁) ⊆ (𝑍(,)𝑊) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))) |
72 | 30, 53, 71 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
73 | 70, 72 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
74 | | cniccibl 23607 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈
𝐿1) |
75 | 44, 41, 73, 74 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈
𝐿1) |
76 | 65, 67, 69, 75 | iblss 23571 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈
𝐿1) |
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈
𝐿1) |
78 | 50, 64, 61, 77 | iblss 23571 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑣) ↦ 𝐶) ∈
𝐿1) |
79 | 62, 78 | itgcl 23550 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ) |
80 | 40, 79 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ) |
81 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) |
82 | 80, 81 | fmptd 6385 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ) |
83 | 31, 32 | syl6ss 3615 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℝ) |
84 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑢 → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) = ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢)) |
85 | | nffvmpt1 6199 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑢((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) |
86 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) |
87 | 84, 85, 86 | cbvitg 23542 |
. . . . . . . . . . . . . . . . . . 19
⊢
∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 |
88 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) |
89 | 88 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ (𝑀(,)𝑁) ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶) |
90 | 51, 62, 89 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶) |
91 | 90 | itgeq2dv 23548 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 = ∫(𝑀(,)𝑣)𝐶 d𝑢) |
92 | 87, 91 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)𝐶 d𝑢) |
93 | 92 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) |
94 | 93 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))) |
95 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) |
96 | 3 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
97 | 4 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
98 | | lbicc2 12288 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌)) |
99 | 96, 97, 1, 98 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌)) |
100 | | n0i 3920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 ∈ (𝑋[,]𝑌) → ¬ (𝑋[,]𝑌) = ∅) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ (𝑋[,]𝑌) = ∅) |
102 | | feq3 6028 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀(,)𝑁) = ∅ → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅)) |
103 | 17, 102 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅)) |
104 | | f00 6087 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ ↔ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = ∅ ∧ (𝑋[,]𝑌) = ∅)) |
105 | 104 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ → (𝑋[,]𝑌) = ∅) |
106 | 103, 105 | syl6 35 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑋[,]𝑌) = ∅)) |
107 | 101, 106 | mtod 189 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ (𝑀(,)𝑁) = ∅) |
108 | 44 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
109 | | ioo0 12200 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ*) → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀)) |
110 | 108, 42, 109 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀)) |
111 | 107, 110 | mtbid 314 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ 𝑁 ≤ 𝑀) |
112 | 41, 44 | letrid 10189 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁)) |
113 | 112 | ord 392 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁)) |
114 | 111, 113 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
115 | | resmpt 5449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
116 | 18, 115 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) |
117 | | rescncf 22700 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ))) |
118 | 18, 73, 117 | mpsyl 68 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
119 | 116, 118 | syl5eqelr 2706 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
120 | 95, 44, 41, 114, 119, 76 | ftc1cn 23806 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
121 | 30, 32 | syl6ss 3615 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) |
122 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
123 | 122 | tgioo2 22606 |
. . . . . . . . . . . . . . . . 17
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
124 | | iccntr 22624 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
125 | 44, 41, 124 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
126 | 6, 121, 79, 123, 122, 125 | dvmptntr 23734 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))) |
127 | 94, 120, 126 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
128 | 127 | dmeqd 5326 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
129 | 88, 60 | dmmptd 6024 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑀(,)𝑁)) |
130 | 128, 129 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) |
131 | | dvcn 23684 |
. . . . . . . . . . . . 13
⊢
(((ℝ ⊆ ℂ ∧ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ ∧ (𝑀(,)𝑁) ⊆ ℝ) ∧ dom (ℝ D
(𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
132 | 6, 82, 83, 130, 131 | syl31anc 1329 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
133 | 39, 132 | cncfco 22710 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
134 | 15, 133 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
135 | | cncff 22696 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ) |
136 | 134, 135 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ) |
137 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) |
138 | 137 | fmpt 6381 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑋[,]𝑌)∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ) |
139 | 136, 138 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ) |
140 | 139 | r19.21bi 2932 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ) |
141 | | iccntr 22624 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌)) |
142 | 3, 4, 141 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌)) |
143 | 6, 8, 140, 123, 122, 142 | dvmptntr 23734 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))) |
144 | | reelprrecn 10028 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
145 | 144 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
146 | | ioossicc 12259 |
. . . . . . . . 9
⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) |
147 | 146 | sseli 3599 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌)) |
148 | 147, 9 | sylan2 491 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝑀(,)𝑁)) |
149 | | itgsubst.b |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩
𝐿1)) |
150 | | elin 3796 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1) ↔
((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1)) |
151 | 149, 150 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1)) |
152 | 151 | simpld 475 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
153 | | cncff 22696 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
154 | 152, 153 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
155 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) |
156 | 155 | fmpt 6381 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑋(,)𝑌)𝐵 ∈ ℂ ↔ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
157 | 154, 156 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)𝐵 ∈ ℂ) |
158 | 157 | r19.21bi 2932 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ) |
159 | 60, 88 | fmptd 6385 |
. . . . . . . . 9
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ) |
160 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑣𝐶 |
161 | | nfcsb1v 3549 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢⦋𝑣 / 𝑢⦌𝐶 |
162 | | csbeq1a 3542 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑢⦌𝐶) |
163 | 160, 161,
162 | cbvmpt 4749 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶) |
164 | 163 | fmpt 6381 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
(𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ) |
165 | 159, 164 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ) |
166 | 165 | r19.21bi 2932 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ) |
167 | 32, 5 | sstri 3612 |
. . . . . . . . . 10
⊢ (𝑍(,)𝑊) ⊆ ℂ |
168 | | cncff 22696 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) |
169 | 36, 168 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) |
170 | 16 | fmpt 6381 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(𝑋[,]𝑌)𝐴 ∈ (𝑍(,)𝑊) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) |
171 | 169, 170 | sylibr 224 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑍(,)𝑊)) |
172 | 171 | r19.21bi 2932 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑍(,)𝑊)) |
173 | 167, 172 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ) |
174 | 6, 8, 173, 123, 122, 142 | dvmptntr 23734 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴))) |
175 | | itgsubst.da |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
176 | 174, 175 | eqtr3d 2658 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
177 | 127, 163 | syl6eq 2672 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶)) |
178 | | csbeq1 3536 |
. . . . . . 7
⊢ (𝑣 = 𝐴 → ⦋𝑣 / 𝑢⦌𝐶 = ⦋𝐴 / 𝑢⦌𝐶) |
179 | 145, 145,
148, 158, 80, 166, 176, 177, 14, 178 | dvmptco 23735 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵))) |
180 | | nfcvd 2765 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑀(,)𝑁) → Ⅎ𝑢𝐸) |
181 | | itgsubst.e |
. . . . . . . . . 10
⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸) |
182 | 180, 181 | csbiegf 3557 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑀(,)𝑁) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸) |
183 | 148, 182 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸) |
184 | 183 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (⦋𝐴 / 𝑢⦌𝐶 · 𝐵) = (𝐸 · 𝐵)) |
185 | 184 | mpteq2dva 4744 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
186 | 143, 179,
185 | 3eqtrd 2660 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
187 | | resmpt 5449 |
. . . . . . . 8
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)) |
188 | 146, 187 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) |
189 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶)) |
190 | 172, 10, 189, 181 | fmptco 6396 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)) |
191 | 36, 53 | cncfco 22710 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
192 | 190, 191 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
193 | | rescncf 22700 |
. . . . . . . 8
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))) |
194 | 146, 192,
193 | mpsyl 68 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
195 | 188, 194 | syl5eqelr 2706 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
196 | 195, 152 | mulcncf 23215 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
197 | 186, 196 | eqeltrd 2701 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
198 | | ioombl 23333 |
. . . . . . . 8
⊢ (𝑋(,)𝑌) ∈ dom vol |
199 | 198 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol) |
200 | | fco 6058 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ) |
201 | 55, 169, 200 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ) |
202 | 190 | feq1d 6030 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)) |
203 | 201, 202 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ) |
204 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) |
205 | 204 | fmpt 6381 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝑋[,]𝑌)𝐸 ∈ ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ) |
206 | 203, 205 | sylibr 224 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐸 ∈ ℂ) |
207 | 206 | r19.21bi 2932 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐸 ∈ ℂ) |
208 | 147, 207 | sylan2 491 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ) |
209 | | eqidd 2623 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)) |
210 | | eqidd 2623 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
211 | 199, 208,
158, 209, 210 | offval2 6914 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 ·
(𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
212 | 186, 211 | eqtr4d 2659 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 ·
(𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))) |
213 | 146 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)) |
214 | | cniccibl 23607 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈
𝐿1) |
215 | 3, 4, 192, 214 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈
𝐿1) |
216 | 213, 199,
207, 215 | iblss 23571 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈
𝐿1) |
217 | | iblmbf 23534 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿1 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn) |
218 | 216, 217 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn) |
219 | 151 | simprd 479 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1) |
220 | | cniccbdd 23230 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
221 | 3, 4, 192, 220 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
222 | | ssralv 3666 |
. . . . . . . . . 10
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
223 | 146, 222 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
224 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) |
225 | 224, 208 | dmmptd 6024 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑋(,)𝑌)) |
226 | 225 | raleqdv 3144 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
227 | 188 | fveq1i 6192 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) |
228 | | fvres 6207 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝑋(,)𝑌) → (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) |
229 | 227, 228 | syl5eqr 2670 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) |
230 | 229 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋(,)𝑌) → (abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) = (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))) |
231 | 230 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
232 | 231 | ralbiia 2979 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
(𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
233 | 226, 232 | syl6rbb 277 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
234 | 223, 233 | syl5ib 234 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
235 | 234 | reximdv 3016 |
. . . . . . 7
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
236 | 221, 235 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
237 | | bddmulibl 23605 |
. . . . . 6
⊢ (((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1 ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 ·
(𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈
𝐿1) |
238 | 218, 219,
236, 237 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 ·
(𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈
𝐿1) |
239 | 212, 238 | eqeltrd 2701 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈
𝐿1) |
240 | 3, 4, 1, 197, 239, 134 | ftc2 23807 |
. . 3
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋))) |
241 | | fveq2 6191 |
. . . . 5
⊢ (𝑡 = 𝑥 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥)) |
242 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥ℝ |
243 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥
D |
244 | | nfmpt1 4747 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) |
245 | 242, 243,
244 | nfov 6676 |
. . . . . 6
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
246 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑥𝑡 |
247 | 245, 246 | nffv 6198 |
. . . . 5
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) |
248 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) |
249 | 241, 247,
248 | cbvitg 23542 |
. . . 4
⊢
∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 |
250 | 186 | fveq1d 6193 |
. . . . . 6
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥)) |
251 | | ovex 6678 |
. . . . . . 7
⊢ (𝐸 · 𝐵) ∈ V |
252 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) |
253 | 252 | fvmpt2 6291 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ∧ (𝐸 · 𝐵) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵)) |
254 | 251, 253 | mpan2 707 |
. . . . . 6
⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵)) |
255 | 250, 254 | sylan9eq 2676 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = (𝐸 · 𝐵)) |
256 | 255 | itgeq2dv 23548 |
. . . 4
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
257 | 249, 256 | syl5eq 2668 |
. . 3
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
258 | 18, 9 | sseldi 3601 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀[,]𝑁)) |
259 | | elicc2 12238 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
260 | 44, 41, 259 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
261 | 260 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
262 | 258, 261 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)) |
263 | 262 | simp2d 1074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝑀 ≤ 𝐴) |
264 | 263 | ditgpos 23620 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
265 | 264 | mpteq2dva 4744 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
266 | 265 | fveq1d 6193 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌)) |
267 | | ubicc2 12289 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌)) |
268 | 96, 97, 1, 267 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌)) |
269 | | itgsubst.l |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿) |
270 | | ditgeq2 23613 |
. . . . . . . . 9
⊢ (𝐴 = 𝐿 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
271 | 269, 270 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
272 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) |
273 | | ditgex 23616 |
. . . . . . . 8
⊢
⨜[𝑀 →
𝐿]𝐶 d𝑢 ∈ V |
274 | 271, 272,
273 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑌 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
275 | 268, 274 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
276 | 266, 275 | eqtr3d 2658 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
277 | 265 | fveq1d 6193 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) |
278 | | itgsubst.k |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾) |
279 | | ditgeq2 23613 |
. . . . . . . . 9
⊢ (𝐴 = 𝐾 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
280 | 278, 279 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
281 | | ditgex 23616 |
. . . . . . . 8
⊢
⨜[𝑀 →
𝐾]𝐶 d𝑢 ∈ V |
282 | 280, 272,
281 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑋 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
283 | 99, 282 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
284 | 277, 283 | eqtr3d 2658 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
285 | 276, 284 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢)) |
286 | | lbicc2 12288 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁)) |
287 | 108, 42, 114, 286 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁)) |
288 | 258 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁)) |
289 | 278 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐾 ∈ (𝑀[,]𝑁))) |
290 | 289 | rspcv 3305 |
. . . . . . 7
⊢ (𝑋 ∈ (𝑋[,]𝑌) → (∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁) → 𝐾 ∈ (𝑀[,]𝑁))) |
291 | 99, 288, 290 | sylc 65 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝑀[,]𝑁)) |
292 | 269 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐿 ∈ (𝑀[,]𝑁))) |
293 | 292 | rspcv 3305 |
. . . . . . 7
⊢ (𝑌 ∈ (𝑋[,]𝑌) → (∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁) → 𝐿 ∈ (𝑀[,]𝑁))) |
294 | 268, 288,
293 | sylc 65 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ (𝑀[,]𝑁)) |
295 | 44, 41, 287, 291, 294, 60, 76 | ditgsplit 23625 |
. . . . 5
⊢ (𝜑 → ⨜[𝑀 → 𝐿]𝐶 d𝑢 = (⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢)) |
296 | 295 | oveq1d 6665 |
. . . 4
⊢ (𝜑 → (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢)) |
297 | 44, 41, 287, 291, 60, 76 | ditgcl 23622 |
. . . . 5
⊢ (𝜑 → ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ ℂ) |
298 | 44, 41, 291, 294, 60, 76 | ditgcl 23622 |
. . . . 5
⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 ∈ ℂ) |
299 | 297, 298 | pncan2d 10394 |
. . . 4
⊢ (𝜑 → ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ⨜[𝐾 → 𝐿]𝐶 d𝑢) |
300 | 285, 296,
299 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = ⨜[𝐾 → 𝐿]𝐶 d𝑢) |
301 | 240, 257,
300 | 3eqtr3d 2664 |
. 2
⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥 = ⨜[𝐾 → 𝐿]𝐶 d𝑢) |
302 | 2, 301 | eqtr2d 2657 |
1
⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥) |