Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lclkrlem2d Structured version   Unicode version

Theorem lclkrlem2d 32245
 Description: Lemma for lclkr 32268. (Contributed by NM, 16-Jan-2015.)
Hypotheses
Ref Expression
lclkrlem2a.h
lclkrlem2a.o
lclkrlem2a.u
lclkrlem2a.v
lclkrlem2a.z
lclkrlem2a.p
lclkrlem2a.n
lclkrlem2a.a LSAtoms
lclkrlem2a.k
lclkrlem2a.b
lclkrlem2a.x
lclkrlem2a.y
lclkrlem2a.e
lclkrlem2b.da
lclkrlem2d.i
Assertion
Ref Expression
lclkrlem2d

Proof of Theorem lclkrlem2d
StepHypRef Expression
1 lclkrlem2a.h . 2
2 lclkrlem2a.u . 2
3 lclkrlem2a.v . 2
4 lclkrlem2a.p . 2
5 lclkrlem2a.n . 2
6 lclkrlem2d.i . 2
7 lclkrlem2a.k . 2
8 lclkrlem2a.x . . . . . 6
98eldifad 3324 . . . . 5
109snssd 3935 . . . 4
11 lclkrlem2a.o . . . . 5
121, 6, 2, 3, 11dochcl 32088 . . . 4
137, 10, 12syl2anc 643 . . 3
14 lclkrlem2a.y . . . . . 6
1514eldifad 3324 . . . . 5
1615snssd 3935 . . . 4
171, 6, 2, 3, 11dochcl 32088 . . . 4
187, 16, 17syl2anc 643 . . 3
191, 6dihmeetcl 32080 . . 3
207, 13, 18, 19syl12anc 1182 . 2
21 lclkrlem2a.b . . 3