Metamath Proof Explorer


Theorem opltn0

Description: A lattice element greater than zero is nonzero. TODO: is this needed? (Contributed by NM, 1-Jun-2012)

Ref Expression
Hypotheses opltne0.b B = Base K
opltne0.s < ˙ = < K
opltne0.z 0 ˙ = 0. K
Assertion opltn0 K OP X B 0 ˙ < ˙ X X 0 ˙

Proof

Step Hyp Ref Expression
1 opltne0.b B = Base K
2 opltne0.s < ˙ = < K
3 opltne0.z 0 ˙ = 0. K
4 simpl K OP X B K OP
5 1 3 op0cl K OP 0 ˙ B
6 5 adantr K OP X B 0 ˙ B
7 simpr K OP X B X B
8 eqid K = K
9 8 2 pltval K OP 0 ˙ B X B 0 ˙ < ˙ X 0 ˙ K X 0 ˙ X
10 4 6 7 9 syl3anc K OP X B 0 ˙ < ˙ X 0 ˙ K X 0 ˙ X
11 necom X 0 ˙ 0 ˙ X
12 1 8 3 op0le K OP X B 0 ˙ K X
13 12 biantrurd K OP X B 0 ˙ X 0 ˙ K X 0 ˙ X
14 11 13 syl5rbb K OP X B 0 ˙ K X 0 ˙ X X 0 ˙
15 10 14 bitrd K OP X B 0 ˙ < ˙ X X 0 ˙