Step | Hyp | Ref
| Expression |
1 | | limelon 5788 |
. . . . . 6
|
2 | | 0ellim 5787 |
. . . . . . 7
|
3 | 2 | adantl 482 |
. . . . . 6
|
4 | | oe0m1 7601 |
. . . . . . 7
|
5 | 4 | biimpa 501 |
. . . . . 6
|
6 | 1, 3, 5 | syl2anc 693 |
. . . . 5
|
7 | | eldif 3584 |
. . . . . . . . 9
|
8 | | limord 5784 |
. . . . . . . . . . . 12
|
9 | | ordelon 5747 |
. . . . . . . . . . . 12
|
10 | 8, 9 | sylan 488 |
. . . . . . . . . . 11
|
11 | | on0eln0 5780 |
. . . . . . . . . . . . 13
|
12 | | el1o 7579 |
. . . . . . . . . . . . . 14
|
13 | 12 | necon3bbii 2841 |
. . . . . . . . . . . . 13
|
14 | 11, 13 | syl6bbr 278 |
. . . . . . . . . . . 12
|
15 | | oe0m1 7601 |
. . . . . . . . . . . . 13
|
16 | 15 | biimpd 219 |
. . . . . . . . . . . 12
|
17 | 14, 16 | sylbird 250 |
. . . . . . . . . . 11
|
18 | 10, 17 | syl 17 |
. . . . . . . . . 10
|
19 | 18 | impr 649 |
. . . . . . . . 9
|
20 | 7, 19 | sylan2b 492 |
. . . . . . . 8
|
21 | 20 | iuneq2dv 4542 |
. . . . . . 7
|
22 | | df-1o 7560 |
. . . . . . . . . . 11
|
23 | | limsuc 7049 |
. . . . . . . . . . . 12
|
24 | 2, 23 | mpbid 222 |
. . . . . . . . . . 11
|
25 | 22, 24 | syl5eqel 2705 |
. . . . . . . . . 10
|
26 | | 1on 7567 |
. . . . . . . . . . 11
|
27 | 26 | onirri 5834 |
. . . . . . . . . 10
|
28 | 25, 27 | jctir 561 |
. . . . . . . . 9
|
29 | | eldif 3584 |
. . . . . . . . 9
|
30 | 28, 29 | sylibr 224 |
. . . . . . . 8
|
31 | | ne0i 3921 |
. . . . . . . 8
|
32 | | iunconst 4529 |
. . . . . . . 8
|
33 | 30, 31, 32 | 3syl 18 |
. . . . . . 7
|
34 | 21, 33 | eqtrd 2656 |
. . . . . 6
|
35 | 34 | adantl 482 |
. . . . 5
|
36 | 6, 35 | eqtr4d 2659 |
. . . 4
|
37 | | oveq1 6657 |
. . . . 5
|
38 | | oveq1 6657 |
. . . . . 6
|
39 | 38 | iuneq2d 4547 |
. . . . 5
|
40 | 37, 39 | eqeq12d 2637 |
. . . 4
|
41 | 36, 40 | syl5ibr 236 |
. . 3
|
42 | 41 | impcom 446 |
. 2
|
43 | | oelim 7614 |
. . 3
|
44 | | limsuc 7049 |
. . . . . . . . . . . . 13
|
45 | 44 | biimpa 501 |
. . . . . . . . . . . 12
|
46 | | nsuceq0 5805 |
. . . . . . . . . . . . 13
|
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
|
48 | | dif1o 7580 |
. . . . . . . . . . . 12
|
49 | 45, 47, 48 | sylanbrc 698 |
. . . . . . . . . . 11
|
50 | 49 | ex 450 |
. . . . . . . . . 10
|
51 | 50 | ad2antlr 763 |
. . . . . . . . 9
|
52 | | sssucid 5802 |
. . . . . . . . . . 11
|
53 | | ordelon 5747 |
. . . . . . . . . . . . . . . . 17
|
54 | 8, 53 | sylan 488 |
. . . . . . . . . . . . . . . 16
|
55 | | suceloni 7013 |
. . . . . . . . . . . . . . . 16
|
56 | 54, 55 | jccir 562 |
. . . . . . . . . . . . . . 15
|
57 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
58 | 57 | 3expa 1265 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | ancoms 469 |
. . . . . . . . . . . . . . 15
|
60 | 56, 59 | sylan2 491 |
. . . . . . . . . . . . . 14
|
61 | 60 | anassrs 680 |
. . . . . . . . . . . . 13
|
62 | | oewordi 7671 |
. . . . . . . . . . . . 13
|
63 | 61, 62 | sylan 488 |
. . . . . . . . . . . 12
|
64 | 63 | an32s 846 |
. . . . . . . . . . 11
|
65 | 52, 64 | mpi 20 |
. . . . . . . . . 10
|
66 | 65 | ex 450 |
. . . . . . . . 9
|
67 | 51, 66 | jcad 555 |
. . . . . . . 8
|
68 | | oveq2 6658 |
. . . . . . . . . 10
|
69 | 68 | sseq2d 3633 |
. . . . . . . . 9
|
70 | 69 | rspcev 3309 |
. . . . . . . 8
|
71 | 67, 70 | syl6 35 |
. . . . . . 7
|
72 | 71 | ralrimiv 2965 |
. . . . . 6
|
73 | | iunss2 4565 |
. . . . . 6
|
74 | 72, 73 | syl 17 |
. . . . 5
|
75 | | difss 3737 |
. . . . . . . 8
|
76 | | iunss1 4532 |
. . . . . . . 8
|
77 | 75, 76 | ax-mp 5 |
. . . . . . 7
|
78 | | oveq2 6658 |
. . . . . . . 8
|
79 | 78 | cbviunv 4559 |
. . . . . . 7
|
80 | 77, 79 | sseqtri 3637 |
. . . . . 6
|
81 | 80 | a1i 11 |
. . . . 5
|
82 | 74, 81 | eqssd 3620 |
. . . 4
|
83 | 82 | adantlrl 756 |
. . 3
|
84 | 43, 83 | eqtrd 2656 |
. 2
|
85 | 42, 84 | oe0lem 7593 |
1
|