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

Theorem lvolex3N 30272
 Description: There is an atom outside of a lattice plane i.e. a 3-dimensional lattice volume exists. (Contributed by NM, 28-Jul-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
lvolex3.l
lvolex3.a
lvolex3.p
Assertion
Ref Expression
lvolex3N
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem lvolex3N
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2435 . . . 4
2 lvolex3.l . . . 4
3 eqid 2435 . . . 4
4 lvolex3.a . . . 4
5 lvolex3.p . . . 4
61, 2, 3, 4, 5islpln2 30270 . . 3
7 simp1l 981 . . . . . . . 8
8 simp1rl 1022 . . . . . . . 8
9 simp1rr 1023 . . . . . . . 8
10 simp2 958 . . . . . . . 8
113, 2, 43dim3 30203 . . . . . . . 8
127, 8, 9, 10, 11syl13anc 1186 . . . . . . 7
13 simp33 995 . . . . . . . 8
14 breq2 4208 . . . . . . . . . 10
1514notbid 286 . . . . . . . . 9
1615rexbidv 2718 . . . . . . . 8
1713, 16syl 16 . . . . . . 7
1812, 17mpbird 224 . . . . . 6
1918rexlimdv3a 2824 . . . . 5
2019rexlimdvva 2829 . . . 4