1re

Description: The number 1 is real. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn , by exploiting properties of the imaginary unit _i . (Contributed by Eric Schmidt, 11-Apr-2007) (Revised by Scott Fenton, 3-Jan-2013)

		Ref	Expression
	Assertion	1re	$⊢ 1 \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	$⊢ 1 \neq 0$
2		ax-1cn	$⊢ 1 \in ℂ$
3		cnre	$⊢ 1 \in ℂ \to \exists a \in ℝ \exists b \in ℝ 1 = a + i b$
4	2 3	ax-mp	$⊢ \exists a \in ℝ \exists b \in ℝ 1 = a + i b$
5		neeq1	$⊢ 1 = a + i b \to (1 \neq 0 \leftrightarrow a + i b \neq 0)$
6	5	biimpcd	$⊢ 1 \neq 0 \to (1 = a + i b \to a + i b \neq 0)$
7		0cn	$⊢ 0 \in ℂ$
8		cnre	$⊢ 0 \in ℂ \to \exists c \in ℝ \exists d \in ℝ 0 = c + i d$
9	7 8	ax-mp	$⊢ \exists c \in ℝ \exists d \in ℝ 0 = c + i d$
10		neeq2	$⊢ 0 = c + i d \to (a + i b \neq 0 \leftrightarrow a + i b \neq c + i d)$
11	10	biimpcd	$⊢ a + i b \neq 0 \to (0 = c + i d \to a + i b \neq c + i d)$
12	11	reximdv	$⊢ a + i b \neq 0 \to (\exists d \in ℝ 0 = c + i d \to \exists d \in ℝ a + i b \neq c + i d)$
13	12	reximdv	$⊢ a + i b \neq 0 \to (\exists c \in ℝ \exists d \in ℝ 0 = c + i d \to \exists c \in ℝ \exists d \in ℝ a + i b \neq c + i d)$
14	6 9 13	syl6mpi	$⊢ 1 \neq 0 \to (1 = a + i b \to \exists c \in ℝ \exists d \in ℝ a + i b \neq c + i d)$
15	14	reximdv	$⊢ 1 \neq 0 \to (\exists b \in ℝ 1 = a + i b \to \exists b \in ℝ \exists c \in ℝ \exists d \in ℝ a + i b \neq c + i d)$
16	15	reximdv	$⊢ 1 \neq 0 \to (\exists a \in ℝ \exists b \in ℝ 1 = a + i b \to \exists a \in ℝ \exists b \in ℝ \exists c \in ℝ \exists d \in ℝ a + i b \neq c + i d)$
17	4 16	mpi	$⊢ 1 \neq 0 \to \exists a \in ℝ \exists b \in ℝ \exists c \in ℝ \exists d \in ℝ a + i b \neq c + i d$
18		id	$⊢ a = c \to a = c$
19		oveq2	$⊢ b = d \to i b = i d$
20	18 19	oveqan12d	$⊢ (a = c \land b = d) \to a + i b = c + i d$
21	20	expcom	$⊢ b = d \to (a = c \to a + i b = c + i d)$
22	21	necon3d	$⊢ b = d \to (a + i b \neq c + i d \to a \neq c)$
23	22	com12	$⊢ a + i b \neq c + i d \to (b = d \to a \neq c)$
24	23	necon3bd	$⊢ a + i b \neq c + i d \to (\neg a \neq c \to b \neq d)$
25	24	orrd	$⊢ a + i b \neq c + i d \to (a \neq c \lor b \neq d)$
26		neeq1	$⊢ x = a \to (x \neq y \leftrightarrow a \neq y)$
27		neeq2	$⊢ y = c \to (a \neq y \leftrightarrow a \neq c)$
28	26 27	rspc2ev	$⊢ (a \in ℝ \land c \in ℝ \land a \neq c) \to \exists x \in ℝ \exists y \in ℝ x \neq y$
29	28	3expia	$⊢ (a \in ℝ \land c \in ℝ) \to (a \neq c \to \exists x \in ℝ \exists y \in ℝ x \neq y)$
30	29	ad2ant2r	$⊢ ((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \to (a \neq c \to \exists x \in ℝ \exists y \in ℝ x \neq y)$
31		neeq1	$⊢ x = b \to (x \neq y \leftrightarrow b \neq y)$
32		neeq2	$⊢ y = d \to (b \neq y \leftrightarrow b \neq d)$
33	31 32	rspc2ev	$⊢ (b \in ℝ \land d \in ℝ \land b \neq d) \to \exists x \in ℝ \exists y \in ℝ x \neq y$
34	33	3expia	$⊢ (b \in ℝ \land d \in ℝ) \to (b \neq d \to \exists x \in ℝ \exists y \in ℝ x \neq y)$
35	34	ad2ant2l	$⊢ ((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \to (b \neq d \to \exists x \in ℝ \exists y \in ℝ x \neq y)$
36	30 35	jaod	$⊢ ((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \to ((a \neq c \lor b \neq d) \to \exists x \in ℝ \exists y \in ℝ x \neq y)$
37	25 36	syl5	$⊢ ((a \in ℝ \land b \in ℝ) \land (c \in ℝ \land d \in ℝ)) \to (a + i b \neq c + i d \to \exists x \in ℝ \exists y \in ℝ x \neq y)$
38	37	rexlimdvva	$⊢ (a \in ℝ \land b \in ℝ) \to (\exists c \in ℝ \exists d \in ℝ a + i b \neq c + i d \to \exists x \in ℝ \exists y \in ℝ x \neq y)$
39	38	rexlimivv	$⊢ \exists a \in ℝ \exists b \in ℝ \exists c \in ℝ \exists d \in ℝ a + i b \neq c + i d \to \exists x \in ℝ \exists y \in ℝ x \neq y$
40	1 17 39	mp2b	$⊢ \exists x \in ℝ \exists y \in ℝ x \neq y$
41		eqtr3	$⊢ (x = 0 \land y = 0) \to x = y$
42	41	ex	$⊢ x = 0 \to (y = 0 \to x = y)$
43	42	necon3d	$⊢ x = 0 \to (x \neq y \to y \neq 0)$
44		neeq1	$⊢ z = y \to (z \neq 0 \leftrightarrow y \neq 0)$
45	44	rspcev	$⊢ (y \in ℝ \land y \neq 0) \to \exists z \in ℝ z \neq 0$
46	45	expcom	$⊢ y \neq 0 \to (y \in ℝ \to \exists z \in ℝ z \neq 0)$
47	43 46	syl6	$⊢ x = 0 \to (x \neq y \to (y \in ℝ \to \exists z \in ℝ z \neq 0))$
48	47	com23	$⊢ x = 0 \to (y \in ℝ \to (x \neq y \to \exists z \in ℝ z \neq 0))$
49	48	adantld	$⊢ x = 0 \to ((x \in ℝ \land y \in ℝ) \to (x \neq y \to \exists z \in ℝ z \neq 0))$
50		neeq1	$⊢ z = x \to (z \neq 0 \leftrightarrow x \neq 0)$
51	50	rspcev	$⊢ (x \in ℝ \land x \neq 0) \to \exists z \in ℝ z \neq 0$
52	51	expcom	$⊢ x \neq 0 \to (x \in ℝ \to \exists z \in ℝ z \neq 0)$
53	52	adantrd	$⊢ x \neq 0 \to ((x \in ℝ \land y \in ℝ) \to \exists z \in ℝ z \neq 0)$
54	53	a1dd	$⊢ x \neq 0 \to ((x \in ℝ \land y \in ℝ) \to (x \neq y \to \exists z \in ℝ z \neq 0))$
55	49 54	pm2.61ine	$⊢ (x \in ℝ \land y \in ℝ) \to (x \neq y \to \exists z \in ℝ z \neq 0)$
56	55	rexlimivv	$⊢ \exists x \in ℝ \exists y \in ℝ x \neq y \to \exists z \in ℝ z \neq 0$
57		ax-rrecex	$⊢ (z \in ℝ \land z \neq 0) \to \exists x \in ℝ z x = 1$
58		remulcl	$⊢ (z \in ℝ \land x \in ℝ) \to z x \in ℝ$
59	58	adantlr	$⊢ ((z \in ℝ \land z \neq 0) \land x \in ℝ) \to z x \in ℝ$
60		eleq1	$⊢ z x = 1 \to (z x \in ℝ \leftrightarrow 1 \in ℝ)$
61	59 60	syl5ibcom	$⊢ ((z \in ℝ \land z \neq 0) \land x \in ℝ) \to (z x = 1 \to 1 \in ℝ)$
62	61	rexlimdva	$⊢ (z \in ℝ \land z \neq 0) \to (\exists x \in ℝ z x = 1 \to 1 \in ℝ)$
63	57 62	mpd	$⊢ (z \in ℝ \land z \neq 0) \to 1 \in ℝ$
64	63	rexlimiva	$⊢ \exists z \in ℝ z \neq 0 \to 1 \in ℝ$
65	40 56 64	mp2b	$⊢ 1 \in ℝ$

Metamath Proof Explorer

Theorem 1re

Proof