Step | Hyp | Ref
| Expression |
1 | | itgioocnicc.a |
. . 3
β’ (π β π΄ β β) |
2 | | itgioocnicc.b |
. . 3
β’ (π β π΅ β β) |
3 | | itgioocnicc.g |
. . . . 5
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
4 | | iftrue 4496 |
. . . . . . . . 9
β’ (π₯ = π΄ β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = π
) |
5 | | iftrue 4496 |
. . . . . . . . 9
β’ (π₯ = π΄ β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯))) = π
) |
6 | 4, 5 | eqtr4d 2776 |
. . . . . . . 8
β’ (π₯ = π΄ β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) |
7 | 6 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) |
8 | | iftrue 4496 |
. . . . . . . . . . . 12
β’ (π₯ = π΅ β if(π₯ = π΅, πΏ, (πΉβπ₯)) = πΏ) |
9 | | iftrue 4496 |
. . . . . . . . . . . 12
β’ (π₯ = π΅ β if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)) = πΏ) |
10 | 8, 9 | eqtr4d 2776 |
. . . . . . . . . . 11
β’ (π₯ = π΅ β if(π₯ = π΅, πΏ, (πΉβπ₯)) = if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯))) |
11 | 10 | adantl 483 |
. . . . . . . . . 10
β’ ((Β¬
π₯ = π΄ β§ π₯ = π΅) β if(π₯ = π΅, πΏ, (πΉβπ₯)) = if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯))) |
12 | 11 | ifeq2d 4510 |
. . . . . . . . 9
β’ ((Β¬
π₯ = π΄ β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) |
13 | 12 | adantll 713 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) |
14 | | iffalse 4499 |
. . . . . . . . . 10
β’ (Β¬
π₯ = π΄ β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΅, πΏ, (πΉβπ₯))) |
15 | 14 | ad2antlr 726 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΅, πΏ, (πΉβπ₯))) |
16 | | iffalse 4499 |
. . . . . . . . . 10
β’ (Β¬
π₯ = π΅ β if(π₯ = π΅, πΏ, (πΉβπ₯)) = (πΉβπ₯)) |
17 | 16 | adantl 483 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β if(π₯ = π΅, πΏ, (πΉβπ₯)) = (πΉβπ₯)) |
18 | | iffalse 4499 |
. . . . . . . . . . 11
β’ (Β¬
π₯ = π΄ β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯))) = if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯))) |
19 | 18 | ad2antlr 726 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯))) = if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯))) |
20 | | iffalse 4499 |
. . . . . . . . . . 11
β’ (Β¬
π₯ = π΅ β if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)) = ((πΉ βΎ (π΄(,)π΅))βπ₯)) |
21 | 20 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)) = ((πΉ βΎ (π΄(,)π΅))βπ₯)) |
22 | 1 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β β) |
23 | 22 | rexrd 11213 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β
β*) |
24 | 23 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π΄ β
β*) |
25 | 2 | rexrd 11213 |
. . . . . . . . . . . . 13
β’ (π β π΅ β
β*) |
26 | 25 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π΅ β
β*) |
27 | 2 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΅ β β) |
28 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β (π΄[,]π΅)) |
29 | | eliccre 43833 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π΅ β β β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
30 | 22, 27, 28, 29 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
31 | 30 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π₯ β β) |
32 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΄ β β) |
33 | 30 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π₯ β β) |
34 | 25 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΅ β
β*) |
35 | | iccgelb 13329 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β*
β§ π΅ β
β* β§ π₯
β (π΄[,]π΅)) β π΄ β€ π₯) |
36 | 23, 34, 28, 35 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β€ π₯) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΄ β€ π₯) |
38 | | neqne 2948 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π₯ = π΄ β π₯ β π΄) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π₯ β π΄) |
40 | 32, 33, 37, 39 | leneltd 11317 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΄ < π₯) |
41 | 40 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π΄ < π₯) |
42 | 30 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π₯ β β) |
43 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π΅ β β) |
44 | | iccleub 13328 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β*
β§ π΅ β
β* β§ π₯
β (π΄[,]π΅)) β π₯ β€ π΅) |
45 | 23, 34, 28, 44 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β€ π΅) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π₯ β€ π΅) |
47 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π΅ β π΅ = π₯) |
48 | 47 | notbii 320 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π₯ = π΅ β Β¬ π΅ = π₯) |
49 | 48 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π₯ = π΅ β Β¬ π΅ = π₯) |
50 | 49 | neqned 2947 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π₯ = π΅ β π΅ β π₯) |
51 | 50 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π΅ β π₯) |
52 | 42, 43, 46, 51 | leneltd 11317 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π₯ < π΅) |
53 | 52 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π₯ < π΅) |
54 | 24, 26, 31, 41, 53 | eliood 43826 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π₯ β (π΄(,)π΅)) |
55 | | fvres 6865 |
. . . . . . . . . . 11
β’ (π₯ β (π΄(,)π΅) β ((πΉ βΎ (π΄(,)π΅))βπ₯) = (πΉβπ₯)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β ((πΉ βΎ (π΄(,)π΅))βπ₯) = (πΉβπ₯)) |
57 | 19, 21, 56 | 3eqtrrd 2778 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β (πΉβπ₯) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) |
58 | 15, 17, 57 | 3eqtrd 2777 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) |
59 | 13, 58 | pm2.61dan 812 |
. . . . . . 7
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) |
60 | 7, 59 | pm2.61dan 812 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) |
61 | 60 | mpteq2dva 5209 |
. . . . 5
β’ (π β (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯))))) |
62 | 3, 61 | eqtrid 2785 |
. . . 4
β’ (π β πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯))))) |
63 | | nfv 1918 |
. . . . 5
β’
β²π₯π |
64 | | eqid 2733 |
. . . . 5
β’ (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) |
65 | | itgioocnicc.fcn |
. . . . 5
β’ (π β (πΉ βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) |
66 | | itgioocnicc.l |
. . . . 5
β’ (π β πΏ β ((πΉ βΎ (π΄(,)π΅)) limβ π΅)) |
67 | | itgioocnicc.r |
. . . . 5
β’ (π β π
β ((πΉ βΎ (π΄(,)π΅)) limβ π΄)) |
68 | 63, 64, 1, 2, 65, 66, 67 | cncfiooicc 44225 |
. . . 4
β’ (π β (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) β ((π΄[,]π΅)βcnββ)) |
69 | 62, 68 | eqeltrd 2834 |
. . 3
β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) |
70 | | cniccibl 25228 |
. . 3
β’ ((π΄ β β β§ π΅ β β β§ πΊ β ((π΄[,]π΅)βcnββ)) β πΊ β
πΏ1) |
71 | 1, 2, 69, 70 | syl3anc 1372 |
. 2
β’ (π β πΊ β
πΏ1) |
72 | 4 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = π
) |
73 | | limccl 25262 |
. . . . . . . . . . 11
β’ ((πΉ βΎ (π΄(,)π΅)) limβ π΄) β β |
74 | 73, 67 | sselid 3946 |
. . . . . . . . . 10
β’ (π β π
β β) |
75 | 74 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ π₯ = π΄) β π
β β) |
76 | 72, 75 | eqeltrd 2834 |
. . . . . . . 8
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
77 | 14, 8 | sylan9eq 2793 |
. . . . . . . . . . 11
β’ ((Β¬
π₯ = π΄ β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = πΏ) |
78 | 77 | adantll 713 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = πΏ) |
79 | | limccl 25262 |
. . . . . . . . . . . 12
β’ ((πΉ βΎ (π΄(,)π΅)) limβ π΅) β β |
80 | 79, 66 | sselid 3946 |
. . . . . . . . . . 11
β’ (π β πΏ β β) |
81 | 80 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β πΏ β β) |
82 | 78, 81 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
83 | 14, 16 | sylan9eq 2793 |
. . . . . . . . . . 11
β’ ((Β¬
π₯ = π΄ β§ Β¬ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = (πΉβπ₯)) |
84 | 83 | adantll 713 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = (πΉβπ₯)) |
85 | 56 | eqcomd 2739 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β (πΉβπ₯) = ((πΉ βΎ (π΄(,)π΅))βπ₯)) |
86 | | cncff 24279 |
. . . . . . . . . . . . . 14
β’ ((πΉ βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ) β (πΉ βΎ (π΄(,)π΅)):(π΄(,)π΅)βΆβ) |
87 | 65, 86 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (πΉ βΎ (π΄(,)π΅)):(π΄(,)π΅)βΆβ) |
88 | 87 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β (πΉ βΎ (π΄(,)π΅)):(π΄(,)π΅)βΆβ) |
89 | 88, 54 | ffvelcdmd 7040 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β ((πΉ βΎ (π΄(,)π΅))βπ₯) β β) |
90 | 85, 89 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β (πΉβπ₯) β β) |
91 | 84, 90 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
92 | 82, 91 | pm2.61dan 812 |
. . . . . . . 8
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
93 | 76, 92 | pm2.61dan 812 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
94 | 3 | fvmpt2 6963 |
. . . . . . 7
β’ ((π₯ β (π΄[,]π΅) β§ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) β (πΊβπ₯) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
95 | 28, 93, 94 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΊβπ₯) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
96 | 95, 93 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΊβπ₯) β β) |
97 | 1, 2, 96 | itgioo 25203 |
. . . 4
β’ (π β β«(π΄(,)π΅)(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΊβπ₯) dπ₯) |
98 | 97 | eqcomd 2739 |
. . 3
β’ (π β β«(π΄[,]π΅)(πΊβπ₯) dπ₯ = β«(π΄(,)π΅)(πΊβπ₯) dπ₯) |
99 | | ioossicc 13359 |
. . . . . . 7
β’ (π΄(,)π΅) β (π΄[,]π΅) |
100 | 99 | sseli 3944 |
. . . . . 6
β’ (π₯ β (π΄(,)π΅) β π₯ β (π΄[,]π΅)) |
101 | 100, 95 | sylan2 594 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΊβπ₯) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
102 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΄ β β) |
103 | | eliooord 13332 |
. . . . . . . . . 10
β’ (π₯ β (π΄(,)π΅) β (π΄ < π₯ β§ π₯ < π΅)) |
104 | 103 | simpld 496 |
. . . . . . . . 9
β’ (π₯ β (π΄(,)π΅) β π΄ < π₯) |
105 | 104 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΄ < π₯) |
106 | 102, 105 | gtned 11298 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β π΄) |
107 | 106 | neneqd 2945 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ = π΄) |
108 | 107, 14 | syl 17 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΅, πΏ, (πΉβπ₯))) |
109 | 100, 30 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β β) |
110 | 103 | simprd 497 |
. . . . . . . . 9
β’ (π₯ β (π΄(,)π΅) β π₯ < π΅) |
111 | 110 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ < π΅) |
112 | 109, 111 | ltned 11299 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β π΅) |
113 | 112 | neneqd 2945 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ = π΅) |
114 | 113, 16 | syl 17 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΅, πΏ, (πΉβπ₯)) = (πΉβπ₯)) |
115 | 101, 108,
114 | 3eqtrd 2777 |
. . . 4
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΊβπ₯) = (πΉβπ₯)) |
116 | 115 | itgeq2dv 25169 |
. . 3
β’ (π β β«(π΄(,)π΅)(πΊβπ₯) dπ₯ = β«(π΄(,)π΅)(πΉβπ₯) dπ₯) |
117 | | itgioocnicc.f |
. . . . . 6
β’ (π β πΉ:dom πΉβΆβ) |
118 | 117 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β πΉ:dom πΉβΆβ) |
119 | | itgioocnicc.fdom |
. . . . . 6
β’ (π β (π΄[,]π΅) β dom πΉ) |
120 | 119 | sselda 3948 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β dom πΉ) |
121 | 118, 120 | ffvelcdmd 7040 |
. . . 4
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) β β) |
122 | 1, 2, 121 | itgioo 25203 |
. . 3
β’ (π β β«(π΄(,)π΅)(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
123 | 98, 116, 122 | 3eqtrd 2777 |
. 2
β’ (π β β«(π΄[,]π΅)(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
124 | 71, 123 | jca 513 |
1
β’ (π β (πΊ β πΏ1 β§
β«(π΄[,]π΅)(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯)) |