Theorem 0ltat

Description: An atom is greater than zero. (Contributed by NM, 4-Jul-2012)

	Ref	Expression
Hypotheses	0ltat.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	0ltat.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	0ltat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	0ltat	$$⊢\left(K\in \mathrm{OP}\wedge P\in A\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}P$$

Proof

Step	Hyp	Ref	Expression
1		0ltat.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
2		0ltat.s	$$⊢\underset{\dot{}}{<}={<}_K$$
3		0ltat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		simpl	$$⊢\left(K\in \mathrm{OP}\wedge P\in A\right)\to K\in \mathrm{OP}$$
5		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
6	5 1	op0cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
7	6	adantr	$$⊢\left(K\in \mathrm{OP}\wedge P\in A\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
8	5 3	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
9	8	adantl	$$⊢\left(K\in \mathrm{OP}\wedge P\in A\right)\to P\in {\mathrm{Base}}_K$$
10		eqid	$$⊢{⋖}_K={⋖}_K$$
11	1 10 3	atcvr0	$$⊢\left(K\in \mathrm{OP}\wedge P\in A\right)\to \underset{\dot{}}{0}{⋖}_{K}P$$
12	5 2 10	cvrlt	$$⊢\left(\left(K\in \mathrm{OP}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_K\wedge P\in {\mathrm{Base}}_K\right)\wedge \underset{\dot{}}{0}{⋖}_{K}P\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}P$$
13	4 7 9 11 12	syl31anc	$$⊢\left(K\in \mathrm{OP}\wedge P\in A\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}P$$