Description: A lattice plane is not less than or equal to a lattice line. (Contributed by NM, 14-Jul-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lplnnlelln.l | |
|
lplnnlelln.n | |
||
lplnnlelln.p | |
||
Assertion | lplnnlelln | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lplnnlelln.l | |
|
2 | lplnnlelln.n | |
|
3 | lplnnlelln.p | |
|
4 | simp3 | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | 5 6 7 2 | islln2 | |
9 | 8 | 3ad2ant1 | |
10 | 4 9 | mpbid | |
11 | simp11 | |
|
12 | simp12 | |
|
13 | simp2l | |
|
14 | simp2r | |
|
15 | 1 6 7 3 | lplnnle2at | |
16 | 11 12 13 14 15 | syl13anc | |
17 | simp3r | |
|
18 | 17 | breq2d | |
19 | 16 18 | mtbird | |
20 | 19 | 3exp | |
21 | 20 | rexlimdvv | |
22 | 21 | adantld | |
23 | 10 22 | mpd | |