Metamath Proof Explorer


Theorem poimirlem24

Description: Lemma for poimir , two ways of expressing that a simplex has an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φ N
poimirlem28.1 p = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 B = C
poimirlem28.2 φ p : 1 N 0 K B 0 N
poimirlem25.3 φ T : 1 N 0 ..^ K
poimirlem25.4 φ U : 1 N 1-1 onto 1 N
poimirlem24.5 φ V 0 N
Assertion poimirlem24 φ x 0 K 1 N 0 N 1 x = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 N 1 ran p ran x B p ran x p N 0 i 0 N 1 j 0 N V i = T U / s C ¬ V = N T N = 0 U N = N

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimirlem28.1 p = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 B = C
3 poimirlem28.2 φ p : 1 N 0 K B 0 N
4 poimirlem25.3 φ T : 1 N 0 ..^ K
5 poimirlem25.4 φ U : 1 N 1-1 onto 1 N
6 poimirlem24.5 φ V 0 N
7 nfv j φ y 0 N 1
8 nfcsb1v _ j y / j T + f U 1 j × 1 U j + 1 N × 0
9 nfcv _ j 1 N
10 nfcv _ j 0 K
11 8 9 10 nff j y / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
12 7 11 nfim j φ y 0 N 1 y / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
13 eleq1 j = y j 0 N 1 y 0 N 1
14 13 anbi2d j = y φ j 0 N 1 φ y 0 N 1
15 csbeq1a j = y T + f U 1 j × 1 U j + 1 N × 0 = y / j T + f U 1 j × 1 U j + 1 N × 0
16 15 feq1d j = y T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K y / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
17 14 16 imbi12d j = y φ j 0 N 1 T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K φ y 0 N 1 y / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
18 1 nncnd φ N
19 npcan1 N N - 1 + 1 = N
20 18 19 syl φ N - 1 + 1 = N
21 1 nnzd φ N
22 peano2zm N N 1
23 21 22 syl φ N 1
24 uzid N 1 N 1 N 1
25 peano2uz N 1 N 1 N - 1 + 1 N 1
26 23 24 25 3syl φ N - 1 + 1 N 1
27 20 26 eqeltrrd φ N N 1
28 fzss2 N N 1 0 N 1 0 N
29 27 28 syl φ 0 N 1 0 N
30 29 sselda φ j 0 N 1 j 0 N
31 elun y 1 0 y 1 y 0
32 fzofzp1 x 0 ..^ K x + 1 0 K
33 elsni y 1 y = 1
34 33 oveq2d y 1 x + y = x + 1
35 34 eleq1d y 1 x + y 0 K x + 1 0 K
36 32 35 syl5ibrcom x 0 ..^ K y 1 x + y 0 K
37 elfzoelz x 0 ..^ K x
38 37 zcnd x 0 ..^ K x
39 38 addid1d x 0 ..^ K x + 0 = x
40 elfzofz x 0 ..^ K x 0 K
41 39 40 eqeltrd x 0 ..^ K x + 0 0 K
42 elsni y 0 y = 0
43 42 oveq2d y 0 x + y = x + 0
44 43 eleq1d y 0 x + y 0 K x + 0 0 K
45 41 44 syl5ibrcom x 0 ..^ K y 0 x + y 0 K
46 36 45 jaod x 0 ..^ K y 1 y 0 x + y 0 K
47 31 46 syl5bi x 0 ..^ K y 1 0 x + y 0 K
48 47 imp x 0 ..^ K y 1 0 x + y 0 K
49 48 adantl φ j 0 N x 0 ..^ K y 1 0 x + y 0 K
50 4 adantr φ j 0 N T : 1 N 0 ..^ K
51 1ex 1 V
52 51 fconst U 1 j × 1 : U 1 j 1
53 c0ex 0 V
54 53 fconst U j + 1 N × 0 : U j + 1 N 0
55 52 54 pm3.2i U 1 j × 1 : U 1 j 1 U j + 1 N × 0 : U j + 1 N 0
56 dff1o3 U : 1 N 1-1 onto 1 N U : 1 N onto 1 N Fun U -1
57 56 simprbi U : 1 N 1-1 onto 1 N Fun U -1
58 imain Fun U -1 U 1 j j + 1 N = U 1 j U j + 1 N
59 5 57 58 3syl φ U 1 j j + 1 N = U 1 j U j + 1 N
60 elfznn0 j 0 N j 0
61 60 nn0red j 0 N j
62 61 ltp1d j 0 N j < j + 1
63 fzdisj j < j + 1 1 j j + 1 N =
64 62 63 syl j 0 N 1 j j + 1 N =
65 64 imaeq2d j 0 N U 1 j j + 1 N = U
66 ima0 U =
67 65 66 eqtrdi j 0 N U 1 j j + 1 N =
68 59 67 sylan9req φ j 0 N U 1 j U j + 1 N =
69 fun U 1 j × 1 : U 1 j 1 U j + 1 N × 0 : U j + 1 N 0 U 1 j U j + 1 N = U 1 j × 1 U j + 1 N × 0 : U 1 j U j + 1 N 1 0
70 55 68 69 sylancr φ j 0 N U 1 j × 1 U j + 1 N × 0 : U 1 j U j + 1 N 1 0
71 nn0p1nn j 0 j + 1
72 60 71 syl j 0 N j + 1
73 nnuz = 1
74 72 73 eleqtrdi j 0 N j + 1 1
75 elfzuz3 j 0 N N j
76 fzsplit2 j + 1 1 N j 1 N = 1 j j + 1 N
77 74 75 76 syl2anc j 0 N 1 N = 1 j j + 1 N
78 77 imaeq2d j 0 N U 1 N = U 1 j j + 1 N
79 imaundi U 1 j j + 1 N = U 1 j U j + 1 N
80 78 79 eqtr2di j 0 N U 1 j U j + 1 N = U 1 N
81 f1ofo U : 1 N 1-1 onto 1 N U : 1 N onto 1 N
82 foima U : 1 N onto 1 N U 1 N = 1 N
83 5 81 82 3syl φ U 1 N = 1 N
84 80 83 sylan9eqr φ j 0 N U 1 j U j + 1 N = 1 N
85 84 feq2d φ j 0 N U 1 j × 1 U j + 1 N × 0 : U 1 j U j + 1 N 1 0 U 1 j × 1 U j + 1 N × 0 : 1 N 1 0
86 70 85 mpbid φ j 0 N U 1 j × 1 U j + 1 N × 0 : 1 N 1 0
87 ovex 1 N V
88 87 a1i φ j 0 N 1 N V
89 inidm 1 N 1 N = 1 N
90 49 50 86 88 88 89 off φ j 0 N T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
91 30 90 syldan φ j 0 N 1 T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
92 12 17 91 chvarfv φ y 0 N 1 y / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
93 fzp1elp1 y 0 N 1 y + 1 0 N - 1 + 1
94 20 oveq2d φ 0 N - 1 + 1 = 0 N
95 94 eleq2d φ y + 1 0 N - 1 + 1 y + 1 0 N
96 95 biimpa φ y + 1 0 N - 1 + 1 y + 1 0 N
97 93 96 sylan2 φ y 0 N 1 y + 1 0 N
98 nfv j φ y + 1 0 N
99 nfcsb1v _ j y + 1 / j T + f U 1 j × 1 U j + 1 N × 0
100 99 9 10 nff j y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
101 98 100 nfim j φ y + 1 0 N y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
102 ovex y + 1 V
103 eleq1 j = y + 1 j 0 N y + 1 0 N
104 103 anbi2d j = y + 1 φ j 0 N φ y + 1 0 N
105 csbeq1a j = y + 1 T + f U 1 j × 1 U j + 1 N × 0 = y + 1 / j T + f U 1 j × 1 U j + 1 N × 0
106 105 feq1d j = y + 1 T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
107 104 106 imbi12d j = y + 1 φ j 0 N T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K φ y + 1 0 N y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
108 101 102 107 90 vtoclf φ y + 1 0 N y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
109 97 108 syldan φ y 0 N 1 y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
110 csbeq1 y = if y < V y y + 1 y / j T + f U 1 j × 1 U j + 1 N × 0 = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0
111 110 feq1d y = if y < V y y + 1 y / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
112 csbeq1 y + 1 = if y < V y y + 1 y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0
113 112 feq1d y + 1 = if y < V y y + 1 y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
114 111 113 ifboth y / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
115 92 109 114 syl2anc φ y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
116 ovex 0 K V
117 116 87 elmap if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 K 1 N if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 1 N 0 K
118 115 117 sylibr φ y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 K 1 N
119 118 fmpttd φ y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 0 N 1 0 K 1 N
120 ovex 0 K 1 N V
121 ovex 0 N 1 V
122 120 121 elmap y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 K 1 N 0 N 1 y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 : 0 N 1 0 K 1 N
123 119 122 sylibr φ y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 K 1 N 0 N 1
124 rneq x = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 ran x = ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0
125 124 mpteq1d x = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 p ran x B = p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B
126 125 rneqd x = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 ran p ran x B = ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B
127 126 sseq2d x = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 N 1 ran p ran x B 0 N 1 ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B
128 124 rexeqdv x = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 p ran x p N 0 p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 p N 0
129 127 128 anbi12d x = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 N 1 ran p ran x B p ran x p N 0 0 N 1 ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 p N 0
130 129 ceqsrexv y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 K 1 N 0 N 1 x 0 K 1 N 0 N 1 x = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 N 1 ran p ran x B p ran x p N 0 0 N 1 ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 p N 0
131 123 130 syl φ x 0 K 1 N 0 N 1 x = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 N 1 ran p ran x B p ran x p N 0 0 N 1 ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 p N 0
132 dfss3 0 N 1 ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B i 0 N 1 i ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B
133 ovex 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 V
134 133 2 csbie 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 / p B = C
135 134 csbeq2i T U / s 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 / p B = T U / s C
136 opex T U V
137 136 a1i φ T U V
138 fveq2 s = T U 1 st s = 1 st T U
139 fex T : 1 N 0 ..^ K 1 N V T V
140 4 87 139 sylancl φ T V
141 f1oexrnex U : 1 N 1-1 onto 1 N 1 N V U V
142 5 87 141 sylancl φ U V
143 op1stg T V U V 1 st T U = T
144 140 142 143 syl2anc φ 1 st T U = T
145 138 144 sylan9eqr φ s = T U 1 st s = T
146 fveq2 s = T U 2 nd s = 2 nd T U
147 op2ndg T V U V 2 nd T U = U
148 140 142 147 syl2anc φ 2 nd T U = U
149 146 148 sylan9eqr φ s = T U 2 nd s = U
150 imaeq1 2 nd s = U 2 nd s 1 j = U 1 j
151 150 xpeq1d 2 nd s = U 2 nd s 1 j × 1 = U 1 j × 1
152 imaeq1 2 nd s = U 2 nd s j + 1 N = U j + 1 N
153 152 xpeq1d 2 nd s = U 2 nd s j + 1 N × 0 = U j + 1 N × 0
154 151 153 uneq12d 2 nd s = U 2 nd s 1 j × 1 2 nd s j + 1 N × 0 = U 1 j × 1 U j + 1 N × 0
155 149 154 syl φ s = T U 2 nd s 1 j × 1 2 nd s j + 1 N × 0 = U 1 j × 1 U j + 1 N × 0
156 145 155 oveq12d φ s = T U 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 = T + f U 1 j × 1 U j + 1 N × 0
157 156 csbeq1d φ s = T U 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 / p B = T + f U 1 j × 1 U j + 1 N × 0 / p B
158 137 157 csbied φ T U / s 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 / p B = T + f U 1 j × 1 U j + 1 N × 0 / p B
159 135 158 eqtr3id φ T U / s C = T + f U 1 j × 1 U j + 1 N × 0 / p B
160 159 csbeq2dv φ if y < V y y + 1 / j T U / s C = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
161 160 eqeq2d φ i = if y < V y y + 1 / j T U / s C i = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
162 161 rexbidv φ y 0 N 1 i = if y < V y y + 1 / j T U / s C y 0 N 1 i = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
163 vex i V
164 eqid p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B = p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B
165 164 elrnmpt i V i ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 i = B
166 163 165 ax-mp i ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 i = B
167 nfv k i = B
168 nfcsb1v _ p k / p B
169 168 nfeq2 p i = k / p B
170 csbeq1a p = k B = k / p B
171 170 eqeq2d p = k i = B i = k / p B
172 167 169 171 cbvrexw p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 i = B k ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 i = k / p B
173 ovex T + f U 1 j × 1 U j + 1 N × 0 V
174 173 csbex if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 V
175 174 rgenw y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 V
176 eqid y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0
177 csbeq1 k = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 k / p B = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
178 vex y V
179 178 102 ifex if y < V y y + 1 V
180 csbnestgw if y < V y y + 1 V if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
181 179 180 ax-mp if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
182 177 181 eqtr4di k = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 k / p B = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
183 182 eqeq2d k = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 i = k / p B i = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
184 176 183 rexrnmptw y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 V k ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 i = k / p B y 0 N 1 i = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
185 175 184 ax-mp k ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 i = k / p B y 0 N 1 i = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
186 166 172 185 3bitri i ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B y 0 N 1 i = if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 / p B
187 162 186 bitr4di φ y 0 N 1 i = if y < V y y + 1 / j T U / s C i ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B
188 29 sselda φ y 0 N 1 y 0 N
189 188 adantr φ y 0 N 1 y < V y 0 N
190 elfzelz y 0 N 1 y
191 190 zred y 0 N 1 y
192 191 adantl φ y 0 N 1 y
193 ltne y y < V V y
194 193 necomd y y < V y V
195 192 194 sylan φ y 0 N 1 y < V y V
196 eldifsn y 0 N V y 0 N y V
197 189 195 196 sylanbrc φ y 0 N 1 y < V y 0 N V
198 97 adantr φ y 0 N 1 ¬ y < V y + 1 0 N
199 6 elfzelzd φ V
200 199 zred φ V
201 200 ad2antrr φ y 0 N 1 ¬ y < V V
202 zre V V
203 zre y y
204 lenlt V y V y ¬ y < V
205 202 203 204 syl2an V y V y ¬ y < V
206 zleltp1 V y V y V < y + 1
207 205 206 bitr3d V y ¬ y < V V < y + 1
208 199 190 207 syl2an φ y 0 N 1 ¬ y < V V < y + 1
209 208 biimpa φ y 0 N 1 ¬ y < V V < y + 1
210 201 209 gtned φ y 0 N 1 ¬ y < V y + 1 V
211 eldifsn y + 1 0 N V y + 1 0 N y + 1 V
212 198 210 211 sylanbrc φ y 0 N 1 ¬ y < V y + 1 0 N V
213 197 212 ifclda φ y 0 N 1 if y < V y y + 1 0 N V
214 nfcsb1v _ j if y < V y y + 1 / j T U / s C
215 214 nfeq2 j i = if y < V y y + 1 / j T U / s C
216 csbeq1a j = if y < V y y + 1 T U / s C = if y < V y y + 1 / j T U / s C
217 216 eqeq2d j = if y < V y y + 1 i = T U / s C i = if y < V y y + 1 / j T U / s C
218 215 217 rspce if y < V y y + 1 0 N V i = if y < V y y + 1 / j T U / s C j 0 N V i = T U / s C
219 218 ex if y < V y y + 1 0 N V i = if y < V y y + 1 / j T U / s C j 0 N V i = T U / s C
220 213 219 syl φ y 0 N 1 i = if y < V y y + 1 / j T U / s C j 0 N V i = T U / s C
221 220 rexlimdva φ y 0 N 1 i = if y < V y y + 1 / j T U / s C j 0 N V i = T U / s C
222 nfv j φ
223 nfcv _ j 0 N 1
224 223 215 nfrex j y 0 N 1 i = if y < V y y + 1 / j T U / s C
225 eldifi j 0 N V j 0 N
226 225 60 syl j 0 N V j 0
227 226 nn0ge0d j 0 N V 0 j
228 227 ad2antlr φ j 0 N V j < V 0 j
229 226 nn0red j 0 N V j
230 229 ad2antlr φ j 0 N V j < V j
231 200 ad2antrr φ j 0 N V j < V V
232 21 zred φ N
233 232 ad2antrr φ j 0 N V j < V N
234 simpr φ j 0 N V j < V j < V
235 elfzle2 V 0 N V N
236 6 235 syl φ V N
237 236 ad2antrr φ j 0 N V j < V V N
238 230 231 233 234 237 ltletrd φ j 0 N V j < V j < N
239 225 elfzelzd j 0 N V j
240 zltlem1 j N j < N j N 1
241 239 21 240 syl2anr φ j 0 N V j < N j N 1
242 241 adantr φ j 0 N V j < V j < N j N 1
243 238 242 mpbid φ j 0 N V j < V j N 1
244 0z 0
245 elfz j 0 N 1 j 0 N 1 0 j j N 1
246 244 245 mp3an2 j N 1 j 0 N 1 0 j j N 1
247 239 23 246 syl2anr φ j 0 N V j 0 N 1 0 j j N 1
248 247 adantr φ j 0 N V j < V j 0 N 1 0 j j N 1
249 228 243 248 mpbir2and φ j 0 N V j < V j 0 N 1
250 0red φ j 0 N V ¬ j < V 0
251 200 ad2antrr φ j 0 N V ¬ j < V V
252 229 ad2antlr φ j 0 N V ¬ j < V j
253 elfzle1 V 0 N 0 V
254 6 253 syl φ 0 V
255 254 ad2antrr φ j 0 N V ¬ j < V 0 V
256 lenlt V j V j ¬ j < V
257 200 229 256 syl2an φ j 0 N V V j ¬ j < V
258 257 biimpar φ j 0 N V ¬ j < V V j
259 eldifsni j 0 N V j V
260 259 ad2antlr φ j 0 N V ¬ j < V j V
261 ltlen V j V < j V j j V
262 200 229 261 syl2an φ j 0 N V V < j V j j V
263 262 adantr φ j 0 N V ¬ j < V V < j V j j V
264 258 260 263 mpbir2and φ j 0 N V ¬ j < V V < j
265 250 251 252 255 264 lelttrd φ j 0 N V ¬ j < V 0 < j
266 zgt0ge1 j 0 < j 1 j
267 239 266 syl j 0 N V 0 < j 1 j
268 267 ad2antlr φ j 0 N V ¬ j < V 0 < j 1 j
269 265 268 mpbid φ j 0 N V ¬ j < V 1 j
270 elfzle2 j 0 N j N
271 225 270 syl j 0 N V j N
272 271 ad2antlr φ j 0 N V ¬ j < V j N
273 1z 1
274 elfz j 1 N j 1 N 1 j j N
275 273 274 mp3an2 j N j 1 N 1 j j N
276 239 21 275 syl2anr φ j 0 N V j 1 N 1 j j N
277 276 adantr φ j 0 N V ¬ j < V j 1 N 1 j j N
278 269 272 277 mpbir2and φ j 0 N V ¬ j < V j 1 N
279 elfzmlbm j 1 N j 1 0 N 1
280 278 279 syl φ j 0 N V ¬ j < V j 1 0 N 1
281 249 280 ifclda φ j 0 N V if j < V j j 1 0 N 1
282 breq1 j = if j < V j j 1 j < V if j < V j j 1 < V
283 id j = if j < V j j 1 j = if j < V j j 1
284 oveq1 j = if j < V j j 1 j + 1 = if j < V j j 1 + 1
285 282 283 284 ifbieq12d j = if j < V j j 1 if j < V j j + 1 = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1
286 285 eqeq2d j = if j < V j j 1 j = if j < V j j + 1 j = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1
287 breq1 j 1 = if j < V j j 1 j 1 < V if j < V j j 1 < V
288 id j 1 = if j < V j j 1 j 1 = if j < V j j 1
289 oveq1 j 1 = if j < V j j 1 j - 1 + 1 = if j < V j j 1 + 1
290 287 288 289 ifbieq12d j 1 = if j < V j j 1 if j 1 < V j 1 j - 1 + 1 = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1
291 290 eqeq2d j 1 = if j < V j j 1 j = if j 1 < V j 1 j - 1 + 1 j = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1
292 iftrue j < V if j < V j j + 1 = j
293 292 eqcomd j < V j = if j < V j j + 1
294 293 adantl φ j 0 N V j < V j = if j < V j j + 1
295 zlem1lt j V j V j 1 < V
296 239 199 295 syl2anr φ j 0 N V j V j 1 < V
297 259 necomd j 0 N V V j
298 297 adantl φ j 0 N V V j
299 ltlen j V j < V j V V j
300 229 200 299 syl2anr φ j 0 N V j < V j V V j
301 300 biimprd φ j 0 N V j V V j j < V
302 298 301 mpan2d φ j 0 N V j V j < V
303 296 302 sylbird φ j 0 N V j 1 < V j < V
304 303 con3dimp φ j 0 N V ¬ j < V ¬ j 1 < V
305 304 iffalsed φ j 0 N V ¬ j < V if j 1 < V j 1 j - 1 + 1 = j - 1 + 1
306 226 nn0cnd j 0 N V j
307 npcan1 j j - 1 + 1 = j
308 306 307 syl j 0 N V j - 1 + 1 = j
309 308 ad2antlr φ j 0 N V ¬ j < V j - 1 + 1 = j
310 305 309 eqtr2d φ j 0 N V ¬ j < V j = if j 1 < V j 1 j - 1 + 1
311 286 291 294 310 ifbothda φ j 0 N V j = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1
312 csbeq1a j = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1 T U / s C = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1 / j T U / s C
313 311 312 syl φ j 0 N V T U / s C = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1 / j T U / s C
314 313 eqeq2d φ j 0 N V i = T U / s C i = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1 / j T U / s C
315 314 biimpd φ j 0 N V i = T U / s C i = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1 / j T U / s C
316 breq1 y = if j < V j j 1 y < V if j < V j j 1 < V
317 id y = if j < V j j 1 y = if j < V j j 1
318 oveq1 y = if j < V j j 1 y + 1 = if j < V j j 1 + 1
319 316 317 318 ifbieq12d y = if j < V j j 1 if y < V y y + 1 = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1
320 319 csbeq1d y = if j < V j j 1 if y < V y y + 1 / j T U / s C = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1 / j T U / s C
321 320 eqeq2d y = if j < V j j 1 i = if y < V y y + 1 / j T U / s C i = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1 / j T U / s C
322 321 rspcev if j < V j j 1 0 N 1 i = if if j < V j j 1 < V if j < V j j 1 if j < V j j 1 + 1 / j T U / s C y 0 N 1 i = if y < V y y + 1 / j T U / s C
323 281 315 322 syl6an φ j 0 N V i = T U / s C y 0 N 1 i = if y < V y y + 1 / j T U / s C
324 323 ex φ j 0 N V i = T U / s C y 0 N 1 i = if y < V y y + 1 / j T U / s C
325 222 224 324 rexlimd φ j 0 N V i = T U / s C y 0 N 1 i = if y < V y y + 1 / j T U / s C
326 221 325 impbid φ y 0 N 1 i = if y < V y y + 1 / j T U / s C j 0 N V i = T U / s C
327 187 326 bitr3d φ i ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B j 0 N V i = T U / s C
328 327 ralbidv φ i 0 N 1 i ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B i 0 N 1 j 0 N V i = T U / s C
329 132 328 syl5bb φ 0 N 1 ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B i 0 N 1 j 0 N V i = T U / s C
330 329 anbi1d φ 0 N 1 ran p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 B p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 p N 0 i 0 N 1 j 0 N V i = T U / s C p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 p N 0
331 1 4 5 6 poimirlem23 φ p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 p N 0 ¬ V = N T N = 0 U N = N
332 331 anbi2d φ i 0 N 1 j 0 N V i = T U / s C p ran y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 p N 0 i 0 N 1 j 0 N V i = T U / s C ¬ V = N T N = 0 U N = N
333 131 330 332 3bitrd φ x 0 K 1 N 0 N 1 x = y 0 N 1 if y < V y y + 1 / j T + f U 1 j × 1 U j + 1 N × 0 0 N 1 ran p ran x B p ran x p N 0 i 0 N 1 j 0 N V i = T U / s C ¬ V = N T N = 0 U N = N