Description: Lemma for poimir showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) of Kulpa p. 548. (Contributed by Brendan Leahy, 21-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | poimir.0 | |
|
poimirlem28.1 | |
||
poimirlem28.2 | |
||
poimirlem28.3 | |
||
poimirlem28.4 | |
||
Assertion | poimirlem27 | |