Metamath Proof Explorer


Theorem poimirlem17

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

Ref Expression
Hypotheses poimir.0 φN
poimirlem22.s S=t0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
poimirlem22.1 φF:0N10K1N
poimirlem22.2 φTS
poimirlem18.3 φn1NpranFpnK
poimirlem18.4 φ2ndT=0
Assertion poimirlem17 φzSzT

Proof

Step Hyp Ref Expression
1 poimir.0 φN
2 poimirlem22.s S=t0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
3 poimirlem22.1 φF:0N10K1N
4 poimirlem22.2 φTS
5 poimirlem18.3 φn1NpranFpnK
6 poimirlem18.4 φ2ndT=0
7 1 2 3 4 5 6 poimirlem16 φF=y0N1n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
8 elfznn0 y0N1y0
9 8 nn0red y0N1y
10 9 adantl φy0N1y
11 1 nnzd φN
12 peano2zm NN1
13 11 12 syl φN1
14 13 zred φN1
15 14 adantr φy0N1N1
16 1 nnred φN
17 16 adantr φy0N1N
18 elfzle2 y0N1yN1
19 18 adantl φy0N1yN1
20 16 ltm1d φN1<N
21 20 adantr φy0N1N1<N
22 10 15 17 19 21 lelttrd φy0N1y<N
23 22 adantlr φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Ny0N1y<N
24 fveq2 t=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N2ndt=2ndn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N
25 opex n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1V
26 op2ndg n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1VN2ndn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N=N
27 25 1 26 sylancr φ2ndn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N=N
28 24 27 sylan9eqr φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N2ndt=N
29 28 adantr φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Ny0N12ndt=N
30 23 29 breqtrrd φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Ny0N1y<2ndt
31 30 iftrued φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Ny0N1ify<2ndtyy+1=y
32 31 csbeq1d φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Ny0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=y/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
33 vex yV
34 oveq2 j=y1j=1y
35 34 imaeq2d j=y2nd1stt1j=2nd1stt1y
36 35 xpeq1d j=y2nd1stt1j×1=2nd1stt1y×1
37 oveq1 j=yj+1=y+1
38 37 oveq1d j=yj+1N=y+1N
39 38 imaeq2d j=y2nd1sttj+1N=2nd1stty+1N
40 39 xpeq1d j=y2nd1sttj+1N×0=2nd1stty+1N×0
41 36 40 uneq12d j=y2nd1stt1j×12nd1sttj+1N×0=2nd1stt1y×12nd1stty+1N×0
42 41 oveq2d j=y1st1stt+f2nd1stt1j×12nd1sttj+1N×0=1st1stt+f2nd1stt1y×12nd1stty+1N×0
43 33 42 csbie y/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=1st1stt+f2nd1stt1y×12nd1stty+1N×0
44 2fveq3 t=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N1st1stt=1st1stn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N
45 op1stg n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1VN1stn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1
46 25 1 45 sylancr φ1stn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1
47 46 fveq2d φ1st1stn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N=1stn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1
48 ovex 1NV
49 48 mptex n1N1st1stTn+ifn=2nd1stT110V
50 fvex 2nd1stTV
51 48 mptex n1Nifn=N1n+1V
52 50 51 coex 2nd1stTn1Nifn=N1n+1V
53 49 52 op1st 1stn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1=n1N1st1stTn+ifn=2nd1stT110
54 47 53 eqtrdi φ1st1stn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N=n1N1st1stTn+ifn=2nd1stT110
55 44 54 sylan9eqr φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N1st1stt=n1N1st1stTn+ifn=2nd1stT110
56 fveq2 t=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N1stt=1stn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N
57 56 46 sylan9eqr φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N1stt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1
58 57 fveq2d φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N2nd1stt=2ndn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1
59 49 52 op2nd 2ndn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1=2nd1stTn1Nifn=N1n+1
60 58 59 eqtrdi φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N2nd1stt=2nd1stTn1Nifn=N1n+1
61 60 imaeq1d φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N2nd1stt1y=2nd1stTn1Nifn=N1n+11y
62 61 xpeq1d φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N2nd1stt1y×1=2nd1stTn1Nifn=N1n+11y×1
63 60 imaeq1d φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N2nd1stty+1N=2nd1stTn1Nifn=N1n+1y+1N
64 63 xpeq1d φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N2nd1stty+1N×0=2nd1stTn1Nifn=N1n+1y+1N×0
65 62 64 uneq12d φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N2nd1stt1y×12nd1stty+1N×0=2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
66 55 65 oveq12d φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N1st1stt+f2nd1stt1y×12nd1stty+1N×0=n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
67 43 66 eqtrid φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Ny/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
68 67 adantr φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Ny0N1y/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
69 32 68 eqtrd φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Ny0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
70 69 mpteq2dva φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Ny0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=y0N1n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
71 70 eqeq2d φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NF=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
72 71 ex φt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NF=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
73 72 alrimiv φtt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NF=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
74 oveq2 1=ifn=2nd1stT1101st1stTn+1=1st1stTn+ifn=2nd1stT110
75 74 eleq1d 1=ifn=2nd1stT1101st1stTn+10..^K1st1stTn+ifn=2nd1stT1100..^K
76 oveq2 0=ifn=2nd1stT1101st1stTn+0=1st1stTn+ifn=2nd1stT110
77 76 eleq1d 0=ifn=2nd1stT1101st1stTn+00..^K1st1stTn+ifn=2nd1stT1100..^K
78 fveq2 n=2nd1stT11st1stTn=1st1stT2nd1stT1
79 78 oveq1d n=2nd1stT11st1stTn+1=1st1stT2nd1stT1+1
80 79 adantl φn=2nd1stT11st1stTn+1=1st1stT2nd1stT1+1
81 elrabi Tt0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0T0..^K1N×f|f:1N1-1 onto1N×0N
82 81 2 eleq2s TST0..^K1N×f|f:1N1-1 onto1N×0N
83 xp1st T0..^K1N×f|f:1N1-1 onto1N×0N1stT0..^K1N×f|f:1N1-1 onto1N
84 4 82 83 3syl φ1stT0..^K1N×f|f:1N1-1 onto1N
85 xp1st 1stT0..^K1N×f|f:1N1-1 onto1N1st1stT0..^K1N
86 elmapi 1st1stT0..^K1N1st1stT:1N0..^K
87 84 85 86 3syl φ1st1stT:1N0..^K
88 4 82 syl φT0..^K1N×f|f:1N1-1 onto1N×0N
89 xp2nd 1stT0..^K1N×f|f:1N1-1 onto1N2nd1stTf|f:1N1-1 onto1N
90 88 83 89 3syl φ2nd1stTf|f:1N1-1 onto1N
91 f1oeq1 f=2nd1stTf:1N1-1 onto1N2nd1stT:1N1-1 onto1N
92 50 91 elab 2nd1stTf|f:1N1-1 onto1N2nd1stT:1N1-1 onto1N
93 90 92 sylib φ2nd1stT:1N1-1 onto1N
94 f1of 2nd1stT:1N1-1 onto1N2nd1stT:1N1N
95 93 94 syl φ2nd1stT:1N1N
96 nnuz =1
97 1 96 eleqtrdi φN1
98 eluzfz1 N111N
99 97 98 syl φ11N
100 95 99 ffvelrnd φ2nd1stT11N
101 87 100 ffvelrnd φ1st1stT2nd1stT10..^K
102 elfzonn0 1st1stT2nd1stT10..^K1st1stT2nd1stT10
103 peano2nn0 1st1stT2nd1stT101st1stT2nd1stT1+10
104 101 102 103 3syl φ1st1stT2nd1stT1+10
105 elfzo0 1st1stT2nd1stT10..^K1st1stT2nd1stT10K1st1stT2nd1stT1<K
106 101 105 sylib φ1st1stT2nd1stT10K1st1stT2nd1stT1<K
107 106 simp2d φK
108 104 nn0red φ1st1stT2nd1stT1+1
109 107 nnred φK
110 elfzolt2 1st1stT2nd1stT10..^K1st1stT2nd1stT1<K
111 101 110 syl φ1st1stT2nd1stT1<K
112 101 102 syl φ1st1stT2nd1stT10
113 112 nn0zd φ1st1stT2nd1stT1
114 107 nnzd φK
115 zltp1le 1st1stT2nd1stT1K1st1stT2nd1stT1<K1st1stT2nd1stT1+1K
116 113 114 115 syl2anc φ1st1stT2nd1stT1<K1st1stT2nd1stT1+1K
117 111 116 mpbid φ1st1stT2nd1stT1+1K
118 fvex 2nd1stT1V
119 eleq1 n=2nd1stT1n1N2nd1stT11N
120 119 anbi2d n=2nd1stT1φn1Nφ2nd1stT11N
121 fveq2 n=2nd1stT1pn=p2nd1stT1
122 121 neeq1d n=2nd1stT1pnKp2nd1stT1K
123 122 rexbidv n=2nd1stT1pranFpnKpranFp2nd1stT1K
124 120 123 imbi12d n=2nd1stT1φn1NpranFpnKφ2nd1stT11NpranFp2nd1stT1K
125 118 124 5 vtocl φ2nd1stT11NpranFp2nd1stT1K
126 100 125 mpdan φpranFp2nd1stT1K
127 fveq1 p=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×0p2nd1stT1=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×02nd1stT1
128 87 ffnd φ1st1stTFn1N
129 128 adantr φy0N11st1stTFn1N
130 1ex 1V
131 fnconstg 1V2nd1stT1y+1×1Fn2nd1stT1y+1
132 130 131 ax-mp 2nd1stT1y+1×1Fn2nd1stT1y+1
133 c0ex 0V
134 fnconstg 0V2nd1stTy+1+1N×0Fn2nd1stTy+1+1N
135 133 134 ax-mp 2nd1stTy+1+1N×0Fn2nd1stTy+1+1N
136 132 135 pm3.2i 2nd1stT1y+1×1Fn2nd1stT1y+12nd1stTy+1+1N×0Fn2nd1stTy+1+1N
137 dff1o3 2nd1stT:1N1-1 onto1N2nd1stT:1Nonto1NFun2nd1stT-1
138 137 simprbi 2nd1stT:1N1-1 onto1NFun2nd1stT-1
139 imain Fun2nd1stT-12nd1stT1y+1y+1+1N=2nd1stT1y+12nd1stTy+1+1N
140 93 138 139 3syl φ2nd1stT1y+1y+1+1N=2nd1stT1y+12nd1stTy+1+1N
141 nn0p1nn y0y+1
142 8 141 syl y0N1y+1
143 142 nnred y0N1y+1
144 143 ltp1d y0N1y+1<y+1+1
145 fzdisj y+1<y+1+11y+1y+1+1N=
146 145 imaeq2d y+1<y+1+12nd1stT1y+1y+1+1N=2nd1stT
147 ima0 2nd1stT=
148 146 147 eqtrdi y+1<y+1+12nd1stT1y+1y+1+1N=
149 144 148 syl y0N12nd1stT1y+1y+1+1N=
150 140 149 sylan9req φy0N12nd1stT1y+12nd1stTy+1+1N=
151 fnun 2nd1stT1y+1×1Fn2nd1stT1y+12nd1stTy+1+1N×0Fn2nd1stTy+1+1N2nd1stT1y+12nd1stTy+1+1N=2nd1stT1y+1×12nd1stTy+1+1N×0Fn2nd1stT1y+12nd1stTy+1+1N
152 136 150 151 sylancr φy0N12nd1stT1y+1×12nd1stTy+1+1N×0Fn2nd1stT1y+12nd1stTy+1+1N
153 imaundi 2nd1stT1y+1y+1+1N=2nd1stT1y+12nd1stTy+1+1N
154 142 peano2nnd y0N1y+1+1
155 154 96 eleqtrdi y0N1y+1+11
156 1 nncnd φN
157 npcan1 NN-1+1=N
158 156 157 syl φN-1+1=N
159 158 adantr φy0N1N-1+1=N
160 elfzuz3 y0N1N1y
161 eluzp1p1 N1yN-1+1y+1
162 160 161 syl y0N1N-1+1y+1
163 162 adantl φy0N1N-1+1y+1
164 159 163 eqeltrrd φy0N1Ny+1
165 fzsplit2 y+1+11Ny+11N=1y+1y+1+1N
166 155 164 165 syl2an2 φy0N11N=1y+1y+1+1N
167 166 imaeq2d φy0N12nd1stT1N=2nd1stT1y+1y+1+1N
168 f1ofo 2nd1stT:1N1-1 onto1N2nd1stT:1Nonto1N
169 foima 2nd1stT:1Nonto1N2nd1stT1N=1N
170 93 168 169 3syl φ2nd1stT1N=1N
171 170 adantr φy0N12nd1stT1N=1N
172 167 171 eqtr3d φy0N12nd1stT1y+1y+1+1N=1N
173 153 172 eqtr3id φy0N12nd1stT1y+12nd1stTy+1+1N=1N
174 173 fneq2d φy0N12nd1stT1y+1×12nd1stTy+1+1N×0Fn2nd1stT1y+12nd1stTy+1+1N2nd1stT1y+1×12nd1stTy+1+1N×0Fn1N
175 152 174 mpbid φy0N12nd1stT1y+1×12nd1stTy+1+1N×0Fn1N
176 48 a1i φy0N11NV
177 inidm 1N1N=1N
178 eqidd φy0N12nd1stT11N1st1stT2nd1stT1=1st1stT2nd1stT1
179 f1ofn 2nd1stT:1N1-1 onto1N2nd1stTFn1N
180 93 179 syl φ2nd1stTFn1N
181 180 adantr φy0N12nd1stTFn1N
182 fzss2 Ny+11y+11N
183 164 182 syl φy0N11y+11N
184 142 96 eleqtrdi y0N1y+11
185 eluzfz1 y+1111y+1
186 184 185 syl y0N111y+1
187 186 adantl φy0N111y+1
188 fnfvima 2nd1stTFn1N1y+11N11y+12nd1stT12nd1stT1y+1
189 181 183 187 188 syl3anc φy0N12nd1stT12nd1stT1y+1
190 fvun1 2nd1stT1y+1×1Fn2nd1stT1y+12nd1stTy+1+1N×0Fn2nd1stTy+1+1N2nd1stT1y+12nd1stTy+1+1N=2nd1stT12nd1stT1y+12nd1stT1y+1×12nd1stTy+1+1N×02nd1stT1=2nd1stT1y+1×12nd1stT1
191 132 135 190 mp3an12 2nd1stT1y+12nd1stTy+1+1N=2nd1stT12nd1stT1y+12nd1stT1y+1×12nd1stTy+1+1N×02nd1stT1=2nd1stT1y+1×12nd1stT1
192 150 189 191 syl2anc φy0N12nd1stT1y+1×12nd1stTy+1+1N×02nd1stT1=2nd1stT1y+1×12nd1stT1
193 130 fvconst2 2nd1stT12nd1stT1y+12nd1stT1y+1×12nd1stT1=1
194 189 193 syl φy0N12nd1stT1y+1×12nd1stT1=1
195 192 194 eqtrd φy0N12nd1stT1y+1×12nd1stTy+1+1N×02nd1stT1=1
196 195 adantr φy0N12nd1stT11N2nd1stT1y+1×12nd1stTy+1+1N×02nd1stT1=1
197 129 175 176 176 177 178 196 ofval φy0N12nd1stT11N1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×02nd1stT1=1st1stT2nd1stT1+1
198 100 197 mpidan φy0N11st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×02nd1stT1=1st1stT2nd1stT1+1
199 127 198 sylan9eqr φy0N1p=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×0p2nd1stT1=1st1stT2nd1stT1+1
200 199 adantllr φpranFy0N1p=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×0p2nd1stT1=1st1stT2nd1stT1+1
201 fveq2 t=T2ndt=2ndT
202 201 breq2d t=Ty<2ndty<2ndT
203 202 ifbid t=Tify<2ndtyy+1=ify<2ndTyy+1
204 2fveq3 t=T1st1stt=1st1stT
205 2fveq3 t=T2nd1stt=2nd1stT
206 205 imaeq1d t=T2nd1stt1j=2nd1stT1j
207 206 xpeq1d t=T2nd1stt1j×1=2nd1stT1j×1
208 205 imaeq1d t=T2nd1sttj+1N=2nd1stTj+1N
209 208 xpeq1d t=T2nd1sttj+1N×0=2nd1stTj+1N×0
210 207 209 uneq12d t=T2nd1stt1j×12nd1sttj+1N×0=2nd1stT1j×12nd1stTj+1N×0
211 204 210 oveq12d t=T1st1stt+f2nd1stt1j×12nd1sttj+1N×0=1st1stT+f2nd1stT1j×12nd1stTj+1N×0
212 203 211 csbeq12dv t=Tify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
213 212 mpteq2dv t=Ty0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
214 213 eqeq2d t=TF=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
215 214 2 elrab2 TST0..^K1N×f|f:1N1-1 onto1N×0NF=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
216 215 simprbi TSF=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
217 4 216 syl φF=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
218 217 rneqd φranF=rany0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
219 218 eleq2d φpranFprany0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
220 eqid y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
221 ovex 1st1stT+f2nd1stT1j×12nd1stTj+1N×0V
222 221 csbex ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0V
223 220 222 elrnmpti prany0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0y0N1p=ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
224 219 223 bitrdi φpranFy0N1p=ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
225 6 adantr φy0N12ndT=0
226 elfzle1 y0N10y
227 226 adantl φy0N10y
228 225 227 eqbrtrd φy0N12ndTy
229 0re 0
230 6 229 eqeltrdi φ2ndT
231 lenlt 2ndTy2ndTy¬y<2ndT
232 230 9 231 syl2an φy0N12ndTy¬y<2ndT
233 228 232 mpbid φy0N1¬y<2ndT
234 233 iffalsed φy0N1ify<2ndTyy+1=y+1
235 234 csbeq1d φy0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0=y+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
236 ovex y+1V
237 oveq2 j=y+11j=1y+1
238 237 imaeq2d j=y+12nd1stT1j=2nd1stT1y+1
239 238 xpeq1d j=y+12nd1stT1j×1=2nd1stT1y+1×1
240 oveq1 j=y+1j+1=y+1+1
241 240 oveq1d j=y+1j+1N=y+1+1N
242 241 imaeq2d j=y+12nd1stTj+1N=2nd1stTy+1+1N
243 242 xpeq1d j=y+12nd1stTj+1N×0=2nd1stTy+1+1N×0
244 239 243 uneq12d j=y+12nd1stT1j×12nd1stTj+1N×0=2nd1stT1y+1×12nd1stTy+1+1N×0
245 244 oveq2d j=y+11st1stT+f2nd1stT1j×12nd1stTj+1N×0=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×0
246 236 245 csbie y+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×0
247 235 246 eqtrdi φy0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×0
248 247 eqeq2d φy0N1p=ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0p=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×0
249 248 rexbidva φy0N1p=ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0y0N1p=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×0
250 224 249 bitrd φpranFy0N1p=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×0
251 250 biimpa φpranFy0N1p=1st1stT+f2nd1stT1y+1×12nd1stTy+1+1N×0
252 200 251 r19.29a φpranFp2nd1stT1=1st1stT2nd1stT1+1
253 eqtr3 p2nd1stT1=1st1stT2nd1stT1+1K=1st1stT2nd1stT1+1p2nd1stT1=K
254 253 ex p2nd1stT1=1st1stT2nd1stT1+1K=1st1stT2nd1stT1+1p2nd1stT1=K
255 252 254 syl φpranFK=1st1stT2nd1stT1+1p2nd1stT1=K
256 255 necon3d φpranFp2nd1stT1KK1st1stT2nd1stT1+1
257 256 rexlimdva φpranFp2nd1stT1KK1st1stT2nd1stT1+1
258 126 257 mpd φK1st1stT2nd1stT1+1
259 108 109 117 258 leneltd φ1st1stT2nd1stT1+1<K
260 elfzo0 1st1stT2nd1stT1+10..^K1st1stT2nd1stT1+10K1st1stT2nd1stT1+1<K
261 104 107 259 260 syl3anbrc φ1st1stT2nd1stT1+10..^K
262 261 adantr φn=2nd1stT11st1stT2nd1stT1+10..^K
263 80 262 eqeltrd φn=2nd1stT11st1stTn+10..^K
264 263 adantlr φn1Nn=2nd1stT11st1stTn+10..^K
265 87 ffvelrnda φn1N1st1stTn0..^K
266 elfzonn0 1st1stTn0..^K1st1stTn0
267 265 266 syl φn1N1st1stTn0
268 267 nn0cnd φn1N1st1stTn
269 268 addid1d φn1N1st1stTn+0=1st1stTn
270 269 265 eqeltrd φn1N1st1stTn+00..^K
271 270 adantr φn1N¬n=2nd1stT11st1stTn+00..^K
272 75 77 264 271 ifbothda φn1N1st1stTn+ifn=2nd1stT1100..^K
273 272 fmpttd φn1N1st1stTn+ifn=2nd1stT110:1N0..^K
274 ovex 0..^KV
275 274 48 elmap n1N1st1stTn+ifn=2nd1stT1100..^K1Nn1N1st1stTn+ifn=2nd1stT110:1N0..^K
276 273 275 sylibr φn1N1st1stTn+ifn=2nd1stT1100..^K1N
277 simpr φn1N1n1N1
278 1z 1
279 13 278 jctil φ1N1
280 elfzelz n1N1n
281 280 278 jctir n1N1n1
282 fzaddel 1N1n1n1N1n+11+1N-1+1
283 279 281 282 syl2an φn1N1n1N1n+11+1N-1+1
284 277 283 mpbid φn1N1n+11+1N-1+1
285 158 oveq2d φ1+1N-1+1=1+1N
286 285 adantr φn1N11+1N-1+1=1+1N
287 284 286 eleqtrd φn1N1n+11+1N
288 287 ralrimiva φn1N1n+11+1N
289 simpr φy1+1Ny1+1N
290 peano2z 11+1
291 278 290 ax-mp 1+1
292 11 291 jctil φ1+1N
293 elfzelz y1+1Ny
294 293 278 jctir y1+1Ny1
295 fzsubel 1+1Ny1y1+1Ny11+1-1N1
296 292 294 295 syl2an φy1+1Ny1+1Ny11+1-1N1
297 289 296 mpbid φy1+1Ny11+1-1N1
298 ax-1cn 1
299 298 298 pncan3oi 1+1-1=1
300 299 oveq1i 1+1-1N1=1N1
301 297 300 eleqtrdi φy1+1Ny11N1
302 293 zcnd y1+1Ny
303 elfznn n1N1n
304 303 nncnd n1N1n
305 subadd2 y1ny1=nn+1=y
306 298 305 mp3an2 yny1=nn+1=y
307 306 bicomd ynn+1=yy1=n
308 eqcom y=n+1n+1=y
309 eqcom n=y1y1=n
310 307 308 309 3bitr4g yny=n+1n=y1
311 302 304 310 syl2an y1+1Nn1N1y=n+1n=y1
312 311 ralrimiva y1+1Nn1N1y=n+1n=y1
313 312 adantl φy1+1Nn1N1y=n+1n=y1
314 reu6i y11N1n1N1y=n+1n=y1∃!n1N1y=n+1
315 301 313 314 syl2anc φy1+1N∃!n1N1y=n+1
316 315 ralrimiva φy1+1N∃!n1N1y=n+1
317 eqid n1N1n+1=n1N1n+1
318 317 f1ompt n1N1n+1:1N11-1 onto1+1Nn1N1n+11+1Ny1+1N∃!n1N1y=n+1
319 288 316 318 sylanbrc φn1N1n+1:1N11-1 onto1+1N
320 f1osng N1VN1:N1-1 onto1
321 1 130 320 sylancl φN1:N1-1 onto1
322 14 16 ltnled φN1<N¬NN1
323 20 322 mpbid φ¬NN1
324 elfzle2 N1N1NN1
325 323 324 nsyl φ¬N1N1
326 disjsn 1N1N=¬N1N1
327 325 326 sylibr φ1N1N=
328 1re 1
329 328 ltp1i 1<1+1
330 291 zrei 1+1
331 328 330 ltnlei 1<1+1¬1+11
332 329 331 mpbi ¬1+11
333 elfzle1 11+1N1+11
334 332 333 mto ¬11+1N
335 disjsn 1+1N1=¬11+1N
336 334 335 mpbir 1+1N1=
337 336 a1i φ1+1N1=
338 f1oun n1N1n+1:1N11-1 onto1+1NN1:N1-1 onto11N1N=1+1N1=n1N1n+1N1:1N1N1-1 onto1+1N1
339 319 321 327 337 338 syl22anc φn1N1n+1N1:1N1N1-1 onto1+1N1
340 130 a1i φ1V
341 158 97 eqeltrd φN-1+11
342 uzid N1N1N1
343 peano2uz N1N1N-1+1N1
344 13 342 343 3syl φN-1+1N1
345 158 344 eqeltrrd φNN1
346 fzsplit2 N-1+11NN11N=1N1N-1+1N
347 341 345 346 syl2anc φ1N=1N1N-1+1N
348 158 oveq1d φN-1+1N=NN
349 fzsn NNN=N
350 11 349 syl φNN=N
351 348 350 eqtrd φN-1+1N=N
352 351 uneq2d φ1N1N-1+1N=1N1N
353 347 352 eqtr2d φ1N1N=1N
354 iftrue n=Nifn=N1n+1=1
355 354 adantl φn=Nifn=N1n+1=1
356 1 340 353 355 fmptapd φn1N1ifn=N1n+1N1=n1Nifn=N1n+1
357 eleq1 n=Nn1N1N1N1
358 357 notbid n=N¬n1N1¬N1N1
359 325 358 syl5ibrcom φn=N¬n1N1
360 359 necon2ad φn1N1nN
361 360 imp φn1N1nN
362 ifnefalse nNifn=N1n+1=n+1
363 361 362 syl φn1N1ifn=N1n+1=n+1
364 363 mpteq2dva φn1N1ifn=N1n+1=n1N1n+1
365 364 uneq1d φn1N1ifn=N1n+1N1=n1N1n+1N1
366 356 365 eqtr3d φn1Nifn=N1n+1=n1N1n+1N1
367 347 352 eqtrd φ1N=1N1N
368 uzid 111
369 peano2uz 111+11
370 278 368 369 mp2b 1+11
371 fzsplit2 1+11N11N=111+1N
372 370 97 371 sylancr φ1N=111+1N
373 fzsn 111=1
374 278 373 ax-mp 11=1
375 374 uneq1i 111+1N=11+1N
376 375 equncomi 111+1N=1+1N1
377 372 376 eqtrdi φ1N=1+1N1
378 366 367 377 f1oeq123d φn1Nifn=N1n+1:1N1-1 onto1Nn1N1n+1N1:1N1N1-1 onto1+1N1
379 339 378 mpbird φn1Nifn=N1n+1:1N1-1 onto1N
380 f1oco 2nd1stT:1N1-1 onto1Nn1Nifn=N1n+1:1N1-1 onto1N2nd1stTn1Nifn=N1n+1:1N1-1 onto1N
381 93 379 380 syl2anc φ2nd1stTn1Nifn=N1n+1:1N1-1 onto1N
382 f1oeq1 f=2nd1stTn1Nifn=N1n+1f:1N1-1 onto1N2nd1stTn1Nifn=N1n+1:1N1-1 onto1N
383 52 382 elab 2nd1stTn1Nifn=N1n+1f|f:1N1-1 onto1N2nd1stTn1Nifn=N1n+1:1N1-1 onto1N
384 381 383 sylibr φ2nd1stTn1Nifn=N1n+1f|f:1N1-1 onto1N
385 276 384 opelxpd φn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+10..^K1N×f|f:1N1-1 onto1N
386 1 nnnn0d φN0
387 nn0fz0 N0N0N
388 386 387 sylib φN0N
389 385 388 opelxpd φn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N0..^K1N×f|f:1N1-1 onto1N×0N
390 elrab3t tt=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NF=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N0..^K1N×f|f:1N1-1 onto1N×0Nn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Nt0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
391 73 389 390 syl2anc φn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Nt0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1n1N1st1stTn+ifn=2nd1stT110+f2nd1stTn1Nifn=N1n+11y×12nd1stTn1Nifn=N1n+1y+1N×0
392 7 391 mpbird φn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1Nt0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
393 392 2 eleqtrrdi φn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NS
394 fveqeq2 n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N=T2ndn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N=N2ndT=N
395 27 394 syl5ibcom φn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N=T2ndT=N
396 1 nnne0d φN0
397 neeq1 2ndT=N2ndT0N0
398 396 397 syl5ibrcom φ2ndT=N2ndT0
399 395 398 syld φn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1N=T2ndT0
400 399 necon2d φ2ndT=0n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NT
401 6 400 mpd φn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NT
402 neeq1 z=n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NzTn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NT
403 402 rspcev n1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NSn1N1st1stTn+ifn=2nd1stT1102nd1stTn1Nifn=N1n+1NTzSzT
404 393 401 403 syl2anc φzSzT