Step | Hyp | Ref
| Expression |
1 | | ioossicc 13416 |
. . . . . . 7
β’ (π΄(,)π΅) β (π΄[,]π΅) |
2 | 1 | sseli 3973 |
. . . . . 6
β’ (π₯ β (π΄(,)π΅) β π₯ β (π΄[,]π΅)) |
3 | 2 | adantl 481 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β (π΄[,]π΅)) |
4 | | ditgeqiooicc.2 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
5 | 4 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΄ β β) |
6 | | simpr 484 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β (π΄(,)π΅)) |
7 | 5 | rexrd 11268 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΄ β
β*) |
8 | | ditgeqiooicc.3 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β β) |
9 | 8 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΅ β β) |
10 | 9 | rexrd 11268 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΅ β
β*) |
11 | | elioo2 13371 |
. . . . . . . . . . . . 13
β’ ((π΄ β β*
β§ π΅ β
β*) β (π₯ β (π΄(,)π΅) β (π₯ β β β§ π΄ < π₯ β§ π₯ < π΅))) |
12 | 7, 10, 11 | syl2anc 583 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄(,)π΅)) β (π₯ β (π΄(,)π΅) β (π₯ β β β§ π΄ < π₯ β§ π₯ < π΅))) |
13 | 6, 12 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄(,)π΅)) β (π₯ β β β§ π΄ < π₯ β§ π₯ < π΅)) |
14 | 13 | simp2d 1140 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΄ < π₯) |
15 | 5, 14 | gtned 11353 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β π΄) |
16 | 15 | neneqd 2939 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ = π΄) |
17 | 16 | iffalsed 4534 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΅, πΏ, (πΉβπ₯))) |
18 | 13 | simp1d 1139 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β β) |
19 | 13 | simp3d 1141 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ < π΅) |
20 | 18, 19 | ltned 11354 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β π΅) |
21 | 20 | neneqd 2939 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ = π΅) |
22 | 21 | iffalsed 4534 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΅, πΏ, (πΉβπ₯)) = (πΉβπ₯)) |
23 | 17, 22 | eqtrd 2766 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = (πΉβπ₯)) |
24 | | ditgeqiooicc.5 |
. . . . . . 7
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
25 | 24 | ffvelcdmda 7080 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) β β) |
26 | 23, 25 | eqeltrd 2827 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
27 | | ditgeqiooicc.1 |
. . . . . 6
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
28 | 27 | fvmpt2 7003 |
. . . . 5
β’ ((π₯ β (π΄[,]π΅) β§ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) β (πΊβπ₯) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
29 | 3, 26, 28 | syl2anc 583 |
. . . 4
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΊβπ₯) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
30 | 29, 17, 22 | 3eqtrrd 2771 |
. . 3
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) = (πΊβπ₯)) |
31 | 30 | itgeq2dv 25666 |
. 2
β’ (π β β«(π΄(,)π΅)(πΉβπ₯) dπ₯ = β«(π΄(,)π΅)(πΊβπ₯) dπ₯) |
32 | | ditgeqiooicc.4 |
. . 3
β’ (π β π΄ β€ π΅) |
33 | 32 | ditgpos 25740 |
. 2
β’ (π β β¨[π΄ β π΅](πΉβπ₯) dπ₯ = β«(π΄(,)π΅)(πΉβπ₯) dπ₯) |
34 | 32 | ditgpos 25740 |
. 2
β’ (π β β¨[π΄ β π΅](πΊβπ₯) dπ₯ = β«(π΄(,)π΅)(πΊβπ₯) dπ₯) |
35 | 31, 33, 34 | 3eqtr4d 2776 |
1
β’ (π β β¨[π΄ β π΅](πΉβπ₯) dπ₯ = β¨[π΄ β π΅](πΊβπ₯) dπ₯) |