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

Theorem atnle 29800
 Description: Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 23832 analog.) (Contributed by NM, 5-Nov-2012.)
Hypotheses
Ref Expression
atnle.b
atnle.l
atnle.m
atnle.z
atnle.a
Assertion
Ref Expression
atnle

Proof of Theorem atnle
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpl1 960 . . . . . 6
2 atllat 29783 . . . . . . . . 9
323ad2ant1 978 . . . . . . . 8
4 atnle.b . . . . . . . . . 10
5 atnle.a . . . . . . . . . 10
64, 5atbase 29772 . . . . . . . . 9
763ad2ant2 979 . . . . . . . 8
8 simp3 959 . . . . . . . 8
9 atnle.m . . . . . . . . 9
104, 9latmcl 14435 . . . . . . . 8
113, 7, 8, 10syl3anc 1184 . . . . . . 7
1211adantr 452 . . . . . 6
13 simpr 448 . . . . . 6
14 atnle.l . . . . . . 7
15 atnle.z . . . . . . 7
164, 14, 15, 5atlex 29799 . . . . . 6
171, 12, 13, 16syl3anc 1184 . . . . 5
18 simpl1 960 . . . . . . . . . 10
1918, 2syl 16 . . . . . . . . 9
204, 5atbase 29772 . . . . . . . . . 10
2120adantl 453 . . . . . . . . 9
22 simpl2 961 . . . . . . . . . 10
2322, 6syl 16 . . . . . . . . 9
24 simpl3 962 . . . . . . . . 9
254, 14, 9latlem12 14462 . . . . . . . . 9
2619, 21, 23, 24, 25syl13anc 1186 . . . . . . . 8
27 simpr 448 . . . . . . . . . . 11
2814, 5atcmp 29794 . . . . . . . . . . 11
2918, 27, 22, 28syl3anc 1184 . . . . . . . . . 10
30 breq1 4175 . . . . . . . . . . 11
3130biimpd 199 . . . . . . . . . 10
3229, 31syl6bi 220 . . . . . . . . 9
3332imp3a 421 . . . . . . . 8
3426, 33sylbird 227 . . . . . . 7
3534adantlr 696 . . . . . 6
3635rexlimdva 2790 . . . . 5
3717, 36mpd 15 . . . 4
3837ex 424 . . 3
3938necon1bd 2635 . 2
4015, 5atn0 29791 . . . 4