ax1ne0

Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1ne0 . (Contributed by NM, 19-Mar-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	ax1ne0	$⊢ 1 \neq 0$

Proof

Step	Hyp	Ref	Expression
1		1ne0sr	$⊢ \neg 1_{𝑹} = 0_{𝑹}$
2		1sr	$⊢ 1_{𝑹} \in 𝑹$
3	2	elexi	$⊢ 1_{𝑹} \in V$
4	3	eqresr	$⊢ ⟨1_{𝑹}, 0_{𝑹}⟩ = ⟨0_{𝑹}, 0_{𝑹}⟩ \leftrightarrow 1_{𝑹} = 0_{𝑹}$
5	1 4	mtbir	$⊢ \neg ⟨1_{𝑹}, 0_{𝑹}⟩ = ⟨0_{𝑹}, 0_{𝑹}⟩$
6		df-1	$⊢ 1 = ⟨1_{𝑹}, 0_{𝑹}⟩$
7		df-0	$⊢ 0 = ⟨0_{𝑹}, 0_{𝑹}⟩$
8	6 7	eqeq12i	$⊢ 1 = 0 \leftrightarrow ⟨1_{𝑹}, 0_{𝑹}⟩ = ⟨0_{𝑹}, 0_{𝑹}⟩$
9	5 8	mtbir	$⊢ \neg 1 = 0$
10	9	neir	$⊢ 1 \neq 0$

Metamath Proof Explorer

Theorem ax1ne0

Proof