Metamath Proof Explorer


Theorem poimirlem8

Description: Lemma for poimir , establishing that away from the opposite vertex the walks in poimirlem9 yield the same vertices. (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
poimirlem9.3 φ U S
Assertion poimirlem8 φ 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N 2 nd T 2 nd T + 1

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 poimirlem9.3 φ U S
6 elrabi U 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 U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
7 6 2 eleq2s U S U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
8 5 7 syl φ U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
9 xp1st U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
10 8 9 syl φ 1 st U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
11 xp2nd 1 st U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st U f | f : 1 N 1-1 onto 1 N
12 10 11 syl φ 2 nd 1 st U f | f : 1 N 1-1 onto 1 N
13 fvex 2 nd 1 st U V
14 f1oeq1 f = 2 nd 1 st U f : 1 N 1-1 onto 1 N 2 nd 1 st U : 1 N 1-1 onto 1 N
15 13 14 elab 2 nd 1 st U f | f : 1 N 1-1 onto 1 N 2 nd 1 st U : 1 N 1-1 onto 1 N
16 12 15 sylib φ 2 nd 1 st U : 1 N 1-1 onto 1 N
17 f1ofn 2 nd 1 st U : 1 N 1-1 onto 1 N 2 nd 1 st U Fn 1 N
18 16 17 syl φ 2 nd 1 st U Fn 1 N
19 difss 1 N 2 nd T 2 nd T + 1 1 N
20 fnssres 2 nd 1 st U Fn 1 N 1 N 2 nd T 2 nd T + 1 1 N 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 Fn 1 N 2 nd T 2 nd T + 1
21 18 19 20 sylancl φ 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 Fn 1 N 2 nd T 2 nd T + 1
22 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
23 22 2 eleq2s T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
24 3 23 syl φ T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
25 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
26 24 25 syl φ 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
27 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
28 26 27 syl φ 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
29 fvex 2 nd 1 st T V
30 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
31 29 30 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
32 28 31 sylib φ 2 nd 1 st T : 1 N 1-1 onto 1 N
33 f1ofn 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T Fn 1 N
34 32 33 syl φ 2 nd 1 st T Fn 1 N
35 fnssres 2 nd 1 st T Fn 1 N 1 N 2 nd T 2 nd T + 1 1 N 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 Fn 1 N 2 nd T 2 nd T + 1
36 34 19 35 sylancl φ 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 Fn 1 N 2 nd T 2 nd T + 1
37 fzp1elp1 2 nd T 1 N 1 2 nd T + 1 1 N - 1 + 1
38 4 37 syl φ 2 nd T + 1 1 N - 1 + 1
39 1 nncnd φ N
40 npcan1 N N - 1 + 1 = N
41 39 40 syl φ N - 1 + 1 = N
42 41 oveq2d φ 1 N - 1 + 1 = 1 N
43 38 42 eleqtrd φ 2 nd T + 1 1 N
44 fzsplit 2 nd T + 1 1 N 1 N = 1 2 nd T + 1 2 nd T + 1 + 1 N
45 43 44 syl φ 1 N = 1 2 nd T + 1 2 nd T + 1 + 1 N
46 45 difeq1d φ 1 N 2 nd T 2 nd T + 1 = 1 2 nd T + 1 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1
47 difundir 1 2 nd T + 1 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1 = 1 2 nd T + 1 2 nd T 2 nd T + 1 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1
48 elfznn 2 nd T 1 N 1 2 nd T
49 4 48 syl φ 2 nd T
50 49 nncnd φ 2 nd T
51 npcan1 2 nd T 2 nd T - 1 + 1 = 2 nd T
52 50 51 syl φ 2 nd T - 1 + 1 = 2 nd T
53 nnuz = 1
54 49 53 eleqtrdi φ 2 nd T 1
55 52 54 eqeltrd φ 2 nd T - 1 + 1 1
56 49 nnzd φ 2 nd T
57 peano2zm 2 nd T 2 nd T 1
58 56 57 syl φ 2 nd T 1
59 uzid 2 nd T 1 2 nd T 1 2 nd T 1
60 peano2uz 2 nd T 1 2 nd T 1 2 nd T - 1 + 1 2 nd T 1
61 58 59 60 3syl φ 2 nd T - 1 + 1 2 nd T 1
62 52 61 eqeltrrd φ 2 nd T 2 nd T 1
63 peano2uz 2 nd T 2 nd T 1 2 nd T + 1 2 nd T 1
64 62 63 syl φ 2 nd T + 1 2 nd T 1
65 fzsplit2 2 nd T - 1 + 1 1 2 nd T + 1 2 nd T 1 1 2 nd T + 1 = 1 2 nd T 1 2 nd T - 1 + 1 2 nd T + 1
66 55 64 65 syl2anc φ 1 2 nd T + 1 = 1 2 nd T 1 2 nd T - 1 + 1 2 nd T + 1
67 52 oveq1d φ 2 nd T - 1 + 1 2 nd T + 1 = 2 nd T 2 nd T + 1
68 fzpr 2 nd T 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1
69 56 68 syl φ 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1
70 67 69 eqtrd φ 2 nd T - 1 + 1 2 nd T + 1 = 2 nd T 2 nd T + 1
71 70 uneq2d φ 1 2 nd T 1 2 nd T - 1 + 1 2 nd T + 1 = 1 2 nd T 1 2 nd T 2 nd T + 1
72 66 71 eqtrd φ 1 2 nd T + 1 = 1 2 nd T 1 2 nd T 2 nd T + 1
73 72 difeq1d φ 1 2 nd T + 1 2 nd T 2 nd T + 1 = 1 2 nd T 1 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1
74 49 nnred φ 2 nd T
75 74 ltm1d φ 2 nd T 1 < 2 nd T
76 58 zred φ 2 nd T 1
77 76 74 ltnled φ 2 nd T 1 < 2 nd T ¬ 2 nd T 2 nd T 1
78 75 77 mpbid φ ¬ 2 nd T 2 nd T 1
79 elfzle2 2 nd T 1 2 nd T 1 2 nd T 2 nd T 1
80 78 79 nsyl φ ¬ 2 nd T 1 2 nd T 1
81 difsn ¬ 2 nd T 1 2 nd T 1 1 2 nd T 1 2 nd T = 1 2 nd T 1
82 80 81 syl φ 1 2 nd T 1 2 nd T = 1 2 nd T 1
83 peano2re 2 nd T 2 nd T + 1
84 74 83 syl φ 2 nd T + 1
85 74 ltp1d φ 2 nd T < 2 nd T + 1
86 76 74 84 75 85 lttrd φ 2 nd T 1 < 2 nd T + 1
87 76 84 ltnled φ 2 nd T 1 < 2 nd T + 1 ¬ 2 nd T + 1 2 nd T 1
88 86 87 mpbid φ ¬ 2 nd T + 1 2 nd T 1
89 elfzle2 2 nd T + 1 1 2 nd T 1 2 nd T + 1 2 nd T 1
90 88 89 nsyl φ ¬ 2 nd T + 1 1 2 nd T 1
91 difsn ¬ 2 nd T + 1 1 2 nd T 1 1 2 nd T 1 2 nd T + 1 = 1 2 nd T 1
92 90 91 syl φ 1 2 nd T 1 2 nd T + 1 = 1 2 nd T 1
93 82 92 ineq12d φ 1 2 nd T 1 2 nd T 1 2 nd T 1 2 nd T + 1 = 1 2 nd T 1 1 2 nd T 1
94 difun2 1 2 nd T 1 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 = 1 2 nd T 1 2 nd T 2 nd T + 1
95 df-pr 2 nd T 2 nd T + 1 = 2 nd T 2 nd T + 1
96 95 difeq2i 1 2 nd T 1 2 nd T 2 nd T + 1 = 1 2 nd T 1 2 nd T 2 nd T + 1
97 difundi 1 2 nd T 1 2 nd T 2 nd T + 1 = 1 2 nd T 1 2 nd T 1 2 nd T 1 2 nd T + 1
98 94 96 97 3eqtrri 1 2 nd T 1 2 nd T 1 2 nd T 1 2 nd T + 1 = 1 2 nd T 1 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1
99 inidm 1 2 nd T 1 1 2 nd T 1 = 1 2 nd T 1
100 93 98 99 3eqtr3g φ 1 2 nd T 1 2 nd T 2 nd T + 1 2 nd T 2 nd T + 1 = 1 2 nd T 1
101 73 100 eqtrd φ 1 2 nd T + 1 2 nd T 2 nd T + 1 = 1 2 nd T 1
102 peano2re 2 nd T + 1 2 nd T + 1 + 1
103 84 102 syl φ 2 nd T + 1 + 1
104 84 ltp1d φ 2 nd T + 1 < 2 nd T + 1 + 1
105 74 84 103 85 104 lttrd φ 2 nd T < 2 nd T + 1 + 1
106 74 103 ltnled φ 2 nd T < 2 nd T + 1 + 1 ¬ 2 nd T + 1 + 1 2 nd T
107 105 106 mpbid φ ¬ 2 nd T + 1 + 1 2 nd T
108 elfzle1 2 nd T 2 nd T + 1 + 1 N 2 nd T + 1 + 1 2 nd T
109 107 108 nsyl φ ¬ 2 nd T 2 nd T + 1 + 1 N
110 difsn ¬ 2 nd T 2 nd T + 1 + 1 N 2 nd T + 1 + 1 N 2 nd T = 2 nd T + 1 + 1 N
111 109 110 syl φ 2 nd T + 1 + 1 N 2 nd T = 2 nd T + 1 + 1 N
112 84 103 ltnled φ 2 nd T + 1 < 2 nd T + 1 + 1 ¬ 2 nd T + 1 + 1 2 nd T + 1
113 104 112 mpbid φ ¬ 2 nd T + 1 + 1 2 nd T + 1
114 elfzle1 2 nd T + 1 2 nd T + 1 + 1 N 2 nd T + 1 + 1 2 nd T + 1
115 113 114 nsyl φ ¬ 2 nd T + 1 2 nd T + 1 + 1 N
116 difsn ¬ 2 nd T + 1 2 nd T + 1 + 1 N 2 nd T + 1 + 1 N 2 nd T + 1 = 2 nd T + 1 + 1 N
117 115 116 syl φ 2 nd T + 1 + 1 N 2 nd T + 1 = 2 nd T + 1 + 1 N
118 111 117 ineq12d φ 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1 + 1 N 2 nd T + 1 = 2 nd T + 1 + 1 N 2 nd T + 1 + 1 N
119 95 difeq2i 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1 = 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1
120 difundi 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1 = 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1 + 1 N 2 nd T + 1
121 119 120 eqtr2i 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1 + 1 N 2 nd T + 1 = 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1
122 inidm 2 nd T + 1 + 1 N 2 nd T + 1 + 1 N = 2 nd T + 1 + 1 N
123 118 121 122 3eqtr3g φ 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1 = 2 nd T + 1 + 1 N
124 101 123 uneq12d φ 1 2 nd T + 1 2 nd T 2 nd T + 1 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1 = 1 2 nd T 1 2 nd T + 1 + 1 N
125 47 124 syl5eq φ 1 2 nd T + 1 2 nd T + 1 + 1 N 2 nd T 2 nd T + 1 = 1 2 nd T 1 2 nd T + 1 + 1 N
126 46 125 eqtrd φ 1 N 2 nd T 2 nd T + 1 = 1 2 nd T 1 2 nd T + 1 + 1 N
127 126 eleq2d φ k 1 N 2 nd T 2 nd T + 1 k 1 2 nd T 1 2 nd T + 1 + 1 N
128 elun k 1 2 nd T 1 2 nd T + 1 + 1 N k 1 2 nd T 1 k 2 nd T + 1 + 1 N
129 127 128 bitrdi φ k 1 N 2 nd T 2 nd T + 1 k 1 2 nd T 1 k 2 nd T + 1 + 1 N
130 129 biimpa φ k 1 N 2 nd T 2 nd T + 1 k 1 2 nd T 1 k 2 nd T + 1 + 1 N
131 fveq2 t = T 2 nd t = 2 nd T
132 131 breq2d t = T y < 2 nd t y < 2 nd T
133 132 ifbid t = T if y < 2 nd t y y + 1 = if y < 2 nd T y y + 1
134 133 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
135 2fveq3 t = T 1 st 1 st t = 1 st 1 st T
136 2fveq3 t = T 2 nd 1 st t = 2 nd 1 st T
137 136 imaeq1d t = T 2 nd 1 st t 1 j = 2 nd 1 st T 1 j
138 137 xpeq1d t = T 2 nd 1 st t 1 j × 1 = 2 nd 1 st T 1 j × 1
139 136 imaeq1d t = T 2 nd 1 st t j + 1 N = 2 nd 1 st T j + 1 N
140 139 xpeq1d t = T 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T j + 1 N × 0
141 138 140 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
142 135 141 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
143 142 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
144 134 143 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
145 144 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
146 145 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
147 146 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
148 147 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
149 3 148 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
150 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
151 26 150 syl φ 1 st 1 st T 0 ..^ K 1 N
152 elmapi 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T : 1 N 0 ..^ K
153 151 152 syl φ 1 st 1 st T : 1 N 0 ..^ K
154 elfzoelz n 0 ..^ K n
155 154 ssriv 0 ..^ K
156 fss 1 st 1 st T : 1 N 0 ..^ K 0 ..^ K 1 st 1 st T : 1 N
157 153 155 156 sylancl φ 1 st 1 st T : 1 N
158 1 149 157 32 4 poimirlem1 φ ¬ * n 1 N F 2 nd T 1 n F 2 nd T n
159 1 adantr φ 2 nd U 2 nd T N
160 fveq2 t = U 2 nd t = 2 nd U
161 160 breq2d t = U y < 2 nd t y < 2 nd U
162 161 ifbid t = U if y < 2 nd t y y + 1 = if y < 2 nd U y y + 1
163 162 csbeq1d t = U 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 U 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
164 2fveq3 t = U 1 st 1 st t = 1 st 1 st U
165 2fveq3 t = U 2 nd 1 st t = 2 nd 1 st U
166 165 imaeq1d t = U 2 nd 1 st t 1 j = 2 nd 1 st U 1 j
167 166 xpeq1d t = U 2 nd 1 st t 1 j × 1 = 2 nd 1 st U 1 j × 1
168 165 imaeq1d t = U 2 nd 1 st t j + 1 N = 2 nd 1 st U j + 1 N
169 168 xpeq1d t = U 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st U j + 1 N × 0
170 167 169 uneq12d t = U 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
171 164 170 oveq12d t = U 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 U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
172 171 csbeq2dv t = U if y < 2 nd U 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 U y y + 1 / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
173 163 172 eqtrd t = U 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 U y y + 1 / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
174 173 mpteq2dv t = U 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 U y y + 1 / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
175 174 eqeq2d t = U 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 U y y + 1 / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
176 175 2 elrab2 U S U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N F = y 0 N 1 if y < 2 nd U y y + 1 / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
177 176 simprbi U S F = y 0 N 1 if y < 2 nd U y y + 1 / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
178 5 177 syl φ F = y 0 N 1 if y < 2 nd U y y + 1 / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
179 178 adantr φ 2 nd U 2 nd T F = y 0 N 1 if y < 2 nd U y y + 1 / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
180 xp1st 1 st U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st 1 st U 0 ..^ K 1 N
181 10 180 syl φ 1 st 1 st U 0 ..^ K 1 N
182 elmapi 1 st 1 st U 0 ..^ K 1 N 1 st 1 st U : 1 N 0 ..^ K
183 181 182 syl φ 1 st 1 st U : 1 N 0 ..^ K
184 fss 1 st 1 st U : 1 N 0 ..^ K 0 ..^ K 1 st 1 st U : 1 N
185 183 155 184 sylancl φ 1 st 1 st U : 1 N
186 185 adantr φ 2 nd U 2 nd T 1 st 1 st U : 1 N
187 16 adantr φ 2 nd U 2 nd T 2 nd 1 st U : 1 N 1-1 onto 1 N
188 4 adantr φ 2 nd U 2 nd T 2 nd T 1 N 1
189 xp2nd U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd U 0 N
190 8 189 syl φ 2 nd U 0 N
191 eldifsn 2 nd U 0 N 2 nd T 2 nd U 0 N 2 nd U 2 nd T
192 191 biimpri 2 nd U 0 N 2 nd U 2 nd T 2 nd U 0 N 2 nd T
193 190 192 sylan φ 2 nd U 2 nd T 2 nd U 0 N 2 nd T
194 159 179 186 187 188 193 poimirlem2 φ 2 nd U 2 nd T * n 1 N F 2 nd T 1 n F 2 nd T n
195 194 ex φ 2 nd U 2 nd T * n 1 N F 2 nd T 1 n F 2 nd T n
196 195 necon1bd φ ¬ * n 1 N F 2 nd T 1 n F 2 nd T n 2 nd U = 2 nd T
197 158 196 mpd φ 2 nd U = 2 nd T
198 197 oveq1d φ 2 nd U 1 = 2 nd T 1
199 198 oveq2d φ 1 2 nd U 1 = 1 2 nd T 1
200 199 eleq2d φ k 1 2 nd U 1 k 1 2 nd T 1
201 200 biimpar φ k 1 2 nd T 1 k 1 2 nd U 1
202 1 adantr φ k 1 2 nd U 1 N
203 5 adantr φ k 1 2 nd U 1 U S
204 197 4 eqeltrd φ 2 nd U 1 N 1
205 204 adantr φ k 1 2 nd U 1 2 nd U 1 N 1
206 simpr φ k 1 2 nd U 1 k 1 2 nd U 1
207 202 2 203 205 206 poimirlem6 φ k 1 2 nd U 1 ι n 1 N | F k 1 n F k n = 2 nd 1 st U k
208 201 207 syldan φ k 1 2 nd T 1 ι n 1 N | F k 1 n F k n = 2 nd 1 st U k
209 1 adantr φ k 1 2 nd T 1 N
210 3 adantr φ k 1 2 nd T 1 T S
211 4 adantr φ k 1 2 nd T 1 2 nd T 1 N 1
212 simpr φ k 1 2 nd T 1 k 1 2 nd T 1
213 209 2 210 211 212 poimirlem6 φ k 1 2 nd T 1 ι n 1 N | F k 1 n F k n = 2 nd 1 st T k
214 208 213 eqtr3d φ k 1 2 nd T 1 2 nd 1 st U k = 2 nd 1 st T k
215 197 oveq1d φ 2 nd U + 1 = 2 nd T + 1
216 215 oveq1d φ 2 nd U + 1 + 1 = 2 nd T + 1 + 1
217 216 oveq1d φ 2 nd U + 1 + 1 N = 2 nd T + 1 + 1 N
218 217 eleq2d φ k 2 nd U + 1 + 1 N k 2 nd T + 1 + 1 N
219 218 biimpar φ k 2 nd T + 1 + 1 N k 2 nd U + 1 + 1 N
220 1 adantr φ k 2 nd U + 1 + 1 N N
221 5 adantr φ k 2 nd U + 1 + 1 N U S
222 204 adantr φ k 2 nd U + 1 + 1 N 2 nd U 1 N 1
223 simpr φ k 2 nd U + 1 + 1 N k 2 nd U + 1 + 1 N
224 220 2 221 222 223 poimirlem7 φ k 2 nd U + 1 + 1 N ι n 1 N | F k 2 n F k 1 n = 2 nd 1 st U k
225 219 224 syldan φ k 2 nd T + 1 + 1 N ι n 1 N | F k 2 n F k 1 n = 2 nd 1 st U k
226 1 adantr φ k 2 nd T + 1 + 1 N N
227 3 adantr φ k 2 nd T + 1 + 1 N T S
228 4 adantr φ k 2 nd T + 1 + 1 N 2 nd T 1 N 1
229 simpr φ k 2 nd T + 1 + 1 N k 2 nd T + 1 + 1 N
230 226 2 227 228 229 poimirlem7 φ k 2 nd T + 1 + 1 N ι n 1 N | F k 2 n F k 1 n = 2 nd 1 st T k
231 225 230 eqtr3d φ k 2 nd T + 1 + 1 N 2 nd 1 st U k = 2 nd 1 st T k
232 214 231 jaodan φ k 1 2 nd T 1 k 2 nd T + 1 + 1 N 2 nd 1 st U k = 2 nd 1 st T k
233 130 232 syldan φ k 1 N 2 nd T 2 nd T + 1 2 nd 1 st U k = 2 nd 1 st T k
234 fvres k 1 N 2 nd T 2 nd T + 1 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 k = 2 nd 1 st U k
235 234 adantl φ k 1 N 2 nd T 2 nd T + 1 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 k = 2 nd 1 st U k
236 fvres k 1 N 2 nd T 2 nd T + 1 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 k = 2 nd 1 st T k
237 236 adantl φ k 1 N 2 nd T 2 nd T + 1 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 k = 2 nd 1 st T k
238 233 235 237 3eqtr4d φ k 1 N 2 nd T 2 nd T + 1 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 k = 2 nd 1 st T 1 N 2 nd T 2 nd T + 1 k
239 21 36 238 eqfnfvd φ 2 nd 1 st U 1 N 2 nd T 2 nd T + 1 = 2 nd 1 st T 1 N 2 nd T 2 nd T + 1