Step | Hyp | Ref
| Expression |
1 | | ioossicc 13359 |
. . . . . . 7
β’ (π΄(,)π΅) β (π΄[,]π΅) |
2 | 1 | sseli 3944 |
. . . . . 6
β’ (π₯ β (π΄(,)π΅) β π₯ β (π΄[,]π΅)) |
3 | 2 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β (π΄[,]π΅)) |
4 | | ditgeqiooicc.2 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
5 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΄ β β) |
6 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β (π΄(,)π΅)) |
7 | 5 | rexrd 11213 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΄ β
β*) |
8 | | ditgeqiooicc.3 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β β) |
9 | 8 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΅ β β) |
10 | 9 | rexrd 11213 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΅ β
β*) |
11 | | elioo2 13314 |
. . . . . . . . . . . . 13
β’ ((π΄ β β*
β§ π΅ β
β*) β (π₯ β (π΄(,)π΅) β (π₯ β β β§ π΄ < π₯ β§ π₯ < π΅))) |
12 | 7, 10, 11 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄(,)π΅)) β (π₯ β (π΄(,)π΅) β (π₯ β β β§ π΄ < π₯ β§ π₯ < π΅))) |
13 | 6, 12 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄(,)π΅)) β (π₯ β β β§ π΄ < π₯ β§ π₯ < π΅)) |
14 | 13 | simp2d 1144 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΄ < π₯) |
15 | 5, 14 | gtned 11298 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β π΄) |
16 | 15 | neneqd 2945 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ = π΄) |
17 | 16 | iffalsed 4501 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΅, πΏ, (πΉβπ₯))) |
18 | 13 | simp1d 1143 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β β) |
19 | 13 | simp3d 1145 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ < π΅) |
20 | 18, 19 | ltned 11299 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β π΅) |
21 | 20 | neneqd 2945 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ = π΅) |
22 | 21 | iffalsed 4501 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΅, πΏ, (πΉβπ₯)) = (πΉβπ₯)) |
23 | 17, 22 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = (πΉβπ₯)) |
24 | | ditgeqiooicc.5 |
. . . . . . 7
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
25 | 24 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) β β) |
26 | 23, 25 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
27 | | ditgeqiooicc.1 |
. . . . . 6
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
28 | 27 | fvmpt2 6963 |
. . . . 5
β’ ((π₯ β (π΄[,]π΅) β§ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) β (πΊβπ₯) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
29 | 3, 26, 28 | syl2anc 585 |
. . . 4
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΊβπ₯) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
30 | 29, 17, 22 | 3eqtrrd 2778 |
. . 3
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) = (πΊβπ₯)) |
31 | 30 | itgeq2dv 25169 |
. 2
β’ (π β β«(π΄(,)π΅)(πΉβπ₯) dπ₯ = β«(π΄(,)π΅)(πΊβπ₯) dπ₯) |
32 | | ditgeqiooicc.4 |
. . 3
β’ (π β π΄ β€ π΅) |
33 | 32 | ditgpos 25243 |
. 2
β’ (π β β¨[π΄ β π΅](πΉβπ₯) dπ₯ = β«(π΄(,)π΅)(πΉβπ₯) dπ₯) |
34 | 32 | ditgpos 25243 |
. 2
β’ (π β β¨[π΄ β π΅](πΊβπ₯) dπ₯ = β«(π΄(,)π΅)(πΊβπ₯) dπ₯) |
35 | 31, 33, 34 | 3eqtr4d 2783 |
1
β’ (π β β¨[π΄ β π΅](πΉβπ₯) dπ₯ = β¨[π΄ β π΅](πΊβπ₯) dπ₯) |