| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: 1 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, ax1cn 5281, by exploiting properties of the imaginary
unit |
| Ref | Expression |
|---|---|
| 1re |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axicn 5282 |
. . . 4
| |
| 2 | axcnre 5298 |
. . . 4
| |
| 3 | 1, 2 | ax-mp 7 |
. . 3
|
| 4 | neeq1 1593 |
. . . . . . . . 9
| |
| 5 | 4 | rcla4ev 1880 |
. . . . . . . 8
|
| 6 | 5 | adantlr 395 |
. . . . . . 7
|
| 7 | neeq1 1593 |
. . . . . . . . 9
| |
| 8 | 7 | rcla4ev 1880 |
. . . . . . . 8
|
| 9 | 8 | adantll 394 |
. . . . . . 7
|
| 10 | 6, 9 | jaodan 428 |
. . . . . 6
|
| 11 | 10 | ex 373 |
. . . . 5
|
| 12 | ine0 5446 |
. . . . . . 7
| |
| 13 | neeq1 1593 |
. . . . . . 7
| |
| 14 | 12, 13 | mpbii 193 |
. . . . . 6
|
| 15 | ioran 306 |
. . . . . . . . 9
| |
| 16 | nne 1592 |
. . . . . . . . . 10
| |
| 17 | nne 1592 |
. . . . . . . . . 10
| |
| 18 | 16, 17 | anbi12i 484 |
. . . . . . . . 9
|
| 19 | 15, 18 | bitr 173 |
. . . . . . . 8
|
| 20 | opreq12 3976 |
. . . . . . . . . 10
| |
| 21 | opreq2 3975 |
. . . . . . . . . . 11
| |
| 22 | 1 | mul01 5443 |
. . . . . . . . . . 11
|
| 23 | 21, 22 | syl6eq 1526 |
. . . . . . . . . 10
|
| 24 | 20, 23 | sylan2 453 |
. . . . . . . . 9
|
| 25 | 0cn 5340 |
. . . . . . . . . 10
| |
| 26 | 25 | addid1 5342 |
. . . . . . . . 9
|
| 27 | 24, 26 | syl6eq 1526 |
. . . . . . . 8
|
| 28 | 19, 27 | sylbi 199 |
. . . . . . 7
|
| 29 | 28 | necon1ai 1611 |
. . . . . 6
|
| 30 | 14, 29 | syl 10 |
. . . . 5
|
| 31 | 11, 30 | syl5 21 |
. . . 4
|
| 32 | 31 | r19.23aivv 1751 |
. . 3
|
| 33 | 3, 32 | ax-mp 7 |
. 2
|
| 34 | axrrecex 5296 |
. . . 4
| |
| 35 | eleq1 1537 |
. . . . . . 7
| |
| 36 | axmulrcl 5286 |
. . . . . . 7
| |
| 37 | 35, 36 | syl5cbi 209 |
. . . . . 6
|
| 38 | 37 | r19.23adva 1750 |
. . . . 5
|
| 39 | 38 | adantr 391 |
. . . 4
|
| 40 | 34, 39 | mpd 26 |
. . 3
|
| 41 | 40 | r19.23aiva 1747 |
. 2
|
| 42 | 33, 41 | ax-mp 7 |
1
|