Proof of Theorem itgsbtaddcnst
Step | Hyp | Ref
| Expression |
1 | | itgsbtaddcnst.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | itgsbtaddcnst.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | itgsbtaddcnst.aleb |
. . 3
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
4 | 1, 2 | iccssred 41656 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
5 | 4 | sselda 3964 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℝ) |
6 | 5 | recnd 10657 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℂ) |
7 | | itgsbtaddcnst.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) |
8 | 7 | recnd 10657 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
9 | 8 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℂ) |
10 | 6, 9 | negsubd 10991 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 + -𝑋) = (𝑡 − 𝑋)) |
11 | 10 | eqcomd 2824 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) = (𝑡 + -𝑋)) |
12 | 11 | mpteq2dva 5152 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋))) |
13 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
14 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ) |
15 | 13, 14 | resubcld 11056 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴 − 𝑋) ∈ ℝ) |
16 | 2 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
17 | 16, 14 | resubcld 11056 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐵 − 𝑋) ∈ ℝ) |
18 | 5, 14 | resubcld 11056 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ∈ ℝ) |
19 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (𝐴[,]𝐵)) |
20 | 1, 2 | jca 512 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
21 | 20 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
22 | | elicc2 12789 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑡 ∈ (𝐴[,]𝐵) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴[,]𝐵) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵))) |
24 | 19, 23 | mpbid 233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵)) |
25 | 24 | simp2d 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑡) |
26 | 13, 5, 14, 25 | lesub1dd 11244 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴 − 𝑋) ≤ (𝑡 − 𝑋)) |
27 | 24 | simp3d 1136 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ≤ 𝐵) |
28 | 5, 16, 14, 27 | lesub1dd 11244 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ≤ (𝐵 − 𝑋)) |
29 | 15, 17, 18, 26, 28 | eliccd 41655 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
30 | 29 | fmpttd 6871 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
31 | 12, 30 | feq1dd 41299 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
32 | 1, 7 | resubcld 11056 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ) |
33 | 2, 7 | resubcld 11056 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ) |
34 | 32, 33 | iccssred 41656 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ⊆ ℝ) |
35 | | ax-resscn 10582 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
36 | 34, 35 | sstrdi 3976 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ⊆ ℂ) |
37 | 4, 35 | sstrdi 3976 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
38 | 37 | resmptd 5901 |
. . . . . . . 8
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ↾ (𝐴[,]𝐵)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋))) |
39 | | ssid 3986 |
. . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ |
40 | | cncfmptid 23447 |
. . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)) |
41 | 39, 39, 40 | mp2an 688 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ) |
42 | 41 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)) |
43 | 39 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ℂ
⊆ ℂ) |
44 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → 𝑋 ∈
ℂ) |
45 | 43, 44, 43 | constcncfg 42030 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑋) ∈ (ℂ–cn→ℂ)) |
46 | 42, 45 | subcncf 42028 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ∈ (ℂ–cn→ℂ)) |
47 | 8, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ∈ (ℂ–cn→ℂ)) |
48 | | rescncf 23432 |
. . . . . . . . 9
⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ∈ (ℂ–cn→ℂ) → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
49 | 37, 47, 48 | sylc 65 |
. . . . . . . 8
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
50 | 38, 49 | eqeltrrd 2911 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
51 | 12, 50 | eqeltrrd 2911 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
52 | | cncffvrn 23433 |
. . . . . 6
⊢ ((((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋))) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
53 | 36, 51, 52 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋))) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
54 | 31, 53 | mpbird 258 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
55 | 12, 54 | eqeltrd 2910 |
. . 3
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
56 | | eqid 2818 |
. . . . 5
⊢ (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) |
57 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑋 ∈ ℂ) |
58 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑠 ∈ ℂ) |
59 | 57, 58 | addcomd 10830 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → (𝑋 + 𝑠) = (𝑠 + 𝑋)) |
60 | 59 | mpteq2dva 5152 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋))) |
61 | | eqid 2818 |
. . . . . . . 8
⊢ (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) |
62 | 61 | addccncf 23451 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ)) |
63 | 8, 62 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ)) |
64 | 60, 63 | eqeltrd 2910 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ)) |
65 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐴 ∈ ℝ) |
66 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐵 ∈ ℝ) |
67 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑋 ∈ ℝ) |
68 | 34 | sselda 3964 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑠 ∈ ℝ) |
69 | 67, 68 | readdcld 10658 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑠) ∈ ℝ) |
70 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
71 | 32 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ∈ ℝ) |
72 | 33 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ) |
73 | | elicc2 12789 |
. . . . . . . . . 10
⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ) → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↔ (𝑠 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑠 ∧ 𝑠 ≤ (𝐵 − 𝑋)))) |
74 | 71, 72, 73 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↔ (𝑠 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑠 ∧ 𝑠 ≤ (𝐵 − 𝑋)))) |
75 | 70, 74 | mpbid 233 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑠 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑠 ∧ 𝑠 ≤ (𝐵 − 𝑋))) |
76 | 75 | simp2d 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ≤ 𝑠) |
77 | 65, 67, 68 | lesubadd2d 11227 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → ((𝐴 − 𝑋) ≤ 𝑠 ↔ 𝐴 ≤ (𝑋 + 𝑠))) |
78 | 76, 77 | mpbid 233 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐴 ≤ (𝑋 + 𝑠)) |
79 | 75 | simp3d 1136 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑠 ≤ (𝐵 − 𝑋)) |
80 | 67, 68, 66 | leaddsub2d 11230 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → ((𝑋 + 𝑠) ≤ 𝐵 ↔ 𝑠 ≤ (𝐵 − 𝑋))) |
81 | 79, 80 | mpbird 258 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑠) ≤ 𝐵) |
82 | 65, 66, 69, 78, 81 | eliccd 41655 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑠) ∈ (𝐴[,]𝐵)) |
83 | 56, 64, 36, 37, 82 | cncfmptssg 42029 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝑋 + 𝑠)) ∈ (((𝐴 − 𝑋)[,](𝐵 − 𝑋))–cn→(𝐴[,]𝐵))) |
84 | | itgsbtaddcnst.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
85 | 83, 84 | cncfcompt 42042 |
. . 3
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝐴 − 𝑋)[,](𝐵 − 𝑋))–cn→ℂ)) |
86 | | ax-1cn 10583 |
. . . . . 6
⊢ 1 ∈
ℂ |
87 | | ioosscn 41645 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ |
88 | | cncfmptc 23446 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
89 | 86, 87, 39, 88 | mp3an 1452 |
. . . . 5
⊢ (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ) |
90 | 89 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
91 | | fconstmpt 5607 |
. . . . 5
⊢ ((𝐴(,)𝐵) × {1}) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) |
92 | | ioombl 24093 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
93 | 92 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
94 | | volioo 24097 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
95 | 1, 2, 3, 94 | syl3anc 1363 |
. . . . . . 7
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
96 | 2, 1 | resubcld 11056 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
97 | 95, 96 | eqeltrd 2910 |
. . . . . 6
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
98 | | 1cnd 10624 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) |
99 | | iblconst 24345 |
. . . . . 6
⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ 1 ∈ ℂ)
→ ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
100 | 93, 97, 98, 99 | syl3anc 1363 |
. . . . 5
⊢ (𝜑 → ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
101 | 91, 100 | eqeltrrid 2915 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈
𝐿1) |
102 | 90, 101 | elind 4168 |
. . 3
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈ (((𝐴(,)𝐵)–cn→ℂ) ∩
𝐿1)) |
103 | 35 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ⊆
ℂ) |
104 | 18 | recnd 10657 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ∈ ℂ) |
105 | | eqid 2818 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
106 | 105 | tgioo2 23338 |
. . . . 5
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
107 | | iccntr 23356 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
108 | 20, 107 | syl 17 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
109 | 103, 4, 104, 106, 105, 108 | dvmptntr 24495 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋))) = (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡 − 𝑋)))) |
110 | | reelprrecn 10617 |
. . . . . 6
⊢ ℝ
∈ {ℝ, ℂ} |
111 | 110 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
112 | | ioossre 12786 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℝ |
113 | 112 | sseli 3960 |
. . . . . . 7
⊢ (𝑡 ∈ (𝐴(,)𝐵) → 𝑡 ∈ ℝ) |
114 | 113 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ ℝ) |
115 | 114 | recnd 10657 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ ℂ) |
116 | | 1cnd 10624 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 1 ∈ ℂ) |
117 | 103 | sselda 3964 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ) |
118 | | 1cnd 10624 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 1 ∈
ℂ) |
119 | 111 | dvmptid 24481 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1)) |
120 | 112 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
121 | | iooretop 23301 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
122 | 121 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran
(,))) |
123 | 111, 117,
118, 119, 120, 106, 105, 122 | dvmptres 24487 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ 𝑡)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1)) |
124 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℂ) |
125 | | 0cnd 10622 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 0 ∈ ℂ) |
126 | 8 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑋 ∈ ℂ) |
127 | | 0cnd 10622 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ∈
ℂ) |
128 | 111, 8 | dvmptc 24482 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 𝑋)) = (𝑡 ∈ ℝ ↦ 0)) |
129 | 111, 126,
127, 128, 120, 106, 105, 122 | dvmptres 24487 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ 𝑋)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 0)) |
130 | 111, 115,
116, 123, 124, 125, 129 | dvmptsub 24491 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡 − 𝑋))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ (1 − 0))) |
131 | 116 | subid1d 10974 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (1 − 0) =
1) |
132 | 131 | mpteq2dva 5152 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ (1 − 0)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1)) |
133 | 109, 130,
132 | 3eqtrd 2857 |
. . 3
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1)) |
134 | | oveq2 7153 |
. . . 4
⊢ (𝑠 = (𝑡 − 𝑋) → (𝑋 + 𝑠) = (𝑋 + (𝑡 − 𝑋))) |
135 | 134 | fveq2d 6667 |
. . 3
⊢ (𝑠 = (𝑡 − 𝑋) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑡 − 𝑋)))) |
136 | | oveq1 7152 |
. . 3
⊢ (𝑡 = 𝐴 → (𝑡 − 𝑋) = (𝐴 − 𝑋)) |
137 | | oveq1 7152 |
. . 3
⊢ (𝑡 = 𝐵 → (𝑡 − 𝑋) = (𝐵 − 𝑋)) |
138 | 1, 2, 3, 55, 85, 102, 133, 135, 136, 137, 32, 33 | itgsubsticc 42137 |
. 2
⊢ (𝜑 → ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐹‘(𝑋 + 𝑠)) d𝑠 = ⨜[𝐴 → 𝐵]((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) d𝑡) |
139 | 124, 115 | pncan3d 10988 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝑋 + (𝑡 − 𝑋)) = 𝑡) |
140 | 139 | fveq2d 6667 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + (𝑡 − 𝑋))) = (𝐹‘𝑡)) |
141 | 140 | oveq1d 7160 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) = ((𝐹‘𝑡) · 1)) |
142 | | cncff 23428 |
. . . . . . . 8
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
143 | 84, 142 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
144 | 143 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
145 | | ioossicc 12810 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
146 | 145 | sseli 3960 |
. . . . . . 7
⊢ (𝑡 ∈ (𝐴(,)𝐵) → 𝑡 ∈ (𝐴[,]𝐵)) |
147 | 146 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ (𝐴[,]𝐵)) |
148 | 144, 147 | ffvelrnd 6844 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑡) ∈ ℂ) |
149 | 148 | mulid1d 10646 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑡) · 1) = (𝐹‘𝑡)) |
150 | 141, 149 | eqtrd 2853 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) = (𝐹‘𝑡)) |
151 | 3, 150 | ditgeq3d 42125 |
. 2
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) d𝑡 = ⨜[𝐴 → 𝐵](𝐹‘𝑡) d𝑡) |
152 | 138, 151 | eqtrd 2853 |
1
⊢ (𝜑 → ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐹‘(𝑋 + 𝑠)) d𝑠 = ⨜[𝐴 → 𝐵](𝐹‘𝑡) d𝑡) |