Step Hyp Ref
Expression 1 limelon 4946 . . . 4
2 omcl 7205 . . . . 5
3 eloni 4893 . . . . 5
4 2 , 3 syl 16 . . . 4
5 1 , 4 sylan2 474 . . 3
6 5 adantr 465 . 2
7 0ellim 4945 . . . . . . . 8
8 n0i 3789 . . . . . . . 8
9 7 , 8 syl 16 . . . . . . 7
10 n0i 3789 . . . . . . 7
11 9 , 10 anim12ci 567 . . . . . 6
12 11 adantll 713 . . . . 5
13 12 adantll 713 . . . 4
14 om00 7243 . . . . . . . 8
15 14 notbid 294 . . . . . . 7
16 ioran 490 . . . . . . 7
17 15 , 16 syl6bb 261 . . . . . 6
18 1 , 17 sylan2 474 . . . . 5
19 18 adantr 465 . . . 4
20 13 , 19 mpbird 232 . . 3
21 vex 3112 . . . . . . . . . . 11
22 21 sucid 4962 . . . . . . . . . 10
23 omlim 7202 . . . . . . . . . . 11
24 eqeq1 2461 . . . . . . . . . . . 12
25 24 biimpac 486 . . . . . . . . . . 11
26 23 , 25 sylan 471 . . . . . . . . . 10
27 22 , 26 syl5eleq 2551 . . . . . . . . 9
28 eliun 4335 . . . . . . . . 9
29 27 , 28 sylib 196 . . . . . . . 8
30 29 adantlr 714 . . . . . . 7
31 onelon 4908 . . . . . . . . . . . . . . . 16
32 1 , 31 sylan 471 . . . . . . . . . . . . . . 15
33 onnbtwn 4974 . . . . . . . . . . . . . . . . . 18
34 imnan 422 . . . . . . . . . . . . . . . . . 18
35 33 , 34 sylibr 212 . . . . . . . . . . . . . . . . 17
36 35 com12 31 . . . . . . . . . . . . . . . 16
37 36 adantl 466 . . . . . . . . . . . . . . 15
38 32 , 37 mpd 15 . . . . . . . . . . . . . 14
39 38 adantll 713 . . . . . . . . . . . . 13
40 39 adantlr 714 . . . . . . . . . . . 12
41 40 adantr 465 . . . . . . . . . . 11
42 simpl 457 . . . . . . . . . . . . . . . . . 18
43 42 , 31 jca 532 . . . . . . . . . . . . . . . . 17
44 1 , 43 sylan 471 . . . . . . . . . . . . . . . 16
45 44 anim2i 569 . . . . . . . . . . . . . . 15
46 45 anassrs 648 . . . . . . . . . . . . . 14
47 omcl 7205 . . . . . . . . . . . . . . . . . . . . 21
48 eloni 4893 . . . . . . . . . . . . . . . . . . . . . . 23
49 ordsucelsuc 6657 . . . . . . . . . . . . . . . . . . . . . . 23
50 48 , 49 syl 16 . . . . . . . . . . . . . . . . . . . . . 22
51 oa1suc 7200 . . . . . . . . . . . . . . . . . . . . . . 23
52 51 eleq2d 2527 . . . . . . . . . . . . . . . . . . . . . 22
53 50 , 52 bitr4d 256 . . . . . . . . . . . . . . . . . . . . 21
54 47 , 53 syl 16 . . . . . . . . . . . . . . . . . . . 20
55 54 adantr 465 . . . . . . . . . . . . . . . . . . 19
56 eloni 4893 . . . . . . . . . . . . . . . . . . . . . . . . 25
57 ordgt0ge1 7166 . . . . . . . . . . . . . . . . . . . . . . . . 25
58 56 , 57 syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
59 58 adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
60 1on 7156 . . . . . . . . . . . . . . . . . . . . . . . . 25
61 oaword 7217 . . . . . . . . . . . . . . . . . . . . . . . . 25
62 60 , 61 mp3an1 1311 . . . . . . . . . . . . . . . . . . . . . . . 24
63 47 , 62 syldan 470 . . . . . . . . . . . . . . . . . . . . . . 23
64 59 , 63 bitrd 253 . . . . . . . . . . . . . . . . . . . . . 22
65 64 biimpa 484 . . . . . . . . . . . . . . . . . . . . 21
66 omsuc 7195 . . . . . . . . . . . . . . . . . . . . . 22
67 66 adantr 465 . . . . . . . . . . . . . . . . . . . . 21
68 65 , 67 sseqtr4d 3540 . . . . . . . . . . . . . . . . . . . 20
69 68 sseld 3502 . . . . . . . . . . . . . . . . . . 19
70 55 , 69 sylbid 215 . . . . . . . . . . . . . . . . . 18
71 eleq1 2529 . . . . . . . . . . . . . . . . . . 19
72 71 biimprd 223 . . . . . . . . . . . . . . . . . 18
73 70 , 72 syl9 71 . . . . . . . . . . . . . . . . 17
74 73 com23 78 . . . . . . . . . . . . . . . 16
75 74 adantlrl 719 . . . . . . . . . . . . . . 15
76 sucelon 6652 . . . . . . . . . . . . . . . . . . 19
77 omord 7236 . . . . . . . . . . . . . . . . . . . 20
78 simpl 457 . . . . . . . . . . . . . . . . . . . 20
79 77 , 78 syl6bir 229 . . . . . . . . . . . . . . . . . . 19
80 76 , 79 syl3an2b 1265 . . . . . . . . . . . . . . . . . 18
81 80 3comr 1204 . . . . . . . . . . . . . . . . 17
82 81 3expb 1197 . . . . . . . . . . . . . . . 16
83 82 adantr 465 . . . . . . . . . . . . . . 15
84 75 , 83 syl6d 69 . . . . . . . . . . . . . 14
85 46 , 84 sylan 471 . . . . . . . . . . . . 13
86 85 an32s 804 . . . . . . . . . . . 12
87 86 imp 429 . . . . . . . . . . 11
88 41 , 87 mtod 177 . . . . . . . . . 10
89 88 exp31 604 . . . . . . . . 9
90 89 rexlimdv 2947 . . . . . . . 8
91 90 adantr 465 . . . . . . 7
92 30 , 91 mpd 15 . . . . . 6
93 92 pm2.01da 442 . . . . 5
94 93 adantr 465 . . . 4
95 94 nrexdv 2913 . . 3
96 ioran 490 . . 3
97 20 , 95 , 96 sylanbrc 664 . 2
98 dflim3 6682 . 2
99 6 , 97 , 98 sylanbrc 664 1
