Step | Hyp | Ref
| Expression |
1 | | itgiccshift.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | itgiccshift.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | itgiccshift.t |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
4 | 3 | rpred 11748 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ℝ) |
5 | | itgiccshift.aleb |
. . . . 5
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
6 | 1, 2, 4, 5 | leadd1dd 10520 |
. . . 4
⊢ (𝜑 → (𝐴 + 𝑇) ≤ (𝐵 + 𝑇)) |
7 | 6 | ditgpos 23426 |
. . 3
⊢ (𝜑 → ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐺‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)(,)(𝐵 + 𝑇))(𝐺‘𝑥) d𝑥) |
8 | 1, 4 | readdcld 9948 |
. . . 4
⊢ (𝜑 → (𝐴 + 𝑇) ∈ ℝ) |
9 | 2, 4 | readdcld 9948 |
. . . 4
⊢ (𝜑 → (𝐵 + 𝑇) ∈ ℝ) |
10 | | itgiccshift.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
11 | | cncff 22504 |
. . . . . . . . 9
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
14 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ) |
15 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ) |
16 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ) |
17 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ) |
18 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
19 | | eliccre 38575 |
. . . . . . . . . 10
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) |
20 | 16, 17, 18, 19 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) |
21 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℝ) |
22 | 20, 21 | resubcld 10337 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ) |
23 | 1 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
24 | 4 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℂ) |
25 | 23, 24 | pncand 10272 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴) |
26 | 25 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) |
27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) |
28 | | elicc2 12109 |
. . . . . . . . . . . . 13
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))) |
29 | 16, 17, 28 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))) |
30 | 18, 29 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))) |
31 | 30 | simp2d 1067 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥) |
32 | 16, 20, 21, 31 | lesub1dd 10522 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) ≤ (𝑥 − 𝑇)) |
33 | 27, 32 | eqbrtrd 4605 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 − 𝑇)) |
34 | 30 | simp3d 1068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇)) |
35 | 20, 17, 21, 34 | lesub1dd 10522 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ ((𝐵 + 𝑇) − 𝑇)) |
36 | 2 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
37 | 36, 24 | pncand 10272 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵) |
38 | 37 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵) |
39 | 35, 38 | breqtrd 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ 𝐵) |
40 | 14, 15, 22, 33, 39 | eliccd 38573 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) |
41 | 13, 40 | ffvelrnd 6268 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 − 𝑇)) ∈ ℂ) |
42 | | itgiccshift.g |
. . . . . 6
⊢ 𝐺 = (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇))) |
43 | 41, 42 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → 𝐺:((𝐴 + 𝑇)[,](𝐵 + 𝑇))⟶ℂ) |
44 | 43 | fnvinran 38196 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐺‘𝑥) ∈ ℂ) |
45 | 8, 9, 44 | itgioo 23388 |
. . 3
⊢ (𝜑 → ∫((𝐴 + 𝑇)(,)(𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥) |
46 | 7, 45 | eqtr2d 2645 |
. 2
⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐺‘𝑥) d𝑥) |
47 | | eqid 2610 |
. . . 4
⊢ (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) = (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) |
48 | 47 | addccncf 22527 |
. . . . 5
⊢ (𝑇 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) ∈ (ℂ–cn→ℂ)) |
49 | 24, 48 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) ∈ (ℂ–cn→ℂ)) |
50 | 1, 2 | iccssred 38574 |
. . . . 5
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
51 | | ax-resscn 9872 |
. . . . 5
⊢ ℝ
⊆ ℂ |
52 | 50, 51 | syl6ss 3580 |
. . . 4
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
53 | 8, 9 | iccssred 38574 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ ℝ) |
54 | 53, 51 | syl6ss 3580 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ ℂ) |
55 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ∈ ℝ) |
56 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵 + 𝑇) ∈ ℝ) |
57 | 50 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ) |
58 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
59 | 57, 58 | readdcld 9948 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ∈ ℝ) |
60 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
61 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ (𝐴[,]𝐵)) |
62 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
63 | | elicc2 12109 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
64 | 60, 62, 63 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
65 | 61, 64 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)) |
66 | 65 | simp2d 1067 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑦) |
67 | 60, 57, 58, 66 | leadd1dd 10520 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑦 + 𝑇)) |
68 | 65 | simp3d 1068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ≤ 𝐵) |
69 | 57, 62, 58, 68 | leadd1dd 10520 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ≤ (𝐵 + 𝑇)) |
70 | 55, 56, 59, 67, 69 | eliccd 38573 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
71 | 47, 49, 52, 54, 70 | cncfmptssg 38755 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
72 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝑥 − 𝑇) = (𝑤 − 𝑇)) |
73 | 72 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝐹‘(𝑥 − 𝑇)) = (𝐹‘(𝑤 − 𝑇))) |
74 | 73 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇))) = (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇))) |
75 | 1, 2, 4 | iccshift 38591 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}) |
76 | 75 | mpteq1d 4666 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇))) = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇)))) |
77 | 74, 76 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇))) = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇)))) |
78 | 42, 77 | syl5eq 2656 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇)))) |
79 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇))) |
80 | 79 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
81 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇)) |
82 | 81 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇))) |
83 | 82 | cbvrexv 3148 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
(𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)) |
84 | 80, 83 | syl6bb 275 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇))) |
85 | 84 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑤 ∈ ℂ ∣
∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} |
86 | 85 | eqcomi 2619 |
. . . . . 6
⊢ {𝑥 ∈ ℂ ∣
∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} |
87 | | eqid 2610 |
. . . . . 6
⊢ (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))) = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))) |
88 | 52, 24, 86, 10, 87 | cncfshift 38759 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))) ∈ ({𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}–cn→ℂ)) |
89 | 78, 88 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ ({𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}–cn→ℂ)) |
90 | 43 | feqmptd 6159 |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐺‘𝑥))) |
91 | 75 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} = ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
92 | 91 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → ({𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}–cn→ℂ) = (((𝐴 + 𝑇)[,](𝐵 + 𝑇))–cn→ℂ)) |
93 | 89, 90, 92 | 3eltr3d 2702 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐺‘𝑥)) ∈ (((𝐴 + 𝑇)[,](𝐵 + 𝑇))–cn→ℂ)) |
94 | | ioosscn 38563 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ |
95 | 94 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
96 | | 1cnd 9935 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℂ) |
97 | | ssid 3587 |
. . . . . 6
⊢ ℂ
⊆ ℂ |
98 | 97 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℂ ⊆
ℂ) |
99 | 95, 96, 98 | constcncfg 38756 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
100 | | fconstmpt 5085 |
. . . . 5
⊢ ((𝐴(,)𝐵) × {1}) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) |
101 | | ioombl 23140 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
102 | 101 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
103 | | ioovolcl 23144 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴(,)𝐵)) ∈
ℝ) |
104 | 1, 2, 103 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
105 | | iblconst 23390 |
. . . . . 6
⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ 1 ∈ ℂ)
→ ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
106 | 102, 104,
96, 105 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
107 | 100, 106 | syl5eqelr 2693 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈
𝐿1) |
108 | 99, 107 | elind 3760 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ (((𝐴(,)𝐵)–cn→ℂ) ∩
𝐿1)) |
109 | 50 | resmptd 5371 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵)) = (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) |
110 | 109 | eqcomd 2616 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)) = ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) |
111 | 110 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵)))) |
112 | 51 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
113 | 112 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
114 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℂ) |
115 | 113, 114 | addcld 9938 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 𝑇) ∈ ℂ) |
116 | | eqid 2610 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) = (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) |
117 | 115, 116 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)):ℝ⟶ℂ) |
118 | | ssid 3587 |
. . . . . . 7
⊢ ℝ
⊆ ℝ |
119 | 118 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℝ) |
120 | | eqid 2610 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
121 | 120 | tgioo2 22414 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
122 | 120, 121 | dvres 23481 |
. . . . . 6
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)):ℝ⟶ℂ) ∧ (ℝ
⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D
((𝑦 ∈ ℝ ↦
(𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
123 | 112, 117,
119, 50, 122 | syl22anc 1319 |
. . . . 5
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
124 | 111, 123 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
125 | | iccntr 22432 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
126 | 1, 2, 125 | syl2anc 691 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
127 | 126 | reseq2d 5317 |
. . . 4
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵))) |
128 | | reelprrecn 9907 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
129 | 128 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
130 | | 1cnd 9935 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
131 | 129 | dvmptid 23526 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1)) |
132 | | 0cnd 9912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ∈
ℂ) |
133 | 129, 24 | dvmptc 23527 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑇)) = (𝑦 ∈ ℝ ↦ 0)) |
134 | 129, 113,
130, 131, 114, 132, 133 | dvmptadd 23529 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) = (𝑦 ∈ ℝ ↦ (1 +
0))) |
135 | 134 | reseq1d 5316 |
. . . . 5
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)) = ((𝑦 ∈ ℝ ↦ (1 + 0)) ↾
(𝐴(,)𝐵))) |
136 | | ioossre 12106 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ ℝ |
137 | 136 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
138 | 137 | resmptd 5371 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (1 + 0)) ↾
(𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0))) |
139 | | 1p0e1 11010 |
. . . . . . 7
⊢ (1 + 0) =
1 |
140 | 139 | mpteq2i 4669 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) |
141 | 140 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
142 | 135, 138,
141 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
143 | 124, 127,
142 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
144 | | fveq2 6103 |
. . 3
⊢ (𝑥 = (𝑦 + 𝑇) → (𝐺‘𝑥) = (𝐺‘(𝑦 + 𝑇))) |
145 | | oveq1 6556 |
. . 3
⊢ (𝑦 = 𝐴 → (𝑦 + 𝑇) = (𝐴 + 𝑇)) |
146 | | oveq1 6556 |
. . 3
⊢ (𝑦 = 𝐵 → (𝑦 + 𝑇) = (𝐵 + 𝑇)) |
147 | 1, 2, 5, 71, 93, 108, 143, 144, 145, 146, 8, 9 | itgsubsticc 38868 |
. 2
⊢ (𝜑 → ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐺‘𝑥) d𝑥 = ⨜[𝐴 → 𝐵]((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦) |
148 | 5 | ditgpos 23426 |
. . 3
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴(,)𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦) |
149 | 43 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐺:((𝐴 + 𝑇)[,](𝐵 + 𝑇))⟶ℂ) |
150 | 149, 70 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐺‘(𝑦 + 𝑇)) ∈ ℂ) |
151 | | 1cnd 9935 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 1 ∈ ℂ) |
152 | 150, 151 | mulcld 9939 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐺‘(𝑦 + 𝑇)) · 1) ∈
ℂ) |
153 | 1, 2, 152 | itgioo 23388 |
. . 3
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦) |
154 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝑦 + 𝑇) = (𝑥 + 𝑇)) |
155 | 154 | fveq2d 6107 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝐺‘(𝑦 + 𝑇)) = (𝐺‘(𝑥 + 𝑇))) |
156 | 155 | oveq1d 6564 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝐺‘(𝑦 + 𝑇)) · 1) = ((𝐺‘(𝑥 + 𝑇)) · 1)) |
157 | 156 | cbvitgv 23349 |
. . . 4
⊢
∫(𝐴[,]𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)((𝐺‘(𝑥 + 𝑇)) · 1) d𝑥 |
158 | 43 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐺:((𝐴 + 𝑇)[,](𝐵 + 𝑇))⟶ℂ) |
159 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ∈ ℝ) |
160 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐵 + 𝑇) ∈ ℝ) |
161 | 50 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
162 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
163 | 161, 162 | readdcld 9948 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ∈ ℝ) |
164 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
165 | 1 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
166 | 165 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈
ℝ*) |
167 | 2 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
168 | 167 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈
ℝ*) |
169 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) |
170 | | iccgelb 12101 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥) |
171 | 166, 168,
169, 170 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥) |
172 | 164, 161,
162, 171 | leadd1dd 10520 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑥 + 𝑇)) |
173 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
174 | | iccleub 12100 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵) |
175 | 166, 168,
169, 174 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵) |
176 | 161, 173,
162, 175 | leadd1dd 10520 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ≤ (𝐵 + 𝑇)) |
177 | 159, 160,
163, 172, 176 | eliccd 38573 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
178 | 158, 177 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐺‘(𝑥 + 𝑇)) ∈ ℂ) |
179 | 178 | mulid1d 9936 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝐺‘(𝑥 + 𝑇)) · 1) = (𝐺‘(𝑥 + 𝑇))) |
180 | 42, 74 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐺 = (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇))) |
181 | 180 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐺 = (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇)))) |
182 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑤 = (𝑥 + 𝑇) → (𝑤 − 𝑇) = ((𝑥 + 𝑇) − 𝑇)) |
183 | 182 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑤 = (𝑥 + 𝑇) → (𝐹‘(𝑤 − 𝑇)) = (𝐹‘((𝑥 + 𝑇) − 𝑇))) |
184 | 161 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℂ) |
185 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℂ) |
186 | 184, 185 | pncand 10272 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 + 𝑇) − 𝑇) = 𝑥) |
187 | 186 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + 𝑇) − 𝑇)) = (𝐹‘𝑥)) |
188 | 183, 187 | sylan9eqr 2666 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑤 = (𝑥 + 𝑇)) → (𝐹‘(𝑤 − 𝑇)) = (𝐹‘𝑥)) |
189 | 12 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
190 | 181, 188,
177, 189 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐺‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
191 | 179, 190 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝐺‘(𝑥 + 𝑇)) · 1) = (𝐹‘𝑥)) |
192 | 191 | itgeq2dv 23354 |
. . . 4
⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝐺‘(𝑥 + 𝑇)) · 1) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
193 | 157, 192 | syl5eq 2656 |
. . 3
⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
194 | 148, 153,
193 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
195 | 46, 147, 194 | 3eqtrd 2648 |
1
⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |