Step | Hyp | Ref
| Expression |
1 | | difssd 4132 |
. . . . . . . 8
β’ (π β ((π΄(,)π΅) β {π΄}) β (π΄(,)π΅)) |
2 | | simpr 485 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β (π΄(,)π΅)) |
3 | | lbioo 13354 |
. . . . . . . . . . . 12
β’ Β¬
π΄ β (π΄(,)π΅) |
4 | | eleq1 2821 |
. . . . . . . . . . . . 13
β’ (π₯ = π΄ β (π₯ β (π΄(,)π΅) β π΄ β (π΄(,)π΅))) |
5 | 4 | biimpcd 248 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄(,)π΅) β (π₯ = π΄ β π΄ β (π΄(,)π΅))) |
6 | 3, 5 | mtoi 198 |
. . . . . . . . . . 11
β’ (π₯ β (π΄(,)π΅) β Β¬ π₯ = π΄) |
7 | 6 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ = π΄) |
8 | | velsn 4644 |
. . . . . . . . . 10
β’ (π₯ β {π΄} β π₯ = π΄) |
9 | 7, 8 | sylnibr 328 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β Β¬ π₯ β {π΄}) |
10 | 2, 9 | eldifd 3959 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β ((π΄(,)π΅) β {π΄})) |
11 | 1, 10 | eqelssd 4003 |
. . . . . . 7
β’ (π β ((π΄(,)π΅) β {π΄}) = (π΄(,)π΅)) |
12 | 11 | ineq2d 4212 |
. . . . . 6
β’ (π β ((π(,)π) β© ((π΄(,)π΅) β {π΄})) = ((π(,)π) β© (π΄(,)π΅))) |
13 | 12 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β ((π(,)π) β© ((π΄(,)π΅) β {π΄})) = ((π(,)π) β© (π΄(,)π΅))) |
14 | | simplrl 775 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β π β β*) |
15 | | simplrr 776 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β π β β*) |
16 | | lptioo1.2 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
17 | 16 | rexrd 11263 |
. . . . . . . . 9
β’ (π β π΄ β
β*) |
18 | | lptioo1.3 |
. . . . . . . . 9
β’ (π β π΅ β
β*) |
19 | 17, 18 | jca 512 |
. . . . . . . 8
β’ (π β (π΄ β β* β§ π΅ β
β*)) |
20 | 19 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β (π΄ β β* β§ π΅ β
β*)) |
21 | | iooin 13357 |
. . . . . . 7
β’ (((π β β*
β§ π β
β*) β§ (π΄ β β* β§ π΅ β β*))
β ((π(,)π) β© (π΄(,)π΅)) = (if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅))) |
22 | 14, 15, 20, 21 | syl21anc 836 |
. . . . . 6
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β ((π(,)π) β© (π΄(,)π΅)) = (if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅))) |
23 | | elioo3g 13352 |
. . . . . . . . . . . . . 14
β’ (π΄ β (π(,)π) β ((π β β* β§ π β β*
β§ π΄ β
β*) β§ (π < π΄ β§ π΄ < π))) |
24 | 23 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π΄ β (π(,)π) β ((π β β* β§ π β β*
β§ π΄ β
β*) β§ (π < π΄ β§ π΄ < π))) |
25 | 24 | simpld 495 |
. . . . . . . . . . . 12
β’ (π΄ β (π(,)π) β (π β β* β§ π β β*
β§ π΄ β
β*)) |
26 | 25 | simp1d 1142 |
. . . . . . . . . . 11
β’ (π΄ β (π(,)π) β π β β*) |
27 | 25 | simp3d 1144 |
. . . . . . . . . . 11
β’ (π΄ β (π(,)π) β π΄ β
β*) |
28 | 24 | simprd 496 |
. . . . . . . . . . . 12
β’ (π΄ β (π(,)π) β (π < π΄ β§ π΄ < π)) |
29 | 28 | simpld 495 |
. . . . . . . . . . 11
β’ (π΄ β (π(,)π) β π < π΄) |
30 | 26, 27, 29 | xrltled 13128 |
. . . . . . . . . 10
β’ (π΄ β (π(,)π) β π β€ π΄) |
31 | 30 | iftrued 4536 |
. . . . . . . . 9
β’ (π΄ β (π(,)π) β if(π β€ π΄, π΄, π) = π΄) |
32 | 31 | adantl 482 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β if(π β€ π΄, π΄, π) = π΄) |
33 | 28 | simprd 496 |
. . . . . . . . . . 11
β’ (π΄ β (π(,)π) β π΄ < π) |
34 | 33 | ad2antlr 725 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ π β€ π΅) β π΄ < π) |
35 | | iftrue 4534 |
. . . . . . . . . . . 12
β’ (π β€ π΅ β if(π β€ π΅, π, π΅) = π) |
36 | 35 | eqcomd 2738 |
. . . . . . . . . . 11
β’ (π β€ π΅ β π = if(π β€ π΅, π, π΅)) |
37 | 36 | adantl 482 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ π β€ π΅) β π = if(π β€ π΅, π, π΅)) |
38 | 34, 37 | breqtrd 5174 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ π β€ π΅) β π΄ < if(π β€ π΅, π, π΅)) |
39 | | lptioo1.4 |
. . . . . . . . . . 11
β’ (π β π΄ < π΅) |
40 | 39 | ad3antrrr 728 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ Β¬ π β€ π΅) β π΄ < π΅) |
41 | | iffalse 4537 |
. . . . . . . . . . . 12
β’ (Β¬
π β€ π΅ β if(π β€ π΅, π, π΅) = π΅) |
42 | 41 | eqcomd 2738 |
. . . . . . . . . . 11
β’ (Β¬
π β€ π΅ β π΅ = if(π β€ π΅, π, π΅)) |
43 | 42 | adantl 482 |
. . . . . . . . . 10
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ Β¬ π β€ π΅) β π΅ = if(π β€ π΅, π, π΅)) |
44 | 40, 43 | breqtrd 5174 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ Β¬ π β€ π΅) β π΄ < if(π β€ π΅, π, π΅)) |
45 | 38, 44 | pm2.61dan 811 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β π΄ < if(π β€ π΅, π, π΅)) |
46 | 32, 45 | eqbrtrd 5170 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β if(π β€ π΄, π΄, π) < if(π β€ π΅, π, π΅)) |
47 | 17 | ad3antrrr 728 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ π β€ π΄) β π΄ β
β*) |
48 | 14 | adantr 481 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ Β¬ π β€ π΄) β π β β*) |
49 | 47, 48 | ifclda 4563 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β if(π β€ π΄, π΄, π) β
β*) |
50 | 15 | adantr 481 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ π β€ π΅) β π β β*) |
51 | 18 | ad3antrrr 728 |
. . . . . . . . 9
β’ ((((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β§ Β¬ π β€ π΅) β π΅ β
β*) |
52 | 50, 51 | ifclda 4563 |
. . . . . . . 8
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β if(π β€ π΅, π, π΅) β
β*) |
53 | | ioon0 13349 |
. . . . . . . 8
β’
((if(π β€ π΄, π΄, π) β β* β§ if(π β€ π΅, π, π΅) β β*) β
((if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅)) β β
β if(π β€ π΄, π΄, π) < if(π β€ π΅, π, π΅))) |
54 | 49, 52, 53 | syl2anc 584 |
. . . . . . 7
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β ((if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅)) β β
β if(π β€ π΄, π΄, π) < if(π β€ π΅, π, π΅))) |
55 | 46, 54 | mpbird 256 |
. . . . . 6
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β (if(π β€ π΄, π΄, π)(,)if(π β€ π΅, π, π΅)) β β
) |
56 | 22, 55 | eqnetrd 3008 |
. . . . 5
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β ((π(,)π) β© (π΄(,)π΅)) β β
) |
57 | 13, 56 | eqnetrd 3008 |
. . . 4
β’ (((π β§ (π β β* β§ π β β*))
β§ π΄ β (π(,)π)) β ((π(,)π) β© ((π΄(,)π΅) β {π΄})) β β
) |
58 | 57 | ex 413 |
. . 3
β’ ((π β§ (π β β* β§ π β β*))
β (π΄ β (π(,)π) β ((π(,)π) β© ((π΄(,)π΅) β {π΄})) β β
)) |
59 | 58 | ralrimivva 3200 |
. 2
β’ (π β βπ β β* βπ β β*
(π΄ β (π(,)π) β ((π(,)π) β© ((π΄(,)π΅) β {π΄})) β β
)) |
60 | | lptioo1.1 |
. . 3
β’ π½ = (topGenβran
(,)) |
61 | | ioossre 13384 |
. . . 4
β’ (π΄(,)π΅) β β |
62 | 61 | a1i 11 |
. . 3
β’ (π β (π΄(,)π΅) β β) |
63 | 60, 62, 16 | islptre 44325 |
. 2
β’ (π β (π΄ β ((limPtβπ½)β(π΄(,)π΅)) β βπ β β* βπ β β*
(π΄ β (π(,)π) β ((π(,)π) β© ((π΄(,)π΅) β {π΄})) β β
))) |
64 | 59, 63 | mpbird 256 |
1
β’ (π β π΄ β ((limPtβπ½)β(π΄(,)π΅))) |