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

Theorem atnle 30177
 Description: Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 23881 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 961 . . . . . 6
2 atllat 30160 . . . . . . . . 9
323ad2ant1 979 . . . . . . . 8
4 atnle.b . . . . . . . . . 10
5 atnle.a . . . . . . . . . 10
64, 5atbase 30149 . . . . . . . . 9
763ad2ant2 980 . . . . . . . 8
8 simp3 960 . . . . . . . 8
9 atnle.m . . . . . . . . 9
104, 9latmcl 14482 . . . . . . . 8
113, 7, 8, 10syl3anc 1185 . . . . . . 7
1211adantr 453 . . . . . 6
13 simpr 449 . . . . . 6
14 atnle.l . . . . . . 7
15 atnle.z . . . . . . 7
164, 14, 15, 5atlex 30176 . . . . . 6
171, 12, 13, 16syl3anc 1185 . . . . 5
18 simpl1 961 . . . . . . . . . 10
1918, 2syl 16 . . . . . . . . 9
204, 5atbase 30149 . . . . . . . . . 10
2120adantl 454 . . . . . . . . 9
22 simpl2 962 . . . . . . . . . 10
2322, 6syl 16 . . . . . . . . 9
24 simpl3 963 . . . . . . . . 9
254, 14, 9latlem12 14509 . . . . . . . . 9
2619, 21, 23, 24, 25syl13anc 1187 . . . . . . . 8
27 simpr 449 . . . . . . . . . . 11
2814, 5atcmp 30171 . . . . . . . . . . 11
2918, 27, 22, 28syl3anc 1185 . . . . . . . . . 10
30 breq1 4217 . . . . . . . . . . 11
3130biimpd 200 . . . . . . . . . 10
3229, 31syl6bi 221 . . . . . . . . 9
3332imp3a 422 . . . . . . . 8
3426, 33sylbird 228 . . . . . . 7
3534adantlr 697 . . . . . 6
3635rexlimdva 2832 . . . . 5
3717, 36mpd 15 . . . 4
3837ex 425 . . 3
3938necon1bd 2674 . 2
4015, 5atn0 30168 . . . 4