Step | Hyp | Ref
| Expression |
1 | | difssd 4093 |
. . . . . . . 8
β’ (π β ((π΄(,)π΅) β {π΅}) β (π΄(,)π΅)) |
2 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β (π΄(,)π΅)) |
3 | | ubioo 13297 |
. . . . . . . . . . . 12
β’ Β¬
π΅ β (π΄(,)π΅) |
4 | | eleq1 2826 |
. . . . . . . . . . . . 13
β’ (π₯ = π΅ β (π₯ β (π΄(,)π΅) β π΅ β (π΄(,)π΅))) |
5 | 4 | biimpcd 249 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄(,)π΅) β (π₯ = π΅ β π΅ β (π΄(,)π΅))) |
6 | 3, 5 | mtoi 198 |
. . . . . . . . . . 11
β’ (π₯ β (π΄(,)π΅) β Β¬ π₯ = π΅) |
7 | 6 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ = π΅) |
8 | | velsn 4603 |
. . . . . . . . . 10
β’ (π₯ β {π΅} β π₯ = π΅) |
9 | 7, 8 | sylnibr 329 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ β {π΅}) |
10 | 2, 9 | eldifd 3922 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β ((π΄(,)π΅) β {π΅})) |
11 | 1, 10 | eqelssd 3966 |
. . . . . . 7
β’ (π β ((π΄(,)π΅) β {π΅}) = (π΄(,)π΅)) |
12 | 11 | ineq2d 4173 |
. . . . . 6
β’ (π β ((π(,)π) β© ((π΄(,)π΅) β {π΅})) = ((π(,)π) β© (π΄(,)π΅))) |
13 | 12 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β ((π(,)π) β© ((π΄(,)π΅) β {π΅})) = ((π(,)π) β© (π΄(,)π΅))) |
14 | | simplrl 776 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β π β β*) |
15 | | simplrr 777 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β π β β*) |
16 | | lptioo2.2 |
. . . . . . . 8
β’ (π β π΄ β
β*) |
17 | 16 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β π΄ β
β*) |
18 | | elioo3g 13294 |
. . . . . . . . . . 11
β’ (π΅ β (π(,)π) β ((π β β* β§ π β β*
β§ π΅ β
β*) β§ (π < π΅ β§ π΅ < π))) |
19 | 18 | biimpi 215 |
. . . . . . . . . 10
β’ (π΅ β (π(,)π) β ((π β β* β§ π β β*
β§ π΅ β
β*) β§ (π < π΅ β§ π΅ < π))) |
20 | 19 | simpld 496 |
. . . . . . . . 9
β’ (π΅ β (π(,)π) β (π β β* β§ π β β*
β§ π΅ β
β*)) |
21 | 20 | simp3d 1145 |
. . . . . . . 8
β’ (π΅ β (π(,)π) β π΅ β
β*) |
22 | 21 | adantl 483 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β π΅ β
β*) |
23 | | iooin 13299 |
. . . . . . 7
β’ (((π β β*
β§ π β
β*) β§ (π΄ β β* β§ π΅ β β*))
β ((π(,)π) β© (π΄(,)π΅)) = (if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅))) |
24 | 14, 15, 17, 22, 23 | syl22anc 838 |
. . . . . 6
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β ((π(,)π) β© (π΄(,)π΅)) = (if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅))) |
25 | | iftrue 4493 |
. . . . . . . . . . 11
β’ (π β€ π΄ β if(π β€ π΄, π΄, π) = π΄) |
26 | 25 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β§ π β€ π΄) β if(π β€ π΄, π΄, π) = π΄) |
27 | | lptioo2.4 |
. . . . . . . . . . 11
β’ (π β π΄ < π΅) |
28 | 27 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β§ π β€ π΄) β π΄ < π΅) |
29 | 26, 28 | eqbrtrd 5128 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β§ π β€ π΄) β if(π β€ π΄, π΄, π) < π΅) |
30 | | iffalse 4496 |
. . . . . . . . . . 11
β’ (Β¬
π β€ π΄ β if(π β€ π΄, π΄, π) = π) |
31 | 30 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β§ Β¬ π β€ π΄) β if(π β€ π΄, π΄, π) = π) |
32 | 19 | simprd 497 |
. . . . . . . . . . . 12
β’ (π΅ β (π(,)π) β (π < π΅ β§ π΅ < π)) |
33 | 32 | simpld 496 |
. . . . . . . . . . 11
β’ (π΅ β (π(,)π) β π < π΅) |
34 | 33 | ad2antlr 726 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β§ Β¬ π β€ π΄) β π < π΅) |
35 | 31, 34 | eqbrtrd 5128 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β§ Β¬ π β€ π΄) β if(π β€ π΄, π΄, π) < π΅) |
36 | 29, 35 | pm2.61dan 812 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β if(π β€ π΄, π΄, π) < π΅) |
37 | 32 | simprd 497 |
. . . . . . . . . . . 12
β’ (π΅ β (π(,)π) β π΅ < π) |
38 | 20 | simp2d 1144 |
. . . . . . . . . . . . 13
β’ (π΅ β (π(,)π) β π β β*) |
39 | | xrltnle 11223 |
. . . . . . . . . . . . 13
β’ ((π΅ β β*
β§ π β
β*) β (π΅ < π β Β¬ π β€ π΅)) |
40 | 21, 38, 39 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π΅ β (π(,)π) β (π΅ < π β Β¬ π β€ π΅)) |
41 | 37, 40 | mpbid 231 |
. . . . . . . . . . 11
β’ (π΅ β (π(,)π) β Β¬ π β€ π΅) |
42 | | iffalse 4496 |
. . . . . . . . . . 11
β’ (Β¬
π β€ π΅ β if(π β€ π΅, π, π΅) = π΅) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
β’ (π΅ β (π(,)π) β if(π β€ π΅, π, π΅) = π΅) |
44 | 43 | eqcomd 2743 |
. . . . . . . . 9
β’ (π΅ β (π(,)π) β π΅ = if(π β€ π΅, π, π΅)) |
45 | 44 | adantl 483 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β π΅ = if(π β€ π΅, π, π΅)) |
46 | 36, 45 | breqtrd 5132 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β if(π β€ π΄, π΄, π) < if(π β€ π΅, π, π΅)) |
47 | 17, 14 | ifcld 4533 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β if(π β€ π΄, π΄, π) β
β*) |
48 | 45, 22 | eqeltrrd 2839 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β if(π β€ π΅, π, π΅) β
β*) |
49 | | ioon0 13291 |
. . . . . . . 8
β’
((if(π β€ π΄, π΄, π) β β* β§ if(π β€ π΅, π, π΅) β β*) β
((if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅)) β β
β if(π β€ π΄, π΄, π) < if(π β€ π΅, π, π΅))) |
50 | 47, 48, 49 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β ((if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅)) β β
β if(π β€ π΄, π΄, π) < if(π β€ π΅, π, π΅))) |
51 | 46, 50 | mpbird 257 |
. . . . . 6
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β (if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅)) β β
) |
52 | 24, 51 | eqnetrd 3012 |
. . . . 5
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β ((π(,)π) β© (π΄(,)π΅)) β β
) |
53 | 13, 52 | eqnetrd 3012 |
. . . 4
β’ (((π β§ (π β β* β§ π β β*))
β§ π΅ β (π(,)π)) β ((π(,)π) β© ((π΄(,)π΅) β {π΅})) β β
) |
54 | 53 | ex 414 |
. . 3
β’ ((π β§ (π β β* β§ π β β*))
β (π΅ β (π(,)π) β ((π(,)π) β© ((π΄(,)π΅) β {π΅})) β β
)) |
55 | 54 | ralrimivva 3198 |
. 2
β’ (π β βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© ((π΄(,)π΅) β {π΅})) β β
)) |
56 | | lptioo2.1 |
. . 3
β’ π½ = (topGenβran
(,)) |
57 | | ioossre 13326 |
. . . 4
β’ (π΄(,)π΅) β β |
58 | 57 | a1i 11 |
. . 3
β’ (π β (π΄(,)π΅) β β) |
59 | | lptioo2.3 |
. . 3
β’ (π β π΅ β β) |
60 | 56, 58, 59 | islptre 43867 |
. 2
β’ (π β (π΅ β ((limPtβπ½)β(π΄(,)π΅)) β βπ β β* βπ β β*
(π΅ β (π(,)π) β ((π(,)π) β© ((π΄(,)π΅) β {π΅})) β β
))) |
61 | 55, 60 | mpbird 257 |
1
β’ (π β π΅ β ((limPtβπ½)β(π΄(,)π΅))) |