# Metamath Proof Explorer

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