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 ) )
34 33 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 ) )
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 ) )
39 38 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 ) )
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 ) ) )
53 52 adantld 
 |-  ( 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 ) )
57 56 adantrd 
 |-  ( 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 )
63 62 adantlr 
 |-  ( ( ( z e. RR /\ z =/= 0 ) /\ x e. RR ) -> ( z x. x ) e. RR )
64 eleq1 
 |-  ( ( z x. x ) = 1 -> ( ( z x. x ) e. RR <-> 1 e. RR ) )
65 63 64 syl5ibcom 
 |-  ( ( ( z e. RR /\ z =/= 0 ) /\ x e. RR ) -> ( ( z x. x ) = 1 -> 1 e. RR ) )
66 65 rexlimdva 
 |-  ( ( z e. RR /\ z =/= 0 ) -> ( E. x e. RR ( z x. x ) = 1 -> 1 e. RR ) )
67 61 66 mpd 
 |-  ( ( z e. RR /\ z =/= 0 ) -> 1 e. RR )
68 67 rexlimiva 
 |-  ( E. z e. RR z =/= 0 -> 1 e. RR )
69 44 60 68 mp2b 
 |-  1 e. RR