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

Theorem lplnnlelln 30340
 Description: A lattice plane is not less than or equal to a lattice line. (Contributed by NM, 14-Jul-2012.)
Hypotheses
Ref Expression
lplnnlelln.l
lplnnlelln.n
lplnnlelln.p
Assertion
Ref Expression
lplnnlelln

Proof of Theorem lplnnlelln
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 959 . . 3
2 eqid 2436 . . . . 5
3 eqid 2436 . . . . 5
4 eqid 2436 . . . . 5
5 lplnnlelln.n . . . . 5
62, 3, 4, 5islln2 30308 . . . 4
81, 7mpbid 202 . 2
9 simp11 987 . . . . . . 7
10 simp12 988 . . . . . . 7
11 simp2l 983 . . . . . . 7
12 simp2r 984 . . . . . . 7
13 lplnnlelln.l . . . . . . . 8
14 lplnnlelln.p . . . . . . . 8
1513, 3, 4, 14lplnnle2at 30338 . . . . . . 7
169, 10, 11, 12, 15syl13anc 1186 . . . . . 6
17 simp3r 986 . . . . . . 7
1817breq2d 4224 . . . . . 6
1916, 18mtbird 293 . . . . 5
20193exp 1152 . . . 4
2120rexlimdvv 2836 . . 3