Step | Hyp | Ref
| Expression |
1 | | suceq 4387 |
. . . . 5
|
2 | 1 | raleqdv 2671 |
. . . 4
|
3 | 2 | rexbidv 2471 |
. . 3
|
4 | | ennnfonelemh.ne |
. . 3
|
5 | | ennnfonelemh.n |
. . . . . . 7
frec |
6 | 5 | frechashgf1o 10384 |
. . . . . 6
|
7 | | f1ocnv 5455 |
. . . . . 6
|
8 | 6, 7 | ax-mp 5 |
. . . . 5
|
9 | | f1of 5442 |
. . . . 5
|
10 | 8, 9 | mp1i 10 |
. . . 4
|
11 | | ennnfonelemex.p |
. . . 4
|
12 | 10, 11 | ffvelrnd 5632 |
. . 3
|
13 | 3, 4, 12 | rspcdva 2839 |
. 2
|
14 | | f1of 5442 |
. . . . 5
|
15 | 6, 14 | mp1i 10 |
. . . 4
|
16 | | peano2 4579 |
. . . . 5
|
17 | 16 | ad2antrl 487 |
. . . 4
|
18 | 15, 17 | ffvelrnd 5632 |
. . 3
|
19 | | ennnfonelemh.f |
. . . . . . . . 9
|
20 | 19 | ad2antrr 485 |
. . . . . . . 8
|
21 | | fofun 5421 |
. . . . . . . 8
|
22 | 20, 21 | syl 14 |
. . . . . . 7
|
23 | | vex 2733 |
. . . . . . . . . 10
|
24 | 23 | sucid 4402 |
. . . . . . . . 9
|
25 | | simprl 526 |
. . . . . . . . . . . 12
|
26 | 25 | adantr 274 |
. . . . . . . . . . 11
|
27 | | fof 5420 |
. . . . . . . . . . . 12
|
28 | | fdm 5353 |
. . . . . . . . . . . 12
|
29 | 20, 27, 28 | 3syl 17 |
. . . . . . . . . . 11
|
30 | 26, 29 | eleqtrrd 2250 |
. . . . . . . . . 10
|
31 | | funfvima 5727 |
. . . . . . . . . 10
|
32 | 22, 30, 31 | syl2anc 409 |
. . . . . . . . 9
|
33 | 24, 32 | mpi 15 |
. . . . . . . 8
|
34 | | simpr 109 |
. . . . . . . . . . 11
|
35 | | ennnfonelemh.dceq |
. . . . . . . . . . . . . . . . . 18
DECID |
36 | 35 | adantr 274 |
. . . . . . . . . . . . . . . . 17
DECID |
37 | 19 | adantr 274 |
. . . . . . . . . . . . . . . . 17
|
38 | 4 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
|
39 | | fveq2 5496 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
40 | 39 | neeq2d 2359 |
. . . . . . . . . . . . . . . . . . . . . 22
|
41 | 40 | cbvralv 2696 |
. . . . . . . . . . . . . . . . . . . . 21
|
42 | 41 | rexbii 2477 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | | fveq2 5496 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
44 | 43 | neeq1d 2358 |
. . . . . . . . . . . . . . . . . . . . . 22
|
45 | 44 | ralbidv 2470 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | 45 | cbvrexv 2697 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | 42, 46 | bitri 183 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 47 | ralbii 2476 |
. . . . . . . . . . . . . . . . . 18
|
49 | 38, 48 | sylib 121 |
. . . . . . . . . . . . . . . . 17
|
50 | | ennnfonelemh.g |
. . . . . . . . . . . . . . . . 17
|
51 | | ennnfonelemh.j |
. . . . . . . . . . . . . . . . 17
|
52 | | ennnfonelemh.h |
. . . . . . . . . . . . . . . . 17
|
53 | 36, 37, 49, 50, 5, 51, 52, 18 | ennnfonelemhf1o 12368 |
. . . . . . . . . . . . . . . 16
|
54 | | f1ofun 5444 |
. . . . . . . . . . . . . . . 16
|
55 | 53, 54 | syl 14 |
. . . . . . . . . . . . . . 15
|
56 | 55 | ad2antrr 485 |
. . . . . . . . . . . . . 14
|
57 | 11 | adantr 274 |
. . . . . . . . . . . . . . . 16
|
58 | 6, 14 | mp1i 10 |
. . . . . . . . . . . . . . . . . 18
|
59 | 16 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
|
60 | 58, 59 | ffvelrnd 5632 |
. . . . . . . . . . . . . . . . 17
|
61 | 60 | adantrr 476 |
. . . . . . . . . . . . . . . 16
|
62 | 57 | nn0red 9189 |
. . . . . . . . . . . . . . . . 17
|
63 | 61 | nn0red 9189 |
. . . . . . . . . . . . . . . . 17
|
64 | | f1ocnvfv2 5757 |
. . . . . . . . . . . . . . . . . . 19
|
65 | 6, 57, 64 | sylancr 412 |
. . . . . . . . . . . . . . . . . 18
|
66 | 12 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . 21
|
67 | | simprr 527 |
. . . . . . . . . . . . . . . . . . . . 21
|
68 | 37, 25, 66, 67 | ennnfonelemk 12355 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | | elelsuc 4394 |
. . . . . . . . . . . . . . . . . . . 20
|
70 | 68, 69 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
|
71 | | 0zd 9224 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 71, 5, 66, 17 | frec2uzltd 10359 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 70, 72 | mpd 13 |
. . . . . . . . . . . . . . . . . 18
|
74 | 65, 73 | eqbrtrrd 4013 |
. . . . . . . . . . . . . . . . 17
|
75 | 62, 63, 74 | ltled 8038 |
. . . . . . . . . . . . . . . 16
|
76 | 36, 37, 38, 50, 5, 51, 52, 57, 61, 75 | ennnfoneleminc 12366 |
. . . . . . . . . . . . . . 15
|
77 | 76 | ad2antrr 485 |
. . . . . . . . . . . . . 14
|
78 | | simpr 109 |
. . . . . . . . . . . . . 14
|
79 | | funssfv 5522 |
. . . . . . . . . . . . . 14
|
80 | 56, 77, 78, 79 | syl3anc 1233 |
. . . . . . . . . . . . 13
|
81 | 80 | eqcomd 2176 |
. . . . . . . . . . . 12
|
82 | 81 | ralrimiva 2543 |
. . . . . . . . . . 11
|
83 | 36, 37, 49, 50, 5, 51, 52, 57 | ennnfonelemhf1o 12368 |
. . . . . . . . . . . . . 14
|
84 | | f1ofun 5444 |
. . . . . . . . . . . . . 14
|
85 | 83, 84 | syl 14 |
. . . . . . . . . . . . 13
|
86 | | eqfunfv 5598 |
. . . . . . . . . . . . 13
|
87 | 85, 55, 86 | syl2anc 409 |
. . . . . . . . . . . 12
|
88 | 87 | adantr 274 |
. . . . . . . . . . 11
|
89 | 34, 82, 88 | mpbir2and 939 |
. . . . . . . . . 10
|
90 | 89 | rneqd 4840 |
. . . . . . . . 9
|
91 | | dff1o5 5451 |
. . . . . . . . . . . 12
|
92 | 83, 91 | sylib 121 |
. . . . . . . . . . 11
|
93 | 92 | simprd 113 |
. . . . . . . . . 10
|
94 | 93 | adantr 274 |
. . . . . . . . 9
|
95 | | f1ocnvfv1 5756 |
. . . . . . . . . . . . . . . 16
|
96 | 6, 17, 95 | sylancr 412 |
. . . . . . . . . . . . . . 15
|
97 | 96 | imaeq2d 4953 |
. . . . . . . . . . . . . 14
|
98 | | f1oeq3 5433 |
. . . . . . . . . . . . . 14
|
99 | 97, 98 | syl 14 |
. . . . . . . . . . . . 13
|
100 | 53, 99 | mpbid 146 |
. . . . . . . . . . . 12
|
101 | | dff1o5 5451 |
. . . . . . . . . . . 12
|
102 | 100, 101 | sylib 121 |
. . . . . . . . . . 11
|
103 | 102 | simprd 113 |
. . . . . . . . . 10
|
104 | 103 | adantr 274 |
. . . . . . . . 9
|
105 | 90, 94, 104 | 3eqtr3d 2211 |
. . . . . . . 8
|
106 | 33, 105 | eleqtrrd 2250 |
. . . . . . 7
|
107 | | fvelima 5548 |
. . . . . . 7
|
108 | 22, 106, 107 | syl2anc 409 |
. . . . . 6
|
109 | | simprr 527 |
. . . . . . 7
|
110 | | fveq2 5496 |
. . . . . . . . . 10
|
111 | 110 | neeq2d 2359 |
. . . . . . . . 9
|
112 | 67 | ad2antrr 485 |
. . . . . . . . 9
|
113 | | elelsuc 4394 |
. . . . . . . . . 10
|
114 | 113 | ad2antrl 487 |
. . . . . . . . 9
|
115 | 111, 112,
114 | rspcdva 2839 |
. . . . . . . 8
|
116 | 115 | necomd 2426 |
. . . . . . 7
|
117 | 109, 116 | pm2.21ddne 2423 |
. . . . . 6
|
118 | 108, 117 | rexlimddv 2592 |
. . . . 5
|
119 | 118 | inegd 1367 |
. . . 4
|
120 | | dmss 4810 |
. . . . . 6
|
121 | 76, 120 | syl 14 |
. . . . 5
|
122 | 35, 19, 4, 50, 5, 51, 52, 11 | ennnfonelemom 12363 |
. . . . . . 7
|
123 | 122 | adantr 274 |
. . . . . 6
|
124 | 42 | a1i 9 |
. . . . . . . . 9
|
125 | 124 | ralbidv 2470 |
. . . . . . . 8
|
126 | 38, 125 | mpbid 146 |
. . . . . . 7
|
127 | 36, 37, 126, 50, 5, 51, 52, 61 | ennnfonelemom 12363 |
. . . . . 6
|
128 | | nntri1 6475 |
. . . . . 6
|
129 | 123, 127,
128 | syl2anc 409 |
. . . . 5
|
130 | 121, 129 | mpbid 146 |
. . . 4
|
131 | | nntri3or 6472 |
. . . . 5
|
132 | 123, 127,
131 | syl2anc 409 |
. . . 4
|
133 | 119, 130,
132 | ecase23d 1345 |
. . 3
|
134 | | fveq2 5496 |
. . . . . 6
|
135 | 134 | dmeqd 4813 |
. . . . 5
|
136 | 135 | eleq2d 2240 |
. . . 4
|
137 | 136 | rspcev 2834 |
. . 3
|
138 | 18, 133, 137 | syl2anc 409 |
. 2
|
139 | 13, 138 | rexlimddv 2592 |
1
|