Proof of Theorem itgsbtaddcnst
Step | Hyp | Ref
| Expression |
1 | | itgsbtaddcnst.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | itgsbtaddcnst.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | itgsbtaddcnst.aleb |
. . 3
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
4 | 1, 2 | iccssred 13166 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
5 | 4 | sselda 3921 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℝ) |
6 | 5 | recnd 11003 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℂ) |
7 | | itgsbtaddcnst.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) |
8 | 7 | recnd 11003 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
9 | 8 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℂ) |
10 | 6, 9 | negsubd 11338 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 + -𝑋) = (𝑡 − 𝑋)) |
11 | 10 | eqcomd 2744 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) = (𝑡 + -𝑋)) |
12 | 11 | mpteq2dva 5174 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋))) |
13 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
14 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ) |
15 | 13, 14 | resubcld 11403 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴 − 𝑋) ∈ ℝ) |
16 | 2 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
17 | 16, 14 | resubcld 11403 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐵 − 𝑋) ∈ ℝ) |
18 | 5, 14 | resubcld 11403 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ∈ ℝ) |
19 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (𝐴[,]𝐵)) |
20 | 1, 2 | jca 512 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
21 | 20 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
22 | | elicc2 13144 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑡 ∈ (𝐴[,]𝐵) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴[,]𝐵) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵))) |
24 | 19, 23 | mpbid 231 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝐵)) |
25 | 24 | simp2d 1142 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑡) |
26 | 13, 5, 14, 25 | lesub1dd 11591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴 − 𝑋) ≤ (𝑡 − 𝑋)) |
27 | 24 | simp3d 1143 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ≤ 𝐵) |
28 | 5, 16, 14, 27 | lesub1dd 11591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ≤ (𝐵 − 𝑋)) |
29 | 15, 17, 18, 26, 28 | eliccd 43042 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
30 | 29 | fmpttd 6989 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
31 | 12, 30 | feq1dd 42703 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
32 | 1, 7 | resubcld 11403 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ) |
33 | 2, 7 | resubcld 11403 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ) |
34 | 32, 33 | iccssred 13166 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ⊆ ℝ) |
35 | | ax-resscn 10928 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
36 | 34, 35 | sstrdi 3933 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ⊆ ℂ) |
37 | 4, 35 | sstrdi 3933 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
38 | 37 | resmptd 5948 |
. . . . . . . 8
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ↾ (𝐴[,]𝐵)) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋))) |
39 | | ssid 3943 |
. . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ |
40 | | cncfmptid 24076 |
. . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)) |
41 | 39, 39, 40 | mp2an 689 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ) |
42 | 41 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)) |
43 | 39 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ℂ
⊆ ℂ) |
44 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → 𝑋 ∈
ℂ) |
45 | 43, 44, 43 | constcncfg 43413 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑋) ∈ (ℂ–cn→ℂ)) |
46 | 42, 45 | subcncf 24609 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ∈ (ℂ–cn→ℂ)) |
47 | 8, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ∈ (ℂ–cn→ℂ)) |
48 | | rescncf 24060 |
. . . . . . . . 9
⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ∈ (ℂ–cn→ℂ) → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
49 | 37, 47, 48 | sylc 65 |
. . . . . . . 8
⊢ (𝜑 → ((𝑡 ∈ ℂ ↦ (𝑡 − 𝑋)) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
50 | 38, 49 | eqeltrrd 2840 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
51 | 12, 50 | eqeltrrd 2840 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
52 | | cncffvrn 24061 |
. . . . . 6
⊢ ((((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋))) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
53 | 36, 51, 52 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋))) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)):(𝐴[,]𝐵)⟶((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
54 | 31, 53 | mpbird 256 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 + -𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
55 | 12, 54 | eqeltrd 2839 |
. . 3
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 − 𝑋)[,](𝐵 − 𝑋)))) |
56 | | eqid 2738 |
. . . . 5
⊢ (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) |
57 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑋 ∈ ℂ) |
58 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑠 ∈ ℂ) |
59 | 57, 58 | addcomd 11177 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → (𝑋 + 𝑠) = (𝑠 + 𝑋)) |
60 | 59 | mpteq2dva 5174 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋))) |
61 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) |
62 | 61 | addccncf 24080 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ)) |
63 | 8, 62 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ)) |
64 | 60, 63 | eqeltrd 2839 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ)) |
65 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐴 ∈ ℝ) |
66 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐵 ∈ ℝ) |
67 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑋 ∈ ℝ) |
68 | 34 | sselda 3921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑠 ∈ ℝ) |
69 | 67, 68 | readdcld 11004 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑠) ∈ ℝ) |
70 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) |
71 | 32 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ∈ ℝ) |
72 | 33 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ) |
73 | | elicc2 13144 |
. . . . . . . . . 10
⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ) → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↔ (𝑠 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑠 ∧ 𝑠 ≤ (𝐵 − 𝑋)))) |
74 | 71, 72, 73 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↔ (𝑠 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑠 ∧ 𝑠 ≤ (𝐵 − 𝑋)))) |
75 | 70, 74 | mpbid 231 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑠 ∈ ℝ ∧ (𝐴 − 𝑋) ≤ 𝑠 ∧ 𝑠 ≤ (𝐵 − 𝑋))) |
76 | 75 | simp2d 1142 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ≤ 𝑠) |
77 | 65, 67, 68 | lesubadd2d 11574 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → ((𝐴 − 𝑋) ≤ 𝑠 ↔ 𝐴 ≤ (𝑋 + 𝑠))) |
78 | 76, 77 | mpbid 231 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐴 ≤ (𝑋 + 𝑠)) |
79 | 75 | simp3d 1143 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑠 ≤ (𝐵 − 𝑋)) |
80 | 67, 68, 66 | leaddsub2d 11577 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → ((𝑋 + 𝑠) ≤ 𝐵 ↔ 𝑠 ≤ (𝐵 − 𝑋))) |
81 | 79, 80 | mpbird 256 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑠) ≤ 𝐵) |
82 | 65, 66, 69, 78, 81 | eliccd 43042 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝑋 + 𝑠) ∈ (𝐴[,]𝐵)) |
83 | 56, 64, 36, 37, 82 | cncfmptssg 43412 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝑋 + 𝑠)) ∈ (((𝐴 − 𝑋)[,](𝐵 − 𝑋))–cn→(𝐴[,]𝐵))) |
84 | | itgsbtaddcnst.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
85 | 83, 84 | cncfcompt 43424 |
. . 3
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝐴 − 𝑋)[,](𝐵 − 𝑋))–cn→ℂ)) |
86 | | ax-1cn 10929 |
. . . . . 6
⊢ 1 ∈
ℂ |
87 | | ioosscn 13141 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ |
88 | | cncfmptc 24075 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
89 | 86, 87, 39, 88 | mp3an 1460 |
. . . . 5
⊢ (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ) |
90 | 89 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
91 | | fconstmpt 5649 |
. . . . 5
⊢ ((𝐴(,)𝐵) × {1}) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) |
92 | | ioombl 24729 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
93 | 92 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
94 | | volioo 24733 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
95 | 1, 2, 3, 94 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
96 | 2, 1 | resubcld 11403 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
97 | 95, 96 | eqeltrd 2839 |
. . . . . 6
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
98 | | 1cnd 10970 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) |
99 | | iblconst 24982 |
. . . . . 6
⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ 1 ∈ ℂ)
→ ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
100 | 93, 97, 98, 99 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
101 | 91, 100 | eqeltrrid 2844 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈
𝐿1) |
102 | 90, 101 | elind 4128 |
. . 3
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ 1) ∈ (((𝐴(,)𝐵)–cn→ℂ) ∩
𝐿1)) |
103 | 35 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ⊆
ℂ) |
104 | 18 | recnd 11003 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 − 𝑋) ∈ ℂ) |
105 | | eqid 2738 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
106 | 105 | tgioo2 23966 |
. . . . 5
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
107 | | iccntr 23984 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
108 | 20, 107 | syl 17 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
109 | 103, 4, 104, 106, 105, 108 | dvmptntr 25135 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋))) = (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡 − 𝑋)))) |
110 | | reelprrecn 10963 |
. . . . . 6
⊢ ℝ
∈ {ℝ, ℂ} |
111 | 110 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
112 | | ioossre 13140 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ ℝ |
113 | 112 | sseli 3917 |
. . . . . . 7
⊢ (𝑡 ∈ (𝐴(,)𝐵) → 𝑡 ∈ ℝ) |
114 | 113 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ ℝ) |
115 | 114 | recnd 11003 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ ℂ) |
116 | | 1cnd 10970 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 1 ∈ ℂ) |
117 | 103 | sselda 3921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ) |
118 | | 1cnd 10970 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 1 ∈
ℂ) |
119 | 111 | dvmptid 25121 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1)) |
120 | 112 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
121 | | iooretop 23929 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
122 | 121 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran
(,))) |
123 | 111, 117,
118, 119, 120, 106, 105, 122 | dvmptres 25127 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ 𝑡)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1)) |
124 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℂ) |
125 | | 0cnd 10968 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 0 ∈ ℂ) |
126 | 8 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 𝑋 ∈ ℂ) |
127 | | 0cnd 10968 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ∈
ℂ) |
128 | 111, 8 | dvmptc 25122 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑡 ∈ ℝ ↦ 𝑋)) = (𝑡 ∈ ℝ ↦ 0)) |
129 | 111, 126,
127, 128, 120, 106, 105, 122 | dvmptres 25127 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ 𝑋)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 0)) |
130 | 111, 115,
116, 123, 124, 125, 129 | dvmptsub 25131 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝑡 − 𝑋))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ (1 − 0))) |
131 | 116 | subid1d 11321 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (1 − 0) =
1) |
132 | 131 | mpteq2dva 5174 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ (1 − 0)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1)) |
133 | 109, 130,
132 | 3eqtrd 2782 |
. . 3
⊢ (𝜑 → (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 − 𝑋))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ 1)) |
134 | | oveq2 7283 |
. . . 4
⊢ (𝑠 = (𝑡 − 𝑋) → (𝑋 + 𝑠) = (𝑋 + (𝑡 − 𝑋))) |
135 | 134 | fveq2d 6778 |
. . 3
⊢ (𝑠 = (𝑡 − 𝑋) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑡 − 𝑋)))) |
136 | | oveq1 7282 |
. . 3
⊢ (𝑡 = 𝐴 → (𝑡 − 𝑋) = (𝐴 − 𝑋)) |
137 | | oveq1 7282 |
. . 3
⊢ (𝑡 = 𝐵 → (𝑡 − 𝑋) = (𝐵 − 𝑋)) |
138 | 1, 2, 3, 55, 85, 102, 133, 135, 136, 137, 32, 33 | itgsubsticc 43517 |
. 2
⊢ (𝜑 → ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐹‘(𝑋 + 𝑠)) d𝑠 = ⨜[𝐴 → 𝐵]((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) d𝑡) |
139 | 124, 115 | pncan3d 11335 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝑋 + (𝑡 − 𝑋)) = 𝑡) |
140 | 139 | fveq2d 6778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + (𝑡 − 𝑋))) = (𝐹‘𝑡)) |
141 | 140 | oveq1d 7290 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) = ((𝐹‘𝑡) · 1)) |
142 | | cncff 24056 |
. . . . . . . 8
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
143 | 84, 142 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
144 | 143 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
145 | | ioossicc 13165 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
146 | 145 | sseli 3917 |
. . . . . . 7
⊢ (𝑡 ∈ (𝐴(,)𝐵) → 𝑡 ∈ (𝐴[,]𝐵)) |
147 | 146 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝑡 ∈ (𝐴[,]𝐵)) |
148 | 144, 147 | ffvelrnd 6962 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑡) ∈ ℂ) |
149 | 148 | mulid1d 10992 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑡) · 1) = (𝐹‘𝑡)) |
150 | 141, 149 | eqtrd 2778 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) = (𝐹‘𝑡)) |
151 | 3, 150 | ditgeq3d 43505 |
. 2
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐹‘(𝑋 + (𝑡 − 𝑋))) · 1) d𝑡 = ⨜[𝐴 → 𝐵](𝐹‘𝑡) d𝑡) |
152 | 138, 151 | eqtrd 2778 |
1
⊢ (𝜑 → ⨜[(𝐴 − 𝑋) → (𝐵 − 𝑋)](𝐹‘(𝑋 + 𝑠)) d𝑠 = ⨜[𝐴 → 𝐵](𝐹‘𝑡) d𝑡) |