Step | Hyp | Ref
| Expression |
1 | | difssd 4093 |
. . . . . . . 8
β’ (π β ((π΄(,)π΅) β {π΄}) β (π΄(,)π΅)) |
2 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β (π΄(,)π΅)) |
3 | | lbioo 13296 |
. . . . . . . . . . . 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 | | lptioo1.2 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
17 | 16 | rexrd 11206 |
. . . . . . . . 9
β’ (π β π΄ β
β*) |
18 | | lptioo1.3 |
. . . . . . . . 9
β’ (π β π΅ β
β*) |
19 | 17, 18 | jca 513 |
. . . . . . . 8
β’ (π β (π΄ β β* β§ π΅ β
β*)) |
20 | 19 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β (π΄ β β* β§ π΅ β
β*)) |
21 | | iooin 13299 |
. . . . . . 7
β’ (((π β β*
β§ π β
β*) β§ (π΄ β β* β§ π΅ β β*))
β ((π(,)π) β© (π΄(,)π΅)) = (if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅))) |
22 | 14, 15, 20, 21 | syl21anc 837 |
. . . . . 6
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β ((π(,)π) β© (π΄(,)π΅)) = (if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅))) |
23 | | elioo3g 13294 |
. . . . . . . . . . . . . 14
β’ (π΄ β (π(,)π) β ((π β β* β§ π β β*
β§ π΄ β
β*) β§ (π < π΄ β§ π΄ < π))) |
24 | 23 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π΄ β (π(,)π) β ((π β β* β§ π β β*
β§ π΄ β
β*) β§ (π < π΄ β§ π΄ < π))) |
25 | 24 | simpld 496 |
. . . . . . . . . . . 12
β’ (π΄ β (π(,)π) β (π β β* β§ π β β*
β§ π΄ β
β*)) |
26 | 25 | simp1d 1143 |
. . . . . . . . . . 11
β’ (π΄ β (π(,)π) β π β β*) |
27 | 25 | simp3d 1145 |
. . . . . . . . . . 11
β’ (π΄ β (π(,)π) β π΄ β
β*) |
28 | 24 | simprd 497 |
. . . . . . . . . . . 12
β’ (π΄ β (π(,)π) β (π < π΄ β§ π΄ < π)) |
29 | 28 | simpld 496 |
. . . . . . . . . . 11
β’ (π΄ β (π(,)π) β π < π΄) |
30 | 26, 27, 29 | xrltled 13070 |
. . . . . . . . . 10
β’ (π΄ β (π(,)π) β π β€ π΄) |
31 | 30 | iftrued 4495 |
. . . . . . . . 9
β’ (π΄ β (π(,)π) β if(π β€ π΄, π΄, π) = π΄) |
32 | 31 | adantl 483 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β if(π β€ π΄, π΄, π) = π΄) |
33 | 28 | simprd 497 |
. . . . . . . . . . 11
β’ (π΄ β (π(,)π) β π΄ < π) |
34 | 33 | ad2antlr 726 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ π β€ π΅) β π΄ < π) |
35 | | iftrue 4493 |
. . . . . . . . . . . 12
β’ (π β€ π΅ β if(π β€ π΅, π, π΅) = π) |
36 | 35 | eqcomd 2743 |
. . . . . . . . . . 11
β’ (π β€ π΅ β π = if(π β€ π΅, π, π΅)) |
37 | 36 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ π β€ π΅) β π = if(π β€ π΅, π, π΅)) |
38 | 34, 37 | breqtrd 5132 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ π β€ π΅) β π΄ < if(π β€ π΅, π, π΅)) |
39 | | lptioo1.4 |
. . . . . . . . . . 11
β’ (π β π΄ < π΅) |
40 | 39 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ Β¬ π β€ π΅) β π΄ < π΅) |
41 | | iffalse 4496 |
. . . . . . . . . . . 12
β’ (Β¬
π β€ π΅ β if(π β€ π΅, π, π΅) = π΅) |
42 | 41 | eqcomd 2743 |
. . . . . . . . . . 11
β’ (Β¬
π β€ π΅ β π΅ = if(π β€ π΅, π, π΅)) |
43 | 42 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ Β¬ π β€ π΅) β π΅ = if(π β€ π΅, π, π΅)) |
44 | 40, 43 | breqtrd 5132 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ Β¬ π β€ π΅) β π΄ < if(π β€ π΅, π, π΅)) |
45 | 38, 44 | pm2.61dan 812 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β π΄ < if(π β€ π΅, π, π΅)) |
46 | 32, 45 | eqbrtrd 5128 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β if(π β€ π΄, π΄, π) < if(π β€ π΅, π, π΅)) |
47 | 17 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ π β€ π΄) β π΄ β
β*) |
48 | 14 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ Β¬ π β€ π΄) β π β β*) |
49 | 47, 48 | ifclda 4522 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β if(π β€ π΄, π΄, π) β
β*) |
50 | 15 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ π β€ π΅) β π β β*) |
51 | 18 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ Β¬ π β€ π΅) β π΅ β
β*) |
52 | 50, 51 | ifclda 4522 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β if(π β€ π΅, π, π΅) β
β*) |
53 | | ioon0 13291 |
. . . . . . . 8
β’
((if(π β€ π΄, π΄, π) β β* β§ if(π β€ π΅, π, π΅) β β*) β
((if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅)) β β
β if(π β€ π΄, π΄, π) < if(π β€ π΅, π, π΅))) |
54 | 49, 52, 53 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β ((if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅)) β β
β if(π β€ π΄, π΄, π) < if(π β€ π΅, π, π΅))) |
55 | 46, 54 | mpbird 257 |
. . . . . 6
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β (if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅)) β β
) |
56 | 22, 55 | eqnetrd 3012 |
. . . . 5
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β ((π(,)π) β© (π΄(,)π΅)) β β
) |
57 | 13, 56 | eqnetrd 3012 |
. . . 4
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β ((π(,)π) β© ((π΄(,)π΅) β {π΄})) β β
) |
58 | 57 | ex 414 |
. . 3
β’ ((π β§ (π β β* β§ π β β*))
β (π΄ β (π(,)π) β ((π(,)π) β© ((π΄(,)π΅) β {π΄})) β β
)) |
59 | 58 | ralrimivva 3198 |
. 2
β’ (π β βπ β β* βπ β β*
(π΄ β (π(,)π) β ((π(,)π) β© ((π΄(,)π΅) β {π΄})) β β
)) |
60 | | lptioo1.1 |
. . 3
β’ π½ = (topGenβran
(,)) |
61 | | ioossre 13326 |
. . . 4
β’ (π΄(,)π΅) β β |
62 | 61 | a1i 11 |
. . 3
β’ (π β (π΄(,)π΅) β β) |
63 | 60, 62, 16 | islptre 43867 |
. 2
β’ (π β (π΄ β ((limPtβπ½)β(π΄(,)π΅)) β βπ β β* βπ β β*
(π΄ β (π(,)π) β ((π(,)π) β© ((π΄(,)π΅) β {π΄})) β β
))) |
64 | 59, 63 | mpbird 257 |
1
β’ (π β π΄ β ((limPtβπ½)β(π΄(,)π΅))) |