# 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 ∈ ℂ → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 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 ∈ ℝ