Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  1re Unicode version

Theorem 1re 9046
 Description: is a real number. 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 9004, by exploiting properties of the imaginary unit . (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
1re

Proof of Theorem 1re
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-1ne0 9015 . . 3
2 ax-1cn 9004 . . . . 5
3 cnre 9043 . . . . 5
42, 3ax-mp 8 . . . 4
5 neeq1 2575 . . . . . . . 8
65biimpcd 216 . . . . . . 7
7 0cn 9040 . . . . . . . 8
8 cnre 9043 . . . . . . . 8
97, 8ax-mp 8 . . . . . . 7
10 neeq2 2576 . . . . . . . . . 10
1110biimpcd 216 . . . . . . . . 9
1211reximdv 2777 . . . . . . . 8
1312reximdv 2777 . . . . . . 7
146, 9, 13syl6mpi 60 . . . . . 6
1514reximdv 2777 . . . . 5
1615reximdv 2777 . . . 4
174, 16mpi 17 . . 3
18 ioran 477 . . . . . . . . 9
19 df-ne 2569 . . . . . . . . . . 11
2019con2bii 323 . . . . . . . . . 10
21 df-ne 2569 . . . . . . . . . . 11
2221con2bii 323 . . . . . . . . . 10
2320, 22anbi12i 679 . . . . . . . . 9
2418, 23bitr4i 244 . . . . . . . 8
25 id 20 . . . . . . . . 9
26 oveq2 6048 . . . . . . . . 9
2725, 26oveqan12d 6059 . . . . . . . 8
2824, 27sylbi 188 . . . . . . 7
2928necon1ai 2609 . . . . . 6
30 neeq1 2575 . . . . . . . . . 10
31 neeq2 2576 . . . . . . . . . 10
3230, 31rspc2ev 3020 . . . . . . . . 9
33323expia 1155 . . . . . . . 8
3433ad2ant2r 728 . . . . . . 7
35 neeq1 2575 . . . . . . . . . 10
36 neeq2 2576 . . . . . . . . . 10
3735, 36rspc2ev 3020 . . . . . . . . 9
38373expia 1155 . . . . . . . 8
3938ad2ant2l 727 . . . . . . 7
4034, 39jaod 370 . . . . . 6
4129, 40syl5 30 . . . . 5
4241rexlimdvva 2797 . . . 4
4342rexlimivv 2795 . . 3
441, 17, 43mp2b 10 . 2
45 eqtr3 2423 . . . . . . . . 9
4645ex 424 . . . . . . . 8
4746necon3d 2605 . . . . . . 7
48 neeq1 2575 . . . . . . . . 9
4948rspcev 3012 . . . . . . . 8
5049expcom 425 . . . . . . 7
5147, 50syl6 31 . . . . . 6
5251com23 74 . . . . 5
5352adantld 454 . . . 4
54 neeq1 2575 . . . . . . . 8
5554rspcev 3012 . . . . . . 7
5655expcom 425 . . . . . 6
5756adantrd 455 . . . . 5
5857a1dd 44 . . . 4
5953, 58pm2.61ine 2643 . . 3
6059rexlimivv 2795 . 2
61 ax-rrecex 9018 . . . 4
62 remulcl 9031 . . . . . . 7
6362adantlr 696 . . . . . 6
64 eleq1 2464 . . . . . 6
6563, 64syl5ibcom 212 . . . . 5
6665rexlimdva 2790 . . . 4
6761, 66mpd 15 . . 3
6867rexlimiva 2785 . 2
6944, 60, 68mp2b 10 1