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		id	⊢ ( 𝑎 = 𝑐 → 𝑎 = 𝑐 )
19		oveq2	⊢ ( 𝑏 = 𝑑 → ( i · 𝑏 ) = ( i · 𝑑 ) )
20	18 19	oveqan12d	⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 + ( i · 𝑏 ) ) = ( 𝑐 + ( i · 𝑑 ) ) )
21	20	expcom	⊢ ( 𝑏 = 𝑑 → ( 𝑎 = 𝑐 → ( 𝑎 + ( i · 𝑏 ) ) = ( 𝑐 + ( i · 𝑑 ) ) ) )
22	21	necon3d	⊢ ( 𝑏 = 𝑑 → ( ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → 𝑎 ≠ 𝑐 ) )
23	22	com12	⊢ ( ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → ( 𝑏 = 𝑑 → 𝑎 ≠ 𝑐 ) )
24	23	necon3bd	⊢ ( ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → ( ¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑 ) )
25	24	orrd	⊢ ( ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) )
26		neeq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦 ) )
27		neeq2	⊢ ( 𝑦 = 𝑐 → ( 𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐 ) )
28	26 27	rspc2ev	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 )
29	28	3expia	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑎 ≠ 𝑐 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
30	29	ad2ant2r	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑎 ≠ 𝑐 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
31		neeq1	⊢ ( 𝑥 = 𝑏 → ( 𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦 ) )
32		neeq2	⊢ ( 𝑦 = 𝑑 → ( 𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑 ) )
33	31 32	rspc2ev	⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 )
34	33	3expia	⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑏 ≠ 𝑑 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
35	34	ad2ant2l	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑏 ≠ 𝑑 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
36	30 35	jaod	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
37	25 36	syl5	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
38	37	rexlimdvva	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 ) )
39	38	rexlimivv	⊢ ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ ( 𝑎 + ( i · 𝑏 ) ) ≠ ( 𝑐 + ( i · 𝑑 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 )
40	1 17 39	mp2b	⊢ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3	⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) → 𝑥 = 𝑦 )
42	41	ex	⊢ ( 𝑥 = 0 → ( 𝑦 = 0 → 𝑥 = 𝑦 ) )
43	42	necon3d	⊢ ( 𝑥 = 0 → ( 𝑥 ≠ 𝑦 → 𝑦 ≠ 0 ) )
44		neeq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ≠ 0 ↔ 𝑦 ≠ 0 ) )
45	44	rspcev	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑦 ≠ 0 ) → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 )
46	45	expcom	⊢ ( 𝑦 ≠ 0 → ( 𝑦 ∈ ℝ → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) )
47	43 46	syl6	⊢ ( 𝑥 = 0 → ( 𝑥 ≠ 𝑦 → ( 𝑦 ∈ ℝ → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) ) )
48	47	com23	⊢ ( 𝑥 = 0 → ( 𝑦 ∈ ℝ → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) ) )
49	48	adantld	⊢ ( 𝑥 = 0 → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) ) )
50		neeq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ≠ 0 ↔ 𝑥 ≠ 0 ) )
51	50	rspcev	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 )
52	51	expcom	⊢ ( 𝑥 ≠ 0 → ( 𝑥 ∈ ℝ → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) )
53	52	adantrd	⊢ ( 𝑥 ≠ 0 → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) )
54	53	a1dd	⊢ ( 𝑥 ≠ 0 → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) ) )
55	49 54	pm2.61ine	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 ) )
56	55	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 )
57		ax-rrecex	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑧 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝑧 · 𝑥 ) = 1 )
58		remulcl	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑧 · 𝑥 ) ∈ ℝ )
59	58	adantlr	⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑧 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑧 · 𝑥 ) ∈ ℝ )
60		eleq1	⊢ ( ( 𝑧 · 𝑥 ) = 1 → ( ( 𝑧 · 𝑥 ) ∈ ℝ ↔ 1 ∈ ℝ ) )
61	59 60	syl5ibcom	⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑧 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑧 · 𝑥 ) = 1 → 1 ∈ ℝ ) )
62	61	rexlimdva	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑧 ≠ 0 ) → ( ∃ 𝑥 ∈ ℝ ( 𝑧 · 𝑥 ) = 1 → 1 ∈ ℝ ) )
63	57 62	mpd	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑧 ≠ 0 ) → 1 ∈ ℝ )
64	63	rexlimiva	⊢ ( ∃ 𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ )
65	40 56 64	mp2b	⊢ 1 ∈ ℝ