Proof of Theorem itgsbtaddcnst
Step | Hyp | Ref
| Expression |
1 | | itgsbtaddcnst.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | itgsbtaddcnst.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | itgsbtaddcnst.aleb |
. . 3
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
4 | 1, 2 | iccssred 38574 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
5 | 4 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℝ) |
6 | 5 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℂ) |
7 | | itgsbtaddcnst.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) |
8 | 7 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℂ) |
10 | 6, 9 | negsubd 10277 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 + -𝑋) = (𝑡 − 𝑋)) |
11 | 10 | eqcomd 2616 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) = (𝑡 + -𝑋)) |
12 | 11 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋))) |
13 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
14 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ) |
15 | 13, 14 | resubcld 10337 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴 − 𝑋) ∈ ℝ) |
16 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
17 | 16, 14 | resubcld 10337 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐵 − 𝑋) ∈ ℝ) |
18 | 5, 14 | resubcld 10337 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ∈ ℝ) |
19 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (𝐴[,]𝐵)) |
20 | 1, 2 | jca 553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
21 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
22 | | elicc2 12109 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑡 ∈ (𝐴[,]𝐵) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴[,]𝐵) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵))) |
24 | 19, 23 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵)) |
25 | 24 | simp2d 1067 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑡) |
26 | 13, 5, 14, 25 | lesub1dd 10522 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴 − 𝑋) ≤ (𝑡 − 𝑋)) |
27 | 24 | simp3d 1068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ≤ 𝐵) |
28 | 5, 16, 14, 27 | lesub1dd 10522 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ≤ (𝐵 − 𝑋)) |
29 | 15, 17, 18, 26, 28 | eliccd 38573 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
30 | | eqid 2610 |
. . . . . . 7
⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) |
31 | 29, 30 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
32 | 12, 31 | feq1dd 38341 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
33 | 1, 7 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ) |
34 | 2, 7 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ) |
35 | 33, 34 | iccssred 38574 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ⊆ ℝ) |
36 | | ax-resscn 9872 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
37 | 35, 36 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ⊆ ℂ) |
38 | 4, 36 | syl6ss 3580 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
39 | 38 | resmptd 5371 |
. . . . . . . 8
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ↾ (𝐴[,]𝐵)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋))) |
40 | | ssid 3587 |
. . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ |
41 | | cncfmptid 22523 |
. . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)) |
42 | 40, 40, 41 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ) |
43 | 42 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)) |
44 | 40 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ℂ
⊆ ℂ) |
45 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → 𝑋 ∈
ℂ) |
46 | 44, 45, 44 | constcncfg 38756 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑋) ∈ (ℂ–cn→ℂ)) |
47 | 43, 46 | subcncf 38754 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ∈ (ℂ–cn→ℂ)) |
48 | 8, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ∈ (ℂ–cn→ℂ)) |
49 | | rescncf 22508 |
. . . . . . . . 9
⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ∈ (ℂ–cn→ℂ) → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
50 | 38, 48, 49 | sylc 63 |
. . . . . . . 8
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
51 | 39, 50 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
52 | 12, 51 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
53 | | cncffvrn 22509 |
. . . . . 6
⊢ ((((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋))) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
54 | 37, 52, 53 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋))) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
55 | 32, 54 | mpbird 246 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
56 | 12, 55 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
57 | | eqid 2610 |
. . . . 5
⊢ (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) |
58 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑋 ∈ ℂ) |
59 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑠 ∈ ℂ) |
60 | 58, 59 | addcomd 10117 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → (𝑋 + 𝑠) = (𝑠 + 𝑋)) |
61 | 60 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋))) |
62 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) |
63 | 62 | addccncf 22527 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ)) |
64 | 8, 63 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ)) |
65 | 61, 64 | eqeltrd 2688 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ)) |
66 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐴 ∈ ℝ) |
67 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐵 ∈ ℝ) |
68 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑋 ∈ ℝ) |
69 | 35 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑠 ∈ ℝ) |
70 | 68, 69 | readdcld 9948 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑠) ∈ ℝ) |
71 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
72 | 33 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ∈ ℝ) |
73 | 34 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ) |
74 | | elicc2 12109 |
. . . . . . . . . 10
⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ) → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↔ (𝑠 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑠 ∧ 𝑠 ≤ (𝐵 − 𝑋)))) |
75 | 72, 73, 74 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↔ (𝑠 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑠 ∧ 𝑠 ≤ (𝐵 − 𝑋)))) |
76 | 71, 75 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑠 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑠 ∧ 𝑠 ≤ (𝐵 − 𝑋))) |
77 | 76 | simp2d 1067 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ≤ 𝑠) |
78 | 66, 68, 69 | lesubadd2d 10505 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → ((𝐴 − 𝑋) ≤ 𝑠 ↔ 𝐴 ≤ (𝑋 + 𝑠))) |
79 | 77, 78 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐴 ≤ (𝑋 + 𝑠)) |
80 | 76 | simp3d 1068 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑠 ≤ (𝐵 − 𝑋)) |
81 | 68, 69, 67 | leaddsub2d 10508 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → ((𝑋 + 𝑠) ≤ 𝐵 ↔ 𝑠 ≤ (𝐵 − 𝑋))) |
82 | 80, 81 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑠) ≤ 𝐵) |
83 | 66, 67, 70, 79, 82 | eliccd 38573 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑠) ∈ (𝐴[,]𝐵)) |
84 | 57, 65, 37, 38, 83 | cncfmptssg 38755 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝑋 + 𝑠)) ∈ (((𝐴 − 𝑋)[,](𝐵 − 𝑋))–cn→(𝐴[,]𝐵))) |
85 | | itgsbtaddcnst.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
86 | 84, 85 | cncfcompt 38768 |
. . 3
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝐴 − 𝑋)[,](𝐵 − 𝑋))–cn→ℂ)) |
87 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
88 | | ioosscn 38563 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ |
89 | | cncfmptc 22522 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
90 | 87, 88, 40, 89 | mp3an 1416 |
. . . . 5
⊢ (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ) |
91 | 90 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
92 | | fconstmpt 5085 |
. . . . 5
⊢ ((𝐴(,)𝐵) × {1}) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) |
93 | | ioombl 23140 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
94 | 93 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
95 | | volioo 38840 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
96 | 1, 2, 3, 95 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
97 | 2, 1 | resubcld 10337 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
98 | 96, 97 | eqeltrd 2688 |
. . . . . 6
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
99 | | 1cnd 9935 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) |
100 | | iblconst 23390 |
. . . . . 6
⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ 1 ∈ ℂ)
→ ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
101 | 94, 98, 99, 100 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
102 | 92, 101 | syl5eqelr 2693 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈
𝐿1) |
103 | 91, 102 | elind 3760 |
. . 3
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈ (((𝐴(,)𝐵)–cn→ℂ) ∩
𝐿1)) |
104 | 36 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ⊆
ℂ) |
105 | 18 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ∈ ℂ) |
106 | | eqid 2610 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
107 | 106 | tgioo2 22414 |
. . . . 5
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
108 | | iccntr 22432 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
109 | 20, 108 | syl 17 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
110 | 104, 4, 105, 107, 106, 109 | dvmptntr 23540 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋))) = (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡 − 𝑋)))) |
111 | | reelprrecn 9907 |
. . . . . 6
⊢ ℝ
∈ {ℝ, ℂ} |
112 | 111 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
113 | | ioossre 12106 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℝ |
114 | 113 | sseli 3564 |
. . . . . . 7
⊢ (𝑡 ∈ (𝐴(,)𝐵) → 𝑡 ∈ ℝ) |
115 | 114 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ ℝ) |
116 | 115 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ ℂ) |
117 | | 1cnd 9935 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 1 ∈ ℂ) |
118 | 104 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ) |
119 | | 1cnd 9935 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 1 ∈
ℂ) |
120 | 112 | dvmptid 23526 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1)) |
121 | 113 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
122 | | iooretop 22379 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
123 | 122 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran
(,))) |
124 | 112, 118,
119, 120, 121, 107, 106, 123 | dvmptres 23532 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ 𝑡)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1)) |
125 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℂ) |
126 | | 0cnd 9912 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 0 ∈ ℂ) |
127 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑋 ∈ ℂ) |
128 | | 0cnd 9912 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ∈
ℂ) |
129 | 112, 8 | dvmptc 23527 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 𝑋)) = (𝑡 ∈ ℝ ↦ 0)) |
130 | 112, 127,
128, 129, 121, 107, 106, 123 | dvmptres 23532 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ 𝑋)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 0)) |
131 | 112, 116,
117, 124, 125, 126, 130 | dvmptsub 23536 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡 − 𝑋))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ (1 − 0))) |
132 | 117 | subid1d 10260 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (1 − 0) =
1) |
133 | 132 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ (1 − 0)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1)) |
134 | 110, 131,
133 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1)) |
135 | | oveq2 6557 |
. . . 4
⊢ (𝑠 = (𝑡 − 𝑋) → (𝑋 + 𝑠) = (𝑋 + (𝑡 − 𝑋))) |
136 | 135 | fveq2d 6107 |
. . 3
⊢ (𝑠 = (𝑡 − 𝑋) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑡 − 𝑋)))) |
137 | | oveq1 6556 |
. . 3
⊢ (𝑡 = 𝐴 → (𝑡 − 𝑋) = (𝐴 − 𝑋)) |
138 | | oveq1 6556 |
. . 3
⊢ (𝑡 = 𝐵 → (𝑡 − 𝑋) = (𝐵 − 𝑋)) |
139 | 1, 2, 3, 56, 86, 103, 134, 136, 137, 138, 33, 34 | itgsubsticc 38868 |
. 2
⊢ (𝜑 → ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐹‘(𝑋 + 𝑠)) d𝑠 = ⨜[𝐴 → 𝐵]((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) d𝑡) |
140 | 125, 116 | pncan3d 10274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝑋 + (𝑡 − 𝑋)) = 𝑡) |
141 | 140 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + (𝑡 − 𝑋))) = (𝐹‘𝑡)) |
142 | 141 | oveq1d 6564 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) = ((𝐹‘𝑡) · 1)) |
143 | | cncff 22504 |
. . . . . . . 8
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
144 | 85, 143 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
145 | 144 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
146 | | ioossicc 12130 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
147 | 146 | sseli 3564 |
. . . . . . 7
⊢ (𝑡 ∈ (𝐴(,)𝐵) → 𝑡 ∈ (𝐴[,]𝐵)) |
148 | 147 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ (𝐴[,]𝐵)) |
149 | 145, 148 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑡) ∈ ℂ) |
150 | 149 | mulid1d 9936 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑡) · 1) = (𝐹‘𝑡)) |
151 | 142, 150 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) = (𝐹‘𝑡)) |
152 | 3, 151 | ditgeq3d 38856 |
. 2
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) d𝑡 = ⨜[𝐴 → 𝐵](𝐹‘𝑡) d𝑡) |
153 | 139, 152 | eqtrd 2644 |
1
⊢ (𝜑 → ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐹‘(𝑋 + 𝑠)) d𝑠 = ⨜[𝐴 → 𝐵](𝐹‘𝑡) d𝑡) |