Metamath Proof Explorer


Theorem atleneN

Description: Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses atlene.l ˙=K
atlene.j ˙=joinK
atlene.a A=AtomsK
Assertion atleneN KHLPAQARAPRP˙Q˙RQR

Proof

Step Hyp Ref Expression
1 atlene.l ˙=K
2 atlene.j ˙=joinK
3 atlene.a A=AtomsK
4 eqid K=K
5 1 2 4 3 atcvrj1 KHLPAQARAPRP˙Q˙RPKQ˙R
6 2 4 3 atcvrneN KHLPAQARAPKQ˙RQR
7 5 6 syld3an3 KHLPAQARAPRP˙Q˙RQR