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

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

Proof of Theorem lvolnlelln
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 960 . . 3
2 eqid 2437 . . . . 5
3 eqid 2437 . . . . 5
4 eqid 2437 . . . . 5
5 lvolnlelln.n . . . . 5
62, 3, 4, 5islln2 30309 . . . 4
81, 7mpbid 203 . 2
9 simp11 988 . . . . . . 7
10 simp12 989 . . . . . . 7
11 simp2l 984 . . . . . . 7
12 simp2r 985 . . . . . . 7
13 lvolnlelln.l . . . . . . . 8
14 lvolnlelln.v . . . . . . . 8
1513, 3, 4, 14lvolnle3at 30380 . . . . . . 7
169, 10, 11, 11, 12, 15syl23anc 1192 . . . . . 6
17 simp3r 987 . . . . . . . 8
183, 4hlatjidm 30167 . . . . . . . . . 10
199, 11, 18syl2anc 644 . . . . . . . . 9
2019oveq1d 6097 . . . . . . . 8
2117, 20eqtr4d 2472 . . . . . . 7
2221breq2d 4225 . . . . . 6
2316, 22mtbird 294 . . . . 5
24233exp 1153 . . . 4
2524rexlimdvv 2837 . . 3