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

Theorem atle 30307
 Description: Any non-zero element has an atom under it. (Contributed by NM, 28-Jun-2012.)
Hypotheses
Ref Expression
atle.b
atle.l
atle.z
atle.a
Assertion
Ref Expression
atle
Distinct variable groups:   ,   ,   ,   ,   ,   ,

Proof of Theorem atle
StepHypRef Expression
1 simp1 958 . . 3
2 hlop 30234 . . . . 5
323ad2ant1 979 . . . 4
4 atle.b . . . . 5
5 atle.z . . . . 5
64, 5op0cl 30056 . . . 4
73, 6syl 16 . . 3
8 simp2 959 . . 3
9 simp3 960 . . . 4
10 eqid 2438 . . . . . 6
114, 10, 5opltn0 30062 . . . . 5
123, 8, 11syl2anc 644 . . . 4
139, 12mpbird 225 . . 3
14 atle.l . . . 4
15 eqid 2438 . . . 4
16 atle.a . . . 4
174, 14, 10, 15, 16hlrelat 30273 . . 3
181, 7, 8, 13, 17syl31anc 1188 . 2
19 simpl1 961 . . . . . . . 8
20 hlol 30233 . . . . . . . 8
2119, 20syl 16 . . . . . . 7
224, 16atbase 30161 . . . . . . . 8
2322adantl 454 . . . . . . 7
244, 15, 5olj02 30098 . . . . . . 7
2521, 23, 24syl2anc 644 . . . . . 6
2625breq1d 4225 . . . . 5
2726biimpd 200 . . . 4