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		ioran	$⊢ \neg (a \neq c \lor b \neq d) \leftrightarrow (\neg a \neq c \land \neg b \neq d)$
19		df-ne	$⊢ a \neq c \leftrightarrow \neg a = c$
20	19	con2bii	$⊢ a = c \leftrightarrow \neg a \neq c$
21		df-ne	$⊢ b \neq d \leftrightarrow \neg b = d$
22	21	con2bii	$⊢ b = d \leftrightarrow \neg b \neq d$
23	20 22	anbi12i	$⊢ (a = c \land b = d) \leftrightarrow (\neg a \neq c \land \neg b \neq d)$
24	18 23	bitr4i	$⊢ \neg (a \neq c \lor b \neq d) \leftrightarrow (a = c \land b = d)$
25		id	$⊢ a = c \to a = c$
26		oveq2	$⊢ b = d \to i b = i d$
27	25 26	oveqan12d	$⊢ (a = c \land b = d) \to a + i b = c + i d$
28	24 27	sylbi	$⊢ \neg (a \neq c \lor b \neq d) \to a + i b = c + i d$
29	28	necon1ai	$⊢ a + i b \neq c + i d \to (a \neq c \lor b \neq d)$
30		neeq1	$⊢ x = a \to (x \neq y \leftrightarrow a \neq y)$
31		neeq2	$⊢ y = c \to (a \neq y \leftrightarrow a \neq c)$
32	30 31	rspc2ev	$⊢ (a \in ℝ \land c \in ℝ \land a \neq c) \to \exists x \in ℝ \exists y \in ℝ x \neq y$
33	32	3expia	$⊢ (a \in ℝ \land c \in ℝ) \to (a \neq c \to \exists x \in ℝ \exists y \in ℝ x \neq y)$
34	33	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)$
35		neeq1	$⊢ x = b \to (x \neq y \leftrightarrow b \neq y)$
36		neeq2	$⊢ y = d \to (b \neq y \leftrightarrow b \neq d)$
37	35 36	rspc2ev	$⊢ (b \in ℝ \land d \in ℝ \land b \neq d) \to \exists x \in ℝ \exists y \in ℝ x \neq y$
38	37	3expia	$⊢ (b \in ℝ \land d \in ℝ) \to (b \neq d \to \exists x \in ℝ \exists y \in ℝ x \neq y)$
39	38	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)$
40	34 39	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)$
41	29 40	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)$
42	41	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)$
43	42	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$
44	1 17 43	mp2b	$⊢ \exists x \in ℝ \exists y \in ℝ x \neq y$
45		eqtr3	$⊢ (x = 0 \land y = 0) \to x = y$
46	45	ex	$⊢ x = 0 \to (y = 0 \to x = y)$
47	46	necon3d	$⊢ x = 0 \to (x \neq y \to y \neq 0)$
48		neeq1	$⊢ z = y \to (z \neq 0 \leftrightarrow y \neq 0)$
49	48	rspcev	$⊢ (y \in ℝ \land y \neq 0) \to \exists z \in ℝ z \neq 0$
50	49	expcom	$⊢ y \neq 0 \to (y \in ℝ \to \exists z \in ℝ z \neq 0)$
51	47 50	syl6	$⊢ x = 0 \to (x \neq y \to (y \in ℝ \to \exists z \in ℝ z \neq 0))$
52	51	com23	$⊢ x = 0 \to (y \in ℝ \to (x \neq y \to \exists z \in ℝ z \neq 0))$
53	52	adantld	$⊢ x = 0 \to ((x \in ℝ \land y \in ℝ) \to (x \neq y \to \exists z \in ℝ z \neq 0))$
54		neeq1	$⊢ z = x \to (z \neq 0 \leftrightarrow x \neq 0)$
55	54	rspcev	$⊢ (x \in ℝ \land x \neq 0) \to \exists z \in ℝ z \neq 0$
56	55	expcom	$⊢ x \neq 0 \to (x \in ℝ \to \exists z \in ℝ z \neq 0)$
57	56	adantrd	$⊢ x \neq 0 \to ((x \in ℝ \land y \in ℝ) \to \exists z \in ℝ z \neq 0)$
58	57	a1dd	$⊢ x \neq 0 \to ((x \in ℝ \land y \in ℝ) \to (x \neq y \to \exists z \in ℝ z \neq 0))$
59	53 58	pm2.61ine	$⊢ (x \in ℝ \land y \in ℝ) \to (x \neq y \to \exists z \in ℝ z \neq 0)$
60	59	rexlimivv	$⊢ \exists x \in ℝ \exists y \in ℝ x \neq y \to \exists z \in ℝ z \neq 0$
61		ax-rrecex	$⊢ (z \in ℝ \land z \neq 0) \to \exists x \in ℝ z x = 1$
62		remulcl	$⊢ (z \in ℝ \land x \in ℝ) \to z x \in ℝ$
63	62	adantlr	$⊢ ((z \in ℝ \land z \neq 0) \land x \in ℝ) \to z x \in ℝ$
64		eleq1	$⊢ z x = 1 \to (z x \in ℝ \leftrightarrow 1 \in ℝ)$
65	63 64	syl5ibcom	$⊢ ((z \in ℝ \land z \neq 0) \land x \in ℝ) \to (z x = 1 \to 1 \in ℝ)$
66	65	rexlimdva	$⊢ (z \in ℝ \land z \neq 0) \to (\exists x \in ℝ z x = 1 \to 1 \in ℝ)$
67	61 66	mpd	$⊢ (z \in ℝ \land z \neq 0) \to 1 \in ℝ$
68	67	rexlimiva	$⊢ \exists z \in ℝ z \neq 0 \to 1 \in ℝ$
69	44 60 68	mp2b	$⊢ 1 \in ℝ$

Metamath Proof Explorer

Theorem 1re

Proof