Step | Hyp | Ref
| Expression |
1 | | itgperiod.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | itgperiod.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | itgperiod.t |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
4 | 3 | rpred 11748 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ℝ) |
5 | | itgperiod.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 | | itgperiod.f |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
11 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐹:ℝ⟶ℂ) |
12 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ) |
13 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ) |
14 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
15 | | eliccre 38575 |
. . . . . 6
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) |
16 | 12, 13, 14, 15 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) |
17 | 11, 16 | ffvelrnd 6268 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘𝑥) ∈ ℂ) |
18 | 8, 9, 17 | itgioo 23388 |
. . 3
⊢ (𝜑 → ∫((𝐴 + 𝑇)(,)(𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥) |
19 | 7, 18 | eqtr2d 2645 |
. 2
⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐹‘𝑥) d𝑥) |
20 | | eqid 2610 |
. . . 4
⊢ (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) = (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) |
21 | 4 | recnd 9947 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ℂ) |
22 | 20 | addccncf 22527 |
. . . . 5
⊢ (𝑇 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) ∈ (ℂ–cn→ℂ)) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) ∈ (ℂ–cn→ℂ)) |
24 | 1, 2 | iccssred 38574 |
. . . . 5
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
25 | | ax-resscn 9872 |
. . . . 5
⊢ ℝ
⊆ ℂ |
26 | 24, 25 | syl6ss 3580 |
. . . 4
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
27 | 8, 9 | iccssred 38574 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ ℝ) |
28 | 27, 25 | syl6ss 3580 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ ℂ) |
29 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ∈ ℝ) |
30 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵 + 𝑇) ∈ ℝ) |
31 | 24 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ) |
32 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
33 | 31, 32 | readdcld 9948 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ∈ ℝ) |
34 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
35 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ (𝐴[,]𝐵)) |
36 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
37 | | elicc2 12109 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
38 | 34, 36, 37 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
39 | 35, 38 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)) |
40 | 39 | simp2d 1067 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑦) |
41 | 34, 31, 32, 40 | leadd1dd 10520 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑦 + 𝑇)) |
42 | 39 | simp3d 1068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ≤ 𝐵) |
43 | 31, 36, 32, 42 | leadd1dd 10520 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ≤ (𝐵 + 𝑇)) |
44 | 29, 30, 33, 41, 43 | eliccd 38573 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
45 | 20, 23, 26, 28, 44 | cncfmptssg 38755 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
46 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇))) |
47 | 46 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
48 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇)) |
49 | 48 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇))) |
50 | 49 | cbvrexv 3148 |
. . . . . . 7
⊢
(∃𝑧 ∈
(𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)) |
51 | 47, 50 | syl6bb 275 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇))) |
52 | 51 | cbvrabv 3172 |
. . . . 5
⊢ {𝑤 ∈ ℂ ∣
∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} |
53 | | ffdm 5975 |
. . . . . . 7
⊢ (𝐹:ℝ⟶ℂ →
(𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) |
54 | 10, 53 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) |
55 | 54 | simpld 474 |
. . . . 5
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) |
56 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (𝑧 + 𝑇)) → 𝑤 = (𝑧 + 𝑇)) |
57 | 24 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ∈ ℝ) |
58 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
59 | 57, 58 | readdcld 9948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 + 𝑇) ∈ ℝ) |
60 | 59 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (𝑧 + 𝑇)) → (𝑧 + 𝑇) ∈ ℝ) |
61 | 56, 60 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (𝑧 + 𝑇)) → 𝑤 ∈ ℝ) |
62 | 61 | rexlimdv3a 3015 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ ℝ)) |
63 | 62 | ralrimivw 2950 |
. . . . . . 7
⊢ (𝜑 → ∀𝑤 ∈ ℂ (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ ℝ)) |
64 | | rabss 3642 |
. . . . . . 7
⊢ ({𝑤 ∈ ℂ ∣
∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ⊆ ℝ ↔ ∀𝑤 ∈ ℂ (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ ℝ)) |
65 | 63, 64 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ⊆ ℝ) |
66 | | fdm 5964 |
. . . . . . 7
⊢ (𝐹:ℝ⟶ℂ →
dom 𝐹 =
ℝ) |
67 | 10, 66 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = ℝ) |
68 | 65, 67 | sseqtr4d 3605 |
. . . . 5
⊢ (𝜑 → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ⊆ dom 𝐹) |
69 | | itgperiod.fper |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
70 | | itgperiod.fcn |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
71 | 26, 4, 52, 55, 68, 69, 70 | cncfperiod 38764 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) ∈ ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}–cn→ℂ)) |
72 | 47 | elrab 3331 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ↔ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
73 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
74 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧𝜑 |
75 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧 𝑥 ∈ ℂ |
76 | | nfre1 2988 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) |
77 | 75, 76 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧(𝑥 ∈ ℂ ∧
∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
78 | 74, 77 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧(𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
79 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) |
80 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 = (𝑧 + 𝑇)) |
81 | 1 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
82 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ∈ (𝐴[,]𝐵)) |
83 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
84 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
85 | 81, 83, 84 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
86 | 82, 85 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)) |
87 | 86 | simp2d 1067 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑧) |
88 | 81, 57, 58, 87 | leadd1dd 10520 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑧 + 𝑇)) |
89 | 86 | simp3d 1068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ≤ 𝐵) |
90 | 57, 83, 58, 89 | leadd1dd 10520 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)) |
91 | 59, 88, 90 | 3jca 1235 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))) |
92 | 91 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))) |
93 | 8 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝐴 + 𝑇) ∈ ℝ) |
94 | 9 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝐵 + 𝑇) ∈ ℝ) |
95 | | elicc2 12109 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → ((𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)))) |
96 | 93, 94, 95 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)))) |
97 | 92, 96 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
98 | 80, 97 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
99 | 98 | 3exp 1256 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) → (𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))))) |
100 | 99 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → (𝑧 ∈ (𝐴[,]𝐵) → (𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))))) |
101 | 78, 79, 100 | rexlimd 3008 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → (∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
102 | 73, 101 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
103 | 72, 102 | sylan2b 491 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
104 | 16 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ) |
105 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ) |
106 | 2 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ) |
107 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℝ) |
108 | 16, 107 | resubcld 10337 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ) |
109 | 1 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℂ) |
110 | 109, 21 | pncand 10272 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴) |
111 | 110 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) |
112 | 111 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) |
113 | | elicc2 12109 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))) |
114 | 12, 13, 113 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))) |
115 | 14, 114 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))) |
116 | 115 | simp2d 1067 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥) |
117 | 12, 16, 107, 116 | lesub1dd 10522 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) ≤ (𝑥 − 𝑇)) |
118 | 112, 117 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 − 𝑇)) |
119 | 115 | simp3d 1068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇)) |
120 | 16, 13, 107, 119 | lesub1dd 10522 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ ((𝐵 + 𝑇) − 𝑇)) |
121 | 2 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ ℂ) |
122 | 121, 21 | pncand 10272 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵) |
123 | 122 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵) |
124 | 120, 123 | breqtrd 4609 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ 𝐵) |
125 | 105, 106,
108, 118, 124 | eliccd 38573 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) |
126 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ) |
127 | 104, 126 | npcand 10275 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 − 𝑇) + 𝑇) = 𝑥) |
128 | 127 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 = ((𝑥 − 𝑇) + 𝑇)) |
129 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑥 − 𝑇) → (𝑧 + 𝑇) = ((𝑥 − 𝑇) + 𝑇)) |
130 | 129 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑥 − 𝑇) → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = ((𝑥 − 𝑇) + 𝑇))) |
131 | 130 | rspcev 3282 |
. . . . . . . . . 10
⊢ (((𝑥 − 𝑇) ∈ (𝐴[,]𝐵) ∧ 𝑥 = ((𝑥 − 𝑇) + 𝑇)) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
132 | 125, 128,
131 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
133 | 104, 132,
72 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) |
134 | 103, 133 | impbida 873 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ↔ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
135 | 134 | eqrdv 2608 |
. . . . . 6
⊢ (𝜑 → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} = ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
136 | 135 | reseq2d 5317 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) = (𝐹 ↾ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
137 | 135, 68 | eqsstr3d 3603 |
. . . . . 6
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ dom 𝐹) |
138 | 55, 137 | feqresmpt 6160 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) = (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘𝑥))) |
139 | 136, 138 | eqtr2d 2645 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘𝑥)) = (𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)})) |
140 | 1, 2, 4 | iccshift 38591 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) |
141 | 140 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → (((𝐴 + 𝑇)[,](𝐵 + 𝑇))–cn→ℂ) = ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}–cn→ℂ)) |
142 | 71, 139, 141 | 3eltr4d 2703 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘𝑥)) ∈ (((𝐴 + 𝑇)[,](𝐵 + 𝑇))–cn→ℂ)) |
143 | | ioosscn 38563 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ |
144 | 143 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
145 | | 1cnd 9935 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℂ) |
146 | | ssid 3587 |
. . . . . 6
⊢ ℂ
⊆ ℂ |
147 | 146 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℂ ⊆
ℂ) |
148 | 144, 145,
147 | constcncfg 38756 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
149 | | fconstmpt 5085 |
. . . . 5
⊢ ((𝐴(,)𝐵) × {1}) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) |
150 | | ioombl 23140 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
151 | 150 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
152 | | ioovolcl 23144 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴(,)𝐵)) ∈
ℝ) |
153 | 1, 2, 152 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
154 | | iblconst 23390 |
. . . . . 6
⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ 1 ∈ ℂ)
→ ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
155 | 151, 153,
145, 154 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
156 | 149, 155 | syl5eqelr 2693 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈
𝐿1) |
157 | 148, 156 | elind 3760 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ (((𝐴(,)𝐵)–cn→ℂ) ∩
𝐿1)) |
158 | 24 | resmptd 5371 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵)) = (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) |
159 | 158 | eqcomd 2616 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)) = ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) |
160 | 159 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵)))) |
161 | 25 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
162 | 161 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
163 | 21 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℂ) |
164 | 162, 163 | addcld 9938 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 𝑇) ∈ ℂ) |
165 | | eqid 2610 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) = (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) |
166 | 164, 165 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)):ℝ⟶ℂ) |
167 | | ssid 3587 |
. . . . . . 7
⊢ ℝ
⊆ ℝ |
168 | 167 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℝ) |
169 | | eqid 2610 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
170 | 169 | tgioo2 22414 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
171 | 169, 170 | dvres 23481 |
. . . . . 6
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)):ℝ⟶ℂ) ∧ (ℝ
⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D
((𝑦 ∈ ℝ ↦
(𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
172 | 161, 166,
168, 24, 171 | syl22anc 1319 |
. . . . 5
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
173 | 160, 172 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
174 | | iccntr 22432 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
175 | 1, 2, 174 | syl2anc 691 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
176 | 175 | reseq2d 5317 |
. . . 4
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵))) |
177 | | reelprrecn 9907 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
178 | 177 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
179 | | 1cnd 9935 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
180 | 178 | dvmptid 23526 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1)) |
181 | | 0cnd 9912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ∈
ℂ) |
182 | 178, 21 | dvmptc 23527 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑇)) = (𝑦 ∈ ℝ ↦ 0)) |
183 | 178, 162,
179, 180, 163, 181, 182 | dvmptadd 23529 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) = (𝑦 ∈ ℝ ↦ (1 +
0))) |
184 | 183 | reseq1d 5316 |
. . . . 5
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)) = ((𝑦 ∈ ℝ ↦ (1 + 0)) ↾
(𝐴(,)𝐵))) |
185 | | ioossre 12106 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ ℝ |
186 | 185 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
187 | 186 | resmptd 5371 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (1 + 0)) ↾
(𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0))) |
188 | | 1p0e1 11010 |
. . . . . . 7
⊢ (1 + 0) =
1 |
189 | 188 | mpteq2i 4669 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) |
190 | 189 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
191 | 184, 187,
190 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
192 | 173, 176,
191 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
193 | | fveq2 6103 |
. . 3
⊢ (𝑥 = (𝑦 + 𝑇) → (𝐹‘𝑥) = (𝐹‘(𝑦 + 𝑇))) |
194 | | oveq1 6556 |
. . 3
⊢ (𝑦 = 𝐴 → (𝑦 + 𝑇) = (𝐴 + 𝑇)) |
195 | | oveq1 6556 |
. . 3
⊢ (𝑦 = 𝐵 → (𝑦 + 𝑇) = (𝐵 + 𝑇)) |
196 | 1, 2, 5, 45, 142, 157, 192, 193, 194, 195, 8, 9 | itgsubsticc 38868 |
. 2
⊢ (𝜑 → ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐹‘𝑥) d𝑥 = ⨜[𝐴 → 𝐵]((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦) |
197 | 5 | ditgpos 23426 |
. . 3
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴(,)𝐵)((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦) |
198 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ) |
199 | 198, 33 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) ∈ ℂ) |
200 | | 1cnd 9935 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 1 ∈ ℂ) |
201 | 199, 200 | mulcld 9939 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑦 + 𝑇)) · 1) ∈
ℂ) |
202 | 1, 2, 201 | itgioo 23388 |
. . 3
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦) |
203 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝑦 + 𝑇) = (𝑥 + 𝑇)) |
204 | 203 | fveq2d 6107 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘(𝑥 + 𝑇))) |
205 | 204 | oveq1d 6564 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝐹‘(𝑦 + 𝑇)) · 1) = ((𝐹‘(𝑥 + 𝑇)) · 1)) |
206 | 205 | cbvitgv 23349 |
. . . 4
⊢
∫(𝐴[,]𝐵)((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)((𝐹‘(𝑥 + 𝑇)) · 1) d𝑥 |
207 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ) |
208 | 24 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
209 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
210 | 208, 209 | readdcld 9948 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ∈ ℝ) |
211 | 207, 210 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) ∈ ℂ) |
212 | 211 | mulid1d 9936 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑥 + 𝑇)) · 1) = (𝐹‘(𝑥 + 𝑇))) |
213 | 212, 69 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑥 + 𝑇)) · 1) = (𝐹‘𝑥)) |
214 | 213 | itgeq2dv 23354 |
. . . 4
⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝐹‘(𝑥 + 𝑇)) · 1) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
215 | 206, 214 | syl5eq 2656 |
. . 3
⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
216 | 197, 202,
215 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
217 | 19, 196, 216 | 3eqtrd 2648 |
1
⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |