| Step | Hyp | Ref
| Expression |
| 1 | | itgsubst.le |
. . 3
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
| 2 | 1 | ditgpos 25891 |
. 2
⊢ (𝜑 → ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
| 3 | | itgsubst.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 4 | | itgsubst.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 5 | | ax-resscn 11212 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
| 6 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 7 | | iccssre 13469 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ) |
| 8 | 3, 4, 7 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
| 9 | | itgsubst.cl2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁)) |
| 10 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) |
| 11 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) |
| 12 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → (𝑀(,)𝑣) = (𝑀(,)𝐴)) |
| 13 | | itgeq1 25808 |
. . . . . . . . . . . 12
⊢ ((𝑀(,)𝑣) = (𝑀(,)𝐴) → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
| 14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐴 → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
| 15 | 9, 10, 11, 14 | fmptco 7149 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
| 16 | 9 | fmpttd 7135 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)) |
| 17 | | ioossicc 13473 |
. . . . . . . . . . . . . . 15
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
| 18 | | itgsubst.z |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑍 ∈
ℝ*) |
| 19 | | itgsubst.w |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑊 ∈
ℝ*) |
| 20 | | itgsubst.m |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊)) |
| 21 | | eliooord 13446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊)) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊)) |
| 23 | 22 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑍 < 𝑀) |
| 24 | | itgsubst.n |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊)) |
| 25 | | eliooord 13446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊)) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊)) |
| 27 | 26 | simprd 495 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 < 𝑊) |
| 28 | | iccssioo 13456 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑍 ∈ ℝ*
∧ 𝑊 ∈
ℝ*) ∧ (𝑍 < 𝑀 ∧ 𝑁 < 𝑊)) → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊)) |
| 29 | 18, 19, 23, 27, 28 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊)) |
| 30 | 17, 29 | sstrid 3995 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑍(,)𝑊)) |
| 31 | | ioossre 13448 |
. . . . . . . . . . . . . . . 16
⊢ (𝑍(,)𝑊) ⊆ ℝ |
| 32 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℝ) |
| 33 | 32, 5 | sstrdi 3996 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℂ) |
| 34 | 30, 33 | sstrd 3994 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℂ) |
| 35 | | itgsubst.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) |
| 36 | | cncfcdm 24924 |
. . . . . . . . . . . . 13
⊢ (((𝑀(,)𝑁) ⊆ ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))) |
| 37 | 34, 35, 36 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))) |
| 38 | 16, 37 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁))) |
| 39 | 17 | sseli 3979 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (𝑀(,)𝑁) → 𝑣 ∈ (𝑀[,]𝑁)) |
| 40 | 31, 24 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 41 | 40 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
| 42 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑁 ∈
ℝ*) |
| 43 | 31, 20 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 44 | | elicc2 13452 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))) |
| 45 | 43, 40, 44 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))) |
| 46 | 45 | biimpa 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)) |
| 47 | 46 | simp3d 1145 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑣 ≤ 𝑁) |
| 48 | | iooss2 13423 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℝ*
∧ 𝑣 ≤ 𝑁) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁)) |
| 49 | 42, 47, 48 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁)) |
| 50 | 49 | sselda 3983 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝑢 ∈ (𝑀(,)𝑁)) |
| 51 | 30 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝑢 ∈ (𝑍(,)𝑊)) |
| 52 | | itgsubst.c |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ)) |
| 53 | | cncff 24919 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ) |
| 54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ) |
| 55 | 54 | fvmptelcdm 7133 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑍(,)𝑊)) → 𝐶 ∈ ℂ) |
| 56 | 51, 55 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ) |
| 57 | 56 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ) |
| 58 | 50, 57 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝐶 ∈ ℂ) |
| 59 | | ioombl 25600 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀(,)𝑣) ∈ dom vol |
| 60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ∈ dom vol) |
| 61 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)) |
| 62 | | ioombl 25600 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀(,)𝑁) ∈ dom vol |
| 63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀(,)𝑁) ∈ dom vol) |
| 64 | 29 | sselda 3983 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝑢 ∈ (𝑍(,)𝑊)) |
| 65 | 64, 55 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ) |
| 66 | 29 | resmptd 6058 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) = (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶)) |
| 67 | | rescncf 24923 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀[,]𝑁) ⊆ (𝑍(,)𝑊) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))) |
| 68 | 29, 52, 67 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
| 69 | 66, 68 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
| 70 | | cniccibl 25876 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈
𝐿1) |
| 71 | 43, 40, 69, 70 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈
𝐿1) |
| 72 | 61, 63, 65, 71 | iblss 25840 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈
𝐿1) |
| 73 | 72 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈
𝐿1) |
| 74 | 49, 60, 57, 73 | iblss 25840 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑣) ↦ 𝐶) ∈
𝐿1) |
| 75 | 58, 74 | itgcl 25819 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ) |
| 76 | 39, 75 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ) |
| 77 | 76 | fmpttd 7135 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ) |
| 78 | 30, 31 | sstrdi 3996 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℝ) |
| 79 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑢 → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) = ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢)) |
| 80 | | nffvmpt1 6917 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑢((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) |
| 81 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) |
| 82 | 79, 80, 81 | cbvitg 25811 |
. . . . . . . . . . . . . . . . . 18
⊢
∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 |
| 83 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) |
| 84 | 83 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 ∈ (𝑀(,)𝑁) ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶) |
| 85 | 50, 58, 84 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶) |
| 86 | 85 | itgeq2dv 25817 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 = ∫(𝑀(,)𝑣)𝐶 d𝑢) |
| 87 | 82, 86 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)𝐶 d𝑢) |
| 88 | 87 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) |
| 89 | 88 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))) |
| 90 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) |
| 91 | 3 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
| 92 | 4 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
| 93 | | lbicc2 13504 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌)) |
| 94 | 91, 92, 1, 93 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌)) |
| 95 | | n0i 4340 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑋 ∈ (𝑋[,]𝑌) → ¬ (𝑋[,]𝑌) = ∅) |
| 96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ (𝑋[,]𝑌) = ∅) |
| 97 | | feq3 6718 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀(,)𝑁) = ∅ → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅)) |
| 98 | 16, 97 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅)) |
| 99 | | f00 6790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ ↔ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = ∅ ∧ (𝑋[,]𝑌) = ∅)) |
| 100 | 99 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ → (𝑋[,]𝑌) = ∅) |
| 101 | 98, 100 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑋[,]𝑌) = ∅)) |
| 102 | 96, 101 | mtod 198 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ (𝑀(,)𝑁) = ∅) |
| 103 | 43 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
| 104 | | ioo0 13412 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ*) → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀)) |
| 105 | 103, 41, 104 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀)) |
| 106 | 102, 105 | mtbid 324 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ 𝑁 ≤ 𝑀) |
| 107 | 40, 43 | letrid 11413 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁)) |
| 108 | 107 | ord 865 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁)) |
| 109 | 106, 108 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
| 110 | | resmpt 6055 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
| 111 | 17, 110 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) |
| 112 | | rescncf 24923 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ))) |
| 113 | 17, 69, 112 | mpsyl 68 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
| 114 | 111, 113 | eqeltrrid 2846 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
| 115 | 90, 43, 40, 109, 114, 72 | ftc1cn 26084 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
| 116 | 29, 31 | sstrdi 3996 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) |
| 117 | | tgioo4 24826 |
. . . . . . . . . . . . . . . 16
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 118 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 119 | | iccntr 24843 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
| 120 | 43, 40, 119 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
| 121 | 6, 116, 75, 117, 118, 120 | dvmptntr 26009 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))) |
| 122 | 89, 115, 121 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
| 123 | 122 | dmeqd 5916 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
| 124 | 83, 56 | dmmptd 6713 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑀(,)𝑁)) |
| 125 | 123, 124 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) |
| 126 | | dvcn 25957 |
. . . . . . . . . . . 12
⊢
(((ℝ ⊆ ℂ ∧ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ ∧ (𝑀(,)𝑁) ⊆ ℝ) ∧ dom (ℝ D
(𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
| 127 | 6, 77, 78, 125, 126 | syl31anc 1375 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
| 128 | 38, 127 | cncfco 24933 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
| 129 | 15, 128 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
| 130 | | cncff 24919 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ) |
| 131 | 129, 130 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ) |
| 132 | 131 | fvmptelcdm 7133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ) |
| 133 | | iccntr 24843 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌)) |
| 134 | 3, 4, 133 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌)) |
| 135 | 6, 8, 132, 117, 118, 134 | dvmptntr 26009 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))) |
| 136 | | reelprrecn 11247 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
| 137 | 136 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
| 138 | | ioossicc 13473 |
. . . . . . . . 9
⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) |
| 139 | 138 | sseli 3979 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌)) |
| 140 | 139, 9 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝑀(,)𝑁)) |
| 141 | | itgsubst.b |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩
𝐿1)) |
| 142 | | elin 3967 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1) ↔
((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1)) |
| 143 | 141, 142 | sylib 218 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1)) |
| 144 | 143 | simpld 494 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
| 145 | | cncff 24919 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
| 146 | 144, 145 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
| 147 | 146 | fvmptelcdm 7133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ) |
| 148 | 56 | fmpttd 7135 |
. . . . . . . . 9
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ) |
| 149 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑣𝐶 |
| 150 | | nfcsb1v 3923 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢⦋𝑣 / 𝑢⦌𝐶 |
| 151 | | csbeq1a 3913 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑢⦌𝐶) |
| 152 | 149, 150,
151 | cbvmpt 5253 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶) |
| 153 | 152 | fmpt 7130 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
(𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ) |
| 154 | 148, 153 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ) |
| 155 | 154 | r19.21bi 3251 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ) |
| 156 | 31, 5 | sstri 3993 |
. . . . . . . . . 10
⊢ (𝑍(,)𝑊) ⊆ ℂ |
| 157 | | cncff 24919 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) |
| 158 | 35, 157 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) |
| 159 | 158 | fvmptelcdm 7133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑍(,)𝑊)) |
| 160 | 156, 159 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ) |
| 161 | 6, 8, 160, 117, 118, 134 | dvmptntr 26009 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴))) |
| 162 | | itgsubst.da |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
| 163 | 161, 162 | eqtr3d 2779 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
| 164 | 122, 152 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶)) |
| 165 | | csbeq1 3902 |
. . . . . . 7
⊢ (𝑣 = 𝐴 → ⦋𝑣 / 𝑢⦌𝐶 = ⦋𝐴 / 𝑢⦌𝐶) |
| 166 | 137, 137,
140, 147, 76, 155, 163, 164, 14, 165 | dvmptco 26010 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵))) |
| 167 | | nfcvd 2906 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑀(,)𝑁) → Ⅎ𝑢𝐸) |
| 168 | | itgsubst.e |
. . . . . . . . . 10
⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸) |
| 169 | 167, 168 | csbiegf 3932 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑀(,)𝑁) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸) |
| 170 | 140, 169 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸) |
| 171 | 170 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (⦋𝐴 / 𝑢⦌𝐶 · 𝐵) = (𝐸 · 𝐵)) |
| 172 | 171 | mpteq2dva 5242 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
| 173 | 135, 166,
172 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
| 174 | | resmpt 6055 |
. . . . . . . 8
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)) |
| 175 | 138, 174 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) |
| 176 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶)) |
| 177 | 159, 10, 176, 168 | fmptco 7149 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)) |
| 178 | 35, 52 | cncfco 24933 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
| 179 | 177, 178 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
| 180 | | rescncf 24923 |
. . . . . . . 8
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))) |
| 181 | 138, 179,
180 | mpsyl 68 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
| 182 | 175, 181 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
| 183 | 182, 144 | mulcncf 25480 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
| 184 | 173, 183 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
| 185 | | ioombl 25600 |
. . . . . . . 8
⊢ (𝑋(,)𝑌) ∈ dom vol |
| 186 | 185 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol) |
| 187 | | fco 6760 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ) |
| 188 | 54, 158, 187 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ) |
| 189 | 177 | feq1d 6720 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)) |
| 190 | 188, 189 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ) |
| 191 | 190 | fvmptelcdm 7133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐸 ∈ ℂ) |
| 192 | 139, 191 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ) |
| 193 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)) |
| 194 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
| 195 | 186, 192,
147, 193, 194 | offval2 7717 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
| 196 | 173, 195 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))) |
| 197 | 138 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)) |
| 198 | | cniccibl 25876 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈
𝐿1) |
| 199 | 3, 4, 179, 198 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈
𝐿1) |
| 200 | 197, 186,
191, 199 | iblss 25840 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈
𝐿1) |
| 201 | | iblmbf 25802 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿1 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn) |
| 202 | 200, 201 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn) |
| 203 | 143 | simprd 495 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1) |
| 204 | | cniccbdd 25496 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
| 205 | 3, 4, 179, 204 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
| 206 | | ssralv 4052 |
. . . . . . . . . 10
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
| 207 | 138, 206 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
| 208 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) |
| 209 | 208, 192 | dmmptd 6713 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑋(,)𝑌)) |
| 210 | 209 | raleqdv 3326 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
| 211 | 175 | fveq1i 6907 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) |
| 212 | | fvres 6925 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝑋(,)𝑌) → (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) |
| 213 | 211, 212 | eqtr3id 2791 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) |
| 214 | 213 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋(,)𝑌) → (abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) = (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))) |
| 215 | 214 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
| 216 | 215 | ralbiia 3091 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
(𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
| 217 | 210, 216 | bitr2di 288 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
| 218 | 207, 217 | imbitrid 244 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
| 219 | 218 | reximdv 3170 |
. . . . . . 7
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
| 220 | 205, 219 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
| 221 | | bddmulibl 25874 |
. . . . . 6
⊢ (((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1 ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈
𝐿1) |
| 222 | 202, 203,
220, 221 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘f · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈
𝐿1) |
| 223 | 196, 222 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈
𝐿1) |
| 224 | 3, 4, 1, 184, 223, 129 | ftc2 26085 |
. . 3
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋))) |
| 225 | | fveq2 6906 |
. . . . 5
⊢ (𝑡 = 𝑥 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥)) |
| 226 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥ℝ |
| 227 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥
D |
| 228 | | nfmpt1 5250 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) |
| 229 | 226, 227,
228 | nfov 7461 |
. . . . . 6
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
| 230 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥𝑡 |
| 231 | 229, 230 | nffv 6916 |
. . . . 5
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) |
| 232 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) |
| 233 | 225, 231,
232 | cbvitg 25811 |
. . . 4
⊢
∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 |
| 234 | 173 | fveq1d 6908 |
. . . . . 6
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥)) |
| 235 | | ovex 7464 |
. . . . . . 7
⊢ (𝐸 · 𝐵) ∈ V |
| 236 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) |
| 237 | 236 | fvmpt2 7027 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ∧ (𝐸 · 𝐵) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵)) |
| 238 | 235, 237 | mpan2 691 |
. . . . . 6
⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵)) |
| 239 | 234, 238 | sylan9eq 2797 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = (𝐸 · 𝐵)) |
| 240 | 239 | itgeq2dv 25817 |
. . . 4
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
| 241 | 233, 240 | eqtrid 2789 |
. . 3
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
| 242 | 17, 9 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀[,]𝑁)) |
| 243 | | elicc2 13452 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
| 244 | 43, 40, 243 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
| 245 | 244 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
| 246 | 242, 245 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)) |
| 247 | 246 | simp2d 1144 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝑀 ≤ 𝐴) |
| 248 | 247 | ditgpos 25891 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
| 249 | 248 | mpteq2dva 5242 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
| 250 | 249 | fveq1d 6908 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌)) |
| 251 | | ubicc2 13505 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌)) |
| 252 | 91, 92, 1, 251 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌)) |
| 253 | | itgsubst.l |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿) |
| 254 | | ditgeq2 25884 |
. . . . . . . . 9
⊢ (𝐴 = 𝐿 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
| 255 | 253, 254 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
| 256 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) |
| 257 | | ditgex 25887 |
. . . . . . . 8
⊢
⨜[𝑀 →
𝐿]𝐶 d𝑢 ∈ V |
| 258 | 255, 256,
257 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑌 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
| 259 | 252, 258 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
| 260 | 250, 259 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
| 261 | 249 | fveq1d 6908 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) |
| 262 | | itgsubst.k |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾) |
| 263 | | ditgeq2 25884 |
. . . . . . . . 9
⊢ (𝐴 = 𝐾 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
| 264 | 262, 263 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
| 265 | | ditgex 25887 |
. . . . . . . 8
⊢
⨜[𝑀 →
𝐾]𝐶 d𝑢 ∈ V |
| 266 | 264, 256,
265 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑋 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
| 267 | 94, 266 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
| 268 | 261, 267 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
| 269 | 260, 268 | oveq12d 7449 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢)) |
| 270 | | lbicc2 13504 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁)) |
| 271 | 103, 41, 109, 270 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁)) |
| 272 | 262 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐾 ∈ (𝑀[,]𝑁))) |
| 273 | 242 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁)) |
| 274 | 272, 273,
94 | rspcdva 3623 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝑀[,]𝑁)) |
| 275 | 253 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐿 ∈ (𝑀[,]𝑁))) |
| 276 | 275, 273,
252 | rspcdva 3623 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ (𝑀[,]𝑁)) |
| 277 | 43, 40, 271, 274, 276, 56, 72 | ditgsplit 25896 |
. . . . 5
⊢ (𝜑 → ⨜[𝑀 → 𝐿]𝐶 d𝑢 = (⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢)) |
| 278 | 277 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢)) |
| 279 | 43, 40, 271, 274, 56, 72 | ditgcl 25893 |
. . . . 5
⊢ (𝜑 → ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ ℂ) |
| 280 | 43, 40, 274, 276, 56, 72 | ditgcl 25893 |
. . . . 5
⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 ∈ ℂ) |
| 281 | 279, 280 | pncan2d 11622 |
. . . 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𝑥) |