Metamath Proof Explorer


Theorem poimirlem19

Description: Lemma for poimir establishing the vertices of the simplex in poimirlem20 . (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 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

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 fveq2 t = T 2 nd t = 2 nd T
8 7 breq2d t = T y < 2 nd t y < 2 nd T
9 8 ifbid t = T if y < 2 nd t y y + 1 = if y < 2 nd T y y + 1
10 2fveq3 t = T 1 st 1 st t = 1 st 1 st T
11 2fveq3 t = T 2 nd 1 st t = 2 nd 1 st T
12 11 imaeq1d t = T 2 nd 1 st t 1 j = 2 nd 1 st T 1 j
13 12 xpeq1d t = T 2 nd 1 st t 1 j × 1 = 2 nd 1 st T 1 j × 1
14 11 imaeq1d t = T 2 nd 1 st t j + 1 N = 2 nd 1 st T j + 1 N
15 14 xpeq1d t = T 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T j + 1 N × 0
16 13 15 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
17 10 16 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
18 9 17 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
19 18 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
20 19 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
21 20 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
22 21 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
23 4 22 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
24 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
25 24 2 eleq2s T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
26 4 25 syl φ T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
27 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
28 26 27 syl φ 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
29 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
30 28 29 syl φ 1 st 1 st T 0 ..^ K 1 N
31 elmapfn 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T Fn 1 N
32 30 31 syl φ 1 st 1 st T Fn 1 N
33 32 adantr φ y 0 N 1 1 st 1 st T Fn 1 N
34 1ex 1 V
35 fnconstg 1 V 2 nd 1 st T 1 y × 1 Fn 2 nd 1 st T 1 y
36 34 35 ax-mp 2 nd 1 st T 1 y × 1 Fn 2 nd 1 st T 1 y
37 c0ex 0 V
38 fnconstg 0 V 2 nd 1 st T y + 1 N × 0 Fn 2 nd 1 st T y + 1 N
39 37 38 ax-mp 2 nd 1 st T y + 1 N × 0 Fn 2 nd 1 st T y + 1 N
40 36 39 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
41 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
42 28 41 syl φ 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
43 fvex 2 nd 1 st T V
44 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
45 43 44 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
46 42 45 sylib φ 2 nd 1 st T : 1 N 1-1 onto 1 N
47 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
48 47 simprbi 2 nd 1 st T : 1 N 1-1 onto 1 N Fun 2 nd 1 st T -1
49 46 48 syl φ Fun 2 nd 1 st T -1
50 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
51 49 50 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
52 elfznn0 y 0 N 1 y 0
53 52 nn0red y 0 N 1 y
54 53 ltp1d y 0 N 1 y < y + 1
55 fzdisj y < y + 1 1 y y + 1 N =
56 54 55 syl y 0 N 1 1 y y + 1 N =
57 56 imaeq2d y 0 N 1 2 nd 1 st T 1 y y + 1 N = 2 nd 1 st T
58 ima0 2 nd 1 st T =
59 57 58 eqtrdi y 0 N 1 2 nd 1 st T 1 y y + 1 N =
60 51 59 sylan9req φ y 0 N 1 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N =
61 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
62 40 60 61 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
63 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
64 nn0p1nn y 0 y + 1
65 52 64 syl y 0 N 1 y + 1
66 nnuz = 1
67 65 66 eleqtrdi y 0 N 1 y + 1 1
68 67 adantl φ y 0 N 1 y + 1 1
69 1 nncnd φ N
70 npcan1 N N - 1 + 1 = N
71 69 70 syl φ N - 1 + 1 = N
72 71 adantr φ y 0 N 1 N - 1 + 1 = N
73 elfzuz3 y 0 N 1 N 1 y
74 peano2uz N 1 y N - 1 + 1 y
75 73 74 syl y 0 N 1 N - 1 + 1 y
76 75 adantl φ y 0 N 1 N - 1 + 1 y
77 72 76 eqeltrrd φ y 0 N 1 N y
78 fzsplit2 y + 1 1 N y 1 N = 1 y y + 1 N
79 68 77 78 syl2anc φ y 0 N 1 1 N = 1 y y + 1 N
80 79 imaeq2d φ y 0 N 1 2 nd 1 st T 1 N = 2 nd 1 st T 1 y y + 1 N
81 f1ofo 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N
82 foima 2 nd 1 st T : 1 N onto 1 N 2 nd 1 st T 1 N = 1 N
83 46 81 82 3syl φ 2 nd 1 st T 1 N = 1 N
84 83 adantr φ y 0 N 1 2 nd 1 st T 1 N = 1 N
85 80 84 eqtr3d φ y 0 N 1 2 nd 1 st T 1 y y + 1 N = 1 N
86 63 85 eqtr3id φ y 0 N 1 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N = 1 N
87 86 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
88 62 87 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
89 ovexd φ y 0 N 1 1 N V
90 inidm 1 N 1 N = 1 N
91 eqidd φ y 0 N 1 n 1 N 1 st 1 st T n = 1 st 1 st T n
92 eqidd φ y 0 N 1 n 1 N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
93 33 88 89 89 90 91 92 offval φ 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 = n 1 N 1 st 1 st T n + 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
94 elmapi 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T : 1 N 0 ..^ K
95 30 94 syl φ 1 st 1 st T : 1 N 0 ..^ K
96 95 ffvelrnda φ n 1 N 1 st 1 st T n 0 ..^ K
97 elfzonn0 1 st 1 st T n 0 ..^ K 1 st 1 st T n 0
98 96 97 syl φ n 1 N 1 st 1 st T n 0
99 98 nn0cnd φ n 1 N 1 st 1 st T n
100 99 adantlr φ y 0 N 1 n 1 N 1 st 1 st T n
101 ax-1cn 1
102 0cn 0
103 101 102 ifcli if n = 2 nd 1 st T N 1 0
104 103 a1i φ y 0 N 1 n 1 N if n = 2 nd 1 st T N 1 0
105 snssi 1 1
106 101 105 ax-mp 1
107 snssi 0 0
108 102 107 ax-mp 0
109 106 108 unssi 1 0
110 34 fconst 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 1 y + 1 1
111 37 fconst 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 : 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N 0
112 110 111 pm3.2i 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 1 y + 1 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 : 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N 0
113 simpr φ n 1 + 1 N n 1 + 1 N
114 1 nnzd φ N
115 1z 1
116 peano2z 1 1 + 1
117 115 116 ax-mp 1 + 1
118 114 117 jctil φ 1 + 1 N
119 elfzelz n 1 + 1 N n
120 119 115 jctir n 1 + 1 N n 1
121 fzsubel 1 + 1 N n 1 n 1 + 1 N n 1 1 + 1 - 1 N 1
122 118 120 121 syl2an φ n 1 + 1 N n 1 + 1 N n 1 1 + 1 - 1 N 1
123 113 122 mpbid φ n 1 + 1 N n 1 1 + 1 - 1 N 1
124 101 101 pncan3oi 1 + 1 - 1 = 1
125 124 oveq1i 1 + 1 - 1 N 1 = 1 N 1
126 123 125 eleqtrdi φ n 1 + 1 N n 1 1 N 1
127 126 ralrimiva φ n 1 + 1 N n 1 1 N 1
128 simpr φ y 1 N 1 y 1 N 1
129 peano2zm N N 1
130 114 129 syl φ N 1
131 130 115 jctil φ 1 N 1
132 elfzelz y 1 N 1 y
133 132 115 jctir y 1 N 1 y 1
134 fzaddel 1 N 1 y 1 y 1 N 1 y + 1 1 + 1 N - 1 + 1
135 131 133 134 syl2an φ y 1 N 1 y 1 N 1 y + 1 1 + 1 N - 1 + 1
136 128 135 mpbid φ y 1 N 1 y + 1 1 + 1 N - 1 + 1
137 71 oveq2d φ 1 + 1 N - 1 + 1 = 1 + 1 N
138 137 adantr φ y 1 N 1 1 + 1 N - 1 + 1 = 1 + 1 N
139 136 138 eleqtrd φ y 1 N 1 y + 1 1 + 1 N
140 119 zcnd n 1 + 1 N n
141 132 zcnd y 1 N 1 y
142 subadd2 n 1 y n 1 = y y + 1 = n
143 101 142 mp3an2 n y n 1 = y y + 1 = n
144 eqcom y = n 1 n 1 = y
145 eqcom n = y + 1 y + 1 = n
146 143 144 145 3bitr4g n y y = n 1 n = y + 1
147 140 141 146 syl2anr y 1 N 1 n 1 + 1 N y = n 1 n = y + 1
148 147 ralrimiva y 1 N 1 n 1 + 1 N y = n 1 n = y + 1
149 148 adantl φ y 1 N 1 n 1 + 1 N y = n 1 n = y + 1
150 reu6i y + 1 1 + 1 N n 1 + 1 N y = n 1 n = y + 1 ∃! n 1 + 1 N y = n 1
151 139 149 150 syl2anc φ y 1 N 1 ∃! n 1 + 1 N y = n 1
152 151 ralrimiva φ y 1 N 1 ∃! n 1 + 1 N y = n 1
153 eqid n 1 + 1 N n 1 = n 1 + 1 N n 1
154 153 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
155 127 152 154 sylanbrc φ n 1 + 1 N n 1 : 1 + 1 N 1-1 onto 1 N 1
156 f1osng 1 V N 1 N : 1 1-1 onto N
157 34 1 156 sylancr φ 1 N : 1 1-1 onto N
158 1 nnred φ N
159 158 ltm1d φ N 1 < N
160 130 zred φ N 1
161 160 158 ltnled φ N 1 < N ¬ N N 1
162 159 161 mpbid φ ¬ N N 1
163 elfzle2 N 1 N 1 N N 1
164 162 163 nsyl φ ¬ N 1 N 1
165 disjsn 1 N 1 N = ¬ N 1 N 1
166 164 165 sylibr φ 1 N 1 N =
167 1re 1
168 167 ltp1i 1 < 1 + 1
169 117 zrei 1 + 1
170 167 169 ltnlei 1 < 1 + 1 ¬ 1 + 1 1
171 168 170 mpbi ¬ 1 + 1 1
172 elfzle1 1 1 + 1 N 1 + 1 1
173 171 172 mto ¬ 1 1 + 1 N
174 disjsn 1 + 1 N 1 = ¬ 1 1 + 1 N
175 173 174 mpbir 1 + 1 N 1 =
176 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
177 175 176 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
178 155 157 166 177 syl21anc φ n 1 + 1 N n 1 1 N : 1 + 1 N 1 1-1 onto 1 N 1 N
179 eleq1 n = 1 n 1 + 1 N 1 1 + 1 N
180 173 179 mtbiri n = 1 ¬ n 1 + 1 N
181 180 necon2ai n 1 + 1 N n 1
182 ifnefalse n 1 if n = 1 N n 1 = n 1
183 181 182 syl n 1 + 1 N if n = 1 N n 1 = n 1
184 183 mpteq2ia n 1 + 1 N if n = 1 N n 1 = n 1 + 1 N n 1
185 184 uneq1i n 1 + 1 N if n = 1 N n 1 1 N = n 1 + 1 N n 1 1 N
186 34 a1i φ 1 V
187 1 66 eleqtrdi φ N 1
188 fzpred N 1 1 N = 1 1 + 1 N
189 187 188 syl φ 1 N = 1 1 + 1 N
190 uncom 1 1 + 1 N = 1 + 1 N 1
191 189 190 eqtr2di φ 1 + 1 N 1 = 1 N
192 iftrue n = 1 if n = 1 N n 1 = N
193 192 adantl φ n = 1 if n = 1 N n 1 = N
194 186 1 191 193 fmptapd φ n 1 + 1 N if n = 1 N n 1 1 N = n 1 N if n = 1 N n 1
195 185 194 eqtr3id φ n 1 + 1 N n 1 1 N = n 1 N if n = 1 N n 1
196 71 187 eqeltrd φ N - 1 + 1 1
197 uzid N 1 N 1 N 1
198 peano2uz N 1 N 1 N - 1 + 1 N 1
199 130 197 198 3syl φ N - 1 + 1 N 1
200 71 199 eqeltrrd φ N N 1
201 fzsplit2 N - 1 + 1 1 N N 1 1 N = 1 N 1 N - 1 + 1 N
202 196 200 201 syl2anc φ 1 N = 1 N 1 N - 1 + 1 N
203 71 oveq1d φ N - 1 + 1 N = N N
204 fzsn N N N = N
205 114 204 syl φ N N = N
206 203 205 eqtrd φ N - 1 + 1 N = N
207 206 uneq2d φ 1 N 1 N - 1 + 1 N = 1 N 1 N
208 202 207 eqtr2d φ 1 N 1 N = 1 N
209 195 191 208 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
210 178 209 mpbid φ n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N
211 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
212 46 210 211 syl2anc φ 2 nd 1 st T n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N
213 dff1o3 2 nd 1 st T 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 onto 1 N Fun 2 nd 1 st T n 1 N if n = 1 N n 1 -1
214 213 simprbi 2 nd 1 st T n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N Fun 2 nd 1 st T n 1 N if n = 1 N n 1 -1
215 imain Fun 2 nd 1 st T n 1 N if n = 1 N n 1 -1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 y + 1 + 1 N = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N
216 212 214 215 3syl φ 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 y + 1 + 1 N = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N
217 65 nnred y 0 N 1 y + 1
218 217 ltp1d y 0 N 1 y + 1 < y + 1 + 1
219 fzdisj y + 1 < y + 1 + 1 1 y + 1 y + 1 + 1 N =
220 218 219 syl y 0 N 1 1 y + 1 y + 1 + 1 N =
221 220 imaeq2d y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 y + 1 + 1 N = 2 nd 1 st T n 1 N if n = 1 N n 1
222 ima0 2 nd 1 st T n 1 N if n = 1 N n 1 =
223 221 222 eqtrdi y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 y + 1 + 1 N =
224 216 223 sylan9req φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N =
225 fun 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 1 y + 1 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 : 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N 0 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N = 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 : 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N 1 0
226 112 224 225 sylancr φ y 0 N 1 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 : 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N 1 0
227 imaundi 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 y + 1 + 1 N = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N
228 65 peano2nnd y 0 N 1 y + 1 + 1
229 228 66 eleqtrdi y 0 N 1 y + 1 + 1 1
230 229 adantl φ y 0 N 1 y + 1 + 1 1
231 eluzp1p1 N 1 y N - 1 + 1 y + 1
232 73 231 syl y 0 N 1 N - 1 + 1 y + 1
233 232 adantl φ y 0 N 1 N - 1 + 1 y + 1
234 72 233 eqeltrrd φ y 0 N 1 N y + 1
235 fzsplit2 y + 1 + 1 1 N y + 1 1 N = 1 y + 1 y + 1 + 1 N
236 230 234 235 syl2anc φ y 0 N 1 1 N = 1 y + 1 y + 1 + 1 N
237 236 imaeq2d φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 N = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 y + 1 + 1 N
238 f1ofo 2 nd 1 st T 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 onto 1 N
239 foima 2 nd 1 st T n 1 N if n = 1 N n 1 : 1 N onto 1 N 2 nd 1 st T n 1 N if n = 1 N n 1 1 N = 1 N
240 212 238 239 3syl φ 2 nd 1 st T n 1 N if n = 1 N n 1 1 N = 1 N
241 240 adantr φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 N = 1 N
242 237 241 eqtr3d φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 y + 1 + 1 N = 1 N
243 227 242 eqtr3id φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N = 1 N
244 243 feq2d φ y 0 N 1 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 : 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N 1 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 : 1 N 1 0
245 226 244 mpbid φ y 0 N 1 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 : 1 N 1 0
246 245 ffvelrnda φ y 0 N 1 n 1 N 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 n 1 0
247 109 246 sseldi φ y 0 N 1 n 1 N 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 n
248 100 104 247 subadd23d φ y 0 N 1 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 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 n = 1 st 1 st T n + 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 n - if n = 2 nd 1 st T N 1 0
249 oveq2 1 = 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 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 n 1 = 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 n if n = 2 nd 1 st T N 1 0
250 249 eqeq1d 1 = 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 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 n 1 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n 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 n if n = 2 nd 1 st T N 1 0 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
251 oveq2 0 = 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 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 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 n if n = 2 nd 1 st T N 1 0
252 251 eqeq1d 0 = 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 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 n 0 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n 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 n if n = 2 nd 1 st T N 1 0 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
253 1m1e0 1 1 = 0
254 f1ofn 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T Fn 1 N
255 46 254 syl φ 2 nd 1 st T Fn 1 N
256 255 adantr φ y 0 N 1 2 nd 1 st T Fn 1 N
257 imassrn n 1 N if n = 1 N n 1 1 y + 1 ran n 1 N if n = 1 N n 1
258 f1of n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N n 1 N if n = 1 N n 1 : 1 N 1 N
259 210 258 syl φ n 1 N if n = 1 N n 1 : 1 N 1 N
260 259 frnd φ ran n 1 N if n = 1 N n 1 1 N
261 257 260 sstrid φ n 1 N if n = 1 N n 1 1 y + 1 1 N
262 261 adantr φ y 0 N 1 n 1 N if n = 1 N n 1 1 y + 1 1 N
263 eqidd φ n 1 N if n = 1 N n 1 = n 1 N if n = 1 N n 1
264 eluzfz1 N 1 1 1 N
265 187 264 syl φ 1 1 N
266 263 193 265 1 fvmptd φ n 1 N if n = 1 N n 1 1 = N
267 266 adantr φ y 0 N 1 n 1 N if n = 1 N n 1 1 = N
268 f1ofn n 1 N if n = 1 N n 1 : 1 N 1-1 onto 1 N n 1 N if n = 1 N n 1 Fn 1 N
269 210 268 syl φ n 1 N if n = 1 N n 1 Fn 1 N
270 269 adantr φ y 0 N 1 n 1 N if n = 1 N n 1 Fn 1 N
271 fzss2 N y + 1 1 y + 1 1 N
272 234 271 syl φ y 0 N 1 1 y + 1 1 N
273 eluzfz1 y + 1 1 1 1 y + 1
274 67 273 syl y 0 N 1 1 1 y + 1
275 274 adantl φ y 0 N 1 1 1 y + 1
276 fnfvima n 1 N if n = 1 N n 1 Fn 1 N 1 y + 1 1 N 1 1 y + 1 n 1 N if n = 1 N n 1 1 n 1 N if n = 1 N n 1 1 y + 1
277 270 272 275 276 syl3anc φ y 0 N 1 n 1 N if n = 1 N n 1 1 n 1 N if n = 1 N n 1 1 y + 1
278 267 277 eqeltrrd φ y 0 N 1 N n 1 N if n = 1 N n 1 1 y + 1
279 fnfvima 2 nd 1 st T Fn 1 N n 1 N if n = 1 N n 1 1 y + 1 1 N N n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T N 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1
280 256 262 278 279 syl3anc φ y 0 N 1 2 nd 1 st T N 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1
281 imaco 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1
282 280 281 eleqtrrdi φ y 0 N 1 2 nd 1 st T N 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1
283 fnconstg 1 V 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 Fn 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1
284 34 283 ax-mp 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 Fn 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1
285 fnconstg 0 V 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 Fn 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N
286 37 285 ax-mp 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 Fn 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N
287 fvun1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 Fn 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 Fn 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N = 2 nd 1 st T N 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 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 2 nd 1 st T N = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 2 nd 1 st T N
288 284 286 287 mp3an12 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N = 2 nd 1 st T N 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 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 2 nd 1 st T N = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 2 nd 1 st T N
289 224 282 288 syl2anc φ y 0 N 1 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 2 nd 1 st T N = 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 2 nd 1 st T N
290 34 fvconst2 2 nd 1 st T N 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 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
291 282 290 syl φ y 0 N 1 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
292 289 291 eqtrd φ y 0 N 1 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 2 nd 1 st T N = 1
293 292 oveq1d φ y 0 N 1 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 2 nd 1 st T N 1 = 1 1
294 fzss1 y + 1 1 y + 1 N 1 N
295 67 294 syl y 0 N 1 y + 1 N 1 N
296 295 adantl φ y 0 N 1 y + 1 N 1 N
297 eluzfz2 N y + 1 N y + 1 N
298 234 297 syl φ y 0 N 1 N y + 1 N
299 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
300 256 296 298 299 syl3anc φ y 0 N 1 2 nd 1 st T N 2 nd 1 st T y + 1 N
301 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
302 36 39 301 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
303 60 300 302 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
304 37 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
305 300 304 syl φ y 0 N 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N = 0
306 303 305 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
307 253 293 306 3eqtr4a φ y 0 N 1 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 2 nd 1 st T 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
308 fveq2 n = 2 nd 1 st T N 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 n = 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 2 nd 1 st T N
309 308 oveq1d n = 2 nd 1 st T N 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 n 1 = 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 2 nd 1 st T N 1
310 fveq2 n = 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 2 nd 1 st T N
311 309 310 eqeq12d n = 2 nd 1 st T N 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 n 1 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n 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 2 nd 1 st T 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
312 307 311 syl5ibrcom φ y 0 N 1 n = 2 nd 1 st T N 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 n 1 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
313 312 imp φ y 0 N 1 n = 2 nd 1 st T N 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 n 1 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
314 313 adantlr φ y 0 N 1 n 1 N n = 2 nd 1 st T N 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 n 1 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
315 247 subid1d φ y 0 N 1 n 1 N 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 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 n
316 315 adantr φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T N 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 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 n
317 eldifsn n 1 N 2 nd 1 st T N n 1 N n 2 nd 1 st T N
318 df-ne n 2 nd 1 st T N ¬ n = 2 nd 1 st T N
319 318 anbi2i n 1 N n 2 nd 1 st T N n 1 N ¬ n = 2 nd 1 st T N
320 317 319 bitri n 1 N 2 nd 1 st T N n 1 N ¬ n = 2 nd 1 st T N
321 fnconstg 0 V 2 nd 1 st T y + 1 N 1 × 0 Fn 2 nd 1 st T y + 1 N 1
322 37 321 ax-mp 2 nd 1 st T y + 1 N 1 × 0 Fn 2 nd 1 st T y + 1 N 1
323 36 322 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 1 × 0 Fn 2 nd 1 st T y + 1 N 1
324 imain Fun 2 nd 1 st T -1 2 nd 1 st T 1 y y + 1 N 1 = 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N 1
325 49 324 syl φ 2 nd 1 st T 1 y y + 1 N 1 = 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N 1
326 fzdisj y < y + 1 1 y y + 1 N 1 =
327 54 326 syl y 0 N 1 1 y y + 1 N 1 =
328 327 imaeq2d y 0 N 1 2 nd 1 st T 1 y y + 1 N 1 = 2 nd 1 st T
329 328 58 eqtrdi y 0 N 1 2 nd 1 st T 1 y y + 1 N 1 =
330 325 329 sylan9req φ y 0 N 1 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N 1 =
331 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 1 × 0 Fn 2 nd 1 st T y + 1 N 1 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N 1 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N 1
332 323 330 331 sylancr φ y 0 N 1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N 1
333 imaundi 2 nd 1 st T 1 y y + 1 N 1 = 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N 1
334 202 207 eqtrd φ 1 N = 1 N 1 N
335 334 difeq1d φ 1 N N = 1 N 1 N N
336 difun2 1 N 1 N N = 1 N 1 N
337 335 336 eqtrdi φ 1 N N = 1 N 1 N
338 difsn ¬ N 1 N 1 1 N 1 N = 1 N 1
339 164 338 syl φ 1 N 1 N = 1 N 1
340 337 339 eqtrd φ 1 N N = 1 N 1
341 340 adantr φ y 0 N 1 1 N N = 1 N 1
342 73 adantl φ y 0 N 1 N 1 y
343 fzsplit2 y + 1 1 N 1 y 1 N 1 = 1 y y + 1 N 1
344 68 342 343 syl2anc φ y 0 N 1 1 N 1 = 1 y y + 1 N 1
345 341 344 eqtrd φ y 0 N 1 1 N N = 1 y y + 1 N 1
346 345 imaeq2d φ y 0 N 1 2 nd 1 st T 1 N N = 2 nd 1 st T 1 y y + 1 N 1
347 imadif Fun 2 nd 1 st T -1 2 nd 1 st T 1 N N = 2 nd 1 st T 1 N 2 nd 1 st T N
348 49 347 syl φ 2 nd 1 st T 1 N N = 2 nd 1 st T 1 N 2 nd 1 st T N
349 elfz1end N N 1 N
350 1 349 sylib φ N 1 N
351 fnsnfv 2 nd 1 st T Fn 1 N N 1 N 2 nd 1 st T N = 2 nd 1 st T N
352 255 350 351 syl2anc φ 2 nd 1 st T N = 2 nd 1 st T N
353 352 eqcomd φ 2 nd 1 st T N = 2 nd 1 st T N
354 83 353 difeq12d φ 2 nd 1 st T 1 N 2 nd 1 st T N = 1 N 2 nd 1 st T N
355 348 354 eqtrd φ 2 nd 1 st T 1 N N = 1 N 2 nd 1 st T N
356 355 adantr φ y 0 N 1 2 nd 1 st T 1 N N = 1 N 2 nd 1 st T N
357 346 356 eqtr3d φ y 0 N 1 2 nd 1 st T 1 y y + 1 N 1 = 1 N 2 nd 1 st T N
358 333 357 eqtr3id φ y 0 N 1 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N 1 = 1 N 2 nd 1 st T N
359 358 fneq2d φ y 0 N 1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 2 nd 1 st T 1 y 2 nd 1 st T y + 1 N 1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 1 N 2 nd 1 st T N
360 332 359 mpbid φ y 0 N 1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 1 N 2 nd 1 st T N
361 disjdifr 1 N 2 nd 1 st T N 2 nd 1 st T N =
362 fnconstg 1 V 2 nd 1 st T N × 1 Fn 2 nd 1 st T N
363 34 362 ax-mp 2 nd 1 st T N × 1 Fn 2 nd 1 st T N
364 fvun1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 1 N 2 nd 1 st T N 2 nd 1 st T N × 1 Fn 2 nd 1 st T N 1 N 2 nd 1 st T N 2 nd 1 st T N = n 1 N 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 n
365 363 364 mp3an2 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 1 N 2 nd 1 st T N 1 N 2 nd 1 st T N 2 nd 1 st T N = n 1 N 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 n
366 fnconstg 0 V 2 nd 1 st T N × 0 Fn 2 nd 1 st T N
367 37 366 ax-mp 2 nd 1 st T N × 0 Fn 2 nd 1 st T N
368 fvun1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 1 N 2 nd 1 st T N 2 nd 1 st T N × 0 Fn 2 nd 1 st T N 1 N 2 nd 1 st T N 2 nd 1 st T N = n 1 N 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 n
369 367 368 mp3an2 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 1 N 2 nd 1 st T N 1 N 2 nd 1 st T N 2 nd 1 st T N = n 1 N 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 n
370 365 369 eqtr4d 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 1 N 2 nd 1 st T N 1 N 2 nd 1 st T N 2 nd 1 st T N = n 1 N 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0 n
371 361 370 mpanr1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 Fn 1 N 2 nd 1 st T N n 1 N 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0 n
372 360 371 sylan φ y 0 N 1 n 1 N 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0 n
373 320 372 sylan2br φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0 n
374 373 anassrs φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0 n
375 imaundi 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1 1 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 1
376 imaco 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1
377 imaco 2 nd 1 st T n 1 N if n = 1 N n 1 1 = 2 nd 1 st T n 1 N if n = 1 N n 1 1
378 376 377 uneq12i 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 1
379 375 378 eqtri 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1 1 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 1
380 fzpred y + 1 1 1 y + 1 = 1 1 + 1 y + 1
381 67 380 syl y 0 N 1 1 y + 1 = 1 1 + 1 y + 1
382 uncom 1 1 + 1 y + 1 = 1 + 1 y + 1 1
383 381 382 eqtrdi y 0 N 1 1 y + 1 = 1 + 1 y + 1 1
384 383 imaeq2d y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1 1
385 384 adantl φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 = 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1 1
386 elfzelz y 0 N 1 y
387 124 a1i y 1 + 1 - 1 = 1
388 zcn y y
389 pncan1 y y + 1 - 1 = y
390 388 389 syl y y + 1 - 1 = y
391 387 390 oveq12d y 1 + 1 - 1 y + 1 - 1 = 1 y
392 elfzelz j 1 + 1 - 1 y + 1 - 1 j
393 392 zcnd j 1 + 1 - 1 y + 1 - 1 j
394 pncan1 j j + 1 - 1 = j
395 393 394 syl j 1 + 1 - 1 y + 1 - 1 j + 1 - 1 = j
396 395 eleq1d j 1 + 1 - 1 y + 1 - 1 j + 1 - 1 1 + 1 - 1 y + 1 - 1 j 1 + 1 - 1 y + 1 - 1
397 396 ibir j 1 + 1 - 1 y + 1 - 1 j + 1 - 1 1 + 1 - 1 y + 1 - 1
398 397 adantl y j 1 + 1 - 1 y + 1 - 1 j + 1 - 1 1 + 1 - 1 y + 1 - 1
399 peano2z y y + 1
400 399 117 jctil y 1 + 1 y + 1
401 392 peano2zd j 1 + 1 - 1 y + 1 - 1 j + 1
402 401 115 jctir j 1 + 1 - 1 y + 1 - 1 j + 1 1
403 fzsubel 1 + 1 y + 1 j + 1 1 j + 1 1 + 1 y + 1 j + 1 - 1 1 + 1 - 1 y + 1 - 1
404 400 402 403 syl2an y j 1 + 1 - 1 y + 1 - 1 j + 1 1 + 1 y + 1 j + 1 - 1 1 + 1 - 1 y + 1 - 1
405 398 404 mpbird y j 1 + 1 - 1 y + 1 - 1 j + 1 1 + 1 y + 1
406 395 eqcomd j 1 + 1 - 1 y + 1 - 1 j = j + 1 - 1
407 406 adantl y j 1 + 1 - 1 y + 1 - 1 j = j + 1 - 1
408 oveq1 n = j + 1 n 1 = j + 1 - 1
409 408 rspceeqv j + 1 1 + 1 y + 1 j = j + 1 - 1 n 1 + 1 y + 1 j = n 1
410 405 407 409 syl2anc y j 1 + 1 - 1 y + 1 - 1 n 1 + 1 y + 1 j = n 1
411 410 ex y j 1 + 1 - 1 y + 1 - 1 n 1 + 1 y + 1 j = n 1
412 simpr y n 1 + 1 y + 1 n 1 + 1 y + 1
413 elfzelz n 1 + 1 y + 1 n
414 413 115 jctir n 1 + 1 y + 1 n 1
415 fzsubel 1 + 1 y + 1 n 1 n 1 + 1 y + 1 n 1 1 + 1 - 1 y + 1 - 1
416 400 414 415 syl2an y n 1 + 1 y + 1 n 1 + 1 y + 1 n 1 1 + 1 - 1 y + 1 - 1
417 412 416 mpbid y n 1 + 1 y + 1 n 1 1 + 1 - 1 y + 1 - 1
418 eleq1 j = n 1 j 1 + 1 - 1 y + 1 - 1 n 1 1 + 1 - 1 y + 1 - 1
419 417 418 syl5ibrcom y n 1 + 1 y + 1 j = n 1 j 1 + 1 - 1 y + 1 - 1
420 419 rexlimdva y n 1 + 1 y + 1 j = n 1 j 1 + 1 - 1 y + 1 - 1
421 411 420 impbid y j 1 + 1 - 1 y + 1 - 1 n 1 + 1 y + 1 j = n 1
422 eqid n 1 + 1 y + 1 n 1 = n 1 + 1 y + 1 n 1
423 422 elrnmpt j V j ran n 1 + 1 y + 1 n 1 n 1 + 1 y + 1 j = n 1
424 423 elv j ran n 1 + 1 y + 1 n 1 n 1 + 1 y + 1 j = n 1
425 421 424 bitr4di y j 1 + 1 - 1 y + 1 - 1 j ran n 1 + 1 y + 1 n 1
426 425 eqrdv y 1 + 1 - 1 y + 1 - 1 = ran n 1 + 1 y + 1 n 1
427 391 426 eqtr3d y 1 y = ran n 1 + 1 y + 1 n 1
428 386 427 syl y 0 N 1 1 y = ran n 1 + 1 y + 1 n 1
429 428 adantl φ y 0 N 1 1 y = ran n 1 + 1 y + 1 n 1
430 df-ima n 1 N if n = 1 N n 1 1 + 1 y + 1 = ran n 1 N if n = 1 N n 1 1 + 1 y + 1
431 uzid 1 1 1
432 peano2uz 1 1 1 + 1 1
433 115 431 432 mp2b 1 + 1 1
434 fzss1 1 + 1 1 1 + 1 y + 1 1 y + 1
435 433 434 ax-mp 1 + 1 y + 1 1 y + 1
436 435 272 sstrid φ y 0 N 1 1 + 1 y + 1 1 N
437 436 resmptd φ y 0 N 1 n 1 N if n = 1 N n 1 1 + 1 y + 1 = n 1 + 1 y + 1 if n = 1 N n 1
438 elfzle1 1 1 + 1 y + 1 1 + 1 1
439 171 438 mto ¬ 1 1 + 1 y + 1
440 eleq1 n = 1 n 1 + 1 y + 1 1 1 + 1 y + 1
441 439 440 mtbiri n = 1 ¬ n 1 + 1 y + 1
442 441 necon2ai n 1 + 1 y + 1 n 1
443 442 182 syl n 1 + 1 y + 1 if n = 1 N n 1 = n 1
444 443 mpteq2ia n 1 + 1 y + 1 if n = 1 N n 1 = n 1 + 1 y + 1 n 1
445 437 444 eqtrdi φ y 0 N 1 n 1 N if n = 1 N n 1 1 + 1 y + 1 = n 1 + 1 y + 1 n 1
446 445 rneqd φ y 0 N 1 ran n 1 N if n = 1 N n 1 1 + 1 y + 1 = ran n 1 + 1 y + 1 n 1
447 430 446 syl5eq φ y 0 N 1 n 1 N if n = 1 N n 1 1 + 1 y + 1 = ran n 1 + 1 y + 1 n 1
448 429 447 eqtr4d φ y 0 N 1 1 y = n 1 N if n = 1 N n 1 1 + 1 y + 1
449 448 imaeq2d φ y 0 N 1 2 nd 1 st T 1 y = 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1
450 266 sneqd φ n 1 N if n = 1 N n 1 1 = N
451 fnsnfv n 1 N if n = 1 N n 1 Fn 1 N 1 1 N n 1 N if n = 1 N n 1 1 = n 1 N if n = 1 N n 1 1
452 269 265 451 syl2anc φ n 1 N if n = 1 N n 1 1 = n 1 N if n = 1 N n 1 1
453 450 452 eqtr3d φ N = n 1 N if n = 1 N n 1 1
454 453 imaeq2d φ 2 nd 1 st T N = 2 nd 1 st T n 1 N if n = 1 N n 1 1
455 352 454 eqtrd φ 2 nd 1 st T N = 2 nd 1 st T n 1 N if n = 1 N n 1 1
456 455 adantr φ y 0 N 1 2 nd 1 st T N = 2 nd 1 st T n 1 N if n = 1 N n 1 1
457 449 456 uneq12d φ y 0 N 1 2 nd 1 st T 1 y 2 nd 1 st T N = 2 nd 1 st T n 1 N if n = 1 N n 1 1 + 1 y + 1 2 nd 1 st T n 1 N if n = 1 N n 1 1
458 379 385 457 3eqtr4a φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 = 2 nd 1 st T 1 y 2 nd 1 st T N
459 458 xpeq1d φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 = 2 nd 1 st T 1 y 2 nd 1 st T N × 1
460 xpundir 2 nd 1 st T 1 y 2 nd 1 st T N × 1 = 2 nd 1 st T 1 y × 1 2 nd 1 st T N × 1
461 459 460 eqtrdi φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1 = 2 nd 1 st T 1 y × 1 2 nd 1 st T N × 1
462 imaco 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N = 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N
463 df-ima n 1 N if n = 1 N n 1 y + 1 + 1 N = ran n 1 N if n = 1 N n 1 y + 1 + 1 N
464 fzss1 y + 1 + 1 1 y + 1 + 1 N 1 N
465 230 464 syl φ y 0 N 1 y + 1 + 1 N 1 N
466 465 resmptd φ y 0 N 1 n 1 N if n = 1 N n 1 y + 1 + 1 N = n y + 1 + 1 N if n = 1 N n 1
467 1red y 0 N 1 1
468 65 nnzd y 0 N 1 y + 1
469 468 peano2zd y 0 N 1 y + 1 + 1
470 469 zred y 0 N 1 y + 1 + 1
471 65 nnge1d y 0 N 1 1 y + 1
472 467 217 470 471 218 lelttrd y 0 N 1 1 < y + 1 + 1
473 467 470 ltnled y 0 N 1 1 < y + 1 + 1 ¬ y + 1 + 1 1
474 472 473 mpbid y 0 N 1 ¬ y + 1 + 1 1
475 elfzle1 1 y + 1 + 1 N y + 1 + 1 1
476 474 475 nsyl y 0 N 1 ¬ 1 y + 1 + 1 N
477 eleq1 n = 1 n y + 1 + 1 N 1 y + 1 + 1 N
478 477 notbid n = 1 ¬ n y + 1 + 1 N ¬ 1 y + 1 + 1 N
479 476 478 syl5ibrcom y 0 N 1 n = 1 ¬ n y + 1 + 1 N
480 479 necon2ad y 0 N 1 n y + 1 + 1 N n 1
481 480 imp y 0 N 1 n y + 1 + 1 N n 1
482 481 182 syl y 0 N 1 n y + 1 + 1 N if n = 1 N n 1 = n 1
483 482 mpteq2dva y 0 N 1 n y + 1 + 1 N if n = 1 N n 1 = n y + 1 + 1 N n 1
484 483 adantl φ y 0 N 1 n y + 1 + 1 N if n = 1 N n 1 = n y + 1 + 1 N n 1
485 466 484 eqtrd φ y 0 N 1 n 1 N if n = 1 N n 1 y + 1 + 1 N = n y + 1 + 1 N n 1
486 485 rneqd φ y 0 N 1 ran n 1 N if n = 1 N n 1 y + 1 + 1 N = ran n y + 1 + 1 N n 1
487 463 486 syl5eq φ y 0 N 1 n 1 N if n = 1 N n 1 y + 1 + 1 N = ran n y + 1 + 1 N n 1
488 eqid n y + 1 + 1 N n 1 = n y + 1 + 1 N n 1
489 488 elrnmpt j V j ran n y + 1 + 1 N n 1 n y + 1 + 1 N j = n 1
490 489 elv j ran n y + 1 + 1 N n 1 n y + 1 + 1 N j = n 1
491 simpr φ y 0 N 1 n y + 1 + 1 N n y + 1 + 1 N
492 114 469 anim12ci φ y 0 N 1 y + 1 + 1 N
493 elfzelz n y + 1 + 1 N n
494 493 115 jctir n y + 1 + 1 N n 1
495 fzsubel y + 1 + 1 N n 1 n y + 1 + 1 N n 1 y + 1 + 1 - 1 N 1
496 492 494 495 syl2an φ y 0 N 1 n y + 1 + 1 N n y + 1 + 1 N n 1 y + 1 + 1 - 1 N 1
497 491 496 mpbid φ y 0 N 1 n y + 1 + 1 N n 1 y + 1 + 1 - 1 N 1
498 eleq1 j = n 1 j y + 1 + 1 - 1 N 1 n 1 y + 1 + 1 - 1 N 1
499 497 498 syl5ibrcom φ y 0 N 1 n y + 1 + 1 N j = n 1 j y + 1 + 1 - 1 N 1
500 499 rexlimdva φ y 0 N 1 n y + 1 + 1 N j = n 1 j y + 1 + 1 - 1 N 1
501 elfzelz j y + 1 + 1 - 1 N 1 j
502 501 zcnd j y + 1 + 1 - 1 N 1 j
503 502 394 syl j y + 1 + 1 - 1 N 1 j + 1 - 1 = j
504 503 eleq1d j y + 1 + 1 - 1 N 1 j + 1 - 1 y + 1 + 1 - 1 N 1 j y + 1 + 1 - 1 N 1
505 504 ibir j y + 1 + 1 - 1 N 1 j + 1 - 1 y + 1 + 1 - 1 N 1
506 505 adantl φ y 0 N 1 j y + 1 + 1 - 1 N 1 j + 1 - 1 y + 1 + 1 - 1 N 1
507 501 peano2zd j y + 1 + 1 - 1 N 1 j + 1
508 507 115 jctir j y + 1 + 1 - 1 N 1 j + 1 1
509 fzsubel y + 1 + 1 N j + 1 1 j + 1 y + 1 + 1 N j + 1 - 1 y + 1 + 1 - 1 N 1
510 492 508 509 syl2an φ y 0 N 1 j y + 1 + 1 - 1 N 1 j + 1 y + 1 + 1 N j + 1 - 1 y + 1 + 1 - 1 N 1
511 506 510 mpbird φ y 0 N 1 j y + 1 + 1 - 1 N 1 j + 1 y + 1 + 1 N
512 503 eqcomd j y + 1 + 1 - 1 N 1 j = j + 1 - 1
513 512 adantl φ y 0 N 1 j y + 1 + 1 - 1 N 1 j = j + 1 - 1
514 408 rspceeqv j + 1 y + 1 + 1 N j = j + 1 - 1 n y + 1 + 1 N j = n 1
515 511 513 514 syl2anc φ y 0 N 1 j y + 1 + 1 - 1 N 1 n y + 1 + 1 N j = n 1
516 515 ex φ y 0 N 1 j y + 1 + 1 - 1 N 1 n y + 1 + 1 N j = n 1
517 500 516 impbid φ y 0 N 1 n y + 1 + 1 N j = n 1 j y + 1 + 1 - 1 N 1
518 490 517 syl5bb φ y 0 N 1 j ran n y + 1 + 1 N n 1 j y + 1 + 1 - 1 N 1
519 518 eqrdv φ y 0 N 1 ran n y + 1 + 1 N n 1 = y + 1 + 1 - 1 N 1
520 65 nncnd y 0 N 1 y + 1
521 pncan1 y + 1 y + 1 + 1 - 1 = y + 1
522 520 521 syl y 0 N 1 y + 1 + 1 - 1 = y + 1
523 522 oveq1d y 0 N 1 y + 1 + 1 - 1 N 1 = y + 1 N 1
524 523 adantl φ y 0 N 1 y + 1 + 1 - 1 N 1 = y + 1 N 1
525 487 519 524 3eqtrd φ y 0 N 1 n 1 N if n = 1 N n 1 y + 1 + 1 N = y + 1 N 1
526 525 imaeq2d φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N = 2 nd 1 st T y + 1 N 1
527 462 526 syl5eq φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N = 2 nd 1 st T y + 1 N 1
528 527 xpeq1d φ y 0 N 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 = 2 nd 1 st T y + 1 N 1 × 0
529 461 528 uneq12d φ y 0 N 1 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 = 2 nd 1 st T 1 y × 1 2 nd 1 st T N × 1 2 nd 1 st T y + 1 N 1 × 0
530 un23 2 nd 1 st T 1 y × 1 2 nd 1 st T N × 1 2 nd 1 st T y + 1 N 1 × 0 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1
531 529 530 eqtrdi φ y 0 N 1 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 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1
532 531 fveq1d φ y 0 N 1 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 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1 n
533 532 ad2antrr φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T N 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 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 1 n
534 imaundi 2 nd 1 st T y + 1 N 1 N = 2 nd 1 st T y + 1 N 1 2 nd 1 st T N
535 fzsplit2 N - 1 + 1 y + 1 N N 1 y + 1 N = y + 1 N 1 N - 1 + 1 N
536 232 200 535 syl2anr φ y 0 N 1 y + 1 N = y + 1 N 1 N - 1 + 1 N
537 206 uneq2d φ y + 1 N 1 N - 1 + 1 N = y + 1 N 1 N
538 537 adantr φ y 0 N 1 y + 1 N 1 N - 1 + 1 N = y + 1 N 1 N
539 536 538 eqtrd φ y 0 N 1 y + 1 N = y + 1 N 1 N
540 539 imaeq2d φ y 0 N 1 2 nd 1 st T y + 1 N = 2 nd 1 st T y + 1 N 1 N
541 352 adantr φ y 0 N 1 2 nd 1 st T N = 2 nd 1 st T N
542 541 uneq2d φ y 0 N 1 2 nd 1 st T y + 1 N 1 2 nd 1 st T N = 2 nd 1 st T y + 1 N 1 2 nd 1 st T N
543 534 540 542 3eqtr4a φ y 0 N 1 2 nd 1 st T y + 1 N = 2 nd 1 st T y + 1 N 1 2 nd 1 st T N
544 543 xpeq1d φ y 0 N 1 2 nd 1 st T y + 1 N × 0 = 2 nd 1 st T y + 1 N 1 2 nd 1 st T N × 0
545 xpundir 2 nd 1 st T y + 1 N 1 2 nd 1 st T N × 0 = 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0
546 544 545 eqtrdi φ y 0 N 1 2 nd 1 st T y + 1 N × 0 = 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0
547 546 uneq2d φ 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 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0
548 unass 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0
549 547 548 eqtr4di φ 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 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0
550 549 fveq1d φ y 0 N 1 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0 n
551 550 ad2antrr φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T N 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N 1 × 0 2 nd 1 st T N × 0 n
552 374 533 551 3eqtr4d φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T N 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 n = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
553 316 552 eqtrd φ y 0 N 1 n 1 N ¬ n = 2 nd 1 st T N 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 n 0 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
554 250 252 314 553 ifbothda φ y 0 N 1 n 1 N 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 n if n = 2 nd 1 st T N 1 0 = 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
555 554 oveq2d φ y 0 N 1 n 1 N 1 st 1 st T n + 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 n - if n = 2 nd 1 st T N 1 0 = 1 st 1 st T n + 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 n
556 248 555 eqtr2d φ y 0 N 1 n 1 N 1 st 1 st T n + 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 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 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 n
557 556 mpteq2dva φ y 0 N 1 n 1 N 1 st 1 st T n + 2 nd 1 st T 1 y × 1 2 nd 1 st T y + 1 N × 0 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 1 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 n
558 93 557 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 = 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 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 n
559 53 adantl φ y 0 N 1 y
560 160 adantr φ y 0 N 1 N 1
561 158 adantr φ y 0 N 1 N
562 elfzle2 y 0 N 1 y N 1
563 562 adantl φ y 0 N 1 y N 1
564 159 adantr φ y 0 N 1 N 1 < N
565 559 560 561 563 564 lelttrd φ y 0 N 1 y < N
566 6 adantr φ y 0 N 1 2 nd T = N
567 565 566 breqtrrd φ y 0 N 1 y < 2 nd T
568 567 iftrued φ y 0 N 1 if y < 2 nd T y y + 1 = y
569 568 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
570 vex y V
571 oveq2 j = y 1 j = 1 y
572 571 imaeq2d j = y 2 nd 1 st T 1 j = 2 nd 1 st T 1 y
573 572 xpeq1d j = y 2 nd 1 st T 1 j × 1 = 2 nd 1 st T 1 y × 1
574 oveq1 j = y j + 1 = y + 1
575 574 oveq1d j = y j + 1 N = y + 1 N
576 575 imaeq2d j = y 2 nd 1 st T j + 1 N = 2 nd 1 st T y + 1 N
577 576 xpeq1d j = y 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T y + 1 N × 0
578 573 577 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
579 578 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
580 570 579 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
581 569 580 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
582 ovexd φ y 0 N 1 n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 V
583 fvexd φ y 0 N 1 n 1 N 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 n V
584 eqidd φ y 0 N 1 n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0 = n 1 N 1 st 1 st T n if n = 2 nd 1 st T N 1 0
585 245 ffnd φ y 0 N 1 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 Fn 1 N
586 nfcv _ n 2 nd 1 st T
587 nfmpt1 _ n n 1 N if n = 1 N n 1
588 586 587 nfco _ n 2 nd 1 st T n 1 N if n = 1 N n 1
589 nfcv _ n 1 y + 1
590 588 589 nfima _ n 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1
591 nfcv _ n 1
592 590 591 nfxp _ n 2 nd 1 st T n 1 N if n = 1 N n 1 1 y + 1 × 1
593 nfcv _ n y + 1 + 1 N
594 588 593 nfima _ n 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N
595 nfcv _ n 0
596 594 595 nfxp _ n 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0
597 592 596 nfun _ n 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
598 597 dffn5f 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 Fn 1 N 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 = n 1 N 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 n
599 585 598 sylib φ y 0 N 1 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 = n 1 N 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 n
600 89 582 583 584 599 offval2 φ 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 = 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 y + 1 × 1 2 nd 1 st T n 1 N if n = 1 N n 1 y + 1 + 1 N × 0 n
601 558 581 600 3eqtr4rd φ 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 = 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
602 601 mpteq2dva φ 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 = 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
603 23 602 eqtr4d φ 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