Metamath Proof Explorer


Theorem poimirlem11

Description: Lemma for poimir connecting walks that could yield from a given cube a given face opposite the first vertex of the walk. (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
poimirlem12.2 φ T S
poimirlem11.3 φ 2 nd T = 0
poimirlem11.4 φ U S
poimirlem11.5 φ 2 nd U = 0
poimirlem11.6 φ M 1 N
Assertion poimirlem11 φ 2 nd 1 st T 1 M 2 nd 1 st U 1 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 poimirlem22.1 φ F : 0 N 1 0 K 1 N
4 poimirlem12.2 φ T S
5 poimirlem11.3 φ 2 nd T = 0
6 poimirlem11.4 φ U S
7 poimirlem11.5 φ 2 nd U = 0
8 poimirlem11.6 φ M 1 N
9 eldif y 2 nd 1 st T 1 M 2 nd 1 st U 1 M y 2 nd 1 st T 1 M ¬ y 2 nd 1 st U 1 M
10 imassrn 2 nd 1 st T 1 M ran 2 nd 1 st T
11 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
12 11 2 eleq2s T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
13 4 12 syl φ T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
14 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
15 13 14 syl φ 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
16 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
17 15 16 syl φ 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
18 fvex 2 nd 1 st T V
19 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
20 18 19 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
21 17 20 sylib φ 2 nd 1 st T : 1 N 1-1 onto 1 N
22 f1of 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1 N
23 21 22 syl φ 2 nd 1 st T : 1 N 1 N
24 23 frnd φ ran 2 nd 1 st T 1 N
25 10 24 sstrid φ 2 nd 1 st T 1 M 1 N
26 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
27 26 2 eleq2s U S U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
28 6 27 syl φ U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
29 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
30 28 29 syl φ 1 st U 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
31 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
32 30 31 syl φ 2 nd 1 st U f | f : 1 N 1-1 onto 1 N
33 fvex 2 nd 1 st U V
34 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
35 33 34 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
36 32 35 sylib φ 2 nd 1 st U : 1 N 1-1 onto 1 N
37 f1ofo 2 nd 1 st U : 1 N 1-1 onto 1 N 2 nd 1 st U : 1 N onto 1 N
38 36 37 syl φ 2 nd 1 st U : 1 N onto 1 N
39 foima 2 nd 1 st U : 1 N onto 1 N 2 nd 1 st U 1 N = 1 N
40 38 39 syl φ 2 nd 1 st U 1 N = 1 N
41 25 40 sseqtrrd φ 2 nd 1 st T 1 M 2 nd 1 st U 1 N
42 41 ssdifd φ 2 nd 1 st T 1 M 2 nd 1 st U 1 M 2 nd 1 st U 1 N 2 nd 1 st U 1 M
43 dff1o3 2 nd 1 st U : 1 N 1-1 onto 1 N 2 nd 1 st U : 1 N onto 1 N Fun 2 nd 1 st U -1
44 43 simprbi 2 nd 1 st U : 1 N 1-1 onto 1 N Fun 2 nd 1 st U -1
45 36 44 syl φ Fun 2 nd 1 st U -1
46 imadif Fun 2 nd 1 st U -1 2 nd 1 st U 1 N 1 M = 2 nd 1 st U 1 N 2 nd 1 st U 1 M
47 45 46 syl φ 2 nd 1 st U 1 N 1 M = 2 nd 1 st U 1 N 2 nd 1 st U 1 M
48 difun2 M + 1 N 1 M 1 M = M + 1 N 1 M
49 fzsplit M 1 N 1 N = 1 M M + 1 N
50 8 49 syl φ 1 N = 1 M M + 1 N
51 uncom 1 M M + 1 N = M + 1 N 1 M
52 50 51 eqtrdi φ 1 N = M + 1 N 1 M
53 52 difeq1d φ 1 N 1 M = M + 1 N 1 M 1 M
54 incom M + 1 N 1 M = 1 M M + 1 N
55 elfznn M 1 N M
56 8 55 syl φ M
57 56 nnred φ M
58 57 ltp1d φ M < M + 1
59 fzdisj M < M + 1 1 M M + 1 N =
60 58 59 syl φ 1 M M + 1 N =
61 54 60 syl5eq φ M + 1 N 1 M =
62 disj3 M + 1 N 1 M = M + 1 N = M + 1 N 1 M
63 61 62 sylib φ M + 1 N = M + 1 N 1 M
64 48 53 63 3eqtr4a φ 1 N 1 M = M + 1 N
65 64 imaeq2d φ 2 nd 1 st U 1 N 1 M = 2 nd 1 st U M + 1 N
66 47 65 eqtr3d φ 2 nd 1 st U 1 N 2 nd 1 st U 1 M = 2 nd 1 st U M + 1 N
67 42 66 sseqtrd φ 2 nd 1 st T 1 M 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N
68 67 sselda φ y 2 nd 1 st T 1 M 2 nd 1 st U 1 M y 2 nd 1 st U M + 1 N
69 9 68 sylan2br φ y 2 nd 1 st T 1 M ¬ y 2 nd 1 st U 1 M y 2 nd 1 st U M + 1 N
70 fveq2 t = U 2 nd t = 2 nd U
71 70 breq2d t = U y < 2 nd t y < 2 nd U
72 71 ifbid t = U if y < 2 nd t y y + 1 = if y < 2 nd U y y + 1
73 72 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
74 2fveq3 t = U 1 st 1 st t = 1 st 1 st U
75 2fveq3 t = U 2 nd 1 st t = 2 nd 1 st U
76 75 imaeq1d t = U 2 nd 1 st t 1 j = 2 nd 1 st U 1 j
77 76 xpeq1d t = U 2 nd 1 st t 1 j × 1 = 2 nd 1 st U 1 j × 1
78 75 imaeq1d t = U 2 nd 1 st t j + 1 N = 2 nd 1 st U j + 1 N
79 78 xpeq1d t = U 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st U j + 1 N × 0
80 77 79 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
81 74 80 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
82 81 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
83 73 82 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
84 83 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
85 84 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
86 85 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
87 86 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
88 6 87 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
89 breq12 y = M 1 2 nd U = 0 y < 2 nd U M 1 < 0
90 7 89 sylan2 y = M 1 φ y < 2 nd U M 1 < 0
91 90 ancoms φ y = M 1 y < 2 nd U M 1 < 0
92 oveq1 y = M 1 y + 1 = M - 1 + 1
93 56 nncnd φ M
94 npcan1 M M - 1 + 1 = M
95 93 94 syl φ M - 1 + 1 = M
96 92 95 sylan9eqr φ y = M 1 y + 1 = M
97 91 96 ifbieq2d φ y = M 1 if y < 2 nd U y y + 1 = if M 1 < 0 y M
98 56 nnzd φ M
99 1 nnzd φ N
100 elfzm1b M N M 1 N M 1 0 N 1
101 98 99 100 syl2anc φ M 1 N M 1 0 N 1
102 8 101 mpbid φ M 1 0 N 1
103 elfzle1 M 1 0 N 1 0 M 1
104 102 103 syl φ 0 M 1
105 0red φ 0
106 nnm1nn0 M M 1 0
107 56 106 syl φ M 1 0
108 107 nn0red φ M 1
109 105 108 lenltd φ 0 M 1 ¬ M 1 < 0
110 104 109 mpbid φ ¬ M 1 < 0
111 110 iffalsed φ if M 1 < 0 y M = M
112 111 adantr φ y = M 1 if M 1 < 0 y M = M
113 97 112 eqtrd φ y = M 1 if y < 2 nd U y y + 1 = M
114 113 csbeq1d φ y = M 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 = M / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0
115 oveq2 j = M 1 j = 1 M
116 115 imaeq2d j = M 2 nd 1 st U 1 j = 2 nd 1 st U 1 M
117 116 xpeq1d j = M 2 nd 1 st U 1 j × 1 = 2 nd 1 st U 1 M × 1
118 oveq1 j = M j + 1 = M + 1
119 118 oveq1d j = M j + 1 N = M + 1 N
120 119 imaeq2d j = M 2 nd 1 st U j + 1 N = 2 nd 1 st U M + 1 N
121 120 xpeq1d j = M 2 nd 1 st U j + 1 N × 0 = 2 nd 1 st U M + 1 N × 0
122 117 121 uneq12d j = M 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0 = 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0
123 122 oveq2d j = M 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0 = 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0
124 123 adantl φ j = M 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0 = 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0
125 8 124 csbied φ M / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0 = 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0
126 125 adantr φ y = M 1 M / j 1 st 1 st U + f 2 nd 1 st U 1 j × 1 2 nd 1 st U j + 1 N × 0 = 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0
127 114 126 eqtrd φ y = M 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 = 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0
128 ovexd φ 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 V
129 88 127 102 128 fvmptd φ F M 1 = 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0
130 129 fveq1d φ F M 1 y = 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 y
131 130 adantr φ y 2 nd 1 st U M + 1 N F M 1 y = 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 y
132 imassrn 2 nd 1 st U M + 1 N ran 2 nd 1 st U
133 f1of 2 nd 1 st U : 1 N 1-1 onto 1 N 2 nd 1 st U : 1 N 1 N
134 36 133 syl φ 2 nd 1 st U : 1 N 1 N
135 134 frnd φ ran 2 nd 1 st U 1 N
136 132 135 sstrid φ 2 nd 1 st U M + 1 N 1 N
137 136 sselda φ y 2 nd 1 st U M + 1 N y 1 N
138 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
139 30 138 syl φ 1 st 1 st U 0 ..^ K 1 N
140 elmapfn 1 st 1 st U 0 ..^ K 1 N 1 st 1 st U Fn 1 N
141 139 140 syl φ 1 st 1 st U Fn 1 N
142 141 adantr φ y 2 nd 1 st U M + 1 N 1 st 1 st U Fn 1 N
143 1ex 1 V
144 fnconstg 1 V 2 nd 1 st U 1 M × 1 Fn 2 nd 1 st U 1 M
145 143 144 ax-mp 2 nd 1 st U 1 M × 1 Fn 2 nd 1 st U 1 M
146 c0ex 0 V
147 fnconstg 0 V 2 nd 1 st U M + 1 N × 0 Fn 2 nd 1 st U M + 1 N
148 146 147 ax-mp 2 nd 1 st U M + 1 N × 0 Fn 2 nd 1 st U M + 1 N
149 145 148 pm3.2i 2 nd 1 st U 1 M × 1 Fn 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N × 0 Fn 2 nd 1 st U M + 1 N
150 imain Fun 2 nd 1 st U -1 2 nd 1 st U 1 M M + 1 N = 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N
151 45 150 syl φ 2 nd 1 st U 1 M M + 1 N = 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N
152 60 imaeq2d φ 2 nd 1 st U 1 M M + 1 N = 2 nd 1 st U
153 ima0 2 nd 1 st U =
154 152 153 eqtrdi φ 2 nd 1 st U 1 M M + 1 N =
155 151 154 eqtr3d φ 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N =
156 fnun 2 nd 1 st U 1 M × 1 Fn 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N × 0 Fn 2 nd 1 st U M + 1 N 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N = 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 Fn 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N
157 149 155 156 sylancr φ 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 Fn 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N
158 imaundi 2 nd 1 st U 1 M M + 1 N = 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N
159 50 imaeq2d φ 2 nd 1 st U 1 N = 2 nd 1 st U 1 M M + 1 N
160 159 40 eqtr3d φ 2 nd 1 st U 1 M M + 1 N = 1 N
161 158 160 eqtr3id φ 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N = 1 N
162 161 fneq2d φ 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 Fn 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 Fn 1 N
163 157 162 mpbid φ 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 Fn 1 N
164 163 adantr φ y 2 nd 1 st U M + 1 N 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 Fn 1 N
165 ovexd φ y 2 nd 1 st U M + 1 N 1 N V
166 inidm 1 N 1 N = 1 N
167 eqidd φ y 2 nd 1 st U M + 1 N y 1 N 1 st 1 st U y = 1 st 1 st U y
168 fvun2 2 nd 1 st U 1 M × 1 Fn 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N × 0 Fn 2 nd 1 st U M + 1 N 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N = y 2 nd 1 st U M + 1 N 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 y = 2 nd 1 st U M + 1 N × 0 y
169 145 148 168 mp3an12 2 nd 1 st U 1 M 2 nd 1 st U M + 1 N = y 2 nd 1 st U M + 1 N 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 y = 2 nd 1 st U M + 1 N × 0 y
170 155 169 sylan φ y 2 nd 1 st U M + 1 N 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 y = 2 nd 1 st U M + 1 N × 0 y
171 146 fvconst2 y 2 nd 1 st U M + 1 N 2 nd 1 st U M + 1 N × 0 y = 0
172 171 adantl φ y 2 nd 1 st U M + 1 N 2 nd 1 st U M + 1 N × 0 y = 0
173 170 172 eqtrd φ y 2 nd 1 st U M + 1 N 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 y = 0
174 173 adantr φ y 2 nd 1 st U M + 1 N y 1 N 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 y = 0
175 142 164 165 165 166 167 174 ofval φ y 2 nd 1 st U M + 1 N y 1 N 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 y = 1 st 1 st U y + 0
176 137 175 mpdan φ y 2 nd 1 st U M + 1 N 1 st 1 st U + f 2 nd 1 st U 1 M × 1 2 nd 1 st U M + 1 N × 0 y = 1 st 1 st U y + 0
177 elmapi 1 st 1 st U 0 ..^ K 1 N 1 st 1 st U : 1 N 0 ..^ K
178 139 177 syl φ 1 st 1 st U : 1 N 0 ..^ K
179 178 ffvelrnda φ y 1 N 1 st 1 st U y 0 ..^ K
180 elfzonn0 1 st 1 st U y 0 ..^ K 1 st 1 st U y 0
181 179 180 syl φ y 1 N 1 st 1 st U y 0
182 181 nn0cnd φ y 1 N 1 st 1 st U y
183 137 182 syldan φ y 2 nd 1 st U M + 1 N 1 st 1 st U y
184 183 addid1d φ y 2 nd 1 st U M + 1 N 1 st 1 st U y + 0 = 1 st 1 st U y
185 131 176 184 3eqtrd φ y 2 nd 1 st U M + 1 N F M 1 y = 1 st 1 st U y
186 69 185 syldan φ y 2 nd 1 st T 1 M ¬ y 2 nd 1 st U 1 M F M 1 y = 1 st 1 st U y
187 fveq2 t = T 2 nd t = 2 nd T
188 187 breq2d t = T y < 2 nd t y < 2 nd T
189 188 ifbid t = T if y < 2 nd t y y + 1 = if y < 2 nd T y y + 1
190 189 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
191 2fveq3 t = T 1 st 1 st t = 1 st 1 st T
192 2fveq3 t = T 2 nd 1 st t = 2 nd 1 st T
193 192 imaeq1d t = T 2 nd 1 st t 1 j = 2 nd 1 st T 1 j
194 193 xpeq1d t = T 2 nd 1 st t 1 j × 1 = 2 nd 1 st T 1 j × 1
195 192 imaeq1d t = T 2 nd 1 st t j + 1 N = 2 nd 1 st T j + 1 N
196 195 xpeq1d t = T 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T j + 1 N × 0
197 194 196 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
198 191 197 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
199 198 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
200 190 199 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
201 200 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
202 201 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
203 202 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
204 203 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
205 4 204 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
206 breq12 y = M 1 2 nd T = 0 y < 2 nd T M 1 < 0
207 5 206 sylan2 y = M 1 φ y < 2 nd T M 1 < 0
208 207 ancoms φ y = M 1 y < 2 nd T M 1 < 0
209 208 96 ifbieq2d φ y = M 1 if y < 2 nd T y y + 1 = if M 1 < 0 y M
210 209 112 eqtrd φ y = M 1 if y < 2 nd T y y + 1 = M
211 210 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
212 115 imaeq2d j = M 2 nd 1 st T 1 j = 2 nd 1 st T 1 M
213 212 xpeq1d j = M 2 nd 1 st T 1 j × 1 = 2 nd 1 st T 1 M × 1
214 119 imaeq2d j = M 2 nd 1 st T j + 1 N = 2 nd 1 st T M + 1 N
215 214 xpeq1d j = M 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T M + 1 N × 0
216 213 215 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
217 216 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
218 217 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
219 8 218 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
220 219 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
221 211 220 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
222 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
223 205 221 102 222 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
224 223 fveq1d φ F M 1 y = 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 y
225 224 adantr φ y 2 nd 1 st T 1 M F M 1 y = 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 y
226 25 sselda φ y 2 nd 1 st T 1 M y 1 N
227 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
228 15 227 syl φ 1 st 1 st T 0 ..^ K 1 N
229 elmapfn 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T Fn 1 N
230 228 229 syl φ 1 st 1 st T Fn 1 N
231 230 adantr φ y 2 nd 1 st T 1 M 1 st 1 st T Fn 1 N
232 fnconstg 1 V 2 nd 1 st T 1 M × 1 Fn 2 nd 1 st T 1 M
233 143 232 ax-mp 2 nd 1 st T 1 M × 1 Fn 2 nd 1 st T 1 M
234 fnconstg 0 V 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T M + 1 N
235 146 234 ax-mp 2 nd 1 st T M + 1 N × 0 Fn 2 nd 1 st T M + 1 N
236 233 235 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
237 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
238 237 simprbi 2 nd 1 st T : 1 N 1-1 onto 1 N Fun 2 nd 1 st T -1
239 21 238 syl φ Fun 2 nd 1 st T -1
240 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
241 239 240 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
242 60 imaeq2d φ 2 nd 1 st T 1 M M + 1 N = 2 nd 1 st T
243 ima0 2 nd 1 st T =
244 242 243 eqtrdi φ 2 nd 1 st T 1 M M + 1 N =
245 241 244 eqtr3d φ 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N =
246 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
247 236 245 246 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
248 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
249 50 imaeq2d φ 2 nd 1 st T 1 N = 2 nd 1 st T 1 M M + 1 N
250 f1ofo 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N
251 21 250 syl φ 2 nd 1 st T : 1 N onto 1 N
252 foima 2 nd 1 st T : 1 N onto 1 N 2 nd 1 st T 1 N = 1 N
253 251 252 syl φ 2 nd 1 st T 1 N = 1 N
254 249 253 eqtr3d φ 2 nd 1 st T 1 M M + 1 N = 1 N
255 248 254 eqtr3id φ 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N = 1 N
256 255 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
257 247 256 mpbid φ 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N
258 257 adantr φ y 2 nd 1 st T 1 M 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 Fn 1 N
259 ovexd φ y 2 nd 1 st T 1 M 1 N V
260 eqidd φ y 2 nd 1 st T 1 M y 1 N 1 st 1 st T y = 1 st 1 st T y
261 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 = y 2 nd 1 st T 1 M 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 y = 2 nd 1 st T 1 M × 1 y
262 233 235 261 mp3an12 2 nd 1 st T 1 M 2 nd 1 st T M + 1 N = y 2 nd 1 st T 1 M 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 y = 2 nd 1 st T 1 M × 1 y
263 245 262 sylan φ y 2 nd 1 st T 1 M 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 y = 2 nd 1 st T 1 M × 1 y
264 143 fvconst2 y 2 nd 1 st T 1 M 2 nd 1 st T 1 M × 1 y = 1
265 264 adantl φ y 2 nd 1 st T 1 M 2 nd 1 st T 1 M × 1 y = 1
266 263 265 eqtrd φ y 2 nd 1 st T 1 M 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 y = 1
267 266 adantr φ y 2 nd 1 st T 1 M y 1 N 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 y = 1
268 231 258 259 259 166 260 267 ofval φ y 2 nd 1 st T 1 M y 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 y = 1 st 1 st T y + 1
269 226 268 mpdan φ y 2 nd 1 st T 1 M 1 st 1 st T + f 2 nd 1 st T 1 M × 1 2 nd 1 st T M + 1 N × 0 y = 1 st 1 st T y + 1
270 225 269 eqtrd φ y 2 nd 1 st T 1 M F M 1 y = 1 st 1 st T y + 1
271 270 adantrr φ y 2 nd 1 st T 1 M ¬ y 2 nd 1 st U 1 M F M 1 y = 1 st 1 st T y + 1
272 1 2 3 6 7 poimirlem10 φ F N 1 f 1 N × 1 = 1 st 1 st U
273 1 2 3 4 5 poimirlem10 φ F N 1 f 1 N × 1 = 1 st 1 st T
274 272 273 eqtr3d φ 1 st 1 st U = 1 st 1 st T
275 274 fveq1d φ 1 st 1 st U y = 1 st 1 st T y
276 275 adantr φ y 2 nd 1 st T 1 M ¬ y 2 nd 1 st U 1 M 1 st 1 st U y = 1 st 1 st T y
277 186 271 276 3eqtr3d φ y 2 nd 1 st T 1 M ¬ y 2 nd 1 st U 1 M 1 st 1 st T y + 1 = 1 st 1 st T y
278 elmapi 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T : 1 N 0 ..^ K
279 228 278 syl φ 1 st 1 st T : 1 N 0 ..^ K
280 279 ffvelrnda φ y 1 N 1 st 1 st T y 0 ..^ K
281 elfzonn0 1 st 1 st T y 0 ..^ K 1 st 1 st T y 0
282 280 281 syl φ y 1 N 1 st 1 st T y 0
283 282 nn0red φ y 1 N 1 st 1 st T y
284 283 ltp1d φ y 1 N 1 st 1 st T y < 1 st 1 st T y + 1
285 283 284 gtned φ y 1 N 1 st 1 st T y + 1 1 st 1 st T y
286 226 285 syldan φ y 2 nd 1 st T 1 M 1 st 1 st T y + 1 1 st 1 st T y
287 286 neneqd φ y 2 nd 1 st T 1 M ¬ 1 st 1 st T y + 1 = 1 st 1 st T y
288 287 adantrr φ y 2 nd 1 st T 1 M ¬ y 2 nd 1 st U 1 M ¬ 1 st 1 st T y + 1 = 1 st 1 st T y
289 277 288 pm2.65da φ ¬ y 2 nd 1 st T 1 M ¬ y 2 nd 1 st U 1 M
290 iman y 2 nd 1 st T 1 M y 2 nd 1 st U 1 M ¬ y 2 nd 1 st T 1 M ¬ y 2 nd 1 st U 1 M
291 289 290 sylibr φ y 2 nd 1 st T 1 M y 2 nd 1 st U 1 M
292 291 ssrdv φ 2 nd 1 st T 1 M 2 nd 1 st U 1 M