Metamath Proof Explorer


Theorem poimirlem20

Description: Lemma for poimir establishing existence for poimirlem21 . (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φ N
poimirlem22.s S = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
poimirlem22.1 φ F : 0 N 1 0 K 1 N
poimirlem22.2 φ T S
poimirlem22.3 φ n 1 N p ran F p n 0
poimirlem21.4 φ 2 nd T = N
Assertion poimirlem20 φ z S z T

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimirlem22.s S = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
3 poimirlem22.1 φ F : 0 N 1 0 K 1 N
4 poimirlem22.2 φ T S
5 poimirlem22.3 φ n 1 N p ran F p n 0
6 poimirlem21.4 φ 2 nd T = N
7 oveq2 1 = if n = 2 nd 1 st T N 1 0 1 st 1 st T n 1 = 1 st 1 st T n if n = 2 nd 1 st T N 1 0
8 7 eleq1d 1 = if n = 2 nd 1 st T N 1 0 1 st 1 st T n 1 0 ..^ K 1 st 1 st T n if n = 2 nd 1 st T N 1 0 0 ..^ K
9 oveq2 0 = if n = 2 nd 1 st T N 1 0 1 st 1 st T n 0 = 1 st 1 st T n if n = 2 nd 1 st T N 1 0
10 9 eleq1d 0 = if n = 2 nd 1 st T N 1 0 1 st 1 st T n 0 0 ..^ K 1 st 1 st T n if n = 2 nd 1 st T N 1 0 0 ..^ K
11 fveq2 n = 2 nd 1 st T N 1 st 1 st T n = 1 st 1 st T 2 nd 1 st T N
12 11 oveq1d n = 2 nd 1 st T N 1 st 1 st T n 1 = 1 st 1 st T 2 nd 1 st T N 1
13 12 adantl φ n = 2 nd 1 st T N 1 st 1 st T n 1 = 1 st 1 st T 2 nd 1 st T N 1
14 elrabi T t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
15 14 2 eleq2s T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
16 4 15 syl φ T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
17 xp1st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
18 16 17 syl φ 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
19 xp1st 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st 1 st T 0 ..^ K 1 N
20 18 19 syl φ 1 st 1 st T 0 ..^ K 1 N
21 elmapi 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T : 1 N 0 ..^ K
22 20 21 syl φ 1 st 1 st T : 1 N 0 ..^ K
23 xp2nd 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
24 18 23 syl φ 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
25 fvex 2 nd 1 st T V
26 f1oeq1 f = 2 nd 1 st T f : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 onto 1 N
27 25 26 elab 2 nd 1 st T f | f : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 onto 1 N
28 24 27 sylib φ 2 nd 1 st T : 1 N 1-1 onto 1 N
29 f1of 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1 N
30 28 29 syl φ 2 nd 1 st T : 1 N 1 N
31 elfz1end N N 1 N
32 1 31 sylib φ N 1 N
33 30 32 ffvelrnd φ 2 nd 1 st T N 1 N
34 22 33 ffvelrnd φ 1 st 1 st T 2 nd 1 st T N 0 ..^ K
35 elfzonn0 1 st 1 st T 2 nd 1 st T N 0 ..^ K 1 st 1 st T 2 nd 1 st T N 0
36 34 35 syl φ 1 st 1 st T 2 nd 1 st T N 0
37 fvex 2 nd 1 st T N V
38 eleq1 n = 2 nd 1 st T N n 1 N 2 nd 1 st T N 1 N
39 38 anbi2d n = 2 nd 1 st T N φ n 1 N φ 2 nd 1 st T N 1 N
40 fveq2 n = 2 nd 1 st T N p n = p 2 nd 1 st T N
41 40 neeq1d n = 2 nd 1 st T N p n 0 p 2 nd 1 st T N 0
42 41 rexbidv n = 2 nd 1 st T N p ran F p n 0 p ran F p 2 nd 1 st T N 0
43 39 42 imbi12d n = 2 nd 1 st T N φ n 1 N p ran F p n 0 φ 2 nd 1 st T N 1 N p ran F p 2 nd 1 st T N 0
44 37 43 5 vtocl φ 2 nd 1 st T N 1 N p ran F p 2 nd 1 st T N 0
45 33 44 mpdan φ p ran F p 2 nd 1 st T N 0
46 fveq1 p = 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 p 2 nd 1 st T N = 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N
47 22 ffnd φ 1 st 1 st T Fn 1 N
48 47 adantr φ y 0 N 1 1 st 1 st T Fn 1 N
49 1ex 1 V
50 fnconstg 1 V 2 nd 1 st T 1 y × 1 Fn 2 nd 1 st T 1 y
51 49 50 ax-mp 2 nd 1 st T 1 y × 1 Fn 2 nd 1 st T 1 y
52 c0ex 0 V
53 fnconstg 0 V 2 nd 1 st T y + 1 N × 0 Fn 2 nd 1 st T y + 1 N
54 52 53 ax-mp 2 nd 1 st T y + 1 N × 0 Fn 2 nd 1 st T y + 1 N
55 51 54 pm3.2i 2 nd 1 st T 1 y × 1 Fn 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N × 0 Fn 2 nd 1 st T y + 1 N
56 dff1o3 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N Fun 2 nd 1 st T -1
57 56 simprbi 2 nd 1 st T : 1 N 1-1 onto 1 N Fun 2 nd 1 st T -1
58 28 57 syl φ Fun 2 nd 1 st T -1
59 imain Fun 2 nd 1 st T -1 2 nd 1 st T 1 y y + 1 N = 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N
60 58 59 syl φ 2 nd 1 st T 1 y y + 1 N = 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N
61 elfznn0 y 0 N 1 y 0
62 61 nn0red y 0 N 1 y
63 62 ltp1d y 0 N 1 y < y + 1
64 fzdisj y < y + 1 1 y y + 1 N =
65 63 64 syl y 0 N 1 1 y y + 1 N =
66 65 imaeq2d y 0 N 1 2 nd 1 st T 1 y y + 1 N = 2 nd 1 st T
67 ima0 2 nd 1 st T =
68 66 67 eqtrdi y 0 N 1 2 nd 1 st T 1 y y + 1 N =
69 60 68 sylan9req φ y 0 N 1 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N =
70 fnun 2 nd 1 st T 1 y × 1 Fn 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N × 0 Fn 2 nd 1 st T y + 1 N 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 Fn 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N
71 55 69 70 sylancr φ y 0 N 1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 Fn 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N
72 imaundi 2 nd 1 st T 1 y y + 1 N = 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N
73 nn0p1nn y 0 y + 1
74 nnuz = 1
75 73 74 eleqtrdi y 0 y + 1 1
76 61 75 syl y 0 N 1 y + 1 1
77 76 adantl φ y 0 N 1 y + 1 1
78 1 nncnd φ N
79 npcan1 N N - 1 + 1 = N
80 78 79 syl φ N - 1 + 1 = N
81 80 adantr φ y 0 N 1 N - 1 + 1 = N
82 elfzuz3 y 0 N 1 N 1 y
83 peano2uz N 1 y N - 1 + 1 y
84 82 83 syl y 0 N 1 N - 1 + 1 y
85 84 adantl φ y 0 N 1 N - 1 + 1 y
86 81 85 eqeltrrd φ y 0 N 1 N y
87 fzsplit2 y + 1 1 N y 1 N = 1 y y + 1 N
88 77 86 87 syl2anc φ y 0 N 1 1 N = 1 y y + 1 N
89 88 imaeq2d φ y 0 N 1 2 nd 1 st T 1 N = 2 nd 1 st T 1 y y + 1 N
90 f1ofo 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N
91 foima 2 nd 1 st T : 1 N onto 1 N 2 nd 1 st T 1 N = 1 N
92 28 90 91 3syl φ 2 nd 1 st T 1 N = 1 N
93 92 adantr φ y 0 N 1 2 nd 1 st T 1 N = 1 N
94 89 93 eqtr3d φ y 0 N 1 2 nd 1 st T 1 y y + 1 N = 1 N
95 72 94 eqtr3id φ y 0 N 1 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N = 1 N
96 95 fneq2d φ y 0 N 1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 Fn 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 Fn 1 N
97 71 96 mpbid φ y 0 N 1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 Fn 1 N
98 ovex 1 N V
99 98 a1i φ y 0 N 1 1 N V
100 inidm 1 N 1 N = 1 N
101 eqidd φ y 0 N 1 2 nd 1 st T N 1 N 1 st 1 st T 2 nd 1 st T N = 1 st 1 st T 2 nd 1 st T N
102 f1ofn 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T Fn 1 N
103 28 102 syl φ 2 nd 1 st T Fn 1 N
104 103 adantr φ y 0 N 1 2 nd 1 st T Fn 1 N
105 fzss1 y + 1 1 y + 1 N 1 N
106 76 105 syl y 0 N 1 y + 1 N 1 N
107 106 adantl φ y 0 N 1 y + 1 N 1 N
108 eluzp1p1 N 1 y N - 1 + 1 y + 1
109 uzss N - 1 + 1 y + 1 N - 1 + 1 y + 1
110 82 108 109 3syl y 0 N 1 N - 1 + 1 y + 1
111 110 adantl φ y 0 N 1 N - 1 + 1 y + 1
112 1 nnzd φ N
113 112 uzidd φ N N
114 80 fveq2d φ N - 1 + 1 = N
115 113 114 eleqtrrd φ N N - 1 + 1
116 115 adantr φ y 0 N 1 N N - 1 + 1
117 111 116 sseldd φ y 0 N 1 N y + 1
118 eluzfz2 N y + 1 N y + 1 N
119 117 118 syl φ y 0 N 1 N y + 1 N
120 fnfvima 2 nd 1 st T Fn 1 N y + 1 N 1 N N y + 1 N 2 nd 1 st T N 2 nd 1 st T y + 1 N
121 104 107 119 120 syl3anc φ y 0 N 1 2 nd 1 st T N 2 nd 1 st T y + 1 N
122 fvun2 2 nd 1 st T 1 y × 1 Fn 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N × 0 Fn 2 nd 1 st T y + 1 N 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N = 2 nd 1 st T N 2 nd 1 st T y + 1 N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N
123 51 54 122 mp3an12 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N = 2 nd 1 st T N 2 nd 1 st T y + 1 N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N
124 69 121 123 syl2anc φ y 0 N 1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N
125 52 fvconst2 2 nd 1 st T N 2 nd 1 st T y + 1 N 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 0
126 121 125 syl φ y 0 N 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 0
127 124 126 eqtrd φ y 0 N 1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 0
128 127 adantr φ y 0 N 1 2 nd 1 st T N 1 N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 0
129 48 97 99 99 100 101 128 ofval φ y 0 N 1 2 nd 1 st T N 1 N 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 1 st 1 st T 2 nd 1 st T N + 0
130 33 129 mpidan φ y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 1 st 1 st T 2 nd 1 st T N + 0
131 36 nn0cnd φ 1 st 1 st T 2 nd 1 st T N
132 131 addid1d φ 1 st 1 st T 2 nd 1 st T N + 0 = 1 st 1 st T 2 nd 1 st T N
133 132 adantr φ y 0 N 1 1 st 1 st T 2 nd 1 st T N + 0 = 1 st 1 st T 2 nd 1 st T N
134 130 133 eqtrd φ y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 1 st 1 st T 2 nd 1 st T N
135 46 134 sylan9eqr φ y 0 N 1 p = 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 p 2 nd 1 st T N = 1 st 1 st T 2 nd 1 st T N
136 135 adantllr φ p ran F y 0 N 1 p = 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 p 2 nd 1 st T N = 1 st 1 st T 2 nd 1 st T N
137 fveq2 t = T 2 nd t = 2 nd T
138 137 breq2d t = T y < 2 nd t y < 2 nd T
139 138 ifbid t = T if y < 2 nd t y y + 1 = if y < 2 nd T y y + 1
140 2fveq3 t = T 1 st 1 st t = 1 st 1 st T
141 2fveq3 t = T 2 nd 1 st t = 2 nd 1 st T
142 141 imaeq1d t = T 2 nd 1 st t 1 j = 2 nd 1 st T 1 j
143 142 xpeq1d t = T 2 nd 1 st t 1 j × 1 = 2 nd 1 st T 1 j × 1
144 141 imaeq1d t = T 2 nd 1 st t j + 1 N = 2 nd 1 st T j + 1 N
145 144 xpeq1d t = T 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T j + 1 N × 0
146 143 145 uneq12d t = T 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
147 140 146 oveq12d t = T 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
148 139 147 csbeq12dv t = T if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
149 148 mpteq2dv t = T y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
150 149 eqeq2d t = T F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
151 150 2 elrab2 T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
152 151 simprbi T S F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
153 4 152 syl φ F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
154 62 adantl φ y 0 N 1 y
155 peano2zm N N 1
156 112 155 syl φ N 1
157 156 zred φ N 1
158 157 adantr φ y 0 N 1 N 1
159 1 nnred φ N
160 159 adantr φ y 0 N 1 N
161 elfzle2 y 0 N 1 y N 1
162 161 adantl φ y 0 N 1 y N 1
163 159 ltm1d φ N 1 < N
164 163 adantr φ y 0 N 1 N 1 < N
165 154 158 160 162 164 lelttrd φ y 0 N 1 y < N
166 6 adantr φ y 0 N 1 2 nd T = N
167 165 166 breqtrrd φ y 0 N 1 y < 2 nd T
168 167 iftrued φ y 0 N 1 if y < 2 nd T y y + 1 = y
169 168 csbeq1d φ y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = y / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
170 vex y V
171 oveq2 j = y 1 j = 1 y
172 171 imaeq2d j = y 2 nd 1 st T 1 j = 2 nd 1 st T 1 y
173 172 xpeq1d j = y 2 nd 1 st T 1 j × 1 = 2 nd 1 st T 1 y × 1
174 oveq1 j = y j + 1 = y + 1
175 174 oveq1d j = y j + 1 N = y + 1 N
176 175 imaeq2d j = y 2 nd 1 st T j + 1 N = 2 nd 1 st T y + 1 N
177 176 xpeq1d j = y 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T y + 1 N × 0
178 173 177 uneq12d j = y 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
179 178 oveq2d j = y 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
180 170 179 csbie y / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
181 169 180 eqtrdi φ y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
182 181 mpteq2dva φ y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
183 153 182 eqtrd φ F = y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
184 183 rneqd φ ran F = ran y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
185 184 eleq2d φ p ran F p ran y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
186 eqid y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 = y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
187 ovex 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 V
188 186 187 elrnmpti p ran y 0 N 1 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 y 0 N 1 p = 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
189 185 188 bitrdi φ p ran F y 0 N 1 p = 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
190 189 biimpa φ p ran F y 0 N 1 p = 1 st 1 st T + f 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0
191 136 190 r19.29a φ p ran F p 2 nd 1 st T N = 1 st 1 st T 2 nd 1 st T N
192 191 neeq1d φ p ran F p 2 nd 1 st T N 0 1 st 1 st T 2 nd 1 st T N 0
193 192 biimpd φ p ran F p 2 nd 1 st T N 0 1 st 1 st T 2 nd 1 st T N 0
194 193 rexlimdva φ p ran F p 2 nd 1 st T N 0 1 st 1 st T 2 nd 1 st T N 0
195 45 194 mpd φ 1 st 1 st T 2 nd 1 st T N 0
196 elnnne0 1 st 1 st T 2 nd 1 st T N 1 st 1 st T 2 nd 1 st T N 0 1 st 1 st T 2 nd 1 st T N 0
197 36 195 196 sylanbrc φ 1 st 1 st T 2 nd 1 st T N
198 nnm1nn0 1 st 1 st T 2 nd 1 st T N 1 st 1 st T 2 nd 1 st T N 1 0
199 197 198 syl φ 1 st 1 st T 2 nd 1 st T N 1 0
200 elfzo0 1 st 1 st T 2 nd 1 st T N 0 ..^ K 1 st 1 st T 2 nd 1 st T N 0 K 1 st 1 st T 2 nd 1 st T N < K
201 34 200 sylib φ 1 st 1 st T 2 nd 1 st T N 0 K 1 st 1 st T 2 nd 1 st T N < K
202 201 simp2d φ K
203 199 nn0red φ 1 st 1 st T 2 nd 1 st T N 1
204 36 nn0red φ 1 st 1 st T 2 nd 1 st T N
205 202 nnred φ K
206 204 ltm1d φ 1 st 1 st T 2 nd 1 st T N 1 < 1 st 1 st T 2 nd 1 st T N
207 elfzolt2 1 st 1 st T 2 nd 1 st T N 0 ..^ K 1 st 1 st T 2 nd 1 st T N < K
208 34 207 syl φ 1 st 1 st T 2 nd 1 st T N < K
209 203 204 205 206 208 lttrd φ 1 st 1 st T 2 nd 1 st T N 1 < K
210 elfzo0 1 st 1 st T 2 nd 1 st T N 1 0 ..^ K 1 st 1 st T 2 nd 1 st T N 1 0 K 1 st 1 st T 2 nd 1 st T N 1 < K
211 199 202 209 210 syl3anbrc φ 1 st 1 st T 2 nd 1 st T N 1 0 ..^ K
212 211 adantr φ n = 2 nd 1 st T N 1 st 1 st T 2 nd 1 st T N 1 0 ..^ K
213 13 212 eqeltrd φ n = 2 nd 1 st T N 1 st 1 st T n 1 0 ..^ K
214 213 adantlr φ n 1 N n = 2 nd 1 st T N 1 st 1 st T n 1 0 ..^ K
215 22 ffvelrnda φ n 1 N 1 st 1 st T n 0 ..^ K
216 elfzonn0 1 st 1 st T n 0 ..^ K 1 st 1 st T n 0
217 215 216 syl φ n 1 N 1 st 1 st T n 0
218 217 nn0cnd φ n 1 N 1 st 1 st T n
219 218 subid1d φ n 1 N 1 st 1 st T n 0 = 1 st 1 st T n
220 219 215 eqeltrd φ n 1 N 1 st 1 st T n 0 0 ..^ K
221 220 adantr φ n 1 N ¬ n = 2 nd 1 st T N 1 st 1 st T n 0 0 ..^ K
222 8 10 214 221 ifbothda φ n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 0 ..^ K
223 222 fmpttd φ n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 : 1 N 0 ..^ K
224 ovex 0 ..^ K V
225 224 98 elmap n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 0 ..^ K 1 N n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 : 1 N 0 ..^ K
226 223 225 sylibr φ n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 0 ..^ K 1 N
227 simpr φ n 1 + 1 N n 1 + 1 N
228 1z 1
229 peano2z 1 1 + 1
230 228 229 ax-mp 1 + 1
231 112 230 jctil φ 1 + 1 N
232 elfzelz n 1 + 1 N n
233 232 228 jctir n 1 + 1 N n 1
234 fzsubel 1 + 1 N n 1 n 1 + 1 N n 1 1 + 1 - 1 N 1
235 231 233 234 syl2an φ n 1 + 1 N n 1 + 1 N n 1 1 + 1 - 1 N 1
236 227 235 mpbid φ n 1 + 1 N n 1 1 + 1 - 1 N 1
237 ax-1cn 1
238 237 237 pncan3oi 1 + 1 - 1 = 1
239 238 oveq1i 1 + 1 - 1 N 1 = 1 N 1
240 236 239 eleqtrdi φ n 1 + 1 N n 1 1 N 1
241 240 ralrimiva φ n 1 + 1 N n 1 1 N 1
242 simpr φ y 1 N 1 y 1 N 1
243 156 228 jctil φ 1 N 1
244 elfzelz y 1 N 1 y
245 244 228 jctir y 1 N 1 y 1
246 fzaddel 1 N 1 y 1 y 1 N 1 y + 1 1 + 1 N - 1 + 1
247 243 245 246 syl2an φ y 1 N 1 y 1 N 1 y + 1 1 + 1 N - 1 + 1
248 242 247 mpbid φ y 1 N 1 y + 1 1 + 1 N - 1 + 1
249 80 oveq2d φ 1 + 1 N - 1 + 1 = 1 + 1 N
250 249 adantr φ y 1 N 1 1 + 1 N - 1 + 1 = 1 + 1 N
251 248 250 eleqtrd φ y 1 N 1 y + 1 1 + 1 N
252 232 zcnd n 1 + 1 N n
253 244 zcnd y 1 N 1 y
254 subadd2 n 1 y n 1 = y y + 1 = n
255 237 254 mp3an2 n y n 1 = y y + 1 = n
256 eqcom y = n 1 n 1 = y
257 eqcom n = y + 1 y + 1 = n
258 255 256 257 3bitr4g n y y = n 1 n = y + 1
259 252 253 258 syl2anr y 1 N 1 n 1 + 1 N y = n 1 n = y + 1
260 259 ralrimiva y 1 N 1 n 1 + 1 N y = n 1 n = y + 1
261 260 adantl φ y 1 N 1 n 1 + 1 N y = n 1 n = y + 1
262 reu6i y + 1 1 + 1 N n 1 + 1 N y = n 1 n = y + 1 ∃! n 1 + 1 N y = n 1
263 251 261 262 syl2anc φ y 1 N 1 ∃! n 1 + 1 N y = n 1
264 263 ralrimiva φ y 1 N 1 ∃! n 1 + 1 N y = n 1
265 eqid n 1 + 1 N n 1 = n 1 + 1 N n 1
266 265 f1ompt n 1 + 1 N n 1 : 1 + 1 N 1-1 onto 1 N 1 n 1 + 1 N n 1 1 N 1 y 1 N 1 ∃! n 1 + 1 N y = n 1
267 241 264 266 sylanbrc φ n 1 + 1 N n 1 : 1 + 1 N 1-1 onto 1 N 1
268 f1osng 1 V N 1 N : 1 1-1 onto N
269 49 1 268 sylancr φ 1 N : 1 1-1 onto N
270 157 159 ltnled φ N 1 < N ¬ N N 1
271 163 270 mpbid φ ¬ N N 1
272 elfzle2 N 1 N 1 N N 1
273 271 272 nsyl φ ¬ N 1 N 1
274 disjsn 1 N 1 N = ¬ N 1 N 1
275 273 274 sylibr φ 1 N 1 N =
276 1re 1
277 276 ltp1i 1 < 1 + 1
278 230 zrei 1 + 1
279 276 278 ltnlei 1 < 1 + 1 ¬ 1 + 1 1
280 277 279 mpbi ¬ 1 + 1 1
281 elfzle1 1 1 + 1 N 1 + 1 1
282 280 281 mto ¬ 1 1 + 1 N
283 disjsn 1 + 1 N 1 = ¬ 1 1 + 1 N
284 282 283 mpbir 1 + 1 N 1 =
285 f1oun n 1 + 1 N n 1 : 1 + 1 N 1-1 onto 1 N 1 1 N : 1 1-1 onto N 1 + 1 N 1 = 1 N 1 N = n 1 + 1 N n 1 1 N : 1 + 1 N 1 1-1 onto 1 N 1 N
286 284 285 mpanr1 n 1 + 1 N n 1 : 1 + 1 N 1-1 onto 1 N 1 1 N : 1 1-1 onto N 1 N 1 N = n 1 + 1 N n 1 1 N : 1 + 1 N 1 1-1 onto 1 N 1 N
287 267 269 275 286 syl21anc φ n 1 + 1 N n 1 1 N : 1 + 1 N 1 1-1 onto 1 N 1 N
288 eleq1 n = 1 n 1 + 1 N 1 1 + 1 N
289 282 288 mtbiri n = 1 ¬ n 1 + 1 N
290 289 necon2ai n 1 + 1 N n 1
291 ifnefalse n 1 if n = 1 N n 1 = n 1
292 290 291 syl n 1 + 1 N if n = 1 N n 1 = n 1
293 292 mpteq2ia n 1 + 1 N if n = 1 N n 1 = n 1 + 1 N n 1
294 293 uneq1i n 1 + 1 N if n = 1 N n 1 1 N = n 1 + 1 N n 1 1 N
295 49 a1i φ 1 V
296 1 74 eleqtrdi φ N 1
297 fzpred N 1 1 N = 1 1 + 1 N
298 296 297 syl φ 1 N = 1 1 + 1 N
299 uncom 1 1 + 1 N = 1 + 1 N 1
300 298 299 eqtr2di φ 1 + 1 N 1 = 1 N
301 iftrue n = 1 if n = 1 N n 1 = N
302 301 adantl φ n = 1 if n = 1 N n 1 = N
303 295 1 300 302 fmptapd φ n 1 + 1 N if n = 1 N n 1 1 N = n 1 N if n = 1 N n 1
304 294 303 eqtr3id φ n 1 + 1 N n 1 1 N = n 1 N if n = 1 N n 1
305 80 296 eqeltrd φ N - 1 + 1 1
306 uzid N 1 N 1 N 1
307 peano2uz N 1 N 1 N - 1 + 1 N 1
308 156 306 307 3syl φ N - 1 + 1 N 1
309 80 308 eqeltrrd φ N N 1
310 fzsplit2 N - 1 + 1 1 N N 1 1 N = 1 N 1 N - 1 + 1 N
311 305 309 310 syl2anc φ 1 N = 1 N 1 N - 1 + 1 N
312 80 oveq1d φ N - 1 + 1 N = N N
313 fzsn N N N = N
314 112 313 syl φ N N = N
315 312 314 eqtrd φ N - 1 + 1 N = N
316 315 uneq2d φ 1 N 1 N - 1 + 1 N = 1 N 1 N
317 311 316 eqtr2d φ 1 N 1 N = 1 N
318 304 300 317 f1oeq123d φ n 1 + 1 N n 1 1 N : 1 + 1 N 1 1-1 onto 1 N 1 N n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N
319 287 318 mpbid φ n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N
320 f1oco 2 nd 1 st T : 1 N 1-1 onto 1 N n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N 2 nd 1 st T n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N
321 28 319 320 syl2anc φ 2 nd 1 st T n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N
322 98 mptex n 1 N if n = 1 N n 1 V
323 25 322 coex 2 nd 1 st T n 1 N if n = 1 N n 1 V
324 f1oeq1 f = 2 nd 1 st T n 1 N if n = 1 N n 1 f : 1 N 1-1 onto 1 N 2 nd 1 st T n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N
325 323 324 elab 2 nd 1 st T n 1 N if n = 1 N n 1 f | f : 1 N 1-1 onto 1 N 2 nd 1 st T n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N
326 321 325 sylibr φ 2 nd 1 st T n 1 N if n = 1 N n 1 f | f : 1 N 1-1 onto 1 N
327 226 326 opelxpd φ n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
328 1 nnnn0d φ N 0
329 0elfz N 0 0 0 N
330 328 329 syl φ 0 0 N
331 327 330 opelxpd φ n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
332 1 2 3 4 5 6 poimirlem19 φ F = y 0 N 1 n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0
333 elfzle1 y 0 N 1 0 y
334 0re 0
335 lenlt 0 y 0 y ¬ y < 0
336 334 62 335 sylancr y 0 N 1 0 y ¬ y < 0
337 333 336 mpbid y 0 N 1 ¬ y < 0
338 337 iffalsed y 0 N 1 if y < 0 y y + 1 = y + 1
339 338 csbeq1d y 0 N 1 if y < 0 y y + 1 / j n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0 = y + 1 / j n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0
340 ovex y + 1 V
341 oveq2 j = y + 1 1 j = 1 y + 1
342 341 imaeq2d j = y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 j = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1
343 342 xpeq1d j = y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1
344 oveq1 j = y + 1 j + 1 = y + 1 + 1
345 344 oveq1d j = y + 1 j + 1 N = y + 1 + 1 N
346 345 imaeq2d j = y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N = 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N
347 346 xpeq1d j = y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0 = 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0
348 343 347 uneq12d j = y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0
349 348 oveq2d j = y + 1 n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0 = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0
350 340 349 csbie y + 1 / j n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0 = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0
351 339 350 eqtrdi y 0 N 1 if y < 0 y y + 1 / j n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0 = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0
352 351 mpteq2ia y 0 N 1 if y < 0 y y + 1 / j n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0 = y 0 N 1 n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0
353 332 352 eqtr4di φ F = y 0 N 1 if y < 0 y y + 1 / j n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0
354 opex n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 V
355 354 52 op2ndd t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 2 nd t = 0
356 355 breq2d t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 y < 2 nd t y < 0
357 356 ifbid t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 if y < 2 nd t y y + 1 = if y < 0 y y + 1
358 354 52 op1std t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 1 st t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1
359 98 mptex n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 V
360 359 323 op1std 1 st t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 1 st 1 st t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0
361 358 360 syl t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 1 st 1 st t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0
362 359 323 op2ndd 1 st t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 2 nd 1 st t = 2 nd 1 st T n 1 N if n = 1 N n 1
363 358 362 syl t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 2 nd 1 st t = 2 nd 1 st T n 1 N if n = 1 N n 1
364 363 imaeq1d t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 2 nd 1 st t 1 j = 2 nd 1 st T n 1 N if n = 1 N n 1 1 j
365 364 xpeq1d t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 2 nd 1 st t 1 j × 1 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1
366 363 imaeq1d t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 2 nd 1 st t j + 1 N = 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N
367 366 xpeq1d t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0
368 365 367 uneq12d t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0
369 361 368 oveq12d t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0
370 357 369 csbeq12dv t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 0 y y + 1 / j n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0
371 370 mpteq2dv t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = y 0 N 1 if y < 0 y y + 1 / j n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0
372 371 eqeq2d t = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 F = y 0 N 1 if y < 0 y y + 1 / j n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0
373 372 2 elrab2 n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 S n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N F = y 0 N 1 if y < 0 y y + 1 / j n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 + f 2 nd 1 st T n 1 N if n = 1 N n 1 1 j × 1 2 nd 1 st T n 1 N if n = 1 N n 1 j + 1 N × 0
374 331 353 373 sylanbrc φ n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 S
375 354 52 op2ndd T = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 2 nd T = 0
376 375 eqcoms n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 = T 2 nd T = 0
377 1 nnne0d φ N 0
378 377 necomd φ 0 N
379 neeq1 2 nd T = 0 2 nd T N 0 N
380 378 379 syl5ibrcom φ 2 nd T = 0 2 nd T N
381 376 380 syl5 φ n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 = T 2 nd T N
382 381 necon2d φ 2 nd T = N n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 T
383 6 382 mpd φ n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 T
384 neeq1 z = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 z T n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 T
385 384 rspcev n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 S n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 2 nd 1 st T n 1 N if n = 1 N n 1 0 T z S z T
386 374 383 385 syl2anc φ z S z T