Theorem 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 ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	⊢ 1 ≠ 0
2		ax-1cn	⊢ 1 ∈ ℂ
3		cnre	⊢ ( 1 ∈ ℂ → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 1 = ( 𝑎 + ( i · 𝑏 ) ) )
4	2 3	ax-mp	⊢ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 1 = ( 𝑎 + ( i · 𝑏 ) )
5		neeq1	⊢ ( 1 = ( 𝑎 + ( i · 𝑏 ) ) → ( 1 ≠ 0 ↔ ( 𝑎 + ( i · 𝑏 ) ) ≠ 0 ) )
6	5	biimpcd	⊢ ( 1 ≠ 0 → ( 1 = ( 𝑎 + ( i · 𝑏 ) ) → ( 𝑎 + ( i · 𝑏 ) ) ≠ 0 ) )
7		0cn	⊢ 0 ∈ ℂ
8		cnre	⊢ ( 0 ∈ ℂ → ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ 0 = ( 𝑐 + ( i · 𝑑 ) ) )
9	7 8	ax-mp	⊢ ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ 0 = ( 𝑐 + ( i · 𝑑 ) )
10		neeq2	⊢ ( 0 = ( 𝑐 + ( i · 𝑑 ) ) → ( ( 𝑎 + ( i · 𝑏 ) ) ≠ 0 ↔ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) ) )
11	10	biimpcd	⊢ ( ( 𝑎 + ( i · 𝑏 ) ) ≠ 0 → ( 0 = ( 𝑐 + ( i · 𝑑 ) ) → ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) ) )
12	11	reximdv	⊢ ( ( 𝑎 + ( i · 𝑏 ) ) ≠ 0 → ( ∃ 𝑑 ∈ ℝ 0 = ( 𝑐 + ( i · 𝑑 ) ) → ∃ 𝑑 ∈ ℝ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) ) )
13	12	reximdv	⊢ ( ( 𝑎 + ( i · 𝑏 ) ) ≠ 0 → ( ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ 0 = ( 𝑐 + ( i · 𝑑 ) ) → ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) ) )
14	6 9 13	syl6mpi	⊢ ( 1 ≠ 0 → ( 1 = ( 𝑎 + ( i · 𝑏 ) ) → ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) ) )
15	14	reximdv	⊢ ( 1 ≠ 0 → ( ∃ 𝑏 ∈ ℝ 1 = ( 𝑎 + ( i · 𝑏 ) ) → ∃ 𝑏 ∈ ℝ ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) ) )
16	15	reximdv	⊢ ( 1 ≠ 0 → ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 1 = ( 𝑎 + ( i · 𝑏 ) ) → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) ) )
17	4 16	mpi	⊢ ( 1 ≠ 0 → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) )
18		ioran	⊢ ( ¬ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ↔ ( ¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑 ) )
19		df-ne	⊢ ( 𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐 )
20	19	con2bii	⊢ ( 𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐 )
21		df-ne	⊢ ( 𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑 )
22	21	con2bii	⊢ ( 𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑 )
23	20 22	anbi12i	⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ↔ ( ¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑 ) )
24	18 23	bitr4i	⊢ ( ¬ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ↔ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) )
25		id	⊢ ( 𝑎 = 𝑐 → 𝑎 = 𝑐 )
26		oveq2	⊢ ( 𝑏 = 𝑑 → ( i · 𝑏 ) = ( i · 𝑑 ) )
27	25 26	oveqan12d	⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 + ( i · 𝑏 ) ) = ( 𝑐 + ( i · 𝑑 ) ) )
28	24 27	sylbi	⊢ ( ¬ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) → ( 𝑎 + ( i · 𝑏 ) ) = ( 𝑐 + ( i · 𝑑 ) ) )
29	28	necon1ai	⊢ ( ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) )
30		neeq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦 ) )
31		neeq2	⊢ ( 𝑦 = 𝑐 → ( 𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐 ) )
32	30 31	rspc2ev	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 )
33	32	3expia	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑎 ≠ 𝑐 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
34	33	ad2ant2r	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑎 ≠ 𝑐 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
35		neeq1	⊢ ( 𝑥 = 𝑏 → ( 𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦 ) )
36		neeq2	⊢ ( 𝑦 = 𝑑 → ( 𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑 ) )
37	35 36	rspc2ev	⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 )
38	37	3expia	⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑏 ≠ 𝑑 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
39	38	ad2ant2l	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑏 ≠ 𝑑 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
40	34 39	jaod	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
41	29 40	syl5	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
42	41	rexlimdvva	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
43	42	rexlimivv	⊢ ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 )
44	1 17 43	mp2b	⊢ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3	⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) → 𝑥 = 𝑦 )
46	45	ex	⊢ ( 𝑥 = 0 → ( 𝑦 = 0 → 𝑥 = 𝑦 ) )
47	46	necon3d	⊢ ( 𝑥 = 0 → ( 𝑥 ≠ 𝑦 → 𝑦 ≠ 0 ) )
48		neeq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ≠ 0 ↔ 𝑦 ≠ 0 ) )
49	48	rspcev	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑦 ≠ 0 ) → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 )
50	49	expcom	⊢ ( 𝑦 ≠ 0 → ( 𝑦 ∈ ℝ → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) )
51	47 50	syl6	⊢ ( 𝑥 = 0 → ( 𝑥 ≠ 𝑦 → ( 𝑦 ∈ ℝ → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) ) )
52	51	com23	⊢ ( 𝑥 = 0 → ( 𝑦 ∈ ℝ → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) ) )
53	52	adantld	⊢ ( 𝑥 = 0 → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) ) )
54		neeq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ≠ 0 ↔ 𝑥 ≠ 0 ) )
55	54	rspcev	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 )
56	55	expcom	⊢ ( 𝑥 ≠ 0 → ( 𝑥 ∈ ℝ → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) )
57	56	adantrd	⊢ ( 𝑥 ≠ 0 → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) )
58	57	a1dd	⊢ ( 𝑥 ≠ 0 → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) ) )
59	53 58	pm2.61ine	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) )
60	59	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 )
61		ax-rrecex	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑧 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝑧 · 𝑥 ) = 1 )
62		remulcl	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑧 · 𝑥 ) ∈ ℝ )
63	62	adantlr	⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑧 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑧 · 𝑥 ) ∈ ℝ )
64		eleq1	⊢ ( ( 𝑧 · 𝑥 ) = 1 → ( ( 𝑧 · 𝑥 ) ∈ ℝ ↔ 1 ∈ ℝ ) )
65	63 64	syl5ibcom	⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑧 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑧 · 𝑥 ) = 1 → 1 ∈ ℝ ) )
66	65	rexlimdva	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑧 ≠ 0 ) → ( ∃ 𝑥 ∈ ℝ ( 𝑧 · 𝑥 ) = 1 → 1 ∈ ℝ ) )
67	61 66	mpd	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑧 ≠ 0 ) → 1 ∈ ℝ )
68	67	rexlimiva	⊢ ( ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ )
69	44 60 68	mp2b	⊢ 1 ∈ ℝ