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

Theorem lvolnlelpln 30382
 Description: A lattice plane cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.)
Hypotheses
Ref Expression
lvolnlelpln.l
lvolnlelpln.p
lvolnlelpln.v
Assertion
Ref Expression
lvolnlelpln

Proof of Theorem lvolnlelpln
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 959 . . 3
2 eqid 2436 . . . . 5
3 lvolnlelpln.l . . . . 5
4 eqid 2436 . . . . 5
5 eqid 2436 . . . . 5
6 lvolnlelpln.p . . . . 5
72, 3, 4, 5, 6islpln2 30333 . . . 4
91, 8mpbid 202 . 2
10 simp1l1 1050 . . . . . . . 8
11 simp1l2 1051 . . . . . . . 8
12 simp1r 982 . . . . . . . 8
13 simp2l 983 . . . . . . . 8
14 simp2r 984 . . . . . . . 8
15 lvolnlelpln.v . . . . . . . . 9
163, 4, 5, 15lvolnle3at 30379 . . . . . . . 8
1710, 11, 12, 13, 14, 16syl23anc 1191 . . . . . . 7
18 simp33 995 . . . . . . . 8
1918breq2d 4224 . . . . . . 7
2017, 19mtbird 293 . . . . . 6
21203exp 1152 . . . . 5
2221rexlimdvv 2836 . . . 4
2322rexlimdva 2830 . . 3