This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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