Step | Hyp | Ref
| Expression |
1 | | itgperiod.a |
. . . . 5
β’ (π β π΄ β β) |
2 | | itgperiod.b |
. . . . 5
β’ (π β π΅ β β) |
3 | | itgperiod.t |
. . . . . 6
β’ (π β π β
β+) |
4 | 3 | rpred 13016 |
. . . . 5
β’ (π β π β β) |
5 | | itgperiod.aleb |
. . . . 5
β’ (π β π΄ β€ π΅) |
6 | 1, 2, 4, 5 | leadd1dd 11828 |
. . . 4
β’ (π β (π΄ + π) β€ (π΅ + π)) |
7 | 6 | ditgpos 25373 |
. . 3
β’ (π β β¨[(π΄ + π) β (π΅ + π)](πΉβπ₯) dπ₯ = β«((π΄ + π)(,)(π΅ + π))(πΉβπ₯) dπ₯) |
8 | 1, 4 | readdcld 11243 |
. . . 4
β’ (π β (π΄ + π) β β) |
9 | 2, 4 | readdcld 11243 |
. . . 4
β’ (π β (π΅ + π) β β) |
10 | | itgperiod.f |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
11 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β πΉ:ββΆβ) |
12 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π΄ + π) β β) |
13 | 9 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π΅ + π) β β) |
14 | | simpr 486 |
. . . . . 6
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ β ((π΄ + π)[,](π΅ + π))) |
15 | | eliccre 44218 |
. . . . . 6
β’ (((π΄ + π) β β β§ (π΅ + π) β β β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ β β) |
16 | 12, 13, 14, 15 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ β β) |
17 | 11, 16 | ffvelcdmd 7088 |
. . . 4
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (πΉβπ₯) β β) |
18 | 8, 9, 17 | itgioo 25333 |
. . 3
β’ (π β β«((π΄ + π)(,)(π΅ + π))(πΉβπ₯) dπ₯ = β«((π΄ + π)[,](π΅ + π))(πΉβπ₯) dπ₯) |
19 | 7, 18 | eqtr2d 2774 |
. 2
β’ (π β β«((π΄ + π)[,](π΅ + π))(πΉβπ₯) dπ₯ = β¨[(π΄ + π) β (π΅ + π)](πΉβπ₯) dπ₯) |
20 | | eqid 2733 |
. . . 4
β’ (π¦ β β β¦ (π¦ + π)) = (π¦ β β β¦ (π¦ + π)) |
21 | 4 | recnd 11242 |
. . . . 5
β’ (π β π β β) |
22 | 20 | addccncf 24433 |
. . . . 5
β’ (π β β β (π¦ β β β¦ (π¦ + π)) β (ββcnββ)) |
23 | 21, 22 | syl 17 |
. . . 4
β’ (π β (π¦ β β β¦ (π¦ + π)) β (ββcnββ)) |
24 | 1, 2 | iccssred 13411 |
. . . . 5
β’ (π β (π΄[,]π΅) β β) |
25 | | ax-resscn 11167 |
. . . . 5
β’ β
β β |
26 | 24, 25 | sstrdi 3995 |
. . . 4
β’ (π β (π΄[,]π΅) β β) |
27 | 8, 9 | iccssred 13411 |
. . . . 5
β’ (π β ((π΄ + π)[,](π΅ + π)) β β) |
28 | 27, 25 | sstrdi 3995 |
. . . 4
β’ (π β ((π΄ + π)[,](π΅ + π)) β β) |
29 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π΄ + π) β β) |
30 | 9 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π΅ + π) β β) |
31 | 24 | sselda 3983 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π¦ β β) |
32 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π β β) |
33 | 31, 32 | readdcld 11243 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ + π) β β) |
34 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π΄ β β) |
35 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄[,]π΅)) β π¦ β (π΄[,]π΅)) |
36 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄[,]π΅)) β π΅ β β) |
37 | | elicc2 13389 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β) β (π¦ β (π΄[,]π΅) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅))) |
38 | 34, 36, 37 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ β (π΄[,]π΅) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅))) |
39 | 35, 38 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅)) |
40 | 39 | simp2d 1144 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π΄ β€ π¦) |
41 | 34, 31, 32, 40 | leadd1dd 11828 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π΄ + π) β€ (π¦ + π)) |
42 | 39 | simp3d 1145 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π¦ β€ π΅) |
43 | 31, 36, 32, 42 | leadd1dd 11828 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ + π) β€ (π΅ + π)) |
44 | 29, 30, 33, 41, 43 | eliccd 44217 |
. . . 4
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ + π) β ((π΄ + π)[,](π΅ + π))) |
45 | 20, 23, 26, 28, 44 | cncfmptssg 44587 |
. . 3
β’ (π β (π¦ β (π΄[,]π΅) β¦ (π¦ + π)) β ((π΄[,]π΅)βcnβ((π΄ + π)[,](π΅ + π)))) |
46 | | eqeq1 2737 |
. . . . . . . 8
β’ (π€ = π₯ β (π€ = (π§ + π) β π₯ = (π§ + π))) |
47 | 46 | rexbidv 3179 |
. . . . . . 7
β’ (π€ = π₯ β (βπ§ β (π΄[,]π΅)π€ = (π§ + π) β βπ§ β (π΄[,]π΅)π₯ = (π§ + π))) |
48 | | oveq1 7416 |
. . . . . . . . 9
β’ (π§ = π¦ β (π§ + π) = (π¦ + π)) |
49 | 48 | eqeq2d 2744 |
. . . . . . . 8
β’ (π§ = π¦ β (π₯ = (π§ + π) β π₯ = (π¦ + π))) |
50 | 49 | cbvrexvw 3236 |
. . . . . . 7
β’
(βπ§ β
(π΄[,]π΅)π₯ = (π§ + π) β βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)) |
51 | 47, 50 | bitrdi 287 |
. . . . . 6
β’ (π€ = π₯ β (βπ§ β (π΄[,]π΅)π€ = (π§ + π) β βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π))) |
52 | 51 | cbvrabv 3443 |
. . . . 5
β’ {π€ β β β£
βπ§ β (π΄[,]π΅)π€ = (π§ + π)} = {π₯ β β β£ βπ¦ β (π΄[,]π΅)π₯ = (π¦ + π)} |
53 | 10 | ffdmd 6749 |
. . . . 5
β’ (π β πΉ:dom πΉβΆβ) |
54 | | simp3 1139 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π΄[,]π΅) β§ π€ = (π§ + π)) β π€ = (π§ + π)) |
55 | 24 | sselda 3983 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (π΄[,]π΅)) β π§ β β) |
56 | 4 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (π΄[,]π΅)) β π β β) |
57 | 55, 56 | readdcld 11243 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π΄[,]π΅)) β (π§ + π) β β) |
58 | 57 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π΄[,]π΅) β§ π€ = (π§ + π)) β (π§ + π) β β) |
59 | 54, 58 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ π§ β (π΄[,]π΅) β§ π€ = (π§ + π)) β π€ β β) |
60 | 59 | rexlimdv3a 3160 |
. . . . . . . 8
β’ (π β (βπ§ β (π΄[,]π΅)π€ = (π§ + π) β π€ β β)) |
61 | 60 | ralrimivw 3151 |
. . . . . . 7
β’ (π β βπ€ β β (βπ§ β (π΄[,]π΅)π€ = (π§ + π) β π€ β β)) |
62 | | rabss 4070 |
. . . . . . 7
β’ ({π€ β β β£
βπ§ β (π΄[,]π΅)π€ = (π§ + π)} β β β βπ€ β β (βπ§ β (π΄[,]π΅)π€ = (π§ + π) β π€ β β)) |
63 | 61, 62 | sylibr 233 |
. . . . . 6
β’ (π β {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)} β β) |
64 | 10 | fdmd 6729 |
. . . . . 6
β’ (π β dom πΉ = β) |
65 | 63, 64 | sseqtrrd 4024 |
. . . . 5
β’ (π β {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)} β dom πΉ) |
66 | | itgperiod.fper |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
67 | | itgperiod.fcn |
. . . . 5
β’ (π β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) |
68 | 26, 4, 52, 53, 65, 66, 67 | cncfperiod 44595 |
. . . 4
β’ (π β (πΉ βΎ {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)}) β ({π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)}βcnββ)) |
69 | 47 | elrab 3684 |
. . . . . . . . 9
β’ (π₯ β {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)} β (π₯ β β β§ βπ§ β (π΄[,]π΅)π₯ = (π§ + π))) |
70 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ βπ§ β (π΄[,]π΅)π₯ = (π§ + π))) β βπ§ β (π΄[,]π΅)π₯ = (π§ + π)) |
71 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π§π |
72 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π§ π₯ β β |
73 | | nfre1 3283 |
. . . . . . . . . . . . 13
β’
β²π§βπ§ β (π΄[,]π΅)π₯ = (π§ + π) |
74 | 72, 73 | nfan 1903 |
. . . . . . . . . . . 12
β’
β²π§(π₯ β β β§
βπ§ β (π΄[,]π΅)π₯ = (π§ + π)) |
75 | 71, 74 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π§(π β§ (π₯ β β β§ βπ§ β (π΄[,]π΅)π₯ = (π§ + π))) |
76 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π§ π₯ β ((π΄ + π)[,](π΅ + π)) |
77 | | simp3 1139 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β (π΄[,]π΅) β§ π₯ = (π§ + π)) β π₯ = (π§ + π)) |
78 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β (π΄[,]π΅)) β π΄ β β) |
79 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π§ β (π΄[,]π΅)) β π§ β (π΄[,]π΅)) |
80 | 2 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π§ β (π΄[,]π΅)) β π΅ β β) |
81 | | elicc2 13389 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β β β§ π΅ β β) β (π§ β (π΄[,]π΅) β (π§ β β β§ π΄ β€ π§ β§ π§ β€ π΅))) |
82 | 78, 80, 81 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π§ β (π΄[,]π΅)) β (π§ β (π΄[,]π΅) β (π§ β β β§ π΄ β€ π§ β§ π§ β€ π΅))) |
83 | 79, 82 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β (π΄[,]π΅)) β (π§ β β β§ π΄ β€ π§ β§ π§ β€ π΅)) |
84 | 83 | simp2d 1144 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β (π΄[,]π΅)) β π΄ β€ π§) |
85 | 78, 55, 56, 84 | leadd1dd 11828 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β (π΄[,]π΅)) β (π΄ + π) β€ (π§ + π)) |
86 | 83 | simp3d 1145 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β (π΄[,]π΅)) β π§ β€ π΅) |
87 | 55, 80, 56, 86 | leadd1dd 11828 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β (π΄[,]π΅)) β (π§ + π) β€ (π΅ + π)) |
88 | 57, 85, 87 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β (π΄[,]π΅)) β ((π§ + π) β β β§ (π΄ + π) β€ (π§ + π) β§ (π§ + π) β€ (π΅ + π))) |
89 | 88 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β (π΄[,]π΅) β§ π₯ = (π§ + π)) β ((π§ + π) β β β§ (π΄ + π) β€ (π§ + π) β§ (π§ + π) β€ (π΅ + π))) |
90 | 8 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β (π΄[,]π΅) β§ π₯ = (π§ + π)) β (π΄ + π) β β) |
91 | 9 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β (π΄[,]π΅) β§ π₯ = (π§ + π)) β (π΅ + π) β β) |
92 | | elicc2 13389 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ + π) β β β§ (π΅ + π) β β) β ((π§ + π) β ((π΄ + π)[,](π΅ + π)) β ((π§ + π) β β β§ (π΄ + π) β€ (π§ + π) β§ (π§ + π) β€ (π΅ + π)))) |
93 | 90, 91, 92 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β (π΄[,]π΅) β§ π₯ = (π§ + π)) β ((π§ + π) β ((π΄ + π)[,](π΅ + π)) β ((π§ + π) β β β§ (π΄ + π) β€ (π§ + π) β§ (π§ + π) β€ (π΅ + π)))) |
94 | 89, 93 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β (π΄[,]π΅) β§ π₯ = (π§ + π)) β (π§ + π) β ((π΄ + π)[,](π΅ + π))) |
95 | 77, 94 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β (π΄[,]π΅) β§ π₯ = (π§ + π)) β π₯ β ((π΄ + π)[,](π΅ + π))) |
96 | 95 | 3exp 1120 |
. . . . . . . . . . . 12
β’ (π β (π§ β (π΄[,]π΅) β (π₯ = (π§ + π) β π₯ β ((π΄ + π)[,](π΅ + π))))) |
97 | 96 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ βπ§ β (π΄[,]π΅)π₯ = (π§ + π))) β (π§ β (π΄[,]π΅) β (π₯ = (π§ + π) β π₯ β ((π΄ + π)[,](π΅ + π))))) |
98 | 75, 76, 97 | rexlimd 3264 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ βπ§ β (π΄[,]π΅)π₯ = (π§ + π))) β (βπ§ β (π΄[,]π΅)π₯ = (π§ + π) β π₯ β ((π΄ + π)[,](π΅ + π)))) |
99 | 70, 98 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ βπ§ β (π΄[,]π΅)π₯ = (π§ + π))) β π₯ β ((π΄ + π)[,](π΅ + π))) |
100 | 69, 99 | sylan2b 595 |
. . . . . . . 8
β’ ((π β§ π₯ β {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)}) β π₯ β ((π΄ + π)[,](π΅ + π))) |
101 | 16 | recnd 11242 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ β β) |
102 | 1 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π΄ β β) |
103 | 2 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π΅ β β) |
104 | 4 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π β β) |
105 | 16, 104 | resubcld 11642 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β π) β β) |
106 | 1 | recnd 11242 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β β) |
107 | 106, 21 | pncand 11572 |
. . . . . . . . . . . . . 14
β’ (π β ((π΄ + π) β π) = π΄) |
108 | 107 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ (π β π΄ = ((π΄ + π) β π)) |
109 | 108 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π΄ = ((π΄ + π) β π)) |
110 | | elicc2 13389 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ + π) β β β§ (π΅ + π) β β) β (π₯ β ((π΄ + π)[,](π΅ + π)) β (π₯ β β β§ (π΄ + π) β€ π₯ β§ π₯ β€ (π΅ + π)))) |
111 | 12, 13, 110 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β ((π΄ + π)[,](π΅ + π)) β (π₯ β β β§ (π΄ + π) β€ π₯ β§ π₯ β€ (π΅ + π)))) |
112 | 14, 111 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β β β§ (π΄ + π) β€ π₯ β§ π₯ β€ (π΅ + π))) |
113 | 112 | simp2d 1144 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π΄ + π) β€ π₯) |
114 | 12, 16, 104, 113 | lesub1dd 11830 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β ((π΄ + π) β π) β€ (π₯ β π)) |
115 | 109, 114 | eqbrtrd 5171 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π΄ β€ (π₯ β π)) |
116 | 112 | simp3d 1145 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ β€ (π΅ + π)) |
117 | 16, 13, 104, 116 | lesub1dd 11830 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β π) β€ ((π΅ + π) β π)) |
118 | 2 | recnd 11242 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β β) |
119 | 118, 21 | pncand 11572 |
. . . . . . . . . . . . 13
β’ (π β ((π΅ + π) β π) = π΅) |
120 | 119 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β ((π΅ + π) β π) = π΅) |
121 | 117, 120 | breqtrd 5175 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β π) β€ π΅) |
122 | 102, 103,
105, 115, 121 | eliccd 44217 |
. . . . . . . . . 10
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β (π₯ β π) β (π΄[,]π΅)) |
123 | 21 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π β β) |
124 | 101, 123 | npcand 11575 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β ((π₯ β π) + π) = π₯) |
125 | 124 | eqcomd 2739 |
. . . . . . . . . 10
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ = ((π₯ β π) + π)) |
126 | | oveq1 7416 |
. . . . . . . . . . 11
β’ (π§ = (π₯ β π) β (π§ + π) = ((π₯ β π) + π)) |
127 | 126 | rspceeqv 3634 |
. . . . . . . . . 10
β’ (((π₯ β π) β (π΄[,]π΅) β§ π₯ = ((π₯ β π) + π)) β βπ§ β (π΄[,]π΅)π₯ = (π§ + π)) |
128 | 122, 125,
127 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β βπ§ β (π΄[,]π΅)π₯ = (π§ + π)) |
129 | 101, 128,
69 | sylanbrc 584 |
. . . . . . . 8
β’ ((π β§ π₯ β ((π΄ + π)[,](π΅ + π))) β π₯ β {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)}) |
130 | 100, 129 | impbida 800 |
. . . . . . 7
β’ (π β (π₯ β {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)} β π₯ β ((π΄ + π)[,](π΅ + π)))) |
131 | 130 | eqrdv 2731 |
. . . . . 6
β’ (π β {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)} = ((π΄ + π)[,](π΅ + π))) |
132 | 131 | reseq2d 5982 |
. . . . 5
β’ (π β (πΉ βΎ {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)}) = (πΉ βΎ ((π΄ + π)[,](π΅ + π)))) |
133 | 131, 65 | eqsstrrd 4022 |
. . . . . 6
β’ (π β ((π΄ + π)[,](π΅ + π)) β dom πΉ) |
134 | 53, 133 | feqresmpt 6962 |
. . . . 5
β’ (π β (πΉ βΎ ((π΄ + π)[,](π΅ + π))) = (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβπ₯))) |
135 | 132, 134 | eqtr2d 2774 |
. . . 4
β’ (π β (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβπ₯)) = (πΉ βΎ {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)})) |
136 | 1, 2, 4 | iccshift 44231 |
. . . . 5
β’ (π β ((π΄ + π)[,](π΅ + π)) = {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)}) |
137 | 136 | oveq1d 7424 |
. . . 4
β’ (π β (((π΄ + π)[,](π΅ + π))βcnββ) = ({π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)}βcnββ)) |
138 | 68, 135, 137 | 3eltr4d 2849 |
. . 3
β’ (π β (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβπ₯)) β (((π΄ + π)[,](π΅ + π))βcnββ)) |
139 | | ioosscn 13386 |
. . . . . 6
β’ (π΄(,)π΅) β β |
140 | 139 | a1i 11 |
. . . . 5
β’ (π β (π΄(,)π΅) β β) |
141 | | 1cnd 11209 |
. . . . 5
β’ (π β 1 β
β) |
142 | | ssid 4005 |
. . . . . 6
β’ β
β β |
143 | 142 | a1i 11 |
. . . . 5
β’ (π β β β
β) |
144 | 140, 141,
143 | constcncfg 44588 |
. . . 4
β’ (π β (π¦ β (π΄(,)π΅) β¦ 1) β ((π΄(,)π΅)βcnββ)) |
145 | | fconstmpt 5739 |
. . . . 5
β’ ((π΄(,)π΅) Γ {1}) = (π¦ β (π΄(,)π΅) β¦ 1) |
146 | | ioombl 25082 |
. . . . . . 7
β’ (π΄(,)π΅) β dom vol |
147 | 146 | a1i 11 |
. . . . . 6
β’ (π β (π΄(,)π΅) β dom vol) |
148 | | ioovolcl 25087 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β) β
(volβ(π΄(,)π΅)) β
β) |
149 | 1, 2, 148 | syl2anc 585 |
. . . . . 6
β’ (π β (volβ(π΄(,)π΅)) β β) |
150 | | iblconst 25335 |
. . . . . 6
β’ (((π΄(,)π΅) β dom vol β§ (volβ(π΄(,)π΅)) β β β§ 1 β β)
β ((π΄(,)π΅) Γ {1}) β
πΏ1) |
151 | 147, 149,
141, 150 | syl3anc 1372 |
. . . . 5
β’ (π β ((π΄(,)π΅) Γ {1}) β
πΏ1) |
152 | 145, 151 | eqeltrrid 2839 |
. . . 4
β’ (π β (π¦ β (π΄(,)π΅) β¦ 1) β
πΏ1) |
153 | 144, 152 | elind 4195 |
. . 3
β’ (π β (π¦ β (π΄(,)π΅) β¦ 1) β (((π΄(,)π΅)βcnββ) β©
πΏ1)) |
154 | 24 | resmptd 6041 |
. . . . . . 7
β’ (π β ((π¦ β β β¦ (π¦ + π)) βΎ (π΄[,]π΅)) = (π¦ β (π΄[,]π΅) β¦ (π¦ + π))) |
155 | 154 | eqcomd 2739 |
. . . . . 6
β’ (π β (π¦ β (π΄[,]π΅) β¦ (π¦ + π)) = ((π¦ β β β¦ (π¦ + π)) βΎ (π΄[,]π΅))) |
156 | 155 | oveq2d 7425 |
. . . . 5
β’ (π β (β D (π¦ β (π΄[,]π΅) β¦ (π¦ + π))) = (β D ((π¦ β β β¦ (π¦ + π)) βΎ (π΄[,]π΅)))) |
157 | 25 | a1i 11 |
. . . . . 6
β’ (π β β β
β) |
158 | 157 | sselda 3983 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β π¦ β β) |
159 | 21 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β π β β) |
160 | 158, 159 | addcld 11233 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (π¦ + π) β β) |
161 | 160 | fmpttd 7115 |
. . . . . 6
β’ (π β (π¦ β β β¦ (π¦ + π)):ββΆβ) |
162 | | ssid 4005 |
. . . . . . 7
β’ β
β β |
163 | 162 | a1i 11 |
. . . . . 6
β’ (π β β β
β) |
164 | | eqid 2733 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
165 | 164 | tgioo2 24319 |
. . . . . . 7
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
166 | 164, 165 | dvres 25428 |
. . . . . 6
β’
(((β β β β§ (π¦ β β β¦ (π¦ + π)):ββΆβ) β§ (β
β β β§ (π΄[,]π΅) β β)) β (β D
((π¦ β β β¦
(π¦ + π)) βΎ (π΄[,]π΅))) = ((β D (π¦ β β β¦ (π¦ + π))) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅)))) |
167 | 157, 161,
163, 24, 166 | syl22anc 838 |
. . . . 5
β’ (π β (β D ((π¦ β β β¦ (π¦ + π)) βΎ (π΄[,]π΅))) = ((β D (π¦ β β β¦ (π¦ + π))) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅)))) |
168 | 156, 167 | eqtrd 2773 |
. . . 4
β’ (π β (β D (π¦ β (π΄[,]π΅) β¦ (π¦ + π))) = ((β D (π¦ β β β¦ (π¦ + π))) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅)))) |
169 | | iccntr 24337 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
170 | 1, 2, 169 | syl2anc 585 |
. . . . 5
β’ (π β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
171 | 170 | reseq2d 5982 |
. . . 4
β’ (π β ((β D (π¦ β β β¦ (π¦ + π))) βΎ ((intβ(topGenβran
(,)))β(π΄[,]π΅))) = ((β D (π¦ β β β¦ (π¦ + π))) βΎ (π΄(,)π΅))) |
172 | | reelprrecn 11202 |
. . . . . . . 8
β’ β
β {β, β} |
173 | 172 | a1i 11 |
. . . . . . 7
β’ (π β β β {β,
β}) |
174 | | 1cnd 11209 |
. . . . . . 7
β’ ((π β§ π¦ β β) β 1 β
β) |
175 | 173 | dvmptid 25474 |
. . . . . . 7
β’ (π β (β D (π¦ β β β¦ π¦)) = (π¦ β β β¦ 1)) |
176 | | 0cnd 11207 |
. . . . . . 7
β’ ((π β§ π¦ β β) β 0 β
β) |
177 | 173, 21 | dvmptc 25475 |
. . . . . . 7
β’ (π β (β D (π¦ β β β¦ π)) = (π¦ β β β¦ 0)) |
178 | 173, 158,
174, 175, 159, 176, 177 | dvmptadd 25477 |
. . . . . 6
β’ (π β (β D (π¦ β β β¦ (π¦ + π))) = (π¦ β β β¦ (1 +
0))) |
179 | 178 | reseq1d 5981 |
. . . . 5
β’ (π β ((β D (π¦ β β β¦ (π¦ + π))) βΎ (π΄(,)π΅)) = ((π¦ β β β¦ (1 + 0)) βΎ
(π΄(,)π΅))) |
180 | | ioossre 13385 |
. . . . . . 7
β’ (π΄(,)π΅) β β |
181 | 180 | a1i 11 |
. . . . . 6
β’ (π β (π΄(,)π΅) β β) |
182 | 181 | resmptd 6041 |
. . . . 5
β’ (π β ((π¦ β β β¦ (1 + 0)) βΎ
(π΄(,)π΅)) = (π¦ β (π΄(,)π΅) β¦ (1 + 0))) |
183 | | 1p0e1 12336 |
. . . . . . 7
β’ (1 + 0) =
1 |
184 | 183 | mpteq2i 5254 |
. . . . . 6
β’ (π¦ β (π΄(,)π΅) β¦ (1 + 0)) = (π¦ β (π΄(,)π΅) β¦ 1) |
185 | 184 | a1i 11 |
. . . . 5
β’ (π β (π¦ β (π΄(,)π΅) β¦ (1 + 0)) = (π¦ β (π΄(,)π΅) β¦ 1)) |
186 | 179, 182,
185 | 3eqtrd 2777 |
. . . 4
β’ (π β ((β D (π¦ β β β¦ (π¦ + π))) βΎ (π΄(,)π΅)) = (π¦ β (π΄(,)π΅) β¦ 1)) |
187 | 168, 171,
186 | 3eqtrd 2777 |
. . 3
β’ (π β (β D (π¦ β (π΄[,]π΅) β¦ (π¦ + π))) = (π¦ β (π΄(,)π΅) β¦ 1)) |
188 | | fveq2 6892 |
. . 3
β’ (π₯ = (π¦ + π) β (πΉβπ₯) = (πΉβ(π¦ + π))) |
189 | | oveq1 7416 |
. . 3
β’ (π¦ = π΄ β (π¦ + π) = (π΄ + π)) |
190 | | oveq1 7416 |
. . 3
β’ (π¦ = π΅ β (π¦ + π) = (π΅ + π)) |
191 | 1, 2, 5, 45, 138, 153, 187, 188, 189, 190, 8, 9 | itgsubsticc 44692 |
. 2
β’ (π β β¨[(π΄ + π) β (π΅ + π)](πΉβπ₯) dπ₯ = β¨[π΄ β π΅]((πΉβ(π¦ + π)) Β· 1) dπ¦) |
192 | 5 | ditgpos 25373 |
. . 3
β’ (π β β¨[π΄ β π΅]((πΉβ(π¦ + π)) Β· 1) dπ¦ = β«(π΄(,)π΅)((πΉβ(π¦ + π)) Β· 1) dπ¦) |
193 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β πΉ:ββΆβ) |
194 | 193, 33 | ffvelcdmd 7088 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (πΉβ(π¦ + π)) β β) |
195 | | 1cnd 11209 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β 1 β β) |
196 | 194, 195 | mulcld 11234 |
. . . 4
β’ ((π β§ π¦ β (π΄[,]π΅)) β ((πΉβ(π¦ + π)) Β· 1) β
β) |
197 | 1, 2, 196 | itgioo 25333 |
. . 3
β’ (π β β«(π΄(,)π΅)((πΉβ(π¦ + π)) Β· 1) dπ¦ = β«(π΄[,]π΅)((πΉβ(π¦ + π)) Β· 1) dπ¦) |
198 | | fvoveq1 7432 |
. . . . . 6
β’ (π¦ = π₯ β (πΉβ(π¦ + π)) = (πΉβ(π₯ + π))) |
199 | 198 | oveq1d 7424 |
. . . . 5
β’ (π¦ = π₯ β ((πΉβ(π¦ + π)) Β· 1) = ((πΉβ(π₯ + π)) Β· 1)) |
200 | 199 | cbvitgv 25294 |
. . . 4
β’
β«(π΄[,]π΅)((πΉβ(π¦ + π)) Β· 1) dπ¦ = β«(π΄[,]π΅)((πΉβ(π₯ + π)) Β· 1) dπ₯ |
201 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄[,]π΅)) β πΉ:ββΆβ) |
202 | 24 | sselda 3983 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
203 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β π β β) |
204 | 202, 203 | readdcld 11243 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π₯ + π) β β) |
205 | 201, 204 | ffvelcdmd 7088 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβ(π₯ + π)) β β) |
206 | 205 | mulridd 11231 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β ((πΉβ(π₯ + π)) Β· 1) = (πΉβ(π₯ + π))) |
207 | 206, 66 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β ((πΉβ(π₯ + π)) Β· 1) = (πΉβπ₯)) |
208 | 207 | itgeq2dv 25299 |
. . . 4
β’ (π β β«(π΄[,]π΅)((πΉβ(π₯ + π)) Β· 1) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
209 | 200, 208 | eqtrid 2785 |
. . 3
β’ (π β β«(π΄[,]π΅)((πΉβ(π¦ + π)) Β· 1) dπ¦ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
210 | 192, 197,
209 | 3eqtrd 2777 |
. 2
β’ (π β β¨[π΄ β π΅]((πΉβ(π¦ + π)) Β· 1) dπ¦ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
211 | 19, 191, 210 | 3eqtrd 2777 |
1
β’ (π β β«((π΄ + π)[,](π΅ + π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |