Step | Hyp | Ref
| Expression |
1 | | itgsubst.le |
. . 3
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
2 | 1 | ditgpos 24753 |
. 2
⊢ (𝜑 → ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
3 | | itgsubst.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) |
4 | | itgsubst.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ℝ) |
5 | | ax-resscn 10786 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℂ) |
7 | | iccssre 13017 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ) |
8 | 3, 4, 7 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
9 | | itgsubst.cl2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁)) |
10 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) |
11 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) |
12 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → (𝑀(,)𝑣) = (𝑀(,)𝐴)) |
13 | | itgeq1 24670 |
. . . . . . . . . . . 12
⊢ ((𝑀(,)𝑣) = (𝑀(,)𝐴) → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐴 → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
15 | 9, 10, 11, 14 | fmptco 6944 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
16 | 9 | fmpttd 6932 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)) |
17 | | ioossicc 13021 |
. . . . . . . . . . . . . . 15
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
18 | | itgsubst.z |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑍 ∈
ℝ*) |
19 | | itgsubst.w |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑊 ∈
ℝ*) |
20 | | itgsubst.m |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊)) |
21 | | eliooord 12994 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊)) |
23 | 22 | simpld 498 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑍 < 𝑀) |
24 | | itgsubst.n |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊)) |
25 | | eliooord 12994 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊)) |
27 | 26 | simprd 499 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 < 𝑊) |
28 | | iccssioo 13004 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑍 ∈ ℝ*
∧ 𝑊 ∈
ℝ*) ∧ (𝑍 < 𝑀 ∧ 𝑁 < 𝑊)) → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊)) |
29 | 18, 19, 23, 27, 28 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊)) |
30 | 17, 29 | sstrid 3912 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑍(,)𝑊)) |
31 | | ioossre 12996 |
. . . . . . . . . . . . . . . 16
⊢ (𝑍(,)𝑊) ⊆ ℝ |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℝ) |
33 | 32, 5 | sstrdi 3913 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℂ) |
34 | 30, 33 | sstrd 3911 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℂ) |
35 | | itgsubst.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) |
36 | | cncffvrn 23795 |
. . . . . . . . . . . . 13
⊢ (((𝑀(,)𝑁) ⊆ ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))) |
37 | 34, 35, 36 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))) |
38 | 16, 37 | mpbird 260 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁))) |
39 | 17 | sseli 3896 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (𝑀(,)𝑁) → 𝑣 ∈ (𝑀[,]𝑁)) |
40 | 31, 24 | sseldi 3899 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℝ) |
41 | 40 | rexrd 10883 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
42 | 41 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑁 ∈
ℝ*) |
43 | 31, 20 | sseldi 3899 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ ℝ) |
44 | | elicc2 13000 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))) |
45 | 43, 40, 44 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))) |
46 | 45 | biimpa 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)) |
47 | 46 | simp3d 1146 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑣 ≤ 𝑁) |
48 | | iooss2 12971 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℝ*
∧ 𝑣 ≤ 𝑁) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁)) |
49 | 42, 47, 48 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁)) |
50 | 49 | sselda 3901 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝑢 ∈ (𝑀(,)𝑁)) |
51 | 30 | sselda 3901 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝑢 ∈ (𝑍(,)𝑊)) |
52 | | itgsubst.c |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ)) |
53 | | cncff 23790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ) |
55 | 54 | fvmptelrn 6930 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑍(,)𝑊)) → 𝐶 ∈ ℂ) |
56 | 51, 55 | syldan 594 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ) |
57 | 56 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ) |
58 | 50, 57 | syldan 594 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝐶 ∈ ℂ) |
59 | | ioombl 24462 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀(,)𝑣) ∈ dom vol |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ∈ dom vol) |
61 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)) |
62 | | ioombl 24462 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀(,)𝑁) ∈ dom vol |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀(,)𝑁) ∈ dom vol) |
64 | 29 | sselda 3901 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝑢 ∈ (𝑍(,)𝑊)) |
65 | 64, 55 | syldan 594 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ) |
66 | 29 | resmptd 5908 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) = (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶)) |
67 | | rescncf 23794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀[,]𝑁) ⊆ (𝑍(,)𝑊) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))) |
68 | 29, 52, 67 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
69 | 66, 68 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
70 | | cniccibl 24738 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈
𝐿1) |
71 | 43, 40, 69, 70 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈
𝐿1) |
72 | 61, 63, 65, 71 | iblss 24702 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈
𝐿1) |
73 | 72 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈
𝐿1) |
74 | 49, 60, 57, 73 | iblss 24702 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑣) ↦ 𝐶) ∈
𝐿1) |
75 | 58, 74 | itgcl 24681 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ) |
76 | 39, 75 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ) |
77 | 76 | fmpttd 6932 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ) |
78 | 30, 31 | sstrdi 3913 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℝ) |
79 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑢 → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) = ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢)) |
80 | | nffvmpt1 6728 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑢((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) |
81 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) |
82 | 79, 80, 81 | cbvitg 24673 |
. . . . . . . . . . . . . . . . . 18
⊢
∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 |
83 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) |
84 | 83 | fvmpt2 6829 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 ∈ (𝑀(,)𝑁) ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶) |
85 | 50, 58, 84 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶) |
86 | 85 | itgeq2dv 24679 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 = ∫(𝑀(,)𝑣)𝐶 d𝑢) |
87 | 82, 86 | syl5eq 2790 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)𝐶 d𝑢) |
88 | 87 | mpteq2dva 5150 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) |
89 | 88 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))) |
90 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) |
91 | 3 | rexrd 10883 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
92 | 4 | rexrd 10883 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
93 | | lbicc2 13052 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌)) |
94 | 91, 92, 1, 93 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌)) |
95 | | n0i 4248 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑋 ∈ (𝑋[,]𝑌) → ¬ (𝑋[,]𝑌) = ∅) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ (𝑋[,]𝑌) = ∅) |
97 | | feq3 6528 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀(,)𝑁) = ∅ → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅)) |
98 | 16, 97 | syl5ibcom 248 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅)) |
99 | | f00 6601 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ ↔ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = ∅ ∧ (𝑋[,]𝑌) = ∅)) |
100 | 99 | simprbi 500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ → (𝑋[,]𝑌) = ∅) |
101 | 98, 100 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑋[,]𝑌) = ∅)) |
102 | 96, 101 | mtod 201 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ (𝑀(,)𝑁) = ∅) |
103 | 43 | rexrd 10883 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
104 | | ioo0 12960 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ*) → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀)) |
105 | 103, 41, 104 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀)) |
106 | 102, 105 | mtbid 327 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ 𝑁 ≤ 𝑀) |
107 | 40, 43 | letrid 10984 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁)) |
108 | 107 | ord 864 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁)) |
109 | 106, 108 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
110 | | resmpt 5905 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
111 | 17, 110 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) |
112 | | rescncf 23794 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ))) |
113 | 17, 69, 112 | mpsyl 68 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
114 | 111, 113 | eqeltrrid 2843 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
115 | 90, 43, 40, 109, 114, 72 | ftc1cn 24940 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
116 | 29, 31 | sstrdi 3913 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) |
117 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
118 | 117 | tgioo2 23700 |
. . . . . . . . . . . . . . . 16
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
119 | | iccntr 23718 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
120 | 43, 40, 119 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
121 | 6, 116, 75, 118, 117, 120 | dvmptntr 24868 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))) |
122 | 89, 115, 121 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
123 | 122 | dmeqd 5774 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
124 | 83, 56 | dmmptd 6523 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑀(,)𝑁)) |
125 | 123, 124 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) |
126 | | dvcn 24818 |
. . . . . . . . . . . 12
⊢
(((ℝ ⊆ ℂ ∧ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ ∧ (𝑀(,)𝑁) ⊆ ℝ) ∧ dom (ℝ D
(𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
127 | 6, 77, 78, 125, 126 | syl31anc 1375 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
128 | 38, 127 | cncfco 23804 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
129 | 15, 128 | eqeltrrd 2839 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
130 | | cncff 23790 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ) |
131 | 129, 130 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ) |
132 | 131 | fvmptelrn 6930 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ) |
133 | | iccntr 23718 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌)) |
134 | 3, 4, 133 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌)) |
135 | 6, 8, 132, 118, 117, 134 | dvmptntr 24868 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))) |
136 | | reelprrecn 10821 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
137 | 136 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
138 | | ioossicc 13021 |
. . . . . . . . 9
⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) |
139 | 138 | sseli 3896 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌)) |
140 | 139, 9 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝑀(,)𝑁)) |
141 | | itgsubst.b |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩
𝐿1)) |
142 | | elin 3882 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1) ↔
((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1)) |
143 | 141, 142 | sylib 221 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1)) |
144 | 143 | simpld 498 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
145 | | cncff 23790 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
146 | 144, 145 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
147 | 146 | fvmptelrn 6930 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ) |
148 | 56 | fmpttd 6932 |
. . . . . . . . 9
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ) |
149 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑣𝐶 |
150 | | nfcsb1v 3836 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢⦋𝑣 / 𝑢⦌𝐶 |
151 | | csbeq1a 3825 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑢⦌𝐶) |
152 | 149, 150,
151 | cbvmpt 5156 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶) |
153 | 152 | fmpt 6927 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
(𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ) |
154 | 148, 153 | sylibr 237 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ) |
155 | 154 | r19.21bi 3130 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ) |
156 | 31, 5 | sstri 3910 |
. . . . . . . . . 10
⊢ (𝑍(,)𝑊) ⊆ ℂ |
157 | | cncff 23790 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) |
158 | 35, 157 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) |
159 | 158 | fvmptelrn 6930 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑍(,)𝑊)) |
160 | 156, 159 | sseldi 3899 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ) |
161 | 6, 8, 160, 118, 117, 134 | dvmptntr 24868 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴))) |
162 | | itgsubst.da |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
163 | 161, 162 | eqtr3d 2779 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
164 | 122, 152 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶)) |
165 | | csbeq1 3814 |
. . . . . . 7
⊢ (𝑣 = 𝐴 → ⦋𝑣 / 𝑢⦌𝐶 = ⦋𝐴 / 𝑢⦌𝐶) |
166 | 137, 137,
140, 147, 76, 155, 163, 164, 14, 165 | dvmptco 24869 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵))) |
167 | | nfcvd 2905 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑀(,)𝑁) → Ⅎ𝑢𝐸) |
168 | | itgsubst.e |
. . . . . . . . . 10
⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸) |
169 | 167, 168 | csbiegf 3845 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑀(,)𝑁) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸) |
170 | 140, 169 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸) |
171 | 170 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (⦋𝐴 / 𝑢⦌𝐶 · 𝐵) = (𝐸 · 𝐵)) |
172 | 171 | mpteq2dva 5150 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
173 | 135, 166,
172 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
174 | | resmpt 5905 |
. . . . . . . 8
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)) |
175 | 138, 174 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) |
176 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶)) |
177 | 159, 10, 176, 168 | fmptco 6944 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)) |
178 | 35, 52 | cncfco 23804 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
179 | 177, 178 | eqeltrrd 2839 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
180 | | rescncf 23794 |
. . . . . . . 8
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))) |
181 | 138, 179,
180 | mpsyl 68 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
182 | 175, 181 | eqeltrrid 2843 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
183 | 182, 144 | mulcncf 24343 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
184 | 173, 183 | eqeltrd 2838 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
185 | | ioombl 24462 |
. . . . . . . 8
⊢ (𝑋(,)𝑌) ∈ dom vol |
186 | 185 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol) |
187 | | fco 6569 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ) |
188 | 54, 158, 187 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ) |
189 | 177 | feq1d 6530 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)) |
190 | 188, 189 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ) |
191 | 190 | fvmptelrn 6930 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐸 ∈ ℂ) |
192 | 139, 191 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ) |
193 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)) |
194 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
195 | 186, 192,
147, 193, 194 | offval2 7488 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
196 | 173, 195 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))) |
197 | 138 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)) |
198 | | cniccibl 24738 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈
𝐿1) |
199 | 3, 4, 179, 198 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈
𝐿1) |
200 | 197, 186,
191, 199 | iblss 24702 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈
𝐿1) |
201 | | iblmbf 24665 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿1 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn) |
202 | 200, 201 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn) |
203 | 143 | simprd 499 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1) |
204 | | cniccbdd 24358 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
205 | 3, 4, 179, 204 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
206 | | ssralv 3967 |
. . . . . . . . . 10
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
207 | 138, 206 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
208 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) |
209 | 208, 192 | dmmptd 6523 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑋(,)𝑌)) |
210 | 209 | raleqdv 3325 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
211 | 175 | fveq1i 6718 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) |
212 | | fvres 6736 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝑋(,)𝑌) → (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) |
213 | 211, 212 | eqtr3id 2792 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) |
214 | 213 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋(,)𝑌) → (abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) = (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))) |
215 | 214 | breq1d 5063 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
216 | 215 | ralbiia 3087 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
(𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
217 | 210, 216 | bitr2di 291 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
218 | 207, 217 | syl5ib 247 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
219 | 218 | reximdv 3192 |
. . . . . . 7
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
220 | 205, 219 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
221 | | bddmulibl 24736 |
. . . . . 6
⊢ (((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1 ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈
𝐿1) |
222 | 202, 203,
220, 221 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈
𝐿1) |
223 | 196, 222 | eqeltrd 2838 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈
𝐿1) |
224 | 3, 4, 1, 184, 223, 129 | ftc2 24941 |
. . 3
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋))) |
225 | | fveq2 6717 |
. . . . 5
⊢ (𝑡 = 𝑥 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥)) |
226 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑥ℝ |
227 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑥
D |
228 | | nfmpt1 5153 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) |
229 | 226, 227,
228 | nfov 7243 |
. . . . . 6
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
230 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑥𝑡 |
231 | 229, 230 | nffv 6727 |
. . . . 5
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) |
232 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) |
233 | 225, 231,
232 | cbvitg 24673 |
. . . 4
⊢
∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 |
234 | 173 | fveq1d 6719 |
. . . . . 6
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥)) |
235 | | ovex 7246 |
. . . . . . 7
⊢ (𝐸 · 𝐵) ∈ V |
236 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) |
237 | 236 | fvmpt2 6829 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ∧ (𝐸 · 𝐵) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵)) |
238 | 235, 237 | mpan2 691 |
. . . . . 6
⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵)) |
239 | 234, 238 | sylan9eq 2798 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = (𝐸 · 𝐵)) |
240 | 239 | itgeq2dv 24679 |
. . . 4
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
241 | 233, 240 | syl5eq 2790 |
. . 3
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
242 | 17, 9 | sseldi 3899 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀[,]𝑁)) |
243 | | elicc2 13000 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
244 | 43, 40, 243 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
245 | 244 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
246 | 242, 245 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)) |
247 | 246 | simp2d 1145 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝑀 ≤ 𝐴) |
248 | 247 | ditgpos 24753 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
249 | 248 | mpteq2dva 5150 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
250 | 249 | fveq1d 6719 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌)) |
251 | | ubicc2 13053 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌)) |
252 | 91, 92, 1, 251 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌)) |
253 | | itgsubst.l |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿) |
254 | | ditgeq2 24746 |
. . . . . . . . 9
⊢ (𝐴 = 𝐿 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
255 | 253, 254 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
256 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) |
257 | | ditgex 24749 |
. . . . . . . 8
⊢
⨜[𝑀 →
𝐿]𝐶 d𝑢 ∈ V |
258 | 255, 256,
257 | fvmpt 6818 |
. . . . . . 7
⊢ (𝑌 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
259 | 252, 258 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
260 | 250, 259 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
261 | 249 | fveq1d 6719 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) |
262 | | itgsubst.k |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾) |
263 | | ditgeq2 24746 |
. . . . . . . . 9
⊢ (𝐴 = 𝐾 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
264 | 262, 263 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
265 | | ditgex 24749 |
. . . . . . . 8
⊢
⨜[𝑀 →
𝐾]𝐶 d𝑢 ∈ V |
266 | 264, 256,
265 | fvmpt 6818 |
. . . . . . 7
⊢ (𝑋 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
267 | 94, 266 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
268 | 261, 267 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
269 | 260, 268 | oveq12d 7231 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢)) |
270 | | lbicc2 13052 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁)) |
271 | 103, 41, 109, 270 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁)) |
272 | 262 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐾 ∈ (𝑀[,]𝑁))) |
273 | 242 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁)) |
274 | 272, 273,
94 | rspcdva 3539 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝑀[,]𝑁)) |
275 | 253 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐿 ∈ (𝑀[,]𝑁))) |
276 | 275, 273,
252 | rspcdva 3539 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ (𝑀[,]𝑁)) |
277 | 43, 40, 271, 274, 276, 56, 72 | ditgsplit 24758 |
. . . . 5
⊢ (𝜑 → ⨜[𝑀 → 𝐿]𝐶 d𝑢 = (⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢)) |
278 | 277 | oveq1d 7228 |
. . . 4
⊢ (𝜑 → (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢)) |
279 | 43, 40, 271, 274, 56, 72 | ditgcl 24755 |
. . . . 5
⊢ (𝜑 → ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ ℂ) |
280 | 43, 40, 274, 276, 56, 72 | ditgcl 24755 |
. . . . 5
⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 ∈ ℂ) |
281 | 279, 280 | pncan2d 11191 |
. . . 4
⊢ (𝜑 → ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ⨜[𝐾 → 𝐿]𝐶 d𝑢) |
282 | 269, 278,
281 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = ⨜[𝐾 → 𝐿]𝐶 d𝑢) |
283 | 224, 241,
282 | 3eqtr3d 2785 |
. 2
⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥 = ⨜[𝐾 → 𝐿]𝐶 d𝑢) |
284 | 2, 283 | eqtr2d 2778 |
1
⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥) |