Step | Hyp | Ref
| Expression |
1 | | itgperiod.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | itgperiod.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | itgperiod.t |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
4 | 3 | rpred 12628 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ℝ) |
5 | | itgperiod.aleb |
. . . . 5
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
6 | 1, 2, 4, 5 | leadd1dd 11446 |
. . . 4
⊢ (𝜑 → (𝐴 + 𝑇) ≤ (𝐵 + 𝑇)) |
7 | 6 | ditgpos 24753 |
. . 3
⊢ (𝜑 → ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐹‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)(,)(𝐵 + 𝑇))(𝐹‘𝑥) d𝑥) |
8 | 1, 4 | readdcld 10862 |
. . . 4
⊢ (𝜑 → (𝐴 + 𝑇) ∈ ℝ) |
9 | 2, 4 | readdcld 10862 |
. . . 4
⊢ (𝜑 → (𝐵 + 𝑇) ∈ ℝ) |
10 | | itgperiod.f |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
11 | 10 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐹:ℝ⟶ℂ) |
12 | 8 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ) |
13 | 9 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ) |
14 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
15 | | eliccre 42718 |
. . . . . 6
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) |
16 | 12, 13, 14, 15 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) |
17 | 11, 16 | ffvelrnd 6905 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘𝑥) ∈ ℂ) |
18 | 8, 9, 17 | itgioo 24713 |
. . 3
⊢ (𝜑 → ∫((𝐴 + 𝑇)(,)(𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥) |
19 | 7, 18 | eqtr2d 2778 |
. 2
⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐹‘𝑥) d𝑥) |
20 | | eqid 2737 |
. . . 4
⊢ (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) = (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) |
21 | 4 | recnd 10861 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ℂ) |
22 | 20 | addccncf 23814 |
. . . . 5
⊢ (𝑇 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) ∈ (ℂ–cn→ℂ)) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) ∈ (ℂ–cn→ℂ)) |
24 | 1, 2 | iccssred 13022 |
. . . . 5
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
25 | | ax-resscn 10786 |
. . . . 5
⊢ ℝ
⊆ ℂ |
26 | 24, 25 | sstrdi 3913 |
. . . 4
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
27 | 8, 9 | iccssred 13022 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ ℝ) |
28 | 27, 25 | sstrdi 3913 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ ℂ) |
29 | 8 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ∈ ℝ) |
30 | 9 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵 + 𝑇) ∈ ℝ) |
31 | 24 | sselda 3901 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ) |
32 | 4 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
33 | 31, 32 | readdcld 10862 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ∈ ℝ) |
34 | 1 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
35 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ (𝐴[,]𝐵)) |
36 | 2 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
37 | | elicc2 13000 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
38 | 34, 36, 37 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
39 | 35, 38 | mpbid 235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)) |
40 | 39 | simp2d 1145 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑦) |
41 | 34, 31, 32, 40 | leadd1dd 11446 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑦 + 𝑇)) |
42 | 39 | simp3d 1146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ≤ 𝐵) |
43 | 31, 36, 32, 42 | leadd1dd 11446 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ≤ (𝐵 + 𝑇)) |
44 | 29, 30, 33, 41, 43 | eliccd 42717 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
45 | 20, 23, 26, 28, 44 | cncfmptssg 43087 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
46 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇))) |
47 | 46 | rexbidv 3216 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
48 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇)) |
49 | 48 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇))) |
50 | 49 | cbvrexvw 3359 |
. . . . . . 7
⊢
(∃𝑧 ∈
(𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)) |
51 | 47, 50 | bitrdi 290 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇))) |
52 | 51 | cbvrabv 3402 |
. . . . 5
⊢ {𝑤 ∈ ℂ ∣
∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} |
53 | 10 | ffdmd 6576 |
. . . . 5
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) |
54 | | simp3 1140 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (𝑧 + 𝑇)) → 𝑤 = (𝑧 + 𝑇)) |
55 | 24 | sselda 3901 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ∈ ℝ) |
56 | 4 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
57 | 55, 56 | readdcld 10862 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 + 𝑇) ∈ ℝ) |
58 | 57 | 3adant3 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (𝑧 + 𝑇)) → (𝑧 + 𝑇) ∈ ℝ) |
59 | 54, 58 | eqeltrd 2838 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (𝑧 + 𝑇)) → 𝑤 ∈ ℝ) |
60 | 59 | rexlimdv3a 3205 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ ℝ)) |
61 | 60 | ralrimivw 3106 |
. . . . . . 7
⊢ (𝜑 → ∀𝑤 ∈ ℂ (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ ℝ)) |
62 | | rabss 3985 |
. . . . . . 7
⊢ ({𝑤 ∈ ℂ ∣
∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ⊆ ℝ ↔ ∀𝑤 ∈ ℂ (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ ℝ)) |
63 | 61, 62 | sylibr 237 |
. . . . . 6
⊢ (𝜑 → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ⊆ ℝ) |
64 | 10 | fdmd 6556 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = ℝ) |
65 | 63, 64 | sseqtrrd 3942 |
. . . . 5
⊢ (𝜑 → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ⊆ dom 𝐹) |
66 | | itgperiod.fper |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
67 | | itgperiod.fcn |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
68 | 26, 4, 52, 53, 65, 66, 67 | cncfperiod 43095 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) ∈ ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}–cn→ℂ)) |
69 | 47 | elrab 3602 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ↔ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
70 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
71 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧𝜑 |
72 | | nfv 1922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧 𝑥 ∈ ℂ |
73 | | nfre1 3225 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) |
74 | 72, 73 | nfan 1907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧(𝑥 ∈ ℂ ∧
∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
75 | 71, 74 | nfan 1907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧(𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
76 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) |
77 | | simp3 1140 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 = (𝑧 + 𝑇)) |
78 | 1 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
79 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ∈ (𝐴[,]𝐵)) |
80 | 2 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
81 | | elicc2 13000 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
82 | 78, 80, 81 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
83 | 79, 82 | mpbid 235 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)) |
84 | 83 | simp2d 1145 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑧) |
85 | 78, 55, 56, 84 | leadd1dd 11446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑧 + 𝑇)) |
86 | 83 | simp3d 1146 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ≤ 𝐵) |
87 | 55, 80, 56, 86 | leadd1dd 11446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)) |
88 | 57, 85, 87 | 3jca 1130 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))) |
89 | 88 | 3adant3 1134 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))) |
90 | 8 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝐴 + 𝑇) ∈ ℝ) |
91 | 9 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝐵 + 𝑇) ∈ ℝ) |
92 | | elicc2 13000 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → ((𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)))) |
93 | 90, 91, 92 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)))) |
94 | 89, 93 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
95 | 77, 94 | eqeltrd 2838 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
96 | 95 | 3exp 1121 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) → (𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))))) |
97 | 96 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → (𝑧 ∈ (𝐴[,]𝐵) → (𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))))) |
98 | 75, 76, 97 | rexlimd 3236 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → (∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
99 | 70, 98 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
100 | 69, 99 | sylan2b 597 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
101 | 16 | recnd 10861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ) |
102 | 1 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ) |
103 | 2 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ) |
104 | 4 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℝ) |
105 | 16, 104 | resubcld 11260 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ) |
106 | 1 | recnd 10861 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℂ) |
107 | 106, 21 | pncand 11190 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴) |
108 | 107 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) |
109 | 108 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) |
110 | | elicc2 13000 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))) |
111 | 12, 13, 110 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))) |
112 | 14, 111 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))) |
113 | 112 | simp2d 1145 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥) |
114 | 12, 16, 104, 113 | lesub1dd 11448 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) ≤ (𝑥 − 𝑇)) |
115 | 109, 114 | eqbrtrd 5075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 − 𝑇)) |
116 | 112 | simp3d 1146 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇)) |
117 | 16, 13, 104, 116 | lesub1dd 11448 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ ((𝐵 + 𝑇) − 𝑇)) |
118 | 2 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ ℂ) |
119 | 118, 21 | pncand 11190 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵) |
120 | 119 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵) |
121 | 117, 120 | breqtrd 5079 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ 𝐵) |
122 | 102, 103,
105, 115, 121 | eliccd 42717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) |
123 | 21 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ) |
124 | 101, 123 | npcand 11193 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 − 𝑇) + 𝑇) = 𝑥) |
125 | 124 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 = ((𝑥 − 𝑇) + 𝑇)) |
126 | | oveq1 7220 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑥 − 𝑇) → (𝑧 + 𝑇) = ((𝑥 − 𝑇) + 𝑇)) |
127 | 126 | rspceeqv 3552 |
. . . . . . . . . 10
⊢ (((𝑥 − 𝑇) ∈ (𝐴[,]𝐵) ∧ 𝑥 = ((𝑥 − 𝑇) + 𝑇)) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
128 | 122, 125,
127 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
129 | 101, 128,
69 | sylanbrc 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) |
130 | 100, 129 | impbida 801 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ↔ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
131 | 130 | eqrdv 2735 |
. . . . . 6
⊢ (𝜑 → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} = ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
132 | 131 | reseq2d 5851 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) = (𝐹 ↾ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
133 | 131, 65 | eqsstrrd 3940 |
. . . . . 6
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ dom 𝐹) |
134 | 53, 133 | feqresmpt 6781 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) = (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘𝑥))) |
135 | 132, 134 | eqtr2d 2778 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘𝑥)) = (𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)})) |
136 | 1, 2, 4 | iccshift 42731 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) |
137 | 136 | oveq1d 7228 |
. . . 4
⊢ (𝜑 → (((𝐴 + 𝑇)[,](𝐵 + 𝑇))–cn→ℂ) = ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}–cn→ℂ)) |
138 | 68, 135, 137 | 3eltr4d 2853 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘𝑥)) ∈ (((𝐴 + 𝑇)[,](𝐵 + 𝑇))–cn→ℂ)) |
139 | | ioosscn 12997 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ |
140 | 139 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
141 | | 1cnd 10828 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℂ) |
142 | | ssid 3923 |
. . . . . 6
⊢ ℂ
⊆ ℂ |
143 | 142 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℂ ⊆
ℂ) |
144 | 140, 141,
143 | constcncfg 43088 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
145 | | fconstmpt 5611 |
. . . . 5
⊢ ((𝐴(,)𝐵) × {1}) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) |
146 | | ioombl 24462 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
147 | 146 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
148 | | ioovolcl 24467 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴(,)𝐵)) ∈
ℝ) |
149 | 1, 2, 148 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
150 | | iblconst 24715 |
. . . . . 6
⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ 1 ∈ ℂ)
→ ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
151 | 147, 149,
141, 150 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
152 | 145, 151 | eqeltrrid 2843 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈
𝐿1) |
153 | 144, 152 | elind 4108 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ (((𝐴(,)𝐵)–cn→ℂ) ∩
𝐿1)) |
154 | 24 | resmptd 5908 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵)) = (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) |
155 | 154 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)) = ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) |
156 | 155 | oveq2d 7229 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵)))) |
157 | 25 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
158 | 157 | sselda 3901 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
159 | 21 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℂ) |
160 | 158, 159 | addcld 10852 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 𝑇) ∈ ℂ) |
161 | 160 | fmpttd 6932 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)):ℝ⟶ℂ) |
162 | | ssid 3923 |
. . . . . . 7
⊢ ℝ
⊆ ℝ |
163 | 162 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℝ) |
164 | | eqid 2737 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
165 | 164 | tgioo2 23700 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
166 | 164, 165 | dvres 24808 |
. . . . . 6
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)):ℝ⟶ℂ) ∧ (ℝ
⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D
((𝑦 ∈ ℝ ↦
(𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
167 | 157, 161,
163, 24, 166 | syl22anc 839 |
. . . . 5
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
168 | 156, 167 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
169 | | iccntr 23718 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
170 | 1, 2, 169 | syl2anc 587 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
171 | 170 | reseq2d 5851 |
. . . 4
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵))) |
172 | | reelprrecn 10821 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
173 | 172 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
174 | | 1cnd 10828 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
175 | 173 | dvmptid 24854 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1)) |
176 | | 0cnd 10826 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ∈
ℂ) |
177 | 173, 21 | dvmptc 24855 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑇)) = (𝑦 ∈ ℝ ↦ 0)) |
178 | 173, 158,
174, 175, 159, 176, 177 | dvmptadd 24857 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) = (𝑦 ∈ ℝ ↦ (1 +
0))) |
179 | 178 | reseq1d 5850 |
. . . . 5
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)) = ((𝑦 ∈ ℝ ↦ (1 + 0)) ↾
(𝐴(,)𝐵))) |
180 | | ioossre 12996 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ ℝ |
181 | 180 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
182 | 181 | resmptd 5908 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (1 + 0)) ↾
(𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0))) |
183 | | 1p0e1 11954 |
. . . . . . 7
⊢ (1 + 0) =
1 |
184 | 183 | mpteq2i 5147 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) |
185 | 184 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
186 | 179, 182,
185 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
187 | 168, 171,
186 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
188 | | fveq2 6717 |
. . 3
⊢ (𝑥 = (𝑦 + 𝑇) → (𝐹‘𝑥) = (𝐹‘(𝑦 + 𝑇))) |
189 | | oveq1 7220 |
. . 3
⊢ (𝑦 = 𝐴 → (𝑦 + 𝑇) = (𝐴 + 𝑇)) |
190 | | oveq1 7220 |
. . 3
⊢ (𝑦 = 𝐵 → (𝑦 + 𝑇) = (𝐵 + 𝑇)) |
191 | 1, 2, 5, 45, 138, 153, 187, 188, 189, 190, 8, 9 | itgsubsticc 43192 |
. 2
⊢ (𝜑 → ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐹‘𝑥) d𝑥 = ⨜[𝐴 → 𝐵]((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦) |
192 | 5 | ditgpos 24753 |
. . 3
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴(,)𝐵)((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦) |
193 | 10 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ) |
194 | 193, 33 | ffvelrnd 6905 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) ∈ ℂ) |
195 | | 1cnd 10828 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 1 ∈ ℂ) |
196 | 194, 195 | mulcld 10853 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑦 + 𝑇)) · 1) ∈
ℂ) |
197 | 1, 2, 196 | itgioo 24713 |
. . 3
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦) |
198 | | fvoveq1 7236 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘(𝑥 + 𝑇))) |
199 | 198 | oveq1d 7228 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝐹‘(𝑦 + 𝑇)) · 1) = ((𝐹‘(𝑥 + 𝑇)) · 1)) |
200 | 199 | cbvitgv 24674 |
. . . 4
⊢
∫(𝐴[,]𝐵)((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)((𝐹‘(𝑥 + 𝑇)) · 1) d𝑥 |
201 | 10 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ) |
202 | 24 | sselda 3901 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
203 | 4 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
204 | 202, 203 | readdcld 10862 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ∈ ℝ) |
205 | 201, 204 | ffvelrnd 6905 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) ∈ ℂ) |
206 | 205 | mulid1d 10850 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑥 + 𝑇)) · 1) = (𝐹‘(𝑥 + 𝑇))) |
207 | 206, 66 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑥 + 𝑇)) · 1) = (𝐹‘𝑥)) |
208 | 207 | itgeq2dv 24679 |
. . . 4
⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝐹‘(𝑥 + 𝑇)) · 1) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
209 | 200, 208 | syl5eq 2790 |
. . 3
⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
210 | 192, 197,
209 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐹‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
211 | 19, 191, 210 | 3eqtrd 2781 |
1
⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |