Step | Hyp | Ref
| Expression |
1 | | 2onn 7720 |
. . . . . . . 8
|
2 | | nnon 7071 |
. . . . . . . . . . 11
|
3 | | 2on 7568 |
. . . . . . . . . . . . . 14
|
4 | | oawordeu 7635 |
. . . . . . . . . . . . . 14
|
5 | 3, 4 | mpanl1 716 |
. . . . . . . . . . . . 13
|
6 | | riotasbc 6626 |
. . . . . . . . . . . . 13
|
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
|
8 | | riotaex 6615 |
. . . . . . . . . . . . . 14
|
9 | | sbceq1g 3988 |
. . . . . . . . . . . . . 14
|
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . . 13
|
11 | | csbov2g 6691 |
. . . . . . . . . . . . . . . 16
|
12 | 8, 11 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
13 | | csbvarg 4003 |
. . . . . . . . . . . . . . . . 17
|
14 | 8, 13 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
15 | 14 | oveq2i 6661 |
. . . . . . . . . . . . . . 15
|
16 | 12, 15 | eqtri 2644 |
. . . . . . . . . . . . . 14
|
17 | 16 | eqeq1i 2627 |
. . . . . . . . . . . . 13
|
18 | 10, 17 | bitri 264 |
. . . . . . . . . . . 12
|
19 | 7, 18 | sylib 208 |
. . . . . . . . . . 11
|
20 | 2, 19 | sylan 488 |
. . . . . . . . . 10
|
21 | | simpl 473 |
. . . . . . . . . 10
|
22 | 20, 21 | eqeltrd 2701 |
. . . . . . . . 9
|
23 | | riotacl 6625 |
. . . . . . . . . . 11
|
24 | | riotaund 6647 |
. . . . . . . . . . . 12
|
25 | | 0elon 5778 |
. . . . . . . . . . . 12
|
26 | 24, 25 | syl6eqel 2709 |
. . . . . . . . . . 11
|
27 | 23, 26 | pm2.61i 176 |
. . . . . . . . . 10
|
28 | | nnarcl 7696 |
. . . . . . . . . . . 12
|
29 | 3, 28 | mpan 706 |
. . . . . . . . . . 11
|
30 | 1 | biantrur 527 |
. . . . . . . . . . 11
|
31 | 29, 30 | syl6bbr 278 |
. . . . . . . . . 10
|
32 | 27, 31 | ax-mp 5 |
. . . . . . . . 9
|
33 | 22, 32 | sylib 208 |
. . . . . . . 8
|
34 | | nnacom 7697 |
. . . . . . . 8
|
35 | 1, 33, 34 | sylancr 695 |
. . . . . . 7
|
36 | | df-2o 7561 |
. . . . . . . . 9
|
37 | 36 | oveq2i 6661 |
. . . . . . . 8
|
38 | | 1onn 7719 |
. . . . . . . . 9
|
39 | | nnasuc 7686 |
. . . . . . . . 9
|
40 | 33, 38, 39 | sylancl 694 |
. . . . . . . 8
|
41 | 37, 40 | syl5eq 2668 |
. . . . . . 7
|
42 | 35, 20, 41 | 3eqtr3d 2664 |
. . . . . 6
|
43 | 2 | adantr 481 |
. . . . . . 7
|
44 | | sucidg 5803 |
. . . . . . . . . . . 12
|
45 | 38, 44 | ax-mp 5 |
. . . . . . . . . . 11
|
46 | 45, 36 | eleqtrri 2700 |
. . . . . . . . . 10
|
47 | | ssel 3597 |
. . . . . . . . . 10
|
48 | 46, 47 | mpi 20 |
. . . . . . . . 9
|
49 | | ne0i 3921 |
. . . . . . . . 9
|
50 | 48, 49 | syl 17 |
. . . . . . . 8
|
51 | 50 | adantl 482 |
. . . . . . 7
|
52 | | nnlim 7078 |
. . . . . . . 8
|
53 | 52 | adantr 481 |
. . . . . . 7
|
54 | | onsucuni3 33215 |
. . . . . . 7
|
55 | 43, 51, 53, 54 | syl3anc 1326 |
. . . . . 6
|
56 | | nnacom 7697 |
. . . . . . . 8
|
57 | 33, 38, 56 | sylancl 694 |
. . . . . . 7
|
58 | | suceq 5790 |
. . . . . . 7
|
59 | 57, 58 | syl 17 |
. . . . . 6
|
60 | 42, 55, 59 | 3eqtr3d 2664 |
. . . . 5
|
61 | | ordom 7074 |
. . . . . . . . 9
|
62 | | ordelss 5739 |
. . . . . . . . 9
|
63 | 61, 62 | mpan 706 |
. . . . . . . 8
|
64 | | nnfi 8153 |
. . . . . . . 8
|
65 | | nnunifi 8211 |
. . . . . . . 8
|
66 | 63, 64, 65 | syl2anc 693 |
. . . . . . 7
|
67 | 66 | adantr 481 |
. . . . . 6
|
68 | | nnacl 7691 |
. . . . . . 7
|
69 | 38, 33, 68 | sylancr 695 |
. . . . . 6
|
70 | | peano4 7088 |
. . . . . 6
|
71 | 67, 69, 70 | syl2anc 693 |
. . . . 5
|
72 | 60, 71 | mpbid 222 |
. . . 4
|
73 | 72 | fveq2d 6195 |
. . 3
|
74 | 73 | adantr 481 |
. 2
|
75 | 33 | adantr 481 |
. . 3
|
76 | | finxpreclem4.1 |
. . . . . . 7
|
77 | 76 | finxpreclem3 33230 |
. . . . . 6
|
78 | | df-1o 7560 |
. . . . . . . 8
|
79 | 78 | fveq2i 6194 |
. . . . . . 7
|
80 | | rdgsuc 7520 |
. . . . . . . 8
|
81 | 25, 80 | ax-mp 5 |
. . . . . . 7
|
82 | | opex 4932 |
. . . . . . . . 9
|
83 | 82 | rdg0 7517 |
. . . . . . . 8
|
84 | 83 | fveq2i 6194 |
. . . . . . 7
|
85 | 79, 81, 84 | 3eqtri 2648 |
. . . . . 6
|
86 | 77, 85 | syl6reqr 2675 |
. . . . 5
|
87 | 86 | fveq2d 6195 |
. . . 4
|
88 | | 2on0 7569 |
. . . . . 6
|
89 | | nnlim 7078 |
. . . . . . 7
|
90 | 1, 89 | ax-mp 5 |
. . . . . 6
|
91 | | rdgsucuni 33217 |
. . . . . 6
|
92 | 3, 88, 90, 91 | mp3an 1424 |
. . . . 5
|
93 | | 1oequni2o 33216 |
. . . . . . 7
|
94 | 93 | fveq2i 6194 |
. . . . . 6
|
95 | 94 | fveq2i 6194 |
. . . . 5
|
96 | 92, 95 | eqtr4i 2647 |
. . . 4
|
97 | 78 | fveq2i 6194 |
. . . . 5
|
98 | | rdgsuc 7520 |
. . . . . 6
|
99 | 25, 98 | ax-mp 5 |
. . . . 5
|
100 | | opex 4932 |
. . . . . . 7
|
101 | 100 | rdg0 7517 |
. . . . . 6
|
102 | 101 | fveq2i 6194 |
. . . . 5
|
103 | 97, 99, 102 | 3eqtri 2648 |
. . . 4
|
104 | 87, 96, 103 | 3eqtr4g 2681 |
. . 3
|
105 | | 1on 7567 |
. . . 4
|
106 | | rdgeqoa 33218 |
. . . 4
|
107 | 3, 105, 106 | mp3an12 1414 |
. . 3
|
108 | 75, 104, 107 | sylc 65 |
. 2
|
109 | 20 | fveq2d 6195 |
. . 3
|
110 | 109 | adantr 481 |
. 2
|
111 | 74, 108, 110 | 3eqtr2rd 2663 |
1
|