sn-1ne2

		Ref	Expression
	Assertion	sn-1ne2	$⊢ 1 \neq 2$

Proof

Step	Hyp	Ref	Expression
1		0ne1	$⊢ 0 \neq 1$
2		ax-icn	$⊢ i \in ℂ$
3	2 2	mulcli	$⊢ i i \in ℂ$
4		ax-1cn	$⊢ 1 \in ℂ$
5	3 4 4	addassi	$⊢ i i + 1 + 1 = i i + 1 + 1$
6	5	a1i	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to i i + 1 + 1 = i i + 1 + 1$
7		simpr	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to 1 = 1 + 1$
8	7	oveq2d	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to i i + 1 = i i + 1 + 1$
9		ax-i2m1	$⊢ i i + 1 = 0$
10	9	a1i	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to i i + 1 = 0$
11	6 8 10	3eqtr2rd	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to 0 = i i + 1 + 1$
12		simpl	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to 0 = 0 + 0$
13	10	oveq1d	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to i i + 1 + 1 = 0 + 1$
14	11 12 13	3eqtr3d	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to 0 + 0 = 0 + 1$
15		0red	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to 0 \in ℝ$
16		1red	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to 1 \in ℝ$
17		readdcan	$⊢ (0 \in ℝ \land 1 \in ℝ \land 0 \in ℝ) \to (0 + 0 = 0 + 1 \leftrightarrow 0 = 1)$
18	15 16 15 17	syl3anc	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to (0 + 0 = 0 + 1 \leftrightarrow 0 = 1)$
19	14 18	mpbid	$⊢ (0 = 0 + 0 \land 1 = 1 + 1) \to 0 = 1$
20	19	ex	$⊢ 0 = 0 + 0 \to (1 = 1 + 1 \to 0 = 1)$
21	20	necon3d	$⊢ 0 = 0 + 0 \to (0 \neq 1 \to 1 \neq 1 + 1)$
22	1 21	mpi	$⊢ 0 = 0 + 0 \to 1 \neq 1 + 1$
23		oveq2	$⊢ 1 = 1 + 1 \to 0 \cdot 1 = 0 \cdot (1 + 1)$
24		0re	$⊢ 0 \in ℝ$
25		ax-1rid	$⊢ 0 \in ℝ \to 0 \cdot 1 = 0$
26	24 25	ax-mp	$⊢ 0 \cdot 1 = 0$
27		0cn	$⊢ 0 \in ℂ$
28	27 4 4	adddii	$⊢ 0 \cdot (1 + 1) = 0 \cdot 1 + 0 \cdot 1$
29	26 26	oveq12i	$⊢ 0 \cdot 1 + 0 \cdot 1 = 0 + 0$
30	28 29	eqtri	$⊢ 0 \cdot (1 + 1) = 0 + 0$
31	23 26 30	3eqtr3g	$⊢ 1 = 1 + 1 \to 0 = 0 + 0$
32	31	necon3i	$⊢ 0 \neq 0 + 0 \to 1 \neq 1 + 1$
33	22 32	pm2.61ine	$⊢ 1 \neq 1 + 1$
34		df-2	$⊢ 2 = 1 + 1$
35	33 34	neeqtrri	$⊢ 1 \neq 2$

Metamath Proof Explorer

Theorem sn-1ne2

Proof