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 id 
 |-  ( a = c -> a = c )
19 oveq2 
 |-  ( b = d -> ( _i x. b ) = ( _i x. d ) )
20 18 19 oveqan12d 
 |-  ( ( a = c /\ b = d ) -> ( a + ( _i x. b ) ) = ( c + ( _i x. d ) ) )
21 20 expcom 
 |-  ( b = d -> ( a = c -> ( a + ( _i x. b ) ) = ( c + ( _i x. d ) ) ) )
22 21 necon3d 
 |-  ( b = d -> ( ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) -> a =/= c ) )
23 22 com12 
 |-  ( ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) -> ( b = d -> a =/= c ) )
24 23 necon3bd 
 |-  ( ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) -> ( -. a =/= c -> b =/= d ) )
25 24 orrd 
 |-  ( ( a + ( _i x. b ) ) =/= ( c + ( _i x. d ) ) -> ( a =/= c \/ b =/= d ) )
26 neeq1 
 |-  ( x = a -> ( x =/= y <-> a =/= y ) )
27 neeq2 
 |-  ( y = c -> ( a =/= y <-> a =/= c ) )
28 26 27 rspc2ev 
 |-  ( ( a e. RR /\ c e. RR /\ a =/= c ) -> E. x e. RR E. y e. RR x =/= y )
29 28 3expia 
 |-  ( ( a e. RR /\ c e. RR ) -> ( a =/= c -> E. x e. RR E. y e. RR x =/= y ) )
30 29 ad2ant2r 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( a =/= c -> E. x e. RR E. y e. RR x =/= y ) )
31 neeq1 
 |-  ( x = b -> ( x =/= y <-> b =/= y ) )
32 neeq2 
 |-  ( y = d -> ( b =/= y <-> b =/= d ) )
33 31 32 rspc2ev 
 |-  ( ( b e. RR /\ d e. RR /\ b =/= d ) -> E. x e. RR E. y e. RR x =/= y )
34 33 3expia 
 |-  ( ( b e. RR /\ d e. RR ) -> ( b =/= d -> E. x e. RR E. y e. RR x =/= y ) )
35 34 ad2ant2l 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( c e. RR /\ d e. RR ) ) -> ( b =/= d -> E. x e. RR E. y e. RR x =/= y ) )
36 30 35 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 ) )
37 25 36 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 ) )
38 37 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 ) )
39 38 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 )
40 1 17 39 mp2b 
 |-  E. x e. RR E. y e. RR x =/= y
41 eqtr3 
 |-  ( ( x = 0 /\ y = 0 ) -> x = y )
42 41 ex 
 |-  ( x = 0 -> ( y = 0 -> x = y ) )
43 42 necon3d 
 |-  ( x = 0 -> ( x =/= y -> y =/= 0 ) )
44 neeq1 
 |-  ( z = y -> ( z =/= 0 <-> y =/= 0 ) )
45 44 rspcev 
 |-  ( ( y e. RR /\ y =/= 0 ) -> E. z e. RR z =/= 0 )
46 45 expcom 
 |-  ( y =/= 0 -> ( y e. RR -> E. z e. RR z =/= 0 ) )
47 43 46 syl6 
 |-  ( x = 0 -> ( x =/= y -> ( y e. RR -> E. z e. RR z =/= 0 ) ) )
48 47 com23 
 |-  ( x = 0 -> ( y e. RR -> ( x =/= y -> E. z e. RR z =/= 0 ) ) )
49 48 adantld 
 |-  ( x = 0 -> ( ( x e. RR /\ y e. RR ) -> ( x =/= y -> E. z e. RR z =/= 0 ) ) )
50 neeq1 
 |-  ( z = x -> ( z =/= 0 <-> x =/= 0 ) )
51 50 rspcev 
 |-  ( ( x e. RR /\ x =/= 0 ) -> E. z e. RR z =/= 0 )
52 51 expcom 
 |-  ( x =/= 0 -> ( x e. RR -> E. z e. RR z =/= 0 ) )
53 52 adantrd 
 |-  ( x =/= 0 -> ( ( x e. RR /\ y e. RR ) -> E. z e. RR z =/= 0 ) )
54 53 a1dd 
 |-  ( x =/= 0 -> ( ( x e. RR /\ y e. RR ) -> ( x =/= y -> E. z e. RR z =/= 0 ) ) )
55 49 54 pm2.61ine 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x =/= y -> E. z e. RR z =/= 0 ) )
56 55 rexlimivv 
 |-  ( E. x e. RR E. y e. RR x =/= y -> E. z e. RR z =/= 0 )
57 ax-rrecex 
 |-  ( ( z e. RR /\ z =/= 0 ) -> E. x e. RR ( z x. x ) = 1 )
58 remulcl 
 |-  ( ( z e. RR /\ x e. RR ) -> ( z x. x ) e. RR )
59 58 adantlr 
 |-  ( ( ( z e. RR /\ z =/= 0 ) /\ x e. RR ) -> ( z x. x ) e. RR )
60 eleq1 
 |-  ( ( z x. x ) = 1 -> ( ( z x. x ) e. RR <-> 1 e. RR ) )
61 59 60 syl5ibcom 
 |-  ( ( ( z e. RR /\ z =/= 0 ) /\ x e. RR ) -> ( ( z x. x ) = 1 -> 1 e. RR ) )
62 61 rexlimdva 
 |-  ( ( z e. RR /\ z =/= 0 ) -> ( E. x e. RR ( z x. x ) = 1 -> 1 e. RR ) )
63 57 62 mpd 
 |-  ( ( z e. RR /\ z =/= 0 ) -> 1 e. RR )
64 63 rexlimiva 
 |-  ( E. z e. RR z =/= 0 -> 1 e. RR )
65 40 56 64 mp2b 
 |-  1 e. RR