Step | Hyp | Ref
| Expression |
1 | | recvguniq.lre |
. . . . 5
β’ (π β πΏ β β) |
2 | | recvguniq.mre |
. . . . 5
β’ (π β π β β) |
3 | | reaplt 8545 |
. . . . 5
β’ ((πΏ β β β§ π β β) β (πΏ # π β (πΏ < π β¨ π < πΏ))) |
4 | 1, 2, 3 | syl2anc 411 |
. . . 4
β’ (π β (πΏ # π β (πΏ < π β¨ π < πΏ))) |
5 | | oveq2 5883 |
. . . . . . . . . . . 12
β’ (π₯ = ((π β πΏ) / 2) β (πΏ + π₯) = (πΏ + ((π β πΏ) / 2))) |
6 | 5 | breq2d 4016 |
. . . . . . . . . . 11
β’ (π₯ = ((π β πΏ) / 2) β ((πΉβπ) < (πΏ + π₯) β (πΉβπ) < (πΏ + ((π β πΏ) / 2)))) |
7 | | oveq2 5883 |
. . . . . . . . . . . 12
β’ (π₯ = ((π β πΏ) / 2) β ((πΉβπ) + π₯) = ((πΉβπ) + ((π β πΏ) / 2))) |
8 | 7 | breq2d 4016 |
. . . . . . . . . . 11
β’ (π₯ = ((π β πΏ) / 2) β (πΏ < ((πΉβπ) + π₯) β πΏ < ((πΉβπ) + ((π β πΏ) / 2)))) |
9 | 6, 8 | anbi12d 473 |
. . . . . . . . . 10
β’ (π₯ = ((π β πΏ) / 2) β (((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β ((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))))) |
10 | | oveq2 5883 |
. . . . . . . . . . . 12
β’ (π₯ = ((π β πΏ) / 2) β (π + π₯) = (π + ((π β πΏ) / 2))) |
11 | 10 | breq2d 4016 |
. . . . . . . . . . 11
β’ (π₯ = ((π β πΏ) / 2) β ((πΉβπ) < (π + π₯) β (πΉβπ) < (π + ((π β πΏ) / 2)))) |
12 | 7 | breq2d 4016 |
. . . . . . . . . . 11
β’ (π₯ = ((π β πΏ) / 2) β (π < ((πΉβπ) + π₯) β π < ((πΉβπ) + ((π β πΏ) / 2)))) |
13 | 11, 12 | anbi12d 473 |
. . . . . . . . . 10
β’ (π₯ = ((π β πΏ) / 2) β (((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)) β ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2))))) |
14 | 9, 13 | anbi12d 473 |
. . . . . . . . 9
β’ (π₯ = ((π β πΏ) / 2) β ((((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) β (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2)))))) |
15 | 14 | rexbidv 2478 |
. . . . . . . 8
β’ (π₯ = ((π β πΏ) / 2) β (βπ β β (((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) β βπ β β (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2)))))) |
16 | | recvguniq.l |
. . . . . . . . . . . 12
β’ (π β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯))) |
17 | | recvguniq.m |
. . . . . . . . . . . 12
β’ (π β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) |
18 | | r19.26 2603 |
. . . . . . . . . . . 12
β’
(βπ₯ β
β+ (βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) β (βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)))) |
19 | 16, 17, 18 | sylanbrc 417 |
. . . . . . . . . . 11
β’ (π β βπ₯ β β+ (βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)))) |
20 | | nnuz 9563 |
. . . . . . . . . . . . 13
β’ β =
(β€β₯β1) |
21 | 20 | rexanuz2 11000 |
. . . . . . . . . . . 12
β’
(βπ β
β βπ β
(β€β₯βπ)(((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) β (βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)))) |
22 | 21 | ralbii 2483 |
. . . . . . . . . . 11
β’
(βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)(((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) β βπ₯ β β+ (βπ β β βπ β
(β€β₯βπ)((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)))) |
23 | 19, 22 | sylibr 134 |
. . . . . . . . . 10
β’ (π β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)))) |
24 | 20 | r19.2uz 11002 |
. . . . . . . . . . 11
β’
(βπ β
β βπ β
(β€β₯βπ)(((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) β βπ β β (((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)))) |
25 | 24 | ralimi 2540 |
. . . . . . . . . 10
β’
(βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)(((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) β βπ₯ β β+ βπ β β (((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)))) |
26 | 23, 25 | syl 14 |
. . . . . . . . 9
β’ (π β βπ₯ β β+ βπ β β (((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)))) |
27 | 26 | adantr 276 |
. . . . . . . 8
β’ ((π β§ πΏ < π) β βπ₯ β β+ βπ β β (((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)))) |
28 | | simpr 110 |
. . . . . . . . . 10
β’ ((π β§ πΏ < π) β πΏ < π) |
29 | 1 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ πΏ < π) β πΏ β β) |
30 | 2 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ πΏ < π) β π β β) |
31 | | difrp 9692 |
. . . . . . . . . . 11
β’ ((πΏ β β β§ π β β) β (πΏ < π β (π β πΏ) β
β+)) |
32 | 29, 30, 31 | syl2anc 411 |
. . . . . . . . . 10
β’ ((π β§ πΏ < π) β (πΏ < π β (π β πΏ) β
β+)) |
33 | 28, 32 | mpbid 147 |
. . . . . . . . 9
β’ ((π β§ πΏ < π) β (π β πΏ) β
β+) |
34 | 33 | rphalfcld 9709 |
. . . . . . . 8
β’ ((π β§ πΏ < π) β ((π β πΏ) / 2) β
β+) |
35 | 15, 27, 34 | rspcdva 2847 |
. . . . . . 7
β’ ((π β§ πΏ < π) β βπ β β (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2))))) |
36 | | recvguniq.f |
. . . . . . . . 9
β’ (π β πΉ:ββΆβ) |
37 | 36 | ad2antrr 488 |
. . . . . . . 8
β’ (((π β§ πΏ < π) β§ (π β β β§ (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2)))))) β πΉ:ββΆβ) |
38 | 2 | ad2antrr 488 |
. . . . . . . 8
β’ (((π β§ πΏ < π) β§ (π β β β§ (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2)))))) β π β β) |
39 | 1 | ad2antrr 488 |
. . . . . . . 8
β’ (((π β§ πΏ < π) β§ (π β β β§ (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2)))))) β πΏ β β) |
40 | | simprl 529 |
. . . . . . . 8
β’ (((π β§ πΏ < π) β§ (π β β β§ (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2)))))) β π β β) |
41 | | simprrr 540 |
. . . . . . . . 9
β’ ((π β β β§ (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2))))) β π < ((πΉβπ) + ((π β πΏ) / 2))) |
42 | 41 | adantl 277 |
. . . . . . . 8
β’ (((π β§ πΏ < π) β§ (π β β β§ (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2)))))) β π < ((πΉβπ) + ((π β πΏ) / 2))) |
43 | | simprll 537 |
. . . . . . . . 9
β’ ((π β β β§ (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2))))) β (πΉβπ) < (πΏ + ((π β πΏ) / 2))) |
44 | 43 | adantl 277 |
. . . . . . . 8
β’ (((π β§ πΏ < π) β§ (π β β β§ (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2)))))) β (πΉβπ) < (πΏ + ((π β πΏ) / 2))) |
45 | 37, 38, 39, 40, 42, 44 | recvguniqlem 11003 |
. . . . . . 7
β’ (((π β§ πΏ < π) β§ (π β β β§ (((πΉβπ) < (πΏ + ((π β πΏ) / 2)) β§ πΏ < ((πΉβπ) + ((π β πΏ) / 2))) β§ ((πΉβπ) < (π + ((π β πΏ) / 2)) β§ π < ((πΉβπ) + ((π β πΏ) / 2)))))) β β₯) |
46 | 35, 45 | rexlimddv 2599 |
. . . . . 6
β’ ((π β§ πΏ < π) β β₯) |
47 | 46 | ex 115 |
. . . . 5
β’ (π β (πΏ < π β β₯)) |
48 | | oveq2 5883 |
. . . . . . . . . . . 12
β’ (π₯ = ((πΏ β π) / 2) β (πΏ + π₯) = (πΏ + ((πΏ β π) / 2))) |
49 | 48 | breq2d 4016 |
. . . . . . . . . . 11
β’ (π₯ = ((πΏ β π) / 2) β ((πΉβπ) < (πΏ + π₯) β (πΉβπ) < (πΏ + ((πΏ β π) / 2)))) |
50 | | oveq2 5883 |
. . . . . . . . . . . 12
β’ (π₯ = ((πΏ β π) / 2) β ((πΉβπ) + π₯) = ((πΉβπ) + ((πΏ β π) / 2))) |
51 | 50 | breq2d 4016 |
. . . . . . . . . . 11
β’ (π₯ = ((πΏ β π) / 2) β (πΏ < ((πΉβπ) + π₯) β πΏ < ((πΉβπ) + ((πΏ β π) / 2)))) |
52 | 49, 51 | anbi12d 473 |
. . . . . . . . . 10
β’ (π₯ = ((πΏ β π) / 2) β (((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β ((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))))) |
53 | | oveq2 5883 |
. . . . . . . . . . . 12
β’ (π₯ = ((πΏ β π) / 2) β (π + π₯) = (π + ((πΏ β π) / 2))) |
54 | 53 | breq2d 4016 |
. . . . . . . . . . 11
β’ (π₯ = ((πΏ β π) / 2) β ((πΉβπ) < (π + π₯) β (πΉβπ) < (π + ((πΏ β π) / 2)))) |
55 | 50 | breq2d 4016 |
. . . . . . . . . . 11
β’ (π₯ = ((πΏ β π) / 2) β (π < ((πΉβπ) + π₯) β π < ((πΉβπ) + ((πΏ β π) / 2)))) |
56 | 54, 55 | anbi12d 473 |
. . . . . . . . . 10
β’ (π₯ = ((πΏ β π) / 2) β (((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)) β ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2))))) |
57 | 52, 56 | anbi12d 473 |
. . . . . . . . 9
β’ (π₯ = ((πΏ β π) / 2) β ((((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) β (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2)))))) |
58 | 57 | rexbidv 2478 |
. . . . . . . 8
β’ (π₯ = ((πΏ β π) / 2) β (βπ β β (((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) β βπ β β (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2)))))) |
59 | 26 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π < πΏ) β βπ₯ β β+ βπ β β (((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯)) β§ ((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯)))) |
60 | | difrp 9692 |
. . . . . . . . . . 11
β’ ((π β β β§ πΏ β β) β (π < πΏ β (πΏ β π) β
β+)) |
61 | 2, 1, 60 | syl2anc 411 |
. . . . . . . . . 10
β’ (π β (π < πΏ β (πΏ β π) β
β+)) |
62 | 61 | biimpa 296 |
. . . . . . . . 9
β’ ((π β§ π < πΏ) β (πΏ β π) β
β+) |
63 | 62 | rphalfcld 9709 |
. . . . . . . 8
β’ ((π β§ π < πΏ) β ((πΏ β π) / 2) β
β+) |
64 | 58, 59, 63 | rspcdva 2847 |
. . . . . . 7
β’ ((π β§ π < πΏ) β βπ β β (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2))))) |
65 | 36 | ad2antrr 488 |
. . . . . . . 8
β’ (((π β§ π < πΏ) β§ (π β β β§ (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2)))))) β πΉ:ββΆβ) |
66 | 1 | ad2antrr 488 |
. . . . . . . 8
β’ (((π β§ π < πΏ) β§ (π β β β§ (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2)))))) β πΏ β β) |
67 | 2 | ad2antrr 488 |
. . . . . . . 8
β’ (((π β§ π < πΏ) β§ (π β β β§ (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2)))))) β π β β) |
68 | | simprl 529 |
. . . . . . . 8
β’ (((π β§ π < πΏ) β§ (π β β β§ (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2)))))) β π β β) |
69 | | simprlr 538 |
. . . . . . . . 9
β’ ((π β β β§ (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2))))) β πΏ < ((πΉβπ) + ((πΏ β π) / 2))) |
70 | 69 | adantl 277 |
. . . . . . . 8
β’ (((π β§ π < πΏ) β§ (π β β β§ (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2)))))) β πΏ < ((πΉβπ) + ((πΏ β π) / 2))) |
71 | | simprrl 539 |
. . . . . . . . 9
β’ ((π β β β§ (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2))))) β (πΉβπ) < (π + ((πΏ β π) / 2))) |
72 | 71 | adantl 277 |
. . . . . . . 8
β’ (((π β§ π < πΏ) β§ (π β β β§ (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2)))))) β (πΉβπ) < (π + ((πΏ β π) / 2))) |
73 | 65, 66, 67, 68, 70, 72 | recvguniqlem 11003 |
. . . . . . 7
β’ (((π β§ π < πΏ) β§ (π β β β§ (((πΉβπ) < (πΏ + ((πΏ β π) / 2)) β§ πΏ < ((πΉβπ) + ((πΏ β π) / 2))) β§ ((πΉβπ) < (π + ((πΏ β π) / 2)) β§ π < ((πΉβπ) + ((πΏ β π) / 2)))))) β β₯) |
74 | 64, 73 | rexlimddv 2599 |
. . . . . 6
β’ ((π β§ π < πΏ) β β₯) |
75 | 74 | ex 115 |
. . . . 5
β’ (π β (π < πΏ β β₯)) |
76 | 47, 75 | jaod 717 |
. . . 4
β’ (π β ((πΏ < π β¨ π < πΏ) β β₯)) |
77 | 4, 76 | sylbid 150 |
. . 3
β’ (π β (πΏ # π β β₯)) |
78 | | dfnot 1371 |
. . 3
β’ (Β¬
πΏ # π β (πΏ # π β β₯)) |
79 | 77, 78 | sylibr 134 |
. 2
β’ (π β Β¬ πΏ # π) |
80 | 1 | recnd 7986 |
. . 3
β’ (π β πΏ β β) |
81 | 2 | recnd 7986 |
. . 3
β’ (π β π β β) |
82 | | apti 8579 |
. . 3
β’ ((πΏ β β β§ π β β) β (πΏ = π β Β¬ πΏ # π)) |
83 | 80, 81, 82 | syl2anc 411 |
. 2
β’ (π β (πΏ = π β Β¬ πΏ # π)) |
84 | 79, 83 | mpbird 167 |
1
β’ (π β πΏ = π) |