Step | Hyp | Ref
| Expression |
1 | | iblcncfioo.f |
. . . . 5
β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) |
2 | | cncff 24272 |
. . . . 5
β’ (πΉ β ((π΄(,)π΅)βcnββ) β πΉ:(π΄(,)π΅)βΆβ) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
4 | 3 | feqmptd 6915 |
. . 3
β’ (π β πΉ = (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯))) |
5 | | iblcncfioo.a |
. . . . . . . . . 10
β’ (π β π΄ β β) |
6 | 5 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΄ β β) |
7 | | eliooord 13330 |
. . . . . . . . . . 11
β’ (π₯ β (π΄(,)π΅) β (π΄ < π₯ β§ π₯ < π΅)) |
8 | 7 | simpld 496 |
. . . . . . . . . 10
β’ (π₯ β (π΄(,)π΅) β π΄ < π₯) |
9 | 8 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π΄ < π₯) |
10 | 6, 9 | gtned 11297 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β π΄) |
11 | 10 | neneqd 2949 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ = π΄) |
12 | 11 | iffalsed 4502 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΅, πΏ, (πΉβπ₯))) |
13 | | elioore 13301 |
. . . . . . . . . 10
β’ (π₯ β (π΄(,)π΅) β π₯ β β) |
14 | 13 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β β) |
15 | 7 | simprd 497 |
. . . . . . . . . 10
β’ (π₯ β (π΄(,)π΅) β π₯ < π΅) |
16 | 15 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ < π΅) |
17 | 14, 16 | ltned 11298 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β π΅) |
18 | 17 | neneqd 2949 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ = π΅) |
19 | 18 | iffalsed 4502 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΅, πΏ, (πΉβπ₯)) = (πΉβπ₯)) |
20 | 12, 19 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = (πΉβπ₯)) |
21 | 20 | eqcomd 2743 |
. . . 4
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) = if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
22 | 21 | mpteq2dva 5210 |
. . 3
β’ (π β (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯)) = (π₯ β (π΄(,)π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))))) |
23 | 4, 22 | eqtrd 2777 |
. 2
β’ (π β πΉ = (π₯ β (π΄(,)π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))))) |
24 | | ioossicc 13357 |
. . . 4
β’ (π΄(,)π΅) β (π΄[,]π΅) |
25 | 24 | a1i 11 |
. . 3
β’ (π β (π΄(,)π΅) β (π΄[,]π΅)) |
26 | | ioombl 24945 |
. . . 4
β’ (π΄(,)π΅) β dom vol |
27 | 26 | a1i 11 |
. . 3
β’ (π β (π΄(,)π΅) β dom vol) |
28 | | iftrue 4497 |
. . . . . . 7
β’ (π₯ = π΄ β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = π
) |
29 | 28 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = π
) |
30 | | limccl 25255 |
. . . . . . . 8
β’ (πΉ limβ π΄) β
β |
31 | | iblcncfioo.r |
. . . . . . . 8
β’ (π β π
β (πΉ limβ π΄)) |
32 | 30, 31 | sselid 3947 |
. . . . . . 7
β’ (π β π
β β) |
33 | 32 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ = π΄) β π
β β) |
34 | 29, 33 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
35 | 34 | adantlr 714 |
. . . 4
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
36 | | iffalse 4500 |
. . . . . . . . 9
β’ (Β¬
π₯ = π΄ β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΅, πΏ, (πΉβπ₯))) |
37 | 36 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΅, πΏ, (πΉβπ₯))) |
38 | | iftrue 4497 |
. . . . . . . . 9
β’ (π₯ = π΅ β if(π₯ = π΅, πΏ, (πΉβπ₯)) = πΏ) |
39 | 38 | adantl 483 |
. . . . . . . 8
β’ (((π β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΅, πΏ, (πΉβπ₯)) = πΏ) |
40 | 37, 39 | eqtrd 2777 |
. . . . . . 7
β’ (((π β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = πΏ) |
41 | | limccl 25255 |
. . . . . . . . 9
β’ (πΉ limβ π΅) β
β |
42 | | iblcncfioo.l |
. . . . . . . . 9
β’ (π β πΏ β (πΉ limβ π΅)) |
43 | 41, 42 | sselid 3947 |
. . . . . . . 8
β’ (π β πΏ β β) |
44 | 43 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β πΏ β β) |
45 | 40, 44 | eqeltrd 2838 |
. . . . . 6
β’ (((π β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
46 | 45 | adantllr 718 |
. . . . 5
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
47 | | simplll 774 |
. . . . . . 7
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π) |
48 | 5 | rexrd 11212 |
. . . . . . . . . 10
β’ (π β π΄ β
β*) |
49 | 47, 48 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π΄ β
β*) |
50 | | iblcncfioo.b |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
51 | 50 | rexrd 11212 |
. . . . . . . . . 10
β’ (π β π΅ β
β*) |
52 | 47, 51 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π΅ β
β*) |
53 | | eliccxr 13359 |
. . . . . . . . . 10
β’ (π₯ β (π΄[,]π΅) β π₯ β β*) |
54 | 53 | ad3antlr 730 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π₯ β β*) |
55 | 49, 52, 54 | 3jca 1129 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β (π΄ β β* β§ π΅ β β*
β§ π₯ β
β*)) |
56 | 5 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΄ β β) |
57 | 5 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β β) |
58 | 50 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΅ β β) |
59 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β (π΄[,]π΅)) |
60 | | eliccre 43817 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΅ β β β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
61 | 57, 58, 59, 60 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
62 | 61 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π₯ β β) |
63 | 5, 50 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΄ β β β§ π΅ β β)) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π΄ β β β§ π΅ β β)) |
65 | | elicc2 13336 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΅ β β) β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
67 | 59, 66 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅)) |
68 | 67 | simp2d 1144 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β€ π₯) |
69 | 68 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΄ β€ π₯) |
70 | | df-ne 2945 |
. . . . . . . . . . . . 13
β’ (π₯ β π΄ β Β¬ π₯ = π΄) |
71 | 70 | biimpri 227 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ = π΄ β π₯ β π΄) |
72 | 71 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π₯ β π΄) |
73 | 56, 62, 69, 72 | leneltd 11316 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΄ < π₯) |
74 | 73 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π΄ < π₯) |
75 | | nesym 3001 |
. . . . . . . . . . . . 13
β’ (π΅ β π₯ β Β¬ π₯ = π΅) |
76 | 75 | biimpri 227 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ = π΅ β π΅ β π₯) |
77 | 76 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π΅ β π₯) |
78 | 67 | simp3d 1145 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β€ π΅) |
79 | 61, 58, 78 | 3jca 1129 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π₯ β β β§ π΅ β β β§ π₯ β€ π΅)) |
80 | 79 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β (π₯ β β β§ π΅ β β β§ π₯ β€ π΅)) |
81 | | leltne 11251 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π΅ β β β§ π₯ β€ π΅) β (π₯ < π΅ β π΅ β π₯)) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β (π₯ < π΅ β π΅ β π₯)) |
83 | 77, 82 | mpbird 257 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π₯ < π΅) |
84 | 83 | adantlr 714 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π₯ < π΅) |
85 | 74, 84 | jca 513 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β (π΄ < π₯ β§ π₯ < π΅)) |
86 | | elioo3g 13300 |
. . . . . . . 8
β’ (π₯ β (π΄(,)π΅) β ((π΄ β β* β§ π΅ β β*
β§ π₯ β
β*) β§ (π΄ < π₯ β§ π₯ < π΅))) |
87 | 55, 85, 86 | sylanbrc 584 |
. . . . . . 7
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π₯ β (π΄(,)π΅)) |
88 | 47, 87 | jca 513 |
. . . . . 6
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β (π β§ π₯ β (π΄(,)π΅))) |
89 | 3 | ffvelcdmda 7040 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) β β) |
90 | 20, 89 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
91 | 88, 90 | syl 17 |
. . . . 5
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
92 | 46, 91 | pm2.61dan 812 |
. . . 4
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
93 | 35, 92 | pm2.61dan 812 |
. . 3
β’ ((π β§ π₯ β (π΄[,]π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
94 | | nfv 1918 |
. . . . 5
β’
β²π₯π |
95 | | eqid 2737 |
. . . . 5
β’ (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
96 | 94, 95, 5, 50, 1, 42, 31 | cncfiooicc 44209 |
. . . 4
β’ (π β (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) β ((π΄[,]π΅)βcnββ)) |
97 | | cniccibl 25221 |
. . . 4
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) β
πΏ1) |
98 | 5, 50, 96, 97 | syl3anc 1372 |
. . 3
β’ (π β (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) β
πΏ1) |
99 | 25, 27, 93, 98 | iblss 25185 |
. 2
β’ (π β (π₯ β (π΄(,)π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) β
πΏ1) |
100 | 23, 99 | eqeltrd 2838 |
1
β’ (π β πΉ β
πΏ1) |