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 |