Metamath Proof Explorer


Theorem poimirlem7

Description: Lemma for poimir , similar to poimirlem6 , but for vertices after the opposite vertex. (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
poimirlem9.1 φ T S
poimirlem9.2 φ 2 nd T 1 N 1
poimirlem7.3 φ M 2 nd T + 1 + 1 N
Assertion poimirlem7 φ ι n 1 N | F M 2 n F M 1 n = 2 nd 1 st T M

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 poimirlem9.1 φ T S
4 poimirlem9.2 φ 2 nd T 1 N 1
5 poimirlem7.3 φ M 2 nd T + 1 + 1 N
6 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
7 6 2 eleq2s T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
8 3 7 syl φ T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
9 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
10 8 9 syl φ 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
11 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
12 10 11 syl φ 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
13 fvex 2 nd 1 st T V
14 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
15 13 14 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
16 12 15 sylib φ 2 nd 1 st T : 1 N 1-1 onto 1 N
17 f1of 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1 N
18 16 17 syl φ 2 nd 1 st T : 1 N 1 N
19 elfznn 2 nd T 1 N 1 2 nd T
20 4 19 syl φ 2 nd T
21 20 peano2nnd φ 2 nd T + 1
22 21 peano2nnd φ 2 nd T + 1 + 1
23 nnuz = 1
24 22 23 eleqtrdi φ 2 nd T + 1 + 1 1
25 fzss1 2 nd T + 1 + 1 1 2 nd T + 1 + 1 N 1 N
26 24 25 syl φ 2 nd T + 1 + 1 N 1 N
27 26 5 sseldd φ M 1 N
28 18 27 ffvelrnd φ 2 nd 1 st T M 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 10 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 φ n 2 nd 1 st T M 1 st 1 st T Fn 1 N
34 1ex 1 V
35 fnconstg 1 V 2 nd 1 st T 1 M 1 × 1 Fn 2 nd 1 st T 1 M 1
36 34 35 ax-mp 2 nd 1 st T 1 M 1 × 1 Fn 2 nd 1 st T 1 M 1
37 c0ex 0 V
38 fnconstg 0 V 2 nd 1 st T M N × 0 Fn 2 nd 1 st T M N
39 37 38 ax-mp 2 nd 1 st T M N × 0 Fn 2 nd 1 st T M N
40 36 39 pm3.2i 2 nd 1 st T 1 M 1 × 1 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M N × 0 Fn 2 nd 1 st T M N
41 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
42 41 simprbi 2 nd 1 st T : 1 N 1-1 onto 1 N Fun 2 nd 1 st T -1
43 16 42 syl φ Fun 2 nd 1 st T -1
44 imain Fun 2 nd 1 st T -1 2 nd 1 st T 1 M 1 M N = 2 nd 1 st T 1 M 1 2 nd 1 st T M N
45 43 44 syl φ 2 nd 1 st T 1 M 1 M N = 2 nd 1 st T 1 M 1 2 nd 1 st T M N
46 5 elfzelzd φ M
47 46 zred φ M
48 47 ltm1d φ M 1 < M
49 fzdisj M 1 < M 1 M 1 M N =
50 48 49 syl φ 1 M 1 M N =
51 50 imaeq2d φ 2 nd 1 st T 1 M 1 M N = 2 nd 1 st T
52 ima0 2 nd 1 st T =
53 51 52 eqtrdi φ 2 nd 1 st T 1 M 1 M N =
54 45 53 eqtr3d φ 2 nd 1 st T 1 M 1 2 nd 1 st T M N =
55 fnun 2 nd 1 st T 1 M 1 × 1 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M N × 0 Fn 2 nd 1 st T M N 2 nd 1 st T 1 M 1 2 nd 1 st T M N = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M N
56 40 54 55 sylancr φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M N
57 46 zcnd φ M
58 npcan1 M M - 1 + 1 = M
59 57 58 syl φ M - 1 + 1 = M
60 1red φ 1
61 22 nnred φ 2 nd T + 1 + 1
62 21 nnred φ 2 nd T + 1
63 21 nnge1d φ 1 2 nd T + 1
64 62 ltp1d φ 2 nd T + 1 < 2 nd T + 1 + 1
65 60 62 61 63 64 lelttrd φ 1 < 2 nd T + 1 + 1
66 elfzle1 M 2 nd T + 1 + 1 N 2 nd T + 1 + 1 M
67 5 66 syl φ 2 nd T + 1 + 1 M
68 60 61 47 65 67 ltletrd φ 1 < M
69 60 47 68 ltled φ 1 M
70 elnnz1 M M 1 M
71 46 69 70 sylanbrc φ M
72 71 23 eleqtrdi φ M 1
73 59 72 eqeltrd φ M - 1 + 1 1
74 peano2zm M M 1
75 46 74 syl φ M 1
76 uzid M 1 M 1 M 1
77 peano2uz M 1 M 1 M - 1 + 1 M 1
78 75 76 77 3syl φ M - 1 + 1 M 1
79 59 78 eqeltrrd φ M M 1
80 uzss M M 1 M M 1
81 79 80 syl φ M M 1
82 elfzuz3 M 2 nd T + 1 + 1 N N M
83 5 82 syl φ N M
84 81 83 sseldd φ N M 1
85 fzsplit2 M - 1 + 1 1 N M 1 1 N = 1 M 1 M - 1 + 1 N
86 73 84 85 syl2anc φ 1 N = 1 M 1 M - 1 + 1 N
87 59 oveq1d φ M - 1 + 1 N = M N
88 87 uneq2d φ 1 M 1 M - 1 + 1 N = 1 M 1 M N
89 86 88 eqtrd φ 1 N = 1 M 1 M N
90 89 imaeq2d φ 2 nd 1 st T 1 N = 2 nd 1 st T 1 M 1 M N
91 imaundi 2 nd 1 st T 1 M 1 M N = 2 nd 1 st T 1 M 1 2 nd 1 st T M N
92 90 91 eqtrdi φ 2 nd 1 st T 1 N = 2 nd 1 st T 1 M 1 2 nd 1 st T M N
93 f1ofo 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N
94 16 93 syl φ 2 nd 1 st T : 1 N onto 1 N
95 foima 2 nd 1 st T : 1 N onto 1 N 2 nd 1 st T 1 N = 1 N
96 94 95 syl φ 2 nd 1 st T 1 N = 1 N
97 92 96 eqtr3d φ 2 nd 1 st T 1 M 1 2 nd 1 st T M N = 1 N
98 97 fneq2d φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M N 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 Fn 1 N
99 56 98 mpbid φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 Fn 1 N
100 99 adantr φ n 2 nd 1 st T M 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 Fn 1 N
101 ovexd φ n 2 nd 1 st T M 1 N V
102 inidm 1 N 1 N = 1 N
103 eqidd φ n 2 nd 1 st T M n 1 N 1 st 1 st T n = 1 st 1 st T n
104 imaundi 2 nd 1 st T M M + 1 N = 2 nd 1 st T M 2 nd 1 st T M + 1 N
105 fzpred N M M N = M M + 1 N
106 83 105 syl φ M N = M M + 1 N
107 106 imaeq2d φ 2 nd 1 st T M N = 2 nd 1 st T M M + 1 N
108 f1ofn 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T Fn 1 N
109 16 108 syl φ 2 nd 1 st T Fn 1 N
110 fnsnfv 2 nd 1 st T Fn 1 N M 1 N 2 nd 1 st T M = 2 nd 1 st T M
111 109 27 110 syl2anc φ 2 nd 1 st T M = 2 nd 1 st T M
112 111 uneq1d φ 2 nd 1 st T M 2 nd 1 st T M + 1 N = 2 nd 1 st T M 2 nd 1 st T M + 1 N
113 104 107 112 3eqtr4a φ 2 nd 1 st T M N = 2 nd 1 st T M 2 nd 1 st T M + 1 N
114 113 xpeq1d φ 2 nd 1 st T M N × 0 = 2 nd 1 st T M 2 nd 1 st T M + 1 N × 0
115 xpundir 2 nd 1 st T M 2 nd 1 st T M + 1 N × 0 = 2 nd 1 st T M × 0 2 nd 1 st T M + 1 N × 0
116 114 115 eqtrdi φ 2 nd 1 st T M N × 0 = 2 nd 1 st T M × 0 2 nd 1 st T M + 1 N × 0
117 116 uneq2d φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M × 0 2 nd 1 st T M + 1 N × 0
118 un12 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M × 0 2 nd 1 st T M + 1 N × 0 = 2 nd 1 st T M × 0 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0
119 117 118 eqtrdi φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 = 2 nd 1 st T M × 0 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0
120 119 fveq1d φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 n = 2 nd 1 st T M × 0 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
121 120 ad2antrr φ n 2 nd 1 st T M n 1 N 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 n = 2 nd 1 st T M × 0 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
122 fnconstg 0 V 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T M + 1 N
123 37 122 ax-mp 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T M + 1 N
124 36 123 pm3.2i 2 nd 1 st T 1 M 1 × 1 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T M + 1 N
125 imain Fun 2 nd 1 st T -1 2 nd 1 st T 1 M 1 M + 1 N = 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N
126 43 125 syl φ 2 nd 1 st T 1 M 1 M + 1 N = 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N
127 75 zred φ M 1
128 peano2re M M + 1
129 47 128 syl φ M + 1
130 47 ltp1d φ M < M + 1
131 127 47 129 48 130 lttrd φ M 1 < M + 1
132 fzdisj M 1 < M + 1 1 M 1 M + 1 N =
133 131 132 syl φ 1 M 1 M + 1 N =
134 133 imaeq2d φ 2 nd 1 st T 1 M 1 M + 1 N = 2 nd 1 st T
135 134 52 eqtrdi φ 2 nd 1 st T 1 M 1 M + 1 N =
136 126 135 eqtr3d φ 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N =
137 fnun 2 nd 1 st T 1 M 1 × 1 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T M + 1 N 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N
138 124 136 137 sylancr φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N
139 imaundi 2 nd 1 st T 1 M 1 M + 1 N = 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N
140 imadif Fun 2 nd 1 st T -1 2 nd 1 st T 1 N M = 2 nd 1 st T 1 N 2 nd 1 st T M
141 43 140 syl φ 2 nd 1 st T 1 N M = 2 nd 1 st T 1 N 2 nd 1 st T M
142 fzsplit M 1 N 1 N = 1 M M + 1 N
143 27 142 syl φ 1 N = 1 M M + 1 N
144 143 difeq1d φ 1 N M = 1 M M + 1 N M
145 difundir 1 M M + 1 N M = 1 M M M + 1 N M
146 fzsplit2 M - 1 + 1 1 M M 1 1 M = 1 M 1 M - 1 + 1 M
147 73 79 146 syl2anc φ 1 M = 1 M 1 M - 1 + 1 M
148 59 oveq1d φ M - 1 + 1 M = M M
149 fzsn M M M = M
150 46 149 syl φ M M = M
151 148 150 eqtrd φ M - 1 + 1 M = M
152 151 uneq2d φ 1 M 1 M - 1 + 1 M = 1 M 1 M
153 147 152 eqtrd φ 1 M = 1 M 1 M
154 153 difeq1d φ 1 M M = 1 M 1 M M
155 difun2 1 M 1 M M = 1 M 1 M
156 127 47 ltnled φ M 1 < M ¬ M M 1
157 48 156 mpbid φ ¬ M M 1
158 elfzle2 M 1 M 1 M M 1
159 157 158 nsyl φ ¬ M 1 M 1
160 difsn ¬ M 1 M 1 1 M 1 M = 1 M 1
161 159 160 syl φ 1 M 1 M = 1 M 1
162 155 161 syl5eq φ 1 M 1 M M = 1 M 1
163 154 162 eqtrd φ 1 M M = 1 M 1
164 47 129 ltnled φ M < M + 1 ¬ M + 1 M
165 130 164 mpbid φ ¬ M + 1 M
166 elfzle1 M M + 1 N M + 1 M
167 165 166 nsyl φ ¬ M M + 1 N
168 difsn ¬ M M + 1 N M + 1 N M = M + 1 N
169 167 168 syl φ M + 1 N M = M + 1 N
170 163 169 uneq12d φ 1 M M M + 1 N M = 1 M 1 M + 1 N
171 145 170 syl5eq φ 1 M M + 1 N M = 1 M 1 M + 1 N
172 144 171 eqtrd φ 1 N M = 1 M 1 M + 1 N
173 172 imaeq2d φ 2 nd 1 st T 1 N M = 2 nd 1 st T 1 M 1 M + 1 N
174 111 eqcomd φ 2 nd 1 st T M = 2 nd 1 st T M
175 96 174 difeq12d φ 2 nd 1 st T 1 N 2 nd 1 st T M = 1 N 2 nd 1 st T M
176 141 173 175 3eqtr3d φ 2 nd 1 st T 1 M 1 M + 1 N = 1 N 2 nd 1 st T M
177 139 176 eqtr3id φ 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N = 1 N 2 nd 1 st T M
178 177 fneq2d φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M + 1 N 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N 2 nd 1 st T M
179 138 178 mpbid φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N 2 nd 1 st T M
180 eldifsn n 1 N 2 nd 1 st T M n 1 N n 2 nd 1 st T M
181 180 biimpri n 1 N n 2 nd 1 st T M n 1 N 2 nd 1 st T M
182 181 ancoms n 2 nd 1 st T M n 1 N n 1 N 2 nd 1 st T M
183 disjdif 2 nd 1 st T M 1 N 2 nd 1 st T M =
184 fnconstg 0 V 2 nd 1 st T M × 0 Fn 2 nd 1 st T M
185 37 184 ax-mp 2 nd 1 st T M × 0 Fn 2 nd 1 st T M
186 fvun2 2 nd 1 st T M × 0 Fn 2 nd 1 st T M 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N 2 nd 1 st T M 2 nd 1 st T M 1 N 2 nd 1 st T M = n 1 N 2 nd 1 st T M 2 nd 1 st T M × 0 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
187 185 186 mp3an1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N 2 nd 1 st T M 2 nd 1 st T M 1 N 2 nd 1 st T M = n 1 N 2 nd 1 st T M 2 nd 1 st T M × 0 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
188 183 187 mpanr1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N 2 nd 1 st T M n 1 N 2 nd 1 st T M 2 nd 1 st T M × 0 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
189 179 182 188 syl2an φ n 2 nd 1 st T M n 1 N 2 nd 1 st T M × 0 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
190 189 anassrs φ n 2 nd 1 st T M n 1 N 2 nd 1 st T M × 0 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
191 121 190 eqtrd φ n 2 nd 1 st T M n 1 N 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
192 33 100 101 101 102 103 191 ofval φ n 2 nd 1 st T M n 1 N 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 n = 1 st 1 st T n + 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
193 fnconstg 1 V 2 nd 1 st T 1 M × 1 Fn 2 nd 1 st T 1 M
194 34 193 ax-mp 2 nd 1 st T 1 M × 1 Fn 2 nd 1 st T 1 M
195 194 123 pm3.2i 2 nd 1 st T 1 M × 1 Fn 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T M + 1 N
196 imain Fun 2 nd 1 st T -1 2 nd 1 st T 1 M M + 1 N = 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N
197 43 196 syl φ 2 nd 1 st T 1 M M + 1 N = 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N
198 fzdisj M < M + 1 1 M M + 1 N =
199 130 198 syl φ 1 M M + 1 N =
200 199 imaeq2d φ 2 nd 1 st T 1 M M + 1 N = 2 nd 1 st T
201 200 52 eqtrdi φ 2 nd 1 st T 1 M M + 1 N =
202 197 201 eqtr3d φ 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N =
203 fnun 2 nd 1 st T 1 M × 1 Fn 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T M + 1 N 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N = 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N
204 195 202 203 sylancr φ 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N
205 143 imaeq2d φ 2 nd 1 st T 1 N = 2 nd 1 st T 1 M M + 1 N
206 imaundi 2 nd 1 st T 1 M M + 1 N = 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N
207 205 206 eqtrdi φ 2 nd 1 st T 1 N = 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N
208 207 96 eqtr3d φ 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N = 1 N
209 208 fneq2d φ 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N
210 204 209 mpbid φ 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N
211 210 adantr φ n 2 nd 1 st T M 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N
212 imaundi 2 nd 1 st T 1 M 1 M = 2 nd 1 st T 1 M 1 2 nd 1 st T M
213 153 imaeq2d φ 2 nd 1 st T 1 M = 2 nd 1 st T 1 M 1 M
214 111 uneq2d φ 2 nd 1 st T 1 M 1 2 nd 1 st T M = 2 nd 1 st T 1 M 1 2 nd 1 st T M
215 212 213 214 3eqtr4a φ 2 nd 1 st T 1 M = 2 nd 1 st T 1 M 1 2 nd 1 st T M
216 215 xpeq1d φ 2 nd 1 st T 1 M × 1 = 2 nd 1 st T 1 M 1 2 nd 1 st T M × 1
217 xpundir 2 nd 1 st T 1 M 1 2 nd 1 st T M × 1 = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M × 1
218 216 217 eqtrdi φ 2 nd 1 st T 1 M × 1 = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M × 1
219 218 uneq1d φ 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M × 1 2 nd 1 st T M + 1 N × 0
220 un23 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M × 1 2 nd 1 st T M + 1 N × 0 = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 2 nd 1 st T M × 1
221 220 equncomi 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M × 1 2 nd 1 st T M + 1 N × 0 = 2 nd 1 st T M × 1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0
222 219 221 eqtrdi φ 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 = 2 nd 1 st T M × 1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0
223 222 fveq1d φ 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T M × 1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
224 223 ad2antrr φ n 2 nd 1 st T M n 1 N 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T M × 1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
225 fnconstg 1 V 2 nd 1 st T M × 1 Fn 2 nd 1 st T M
226 34 225 ax-mp 2 nd 1 st T M × 1 Fn 2 nd 1 st T M
227 fvun2 2 nd 1 st T M × 1 Fn 2 nd 1 st T M 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N 2 nd 1 st T M 2 nd 1 st T M 1 N 2 nd 1 st T M = n 1 N 2 nd 1 st T M 2 nd 1 st T M × 1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
228 226 227 mp3an1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N 2 nd 1 st T M 2 nd 1 st T M 1 N 2 nd 1 st T M = n 1 N 2 nd 1 st T M 2 nd 1 st T M × 1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
229 183 228 mpanr1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N 2 nd 1 st T M n 1 N 2 nd 1 st T M 2 nd 1 st T M × 1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
230 179 182 229 syl2an φ n 2 nd 1 st T M n 1 N 2 nd 1 st T M × 1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
231 230 anassrs φ n 2 nd 1 st T M n 1 N 2 nd 1 st T M × 1 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
232 224 231 eqtrd φ n 2 nd 1 st T M n 1 N 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 n = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
233 33 211 101 101 102 103 232 ofval φ n 2 nd 1 st T M n 1 N 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 n = 1 st 1 st T n + 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M + 1 N × 0 n
234 192 233 eqtr4d φ n 2 nd 1 st T M n 1 N 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 n = 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 n
235 234 an32s φ n 1 N n 2 nd 1 st T M 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 n = 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 n
236 235 anasss φ n 1 N n 2 nd 1 st T M 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 n = 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 n
237 fveq2 t = T 2 nd t = 2 nd T
238 237 breq2d t = T y < 2 nd t y < 2 nd T
239 238 ifbid t = T if y < 2 nd t y y + 1 = if y < 2 nd T y y + 1
240 239 csbeq1d 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
241 2fveq3 t = T 1 st 1 st t = 1 st 1 st T
242 2fveq3 t = T 2 nd 1 st t = 2 nd 1 st T
243 242 imaeq1d t = T 2 nd 1 st t 1 j = 2 nd 1 st T 1 j
244 243 xpeq1d t = T 2 nd 1 st t 1 j × 1 = 2 nd 1 st T 1 j × 1
245 242 imaeq1d t = T 2 nd 1 st t j + 1 N = 2 nd 1 st T j + 1 N
246 245 xpeq1d t = T 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T j + 1 N × 0
247 244 246 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
248 241 247 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
249 248 csbeq2dv 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
250 240 249 eqtrd 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
251 250 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
252 251 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
253 252 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
254 253 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
255 3 254 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
256 breq1 y = M 2 y < 2 nd T M 2 < 2 nd T
257 256 adantl φ y = M 2 y < 2 nd T M 2 < 2 nd T
258 oveq1 y = M 2 y + 1 = M - 2 + 1
259 sub1m1 M M - 1 - 1 = M 2
260 57 259 syl φ M - 1 - 1 = M 2
261 260 oveq1d φ M 1 - 1 + 1 = M - 2 + 1
262 75 zcnd φ M 1
263 npcan1 M 1 M 1 - 1 + 1 = M 1
264 262 263 syl φ M 1 - 1 + 1 = M 1
265 261 264 eqtr3d φ M - 2 + 1 = M 1
266 258 265 sylan9eqr φ y = M 2 y + 1 = M 1
267 257 266 ifbieq2d φ y = M 2 if y < 2 nd T y y + 1 = if M 2 < 2 nd T y M 1
268 20 nncnd φ 2 nd T
269 add1p1 2 nd T 2 nd T + 1 + 1 = 2 nd T + 2
270 268 269 syl φ 2 nd T + 1 + 1 = 2 nd T + 2
271 270 67 eqbrtrrd φ 2 nd T + 2 M
272 20 nnred φ 2 nd T
273 2re 2
274 leaddsub 2 nd T 2 M 2 nd T + 2 M 2 nd T M 2
275 273 274 mp3an2 2 nd T M 2 nd T + 2 M 2 nd T M 2
276 272 47 275 syl2anc φ 2 nd T + 2 M 2 nd T M 2
277 60 47 posdifd φ 1 < M 0 < M 1
278 68 277 mpbid φ 0 < M 1
279 elnnz M 1 M 1 0 < M 1
280 75 278 279 sylanbrc φ M 1
281 nnm1nn0 M 1 M - 1 - 1 0
282 280 281 syl φ M - 1 - 1 0
283 260 282 eqeltrrd φ M 2 0
284 283 nn0red φ M 2
285 272 284 lenltd φ 2 nd T M 2 ¬ M 2 < 2 nd T
286 276 285 bitrd φ 2 nd T + 2 M ¬ M 2 < 2 nd T
287 271 286 mpbid φ ¬ M 2 < 2 nd T
288 287 iffalsed φ if M 2 < 2 nd T y M 1 = M 1
289 288 adantr φ y = M 2 if M 2 < 2 nd T y M 1 = M 1
290 267 289 eqtrd φ y = M 2 if y < 2 nd T y y + 1 = M 1
291 290 csbeq1d φ y = M 2 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 = M 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
292 oveq2 j = M 1 1 j = 1 M 1
293 292 imaeq2d j = M 1 2 nd 1 st T 1 j = 2 nd 1 st T 1 M 1
294 293 xpeq1d j = M 1 2 nd 1 st T 1 j × 1 = 2 nd 1 st T 1 M 1 × 1
295 294 adantl φ j = M 1 2 nd 1 st T 1 j × 1 = 2 nd 1 st T 1 M 1 × 1
296 oveq1 j = M 1 j + 1 = M - 1 + 1
297 296 59 sylan9eqr φ j = M 1 j + 1 = M
298 297 oveq1d φ j = M 1 j + 1 N = M N
299 298 imaeq2d φ j = M 1 2 nd 1 st T j + 1 N = 2 nd 1 st T M N
300 299 xpeq1d φ j = M 1 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T M N × 0
301 295 300 uneq12d φ j = M 1 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0
302 301 oveq2d φ j = M 1 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 M 1 × 1 2 nd 1 st T M N × 0
303 75 302 csbied φ M 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 M 1 × 1 2 nd 1 st T M N × 0
304 303 adantr φ y = M 2 M 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 M 1 × 1 2 nd 1 st T M N × 0
305 291 304 eqtrd φ y = M 2 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 M 1 × 1 2 nd 1 st T M N × 0
306 nnm1nn0 N N 1 0
307 1 306 syl φ N 1 0
308 1 nnred φ N
309 47 lem1d φ M 1 M
310 elfzle2 M 2 nd T + 1 + 1 N M N
311 5 310 syl φ M N
312 127 47 308 309 311 letrd φ M 1 N
313 127 308 60 312 lesub1dd φ M - 1 - 1 N 1
314 260 313 eqbrtrrd φ M 2 N 1
315 elfz2nn0 M 2 0 N 1 M 2 0 N 1 0 M 2 N 1
316 283 307 314 315 syl3anbrc φ M 2 0 N 1
317 ovexd φ 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 V
318 255 305 316 317 fvmptd φ F M 2 = 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0
319 318 fveq1d φ F M 2 n = 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 n
320 319 adantr φ n 1 N n 2 nd 1 st T M F M 2 n = 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 n
321 breq1 y = M 1 y < 2 nd T M 1 < 2 nd T
322 321 adantl φ y = M 1 y < 2 nd T M 1 < 2 nd T
323 oveq1 y = M 1 y + 1 = M - 1 + 1
324 323 59 sylan9eqr φ y = M 1 y + 1 = M
325 322 324 ifbieq2d φ y = M 1 if y < 2 nd T y y + 1 = if M 1 < 2 nd T y M
326 62 lep1d φ 2 nd T + 1 2 nd T + 1 + 1
327 62 61 47 326 67 letrd φ 2 nd T + 1 M
328 1re 1
329 leaddsub 2 nd T 1 M 2 nd T + 1 M 2 nd T M 1
330 328 329 mp3an2 2 nd T M 2 nd T + 1 M 2 nd T M 1
331 272 47 330 syl2anc φ 2 nd T + 1 M 2 nd T M 1
332 272 127 lenltd φ 2 nd T M 1 ¬ M 1 < 2 nd T
333 331 332 bitrd φ 2 nd T + 1 M ¬ M 1 < 2 nd T
334 327 333 mpbid φ ¬ M 1 < 2 nd T
335 334 iffalsed φ if M 1 < 2 nd T y M = M
336 335 adantr φ y = M 1 if M 1 < 2 nd T y M = M
337 325 336 eqtrd φ y = M 1 if y < 2 nd T y y + 1 = M
338 337 csbeq1d φ y = M 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 = M / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
339 oveq2 j = M 1 j = 1 M
340 339 imaeq2d j = M 2 nd 1 st T 1 j = 2 nd 1 st T 1 M
341 340 xpeq1d j = M 2 nd 1 st T 1 j × 1 = 2 nd 1 st T 1 M × 1
342 oveq1 j = M j + 1 = M + 1
343 342 oveq1d j = M j + 1 N = M + 1 N
344 343 imaeq2d j = M 2 nd 1 st T j + 1 N = 2 nd 1 st T M + 1 N
345 344 xpeq1d j = M 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T M + 1 N × 0
346 341 345 uneq12d j = M 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0
347 346 oveq2d j = M 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 M × 1 2 nd 1 st T M + 1 N × 0
348 347 adantl φ j = M 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 M × 1 2 nd 1 st T M + 1 N × 0
349 5 348 csbied φ M / 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 M × 1 2 nd 1 st T M + 1 N × 0
350 349 adantr φ y = M 1 M / 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 M × 1 2 nd 1 st T M + 1 N × 0
351 338 350 eqtrd φ y = M 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 M × 1 2 nd 1 st T M + 1 N × 0
352 280 nnnn0d φ M 1 0
353 47 308 60 311 lesub1dd φ M 1 N 1
354 elfz2nn0 M 1 0 N 1 M 1 0 N 1 0 M 1 N 1
355 352 307 353 354 syl3anbrc φ M 1 0 N 1
356 ovexd φ 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 V
357 255 351 355 356 fvmptd φ F M 1 = 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0
358 357 fveq1d φ F M 1 n = 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 n
359 358 adantr φ n 1 N n 2 nd 1 st T M F M 1 n = 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 n
360 236 320 359 3eqtr4d φ n 1 N n 2 nd 1 st T M F M 2 n = F M 1 n
361 360 expr φ n 1 N n 2 nd 1 st T M F M 2 n = F M 1 n
362 361 necon1d φ n 1 N F M 2 n F M 1 n n = 2 nd 1 st T M
363 elmapi 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T : 1 N 0 ..^ K
364 30 363 syl φ 1 st 1 st T : 1 N 0 ..^ K
365 364 28 ffvelrnd φ 1 st 1 st T 2 nd 1 st T M 0 ..^ K
366 elfzonn0 1 st 1 st T 2 nd 1 st T M 0 ..^ K 1 st 1 st T 2 nd 1 st T M 0
367 365 366 syl φ 1 st 1 st T 2 nd 1 st T M 0
368 367 nn0red φ 1 st 1 st T 2 nd 1 st T M
369 368 ltp1d φ 1 st 1 st T 2 nd 1 st T M < 1 st 1 st T 2 nd 1 st T M + 1
370 368 369 ltned φ 1 st 1 st T 2 nd 1 st T M 1 st 1 st T 2 nd 1 st T M + 1
371 318 fveq1d φ F M 2 2 nd 1 st T M = 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 2 nd 1 st T M
372 ovexd φ 1 N V
373 eqidd φ 2 nd 1 st T M 1 N 1 st 1 st T 2 nd 1 st T M = 1 st 1 st T 2 nd 1 st T M
374 fzss1 M 1 M N 1 N
375 72 374 syl φ M N 1 N
376 eluzfz1 N M M M N
377 83 376 syl φ M M N
378 fnfvima 2 nd 1 st T Fn 1 N M N 1 N M M N 2 nd 1 st T M 2 nd 1 st T M N
379 109 375 377 378 syl3anc φ 2 nd 1 st T M 2 nd 1 st T M N
380 fvun2 2 nd 1 st T 1 M 1 × 1 Fn 2 nd 1 st T 1 M 1 2 nd 1 st T M N × 0 Fn 2 nd 1 st T M N 2 nd 1 st T 1 M 1 2 nd 1 st T M N = 2 nd 1 st T M 2 nd 1 st T M N 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 2 nd 1 st T M = 2 nd 1 st T M N × 0 2 nd 1 st T M
381 36 39 380 mp3an12 2 nd 1 st T 1 M 1 2 nd 1 st T M N = 2 nd 1 st T M 2 nd 1 st T M N 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 2 nd 1 st T M = 2 nd 1 st T M N × 0 2 nd 1 st T M
382 54 379 381 syl2anc φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 2 nd 1 st T M = 2 nd 1 st T M N × 0 2 nd 1 st T M
383 37 fvconst2 2 nd 1 st T M 2 nd 1 st T M N 2 nd 1 st T M N × 0 2 nd 1 st T M = 0
384 379 383 syl φ 2 nd 1 st T M N × 0 2 nd 1 st T M = 0
385 382 384 eqtrd φ 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 2 nd 1 st T M = 0
386 385 adantr φ 2 nd 1 st T M 1 N 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 2 nd 1 st T M = 0
387 32 99 372 372 102 373 386 ofval φ 2 nd 1 st T M 1 N 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 2 nd 1 st T M = 1 st 1 st T 2 nd 1 st T M + 0
388 28 387 mpdan φ 1 st 1 st T + f 2 nd 1 st T 1 M 1 × 1 2 nd 1 st T M N × 0 2 nd 1 st T M = 1 st 1 st T 2 nd 1 st T M + 0
389 367 nn0cnd φ 1 st 1 st T 2 nd 1 st T M
390 389 addid1d φ 1 st 1 st T 2 nd 1 st T M + 0 = 1 st 1 st T 2 nd 1 st T M
391 371 388 390 3eqtrd φ F M 2 2 nd 1 st T M = 1 st 1 st T 2 nd 1 st T M
392 357 fveq1d φ F M 1 2 nd 1 st T M = 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 2 nd 1 st T M
393 fzss2 N M 1 M 1 N
394 83 393 syl φ 1 M 1 N
395 elfz1end M M 1 M
396 71 395 sylib φ M 1 M
397 fnfvima 2 nd 1 st T Fn 1 N 1 M 1 N M 1 M 2 nd 1 st T M 2 nd 1 st T 1 M
398 109 394 396 397 syl3anc φ 2 nd 1 st T M 2 nd 1 st T 1 M
399 fvun1 2 nd 1 st T 1 M × 1 Fn 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T M + 1 N 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N = 2 nd 1 st T M 2 nd 1 st T 1 M 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 2 nd 1 st T M = 2 nd 1 st T 1 M × 1 2 nd 1 st T M
400 194 123 399 mp3an12 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N = 2 nd 1 st T M 2 nd 1 st T 1 M 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 2 nd 1 st T M = 2 nd 1 st T 1 M × 1 2 nd 1 st T M
401 202 398 400 syl2anc φ 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 2 nd 1 st T M = 2 nd 1 st T 1 M × 1 2 nd 1 st T M
402 34 fvconst2 2 nd 1 st T M 2 nd 1 st T 1 M 2 nd 1 st T 1 M × 1 2 nd 1 st T M = 1
403 398 402 syl φ 2 nd 1 st T 1 M × 1 2 nd 1 st T M = 1
404 401 403 eqtrd φ 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 2 nd 1 st T M = 1
405 404 adantr φ 2 nd 1 st T M 1 N 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 2 nd 1 st T M = 1
406 32 210 372 372 102 373 405 ofval φ 2 nd 1 st T M 1 N 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 2 nd 1 st T M = 1 st 1 st T 2 nd 1 st T M + 1
407 28 406 mpdan φ 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 2 nd 1 st T M = 1 st 1 st T 2 nd 1 st T M + 1
408 392 407 eqtrd φ F M 1 2 nd 1 st T M = 1 st 1 st T 2 nd 1 st T M + 1
409 370 391 408 3netr4d φ F M 2 2 nd 1 st T M F M 1 2 nd 1 st T M
410 fveq2 n = 2 nd 1 st T M F M 2 n = F M 2 2 nd 1 st T M
411 fveq2 n = 2 nd 1 st T M F M 1 n = F M 1 2 nd 1 st T M
412 410 411 neeq12d n = 2 nd 1 st T M F M 2 n F M 1 n F M 2 2 nd 1 st T M F M 1 2 nd 1 st T M
413 409 412 syl5ibrcom φ n = 2 nd 1 st T M F M 2 n F M 1 n
414 413 adantr φ n 1 N n = 2 nd 1 st T M F M 2 n F M 1 n
415 362 414 impbid φ n 1 N F M 2 n F M 1 n n = 2 nd 1 st T M
416 28 415 riota5 φ ι n 1 N | F M 2 n F M 1 n = 2 nd 1 st T M