| Step | Hyp | Ref
| Expression |
| 1 | | itgiccshift.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 2 | | itgiccshift.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 3 | | itgiccshift.t |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
| 4 | 3 | rpred 13077 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 5 | | itgiccshift.aleb |
. . . . 5
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 6 | 1, 2, 4, 5 | leadd1dd 11877 |
. . . 4
⊢ (𝜑 → (𝐴 + 𝑇) ≤ (𝐵 + 𝑇)) |
| 7 | 6 | ditgpos 25891 |
. . 3
⊢ (𝜑 → ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐺‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)(,)(𝐵 + 𝑇))(𝐺‘𝑥) d𝑥) |
| 8 | 1, 4 | readdcld 11290 |
. . . 4
⊢ (𝜑 → (𝐴 + 𝑇) ∈ ℝ) |
| 9 | 2, 4 | readdcld 11290 |
. . . 4
⊢ (𝜑 → (𝐵 + 𝑇) ∈ ℝ) |
| 10 | | itgiccshift.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 11 | | cncff 24919 |
. . . . . . . . 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 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
| 19 | | eliccre 45518 |
. . . . . . . . . 10
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) |
| 20 | 16, 17, 18, 19 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) |
| 21 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℝ) |
| 22 | 20, 21 | resubcld 11691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ) |
| 23 | 1 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 24 | 4 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℂ) |
| 25 | 23, 24 | pncand 11621 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴) |
| 26 | 25 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) |
| 27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) |
| 28 | | elicc2 13452 |
. . . . . . . . . . . . 13
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))) |
| 29 | 16, 17, 28 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))) |
| 30 | 18, 29 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))) |
| 31 | 30 | simp2d 1144 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥) |
| 32 | 16, 20, 21, 31 | lesub1dd 11879 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) ≤ (𝑥 − 𝑇)) |
| 33 | 27, 32 | eqbrtrd 5165 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 − 𝑇)) |
| 34 | 30 | simp3d 1145 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇)) |
| 35 | 20, 17, 21, 34 | lesub1dd 11879 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ ((𝐵 + 𝑇) − 𝑇)) |
| 36 | 2 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 37 | 36, 24 | pncand 11621 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵) |
| 38 | 37 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵) |
| 39 | 35, 38 | breqtrd 5169 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ 𝐵) |
| 40 | 14, 15, 22, 33, 39 | eliccd 45517 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) |
| 41 | 13, 40 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 − 𝑇)) ∈ ℂ) |
| 42 | | itgiccshift.g |
. . . . . 6
⊢ 𝐺 = (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇))) |
| 43 | 41, 42 | fmptd 7134 |
. . . . 5
⊢ (𝜑 → 𝐺:((𝐴 + 𝑇)[,](𝐵 + 𝑇))⟶ℂ) |
| 44 | 43 | ffvelcdmda 7104 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐺‘𝑥) ∈ ℂ) |
| 45 | 8, 9, 44 | itgioo 25851 |
. . 3
⊢ (𝜑 → ∫((𝐴 + 𝑇)(,)(𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥) |
| 46 | 7, 45 | eqtr2d 2778 |
. 2
⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐺‘𝑥) d𝑥) |
| 47 | | eqid 2737 |
. . . 4
⊢ (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) = (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) |
| 48 | 47 | addccncf 24943 |
. . . . 5
⊢ (𝑇 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) ∈ (ℂ–cn→ℂ)) |
| 49 | 24, 48 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) ∈ (ℂ–cn→ℂ)) |
| 50 | 1, 2 | iccssred 13474 |
. . . . 5
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
| 51 | | ax-resscn 11212 |
. . . . 5
⊢ ℝ
⊆ ℂ |
| 52 | 50, 51 | sstrdi 3996 |
. . . 4
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
| 53 | 8, 9 | iccssred 13474 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ ℝ) |
| 54 | 53, 51 | sstrdi 3996 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ ℂ) |
| 55 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ∈ ℝ) |
| 56 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵 + 𝑇) ∈ ℝ) |
| 57 | 50 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ) |
| 58 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
| 59 | 57, 58 | readdcld 11290 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ∈ ℝ) |
| 60 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
| 61 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ (𝐴[,]𝐵)) |
| 62 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
| 63 | | elicc2 13452 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
| 64 | 60, 62, 63 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))) |
| 65 | 61, 64 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)) |
| 66 | 65 | simp2d 1144 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑦) |
| 67 | 60, 57, 58, 66 | leadd1dd 11877 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑦 + 𝑇)) |
| 68 | 65 | simp3d 1145 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ≤ 𝐵) |
| 69 | 57, 62, 58, 68 | leadd1dd 11877 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ≤ (𝐵 + 𝑇)) |
| 70 | 55, 56, 59, 67, 69 | eliccd 45517 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
| 71 | 47, 49, 52, 54, 70 | cncfmptssg 45886 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
| 72 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝐹‘(𝑥 − 𝑇)) = (𝐹‘(𝑤 − 𝑇))) |
| 73 | 72 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇))) = (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇))) |
| 74 | 1, 2, 4 | iccshift 45531 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}) |
| 75 | 74 | mpteq1d 5237 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇))) = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇)))) |
| 76 | 73, 75 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇))) = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇)))) |
| 77 | 42, 76 | eqtrid 2789 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇)))) |
| 78 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇))) |
| 79 | 78 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
| 80 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇)) |
| 81 | 80 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇))) |
| 82 | 81 | cbvrexvw 3238 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
(𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)) |
| 83 | 79, 82 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇))) |
| 84 | 83 | cbvrabv 3447 |
. . . . . . 7
⊢ {𝑤 ∈ ℂ ∣
∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} |
| 85 | 84 | eqcomi 2746 |
. . . . . 6
⊢ {𝑥 ∈ ℂ ∣
∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} |
| 86 | | eqid 2737 |
. . . . . 6
⊢ (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))) = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))) |
| 87 | 52, 24, 85, 10, 86 | cncfshift 45889 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))) ∈ ({𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}–cn→ℂ)) |
| 88 | 77, 87 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ ({𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}–cn→ℂ)) |
| 89 | 43 | feqmptd 6977 |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐺‘𝑥))) |
| 90 | 74 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} = ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
| 91 | 90 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → ({𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}–cn→ℂ) = (((𝐴 + 𝑇)[,](𝐵 + 𝑇))–cn→ℂ)) |
| 92 | 88, 89, 91 | 3eltr3d 2855 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐺‘𝑥)) ∈ (((𝐴 + 𝑇)[,](𝐵 + 𝑇))–cn→ℂ)) |
| 93 | | ioosscn 13449 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ |
| 94 | 93 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
| 95 | | 1cnd 11256 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℂ) |
| 96 | | ssid 4006 |
. . . . . 6
⊢ ℂ
⊆ ℂ |
| 97 | 96 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 98 | 94, 95, 97 | constcncfg 45887 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 99 | | fconstmpt 5747 |
. . . . 5
⊢ ((𝐴(,)𝐵) × {1}) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) |
| 100 | | ioombl 25600 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
| 101 | 100 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
| 102 | | ioovolcl 25605 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴(,)𝐵)) ∈
ℝ) |
| 103 | 1, 2, 102 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
| 104 | | iblconst 25853 |
. . . . . 6
⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ 1 ∈ ℂ)
→ ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
| 105 | 101, 103,
95, 104 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ((𝐴(,)𝐵) × {1}) ∈
𝐿1) |
| 106 | 99, 105 | eqeltrrid 2846 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈
𝐿1) |
| 107 | 98, 106 | elind 4200 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ (((𝐴(,)𝐵)–cn→ℂ) ∩
𝐿1)) |
| 108 | 50 | resmptd 6058 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵)) = (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) |
| 109 | 108 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)) = ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) |
| 110 | 109 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵)))) |
| 111 | 51 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 112 | 111 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
| 113 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℂ) |
| 114 | 112, 113 | addcld 11280 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 𝑇) ∈ ℂ) |
| 115 | 114 | fmpttd 7135 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)):ℝ⟶ℂ) |
| 116 | | ssid 4006 |
. . . . . . 7
⊢ ℝ
⊆ ℝ |
| 117 | 116 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℝ) |
| 118 | | eqid 2737 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 119 | | tgioo4 24826 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 120 | 118, 119 | dvres 25946 |
. . . . . 6
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)):ℝ⟶ℂ) ∧ (ℝ
⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D
((𝑦 ∈ ℝ ↦
(𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
| 121 | 111, 115,
117, 50, 120 | syl22anc 839 |
. . . . 5
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
| 122 | 110, 121 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
| 123 | | iccntr 24843 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
| 124 | 1, 2, 123 | syl2anc 584 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
| 125 | 124 | reseq2d 5997 |
. . . 4
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵))) |
| 126 | | reelprrecn 11247 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
| 127 | 126 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
| 128 | | 1cnd 11256 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
| 129 | 127 | dvmptid 25995 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1)) |
| 130 | | 0cnd 11254 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ∈
ℂ) |
| 131 | 127, 24 | dvmptc 25996 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑇)) = (𝑦 ∈ ℝ ↦ 0)) |
| 132 | 127, 112,
128, 129, 113, 130, 131 | dvmptadd 25998 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) = (𝑦 ∈ ℝ ↦ (1 +
0))) |
| 133 | 132 | reseq1d 5996 |
. . . . 5
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)) = ((𝑦 ∈ ℝ ↦ (1 + 0)) ↾
(𝐴(,)𝐵))) |
| 134 | | ioossre 13448 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 135 | 134 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
| 136 | 135 | resmptd 6058 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (1 + 0)) ↾
(𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0))) |
| 137 | | 1p0e1 12390 |
. . . . . . 7
⊢ (1 + 0) =
1 |
| 138 | 137 | mpteq2i 5247 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) |
| 139 | 138 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
| 140 | 133, 136,
139 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
| 141 | 122, 125,
140 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)) |
| 142 | | fveq2 6906 |
. . 3
⊢ (𝑥 = (𝑦 + 𝑇) → (𝐺‘𝑥) = (𝐺‘(𝑦 + 𝑇))) |
| 143 | | oveq1 7438 |
. . 3
⊢ (𝑦 = 𝐴 → (𝑦 + 𝑇) = (𝐴 + 𝑇)) |
| 144 | | oveq1 7438 |
. . 3
⊢ (𝑦 = 𝐵 → (𝑦 + 𝑇) = (𝐵 + 𝑇)) |
| 145 | 1, 2, 5, 71, 92, 107, 141, 142, 143, 144, 8, 9 | itgsubsticc 45991 |
. 2
⊢ (𝜑 → ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐺‘𝑥) d𝑥 = ⨜[𝐴 → 𝐵]((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦) |
| 146 | 5 | ditgpos 25891 |
. . 3
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴(,)𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦) |
| 147 | 43 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐺:((𝐴 + 𝑇)[,](𝐵 + 𝑇))⟶ℂ) |
| 148 | 147, 70 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐺‘(𝑦 + 𝑇)) ∈ ℂ) |
| 149 | | 1cnd 11256 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 1 ∈ ℂ) |
| 150 | 148, 149 | mulcld 11281 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐺‘(𝑦 + 𝑇)) · 1) ∈
ℂ) |
| 151 | 1, 2, 150 | itgioo 25851 |
. . 3
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦) |
| 152 | | fvoveq1 7454 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝐺‘(𝑦 + 𝑇)) = (𝐺‘(𝑥 + 𝑇))) |
| 153 | 152 | oveq1d 7446 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝐺‘(𝑦 + 𝑇)) · 1) = ((𝐺‘(𝑥 + 𝑇)) · 1)) |
| 154 | 153 | cbvitgv 25812 |
. . . 4
⊢
∫(𝐴[,]𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)((𝐺‘(𝑥 + 𝑇)) · 1) d𝑥 |
| 155 | 43 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐺:((𝐴 + 𝑇)[,](𝐵 + 𝑇))⟶ℂ) |
| 156 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ∈ ℝ) |
| 157 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐵 + 𝑇) ∈ ℝ) |
| 158 | 50 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
| 159 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
| 160 | 158, 159 | readdcld 11290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ∈ ℝ) |
| 161 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
| 162 | 1 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 163 | 162 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈
ℝ*) |
| 164 | 2 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 165 | 164 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈
ℝ*) |
| 166 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) |
| 167 | | iccgelb 13443 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥) |
| 168 | 163, 165,
166, 167 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥) |
| 169 | 161, 158,
159, 168 | leadd1dd 11877 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑥 + 𝑇)) |
| 170 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
| 171 | | iccleub 13442 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵) |
| 172 | 163, 165,
166, 171 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵) |
| 173 | 158, 170,
159, 172 | leadd1dd 11877 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ≤ (𝐵 + 𝑇)) |
| 174 | 156, 157,
160, 169, 173 | eliccd 45517 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
| 175 | 155, 174 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐺‘(𝑥 + 𝑇)) ∈ ℂ) |
| 176 | 175 | mulridd 11278 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝐺‘(𝑥 + 𝑇)) · 1) = (𝐺‘(𝑥 + 𝑇))) |
| 177 | 42, 73 | eqtri 2765 |
. . . . . . . 8
⊢ 𝐺 = (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇))) |
| 178 | 177 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐺 = (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇)))) |
| 179 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑤 = (𝑥 + 𝑇) → (𝐹‘(𝑤 − 𝑇)) = (𝐹‘((𝑥 + 𝑇) − 𝑇))) |
| 180 | 158 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℂ) |
| 181 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℂ) |
| 182 | 180, 181 | pncand 11621 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 + 𝑇) − 𝑇) = 𝑥) |
| 183 | 182 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + 𝑇) − 𝑇)) = (𝐹‘𝑥)) |
| 184 | 179, 183 | sylan9eqr 2799 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑤 = (𝑥 + 𝑇)) → (𝐹‘(𝑤 − 𝑇)) = (𝐹‘𝑥)) |
| 185 | 12 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
| 186 | 178, 184,
174, 185 | fvmptd 7023 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐺‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
| 187 | 176, 186 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝐺‘(𝑥 + 𝑇)) · 1) = (𝐹‘𝑥)) |
| 188 | 187 | itgeq2dv 25817 |
. . . 4
⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝐺‘(𝑥 + 𝑇)) · 1) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
| 189 | 154, 188 | eqtrid 2789 |
. . 3
⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
| 190 | 146, 151,
189 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |
| 191 | 46, 145, 190 | 3eqtrd 2781 |
1
⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) |