# 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 e. RR`

### Proof

Step Hyp Ref Expression
1 ax-1ne0
` |-  1 =/= 0`
2 ax-1cn
` |-  1 e. CC`
3 cnre
` |-  ( 1 e. CC -> E. a e. RR E. b e. RR 1 = ( a + ( _i x. b ) ) )`
4 2 3 ax-mp
` |-  E. a e. RR E. b e. RR 1 = ( a + ( _i x. b ) )`
5 neeq1
` |-  ( 1 = ( a + ( _i x. b ) ) -> ( 1 =/= 0 <-> ( a + ( _i x. b ) ) =/= 0 ) )`
6 5 biimpcd
` |-  ( 1 =/= 0 -> ( 1 = ( a + ( _i x. b ) ) -> ( a + ( _i x. b ) ) =/= 0 ) )`
7 0cn
` |-  0 e. CC`
8 cnre
` |-  ( 0 e. CC -> E. c e. RR E. d e. RR 0 = ( c + ( _i x. d ) ) )`
9 7 8 ax-mp
` |-  E. c e. RR E. d e. RR 0 = ( c + ( _i x. d ) )`
10 neeq2
` |-  ( 0 = ( c + ( _i x. d ) ) -> ( ( a + ( _i x. b ) ) =/= 0 <-> ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) ) )`
11 10 biimpcd
` |-  ( ( a + ( _i x. b ) ) =/= 0 -> ( 0 = ( c + ( _i x. d ) ) -> ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) ) )`
12 11 reximdv
` |-  ( ( a + ( _i x. b ) ) =/= 0 -> ( E. d e. RR 0 = ( c + ( _i x. d ) ) -> E. d e. RR ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) ) )`
13 12 reximdv
` |-  ( ( a + ( _i x. b ) ) =/= 0 -> ( E. c e. RR E. d e. RR 0 = ( c + ( _i x. d ) ) -> E. c e. RR E. d e. RR ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) ) )`
14 6 9 13 syl6mpi
` |-  ( 1 =/= 0 -> ( 1 = ( a + ( _i x. b ) ) -> E. c e. RR E. d e. RR ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) ) )`
15 14 reximdv
` |-  ( 1 =/= 0 -> ( E. b e. RR 1 = ( a + ( _i x. b ) ) -> E. b e. RR E. c e. RR E. d e. RR ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) ) )`
16 15 reximdv
` |-  ( 1 =/= 0 -> ( E. a e. RR E. b e. RR 1 = ( a + ( _i x. b ) ) -> E. a e. RR E. b e. RR E. c e. RR E. d e. RR ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) ) )`
17 4 16 mpi
` |-  ( 1 =/= 0 -> E. a e. RR E. b e. RR E. c e. RR E. d e. RR ( a + ( _i x. b ) ) =/= ( c + ( _i x. 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 x. b ) = ( _i x. d ) )`
27 25 26 oveqan12d
` |-  ( ( a = c /\ b = d ) -> ( a + ( _i x. b ) ) = ( c + ( _i x. d ) ) )`
28 24 27 sylbi
` |-  ( -. ( a =/= c \/ b =/= d ) -> ( a + ( _i x. b ) ) = ( c + ( _i x. d ) ) )`
29 28 necon1ai
` |-  ( ( a + ( _i x. b ) ) =/= ( c + ( _i x. 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 e. RR /\ c e. RR /\ a =/= c ) -> E. x e. RR E. y e. RR x =/= y )`
33 32 3expia
` |-  ( ( a e. RR /\ c e. RR ) -> ( a =/= c -> E. x e. RR E. y e. RR x =/= y ) )`
` |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( a =/= c -> E. x e. RR E. y e. RR x =/= y ) )`
35 neeq1
` |-  ( x = b -> ( x =/= y <-> b =/= y ) )`
36 neeq2
` |-  ( y = d -> ( b =/= y <-> b =/= d ) )`
37 35 36 rspc2ev
` |-  ( ( b e. RR /\ d e. RR /\ b =/= d ) -> E. x e. RR E. y e. RR x =/= y )`
38 37 3expia
` |-  ( ( b e. RR /\ d e. RR ) -> ( b =/= d -> E. x e. RR E. y e. RR x =/= y ) )`
` |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( b =/= d -> E. x e. RR E. y e. RR x =/= y ) )`
40 34 39 jaod
` |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( ( a =/= c \/ b =/= d ) -> E. x e. RR E. y e. RR x =/= y ) )`
41 29 40 syl5
` |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) -> E. x e. RR E. y e. RR x =/= y ) )`
42 41 rexlimdvva
` |-  ( ( a e. RR /\ b e. RR ) -> ( E. c e. RR E. d e. RR ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) -> E. x e. RR E. y e. RR x =/= y ) )`
43 42 rexlimivv
` |-  ( E. a e. RR E. b e. RR E. c e. RR E. d e. RR ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) -> E. x e. RR E. y e. RR x =/= y )`
44 1 17 43 mp2b
` |-  E. x e. RR E. y e. RR 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 e. RR /\ y =/= 0 ) -> E. z e. RR z =/= 0 )`
50 49 expcom
` |-  ( y =/= 0 -> ( y e. RR -> E. z e. RR z =/= 0 ) )`
51 47 50 syl6
` |-  ( x = 0 -> ( x =/= y -> ( y e. RR -> E. z e. RR z =/= 0 ) ) )`
52 51 com23
` |-  ( x = 0 -> ( y e. RR -> ( x =/= y -> E. z e. RR z =/= 0 ) ) )`
` |-  ( x = 0 -> ( ( x e. RR /\ y e. RR ) -> ( x =/= y -> E. z e. RR z =/= 0 ) ) )`
54 neeq1
` |-  ( z = x -> ( z =/= 0 <-> x =/= 0 ) )`
55 54 rspcev
` |-  ( ( x e. RR /\ x =/= 0 ) -> E. z e. RR z =/= 0 )`
56 55 expcom
` |-  ( x =/= 0 -> ( x e. RR -> E. z e. RR z =/= 0 ) )`
` |-  ( x =/= 0 -> ( ( x e. RR /\ y e. RR ) -> E. z e. RR z =/= 0 ) )`
58 57 a1dd
` |-  ( x =/= 0 -> ( ( x e. RR /\ y e. RR ) -> ( x =/= y -> E. z e. RR z =/= 0 ) ) )`
59 53 58 pm2.61ine
` |-  ( ( x e. RR /\ y e. RR ) -> ( x =/= y -> E. z e. RR z =/= 0 ) )`
60 59 rexlimivv
` |-  ( E. x e. RR E. y e. RR x =/= y -> E. z e. RR z =/= 0 )`
61 ax-rrecex
` |-  ( ( z e. RR /\ z =/= 0 ) -> E. x e. RR ( z x. x ) = 1 )`
62 remulcl
` |-  ( ( z e. RR /\ x e. RR ) -> ( z x. x ) e. RR )`
` |-  ( ( ( z e. RR /\ z =/= 0 ) /\ x e. RR ) -> ( z x. x ) e. RR )`
` |-  ( ( z x. x ) = 1 -> ( ( z x. x ) e. RR <-> 1 e. RR ) )`
` |-  ( ( ( z e. RR /\ z =/= 0 ) /\ x e. RR ) -> ( ( z x. x ) = 1 -> 1 e. RR ) )`
` |-  ( ( z e. RR /\ z =/= 0 ) -> ( E. x e. RR ( z x. x ) = 1 -> 1 e. RR ) )`
` |-  ( ( z e. RR /\ z =/= 0 ) -> 1 e. RR )`
` |-  ( E. z e. RR z =/= 0 -> 1 e. RR )`
` |-  1 e. RR`