Step | Hyp | Ref
| Expression |
1 | | itgiccshift.a |
. . . . 5
β’ (π β π΄ β β) |
2 | | itgiccshift.b |
. . . . 5
β’ (π β π΅ β β) |
3 | | itgiccshift.t |
. . . . . 6
β’ (π β π β
β+) |
4 | 3 | rpred 12965 |
. . . . 5
β’ (π β π β β) |
5 | | itgiccshift.aleb |
. . . . 5
β’ (π β π΄ β€ π΅) |
6 | 1, 2, 4, 5 | leadd1dd 11777 |
. . . 4
β’ (π β (π΄ + π) β€ (π΅ + π)) |
7 | 6 | ditgpos 25243 |
. . 3
β’ (π β β¨[(π΄ + π) β (π΅ + π)](πΊβπ₯) dπ₯ = β«((π΄ + π)(,)(π΅ + π))(πΊβπ₯) dπ₯) |
8 | 1, 4 | readdcld 11192 |
. . . 4
β’ (π β (π΄ + π) β β) |
9 | 2, 4 | readdcld 11192 |
. . . 4
β’ (π β (π΅ + π) β β) |
10 | | itgiccshift.f |
. . . . . . . . 9
β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) |
11 | | cncff 24279 |
. . . . . . . . 9
β’ (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
13 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β πΉ:(π΄[,]π΅)βΆβ) |
14 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π΄ β β) |
15 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π΅ β β) |
16 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π΄ + π) β β) |
17 | 9 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π΅ + π) β β) |
18 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ β ((π΄ + π)[,](π΅ + π))) |
19 | | eliccre 43833 |
. . . . . . . . . 10
β’ (((π΄ + π) β β β§ (π΅ + π) β β β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ β β) |
20 | 16, 17, 18, 19 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ β β) |
21 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π β β) |
22 | 20, 21 | resubcld 11591 |
. . . . . . . 8
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β π) β β) |
23 | 1 | recnd 11191 |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
24 | 4 | recnd 11191 |
. . . . . . . . . . . 12
β’ (π β π β β) |
25 | 23, 24 | pncand 11521 |
. . . . . . . . . . 11
β’ (π β ((π΄ + π) β π) = π΄) |
26 | 25 | eqcomd 2739 |
. . . . . . . . . 10
β’ (π β π΄ = ((π΄ + π) β π)) |
27 | 26 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π΄ = ((π΄ + π) β π)) |
28 | | elicc2 13338 |
. . . . . . . . . . . . 13
β’ (((π΄ + π) β β β§ (π΅ + π) β β) β (π₯ β ((π΄ + π)[,](π΅ + π)) β (π₯ β β β§ (π΄ + π) β€ π₯ β§ π₯ β€ (π΅ + π)))) |
29 | 16, 17, 28 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β ((π΄ + π)[,](π΅ + π)) β (π₯ β β β§ (π΄ + π) β€ π₯ β§ π₯ β€ (π΅ + π)))) |
30 | 18, 29 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β β β§ (π΄ + π) β€ π₯ β§ π₯ β€ (π΅ + π))) |
31 | 30 | simp2d 1144 |
. . . . . . . . . 10
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π΄ + π) β€ π₯) |
32 | 16, 20, 21, 31 | lesub1dd 11779 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β ((π΄ + π) β π) β€ (π₯ β π)) |
33 | 27, 32 | eqbrtrd 5131 |
. . . . . . . 8
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π΄ β€ (π₯ β π)) |
34 | 30 | simp3d 1145 |
. . . . . . . . . 10
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ β€ (π΅ + π)) |
35 | 20, 17, 21, 34 | lesub1dd 11779 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β π) β€ ((π΅ + π) β π)) |
36 | 2 | recnd 11191 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
37 | 36, 24 | pncand 11521 |
. . . . . . . . . 10
β’ (π β ((π΅ + π) β π) = π΅) |
38 | 37 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β ((π΅ + π) β π) = π΅) |
39 | 35, 38 | breqtrd 5135 |
. . . . . . . 8
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β π) β€ π΅) |
40 | 14, 15, 22, 33, 39 | eliccd 43832 |
. . . . . . 7
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β π) β (π΄[,]π΅)) |
41 | 13, 40 | ffvelcdmd 7040 |
. . . . . 6
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (πΉβ(π₯ β π)) β β) |
42 | | itgiccshift.g |
. . . . . 6
β’ πΊ = (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π₯ β π))) |
43 | 41, 42 | fmptd 7066 |
. . . . 5
β’ (π β πΊ:((π΄ + π)[,](π΅ + π))βΆβ) |
44 | 43 | ffvelcdmda 7039 |
. . . 4
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (πΊβπ₯) β β) |
45 | 8, 9, 44 | itgioo 25203 |
. . 3
β’ (π β β«((π΄ + π)(,)(π΅ + π))(πΊβπ₯) dπ₯ = β«((π΄ + π)[,](π΅ + π))(πΊβπ₯) dπ₯) |
46 | 7, 45 | eqtr2d 2774 |
. 2
β’ (π β β«((π΄ + π)[,](π΅ + π))(πΊβπ₯) dπ₯ = β¨[(π΄ + π) β (π΅ + π)](πΊβπ₯) dπ₯) |
47 | | eqid 2733 |
. . . 4
β’ (π¦ β β β¦ (π¦ + π)) = (π¦ β β β¦ (π¦ + π)) |
48 | 47 | addccncf 24303 |
. . . . 5
β’ (π β β β (π¦ β β β¦ (π¦ + π)) β (ββcnββ)) |
49 | 24, 48 | syl 17 |
. . . 4
β’ (π β (π¦ β β β¦ (π¦ + π)) β (ββcnββ)) |
50 | 1, 2 | iccssred 13360 |
. . . . 5
β’ (π β (π΄[,]π΅) β β) |
51 | | ax-resscn 11116 |
. . . . 5
β’ β
β β |
52 | 50, 51 | sstrdi 3960 |
. . . 4
β’ (π β (π΄[,]π΅) β β) |
53 | 8, 9 | iccssred 13360 |
. . . . 5
β’ (π β ((π΄ + π)[,](π΅ + π)) β β) |
54 | 53, 51 | sstrdi 3960 |
. . . 4
β’ (π β ((π΄ + π)[,](π΅ + π)) β β) |
55 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π΄ + π) β β) |
56 | 9 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π΅ + π) β β) |
57 | 50 | sselda 3948 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π¦ β β) |
58 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π β β) |
59 | 57, 58 | readdcld 11192 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ + π) β β) |
60 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π΄ β β) |
61 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄[,]π΅)) β π¦ β (π΄[,]π΅)) |
62 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄[,]π΅)) β π΅ β β) |
63 | | elicc2 13338 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β) β (π¦ β (π΄[,]π΅) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅))) |
64 | 60, 62, 63 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ β (π΄[,]π΅) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅))) |
65 | 61, 64 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅)) |
66 | 65 | simp2d 1144 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π΄ β€ π¦) |
67 | 60, 57, 58, 66 | leadd1dd 11777 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π΄ + π) β€ (π¦ + π)) |
68 | 65 | simp3d 1145 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π¦ β€ π΅) |
69 | 57, 62, 58, 68 | leadd1dd 11777 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ + π) β€ (π΅ + π)) |
70 | 55, 56, 59, 67, 69 | eliccd 43832 |
. . . 4
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ + π) β ((π΄ + π)[,](π΅ + π))) |
71 | 47, 49, 52, 54, 70 | cncfmptssg 44202 |
. . 3
β’ (π β (π¦ β (π΄[,]π΅) β¦ (π¦ + π)) β ((π΄[,]π΅)βcnβ((π΄ + π)[,](π΅ + π)))) |
72 | | fvoveq1 7384 |
. . . . . . . 8
β’ (π₯ = π€ β (πΉβ(π₯ β π)) = (πΉβ(π€ β π))) |
73 | 72 | cbvmptv 5222 |
. . . . . . 7
β’ (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π₯ β π))) = (π€ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π€ β π))) |
74 | 1, 2, 4 | iccshift 43846 |
. . . . . . . 8
β’ (π β ((π΄ + π)[,](π΅ + π)) = {π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)}) |
75 | 74 | mpteq1d 5204 |
. . . . . . 7
β’ (π β (π€ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π€ β π))) = (π€ β {π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)} β¦ (πΉβ(π€ β π)))) |
76 | 73, 75 | eqtrid 2785 |
. . . . . 6
β’ (π β (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π₯ β π))) = (π€ β {π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)} β¦ (πΉβ(π€ β π)))) |
77 | 42, 76 | eqtrid 2785 |
. . . . 5
β’ (π β πΊ = (π€ β {π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)} β¦ (πΉβ(π€ β π)))) |
78 | | eqeq1 2737 |
. . . . . . . . . 10
β’ (π€ = π₯ β (π€ = (π§ + π) β π₯ = (π§ + π))) |
79 | 78 | rexbidv 3172 |
. . . . . . . . 9
β’ (π€ = π₯ β (βπ§ β (π΄[,]π΅)π€ = (π§ + π) β βπ§ β (π΄[,]π΅)π₯ = (π§ + π))) |
80 | | oveq1 7368 |
. . . . . . . . . . 11
β’ (π§ = π¦ β (π§ + π) = (π¦ + π)) |
81 | 80 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π§ = π¦ β (π₯ = (π§ + π) β π₯ = (π¦ + π))) |
82 | 81 | cbvrexvw 3225 |
. . . . . . . . 9
β’
(βπ§ β
(π΄[,]π΅)π₯ = (π§ + π) β βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)) |
83 | 79, 82 | bitrdi 287 |
. . . . . . . 8
β’ (π€ = π₯ β (βπ§ β (π΄[,]π΅)π€ = (π§ + π) β βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π))) |
84 | 83 | cbvrabv 3416 |
. . . . . . 7
β’ {π€ β β β£
βπ§ β (π΄[,]π΅)π€ = (π§ + π)} = {π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)} |
85 | 84 | eqcomi 2742 |
. . . . . 6
β’ {π₯ β β β£
βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)} = {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)} |
86 | | eqid 2733 |
. . . . . 6
β’ (π€ β {π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)} β¦ (πΉβ(π€ β π))) = (π€ β {π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)} β¦ (πΉβ(π€ β π))) |
87 | 52, 24, 85, 10, 86 | cncfshift 44205 |
. . . . 5
β’ (π β (π€ β {π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)} β¦ (πΉβ(π€ β π))) β ({π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)}βcnββ)) |
88 | 77, 87 | eqeltrd 2834 |
. . . 4
β’ (π β πΊ β ({π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)}βcnββ)) |
89 | 43 | feqmptd 6914 |
. . . 4
β’ (π β πΊ = (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΊβπ₯))) |
90 | 74 | eqcomd 2739 |
. . . . 5
β’ (π β {π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)} = ((π΄ + π)[,](π΅ + π))) |
91 | 90 | oveq1d 7376 |
. . . 4
β’ (π β ({π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)}βcnββ) = (((π΄ + π)[,](π΅ + π))βcnββ)) |
92 | 88, 89, 91 | 3eltr3d 2848 |
. . 3
β’ (π β (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΊβπ₯)) β (((π΄ + π)[,](π΅ + π))βcnββ)) |
93 | | ioosscn 13335 |
. . . . . 6
β’ (π΄(,)π΅) β β |
94 | 93 | a1i 11 |
. . . . 5
β’ (π β (π΄(,)π΅) β β) |
95 | | 1cnd 11158 |
. . . . 5
β’ (π β 1 β
β) |
96 | | ssid 3970 |
. . . . . 6
β’ β
β β |
97 | 96 | a1i 11 |
. . . . 5
β’ (π β β β
β) |
98 | 94, 95, 97 | constcncfg 44203 |
. . . 4
β’ (π β (π¦ β (π΄(,)π΅) β¦ 1) β ((π΄(,)π΅)βcnββ)) |
99 | | fconstmpt 5698 |
. . . . 5
β’ ((π΄(,)π΅) Γ {1}) = (π¦ β (π΄(,)π΅) β¦ 1) |
100 | | ioombl 24952 |
. . . . . . 7
β’ (π΄(,)π΅) β dom vol |
101 | 100 | a1i 11 |
. . . . . 6
β’ (π β (π΄(,)π΅) β dom vol) |
102 | | ioovolcl 24957 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β) β
(volβ(π΄(,)π΅)) β
β) |
103 | 1, 2, 102 | syl2anc 585 |
. . . . . 6
β’ (π β (volβ(π΄(,)π΅)) β β) |
104 | | iblconst 25205 |
. . . . . 6
β’ (((π΄(,)π΅) β dom vol β§ (volβ(π΄(,)π΅)) β β β§ 1 β β)
β ((π΄(,)π΅) Γ {1}) β
πΏ1) |
105 | 101, 103,
95, 104 | syl3anc 1372 |
. . . . 5
β’ (π β ((π΄(,)π΅) Γ {1}) β
πΏ1) |
106 | 99, 105 | eqeltrrid 2839 |
. . . 4
β’ (π β (π¦ β (π΄(,)π΅) β¦ 1) β
πΏ1) |
107 | 98, 106 | elind 4158 |
. . 3
β’ (π β (π¦ β (π΄(,)π΅) β¦ 1) β (((π΄(,)π΅)βcnββ) β©
πΏ1)) |
108 | 50 | resmptd 5998 |
. . . . . . 7
β’ (π β ((π¦ β β β¦ (π¦ + π)) βΎ (π΄[,]π΅)) = (π¦ β (π΄[,]π΅) β¦ (π¦ + π))) |
109 | 108 | eqcomd 2739 |
. . . . . 6
β’ (π β (π¦ β (π΄[,]π΅) β¦ (π¦ + π)) = ((π¦ β β β¦ (π¦ + π)) βΎ (π΄[,]π΅))) |
110 | 109 | oveq2d 7377 |
. . . . 5
β’ (π β (β D (π¦ β (π΄[,]π΅) β¦ (π¦ + π))) = (β D ((π¦ β β β¦ (π¦ + π)) βΎ (π΄[,]π΅)))) |
111 | 51 | a1i 11 |
. . . . . 6
β’ (π β β β
β) |
112 | 111 | sselda 3948 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β π¦ β β) |
113 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β π β β) |
114 | 112, 113 | addcld 11182 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (π¦ + π) β β) |
115 | 114 | fmpttd 7067 |
. . . . . 6
β’ (π β (π¦ β β β¦ (π¦ + π)):ββΆβ) |
116 | | ssid 3970 |
. . . . . . 7
β’ β
β β |
117 | 116 | a1i 11 |
. . . . . 6
β’ (π β β β
β) |
118 | | eqid 2733 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
119 | 118 | tgioo2 24189 |
. . . . . . 7
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
120 | 118, 119 | dvres 25298 |
. . . . . 6
β’
(((β β β β§ (π¦ β β β¦ (π¦ + π)):ββΆβ) β§ (β
β β β§ (π΄[,]π΅) β β)) β (β D
((π¦ β β β¦
(π¦ + π)) βΎ (π΄[,]π΅))) = ((β D (π¦ β β β¦ (π¦ + π))) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅)))) |
121 | 111, 115,
117, 50, 120 | syl22anc 838 |
. . . . 5
β’ (π β (β D ((π¦ β β β¦ (π¦ + π)) βΎ (π΄[,]π΅))) = ((β D (π¦ β β β¦ (π¦ + π))) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅)))) |
122 | 110, 121 | eqtrd 2773 |
. . . 4
β’ (π β (β D (π¦ β (π΄[,]π΅) β¦ (π¦ + π))) = ((β D (π¦ β β β¦ (π¦ + π))) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅)))) |
123 | | iccntr 24207 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
124 | 1, 2, 123 | syl2anc 585 |
. . . . 5
β’ (π β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
125 | 124 | reseq2d 5941 |
. . . 4
β’ (π β ((β D (π¦ β β β¦ (π¦ + π))) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅))) = ((β D (π¦ β β β¦ (π¦ + π))) βΎ (π΄(,)π΅))) |
126 | | reelprrecn 11151 |
. . . . . . . 8
β’ β
β {β, β} |
127 | 126 | a1i 11 |
. . . . . . 7
β’ (π β β β {β,
β}) |
128 | | 1cnd 11158 |
. . . . . . 7
β’ ((π β§ π¦ β β) β 1 β
β) |
129 | 127 | dvmptid 25344 |
. . . . . . 7
β’ (π β (β D (π¦ β β β¦ π¦)) = (π¦ β β β¦ 1)) |
130 | | 0cnd 11156 |
. . . . . . 7
β’ ((π β§ π¦ β β) β 0 β
β) |
131 | 127, 24 | dvmptc 25345 |
. . . . . . 7
β’ (π β (β D (π¦ β β β¦ π)) = (π¦ β β β¦ 0)) |
132 | 127, 112,
128, 129, 113, 130, 131 | dvmptadd 25347 |
. . . . . 6
β’ (π β (β D (π¦ β β β¦ (π¦ + π))) = (π¦ β β β¦ (1 +
0))) |
133 | 132 | reseq1d 5940 |
. . . . 5
β’ (π β ((β D (π¦ β β β¦ (π¦ + π))) βΎ (π΄(,)π΅)) = ((π¦ β β β¦ (1 + 0)) βΎ
(π΄(,)π΅))) |
134 | | ioossre 13334 |
. . . . . . 7
β’ (π΄(,)π΅) β β |
135 | 134 | a1i 11 |
. . . . . 6
β’ (π β (π΄(,)π΅) β β) |
136 | 135 | resmptd 5998 |
. . . . 5
β’ (π β ((π¦ β β β¦ (1 + 0)) βΎ
(π΄(,)π΅)) = (π¦ β (π΄(,)π΅) β¦ (1 + 0))) |
137 | | 1p0e1 12285 |
. . . . . . 7
β’ (1 + 0) =
1 |
138 | 137 | mpteq2i 5214 |
. . . . . 6
β’ (π¦ β (π΄(,)π΅) β¦ (1 + 0)) = (π¦ β (π΄(,)π΅) β¦ 1) |
139 | 138 | a1i 11 |
. . . . 5
β’ (π β (π¦ β (π΄(,)π΅) β¦ (1 + 0)) = (π¦ β (π΄(,)π΅) β¦ 1)) |
140 | 133, 136,
139 | 3eqtrd 2777 |
. . . 4
β’ (π β ((β D (π¦ β β β¦ (π¦ + π))) βΎ (π΄(,)π΅)) = (π¦ β (π΄(,)π΅) β¦ 1)) |
141 | 122, 125,
140 | 3eqtrd 2777 |
. . 3
β’ (π β (β D (π¦ β (π΄[,]π΅) β¦ (π¦ + π))) = (π¦ β (π΄(,)π΅) β¦ 1)) |
142 | | fveq2 6846 |
. . 3
β’ (π₯ = (π¦ + π) β (πΊβπ₯) = (πΊβ(π¦ + π))) |
143 | | oveq1 7368 |
. . 3
β’ (π¦ = π΄ β (π¦ + π) = (π΄ + π)) |
144 | | oveq1 7368 |
. . 3
β’ (π¦ = π΅ β (π¦ + π) = (π΅ + π)) |
145 | 1, 2, 5, 71, 92, 107, 141, 142, 143, 144, 8, 9 | itgsubsticc 44307 |
. 2
β’ (π β β¨[(π΄ + π) β (π΅ + π)](πΊβπ₯) dπ₯ = β¨[π΄ β π΅]((πΊβ(π¦ + π)) Β· 1) dπ¦) |
146 | 5 | ditgpos 25243 |
. . 3
β’ (π β β¨[π΄ β π΅]((πΊβ(π¦ + π)) Β· 1) dπ¦ = β«(π΄(,)π΅)((πΊβ(π¦ + π)) Β· 1) dπ¦) |
147 | 43 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β πΊ:((π΄ + π)[,](π΅ + π))βΆβ) |
148 | 147, 70 | ffvelcdmd 7040 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (πΊβ(π¦ + π)) β β) |
149 | | 1cnd 11158 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β 1 β β) |
150 | 148, 149 | mulcld 11183 |
. . . 4
β’ ((π β§ π¦ β (π΄[,]π΅)) β ((πΊβ(π¦ + π)) Β· 1) β
β) |
151 | 1, 2, 150 | itgioo 25203 |
. . 3
β’ (π β β«(π΄(,)π΅)((πΊβ(π¦ + π)) Β· 1) dπ¦ = β«(π΄[,]π΅)((πΊβ(π¦ + π)) Β· 1) dπ¦) |
152 | | fvoveq1 7384 |
. . . . . 6
β’ (π¦ = π₯ β (πΊβ(π¦ + π)) = (πΊβ(π₯ + π))) |
153 | 152 | oveq1d 7376 |
. . . . 5
β’ (π¦ = π₯ β ((πΊβ(π¦ + π)) Β· 1) = ((πΊβ(π₯ + π)) Β· 1)) |
154 | 153 | cbvitgv 25164 |
. . . 4
β’
β«(π΄[,]π΅)((πΊβ(π¦ + π)) Β· 1) dπ¦ = β«(π΄[,]π΅)((πΊβ(π₯ + π)) Β· 1) dπ₯ |
155 | 43 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄[,]π΅)) β πΊ:((π΄ + π)[,](π΅ + π))βΆβ) |
156 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π΄ + π) β β) |
157 | 9 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π΅ + π) β β) |
158 | 50 | sselda 3948 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
159 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π β β) |
160 | 158, 159 | readdcld 11192 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π₯ + π) β β) |
161 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β β) |
162 | 1 | rexrd 11213 |
. . . . . . . . . . . 12
β’ (π β π΄ β
β*) |
163 | 162 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β
β*) |
164 | 2 | rexrd 11213 |
. . . . . . . . . . . 12
β’ (π β π΅ β
β*) |
165 | 164 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΅ β
β*) |
166 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β (π΄[,]π΅)) |
167 | | iccgelb 13329 |
. . . . . . . . . . 11
β’ ((π΄ β β*
β§ π΅ β
β* β§ π₯
β (π΄[,]π΅)) β π΄ β€ π₯) |
168 | 163, 165,
166, 167 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β€ π₯) |
169 | 161, 158,
159, 168 | leadd1dd 11777 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π΄ + π) β€ (π₯ + π)) |
170 | 2 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΅ β β) |
171 | | iccleub 13328 |
. . . . . . . . . . 11
β’ ((π΄ β β*
β§ π΅ β
β* β§ π₯
β (π΄[,]π΅)) β π₯ β€ π΅) |
172 | 163, 165,
166, 171 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β€ π΅) |
173 | 158, 170,
159, 172 | leadd1dd 11777 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π₯ + π) β€ (π΅ + π)) |
174 | 156, 157,
160, 169, 173 | eliccd 43832 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π₯ + π) β ((π΄ + π)[,](π΅ + π))) |
175 | 155, 174 | ffvelcdmd 7040 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΊβ(π₯ + π)) β β) |
176 | 175 | mulid1d 11180 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β ((πΊβ(π₯ + π)) Β· 1) = (πΊβ(π₯ + π))) |
177 | 42, 73 | eqtri 2761 |
. . . . . . . 8
β’ πΊ = (π€ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π€ β π))) |
178 | 177 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β πΊ = (π€ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π€ β π)))) |
179 | | fvoveq1 7384 |
. . . . . . . 8
β’ (π€ = (π₯ + π) β (πΉβ(π€ β π)) = (πΉβ((π₯ + π) β π))) |
180 | 158 | recnd 11191 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
181 | 24 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π β β) |
182 | 180, 181 | pncand 11521 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β ((π₯ + π) β π) = π₯) |
183 | 182 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβ((π₯ + π) β π)) = (πΉβπ₯)) |
184 | 179, 183 | sylan9eqr 2795 |
. . . . . . 7
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ π€ = (π₯ + π)) β (πΉβ(π€ β π)) = (πΉβπ₯)) |
185 | 12 | ffvelcdmda 7039 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) β β) |
186 | 178, 184,
174, 185 | fvmptd 6959 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΊβ(π₯ + π)) = (πΉβπ₯)) |
187 | 176, 186 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β ((πΊβ(π₯ + π)) Β· 1) = (πΉβπ₯)) |
188 | 187 | itgeq2dv 25169 |
. . . 4
β’ (π β β«(π΄[,]π΅)((πΊβ(π₯ + π)) Β· 1) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
189 | 154, 188 | eqtrid 2785 |
. . 3
β’ (π β β«(π΄[,]π΅)((πΊβ(π¦ + π)) Β· 1) dπ¦ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
190 | 146, 151,
189 | 3eqtrd 2777 |
. 2
β’ (π β β¨[π΄ β π΅]((πΊβ(π¦ + π)) Β· 1) dπ¦ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
191 | 46, 145, 190 | 3eqtrd 2777 |
1
β’ (π β β«((π΄ + π)[,](π΅ + π))(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |