Description: The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | recrng | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rebase | |
|
2 | refldcj | |
|
3 | refld | |
|
4 | isfld | |
|
5 | 3 4 | mpbi | |
6 | 5 | simpri | |
7 | 6 | a1i | |
8 | cjre | |
|
9 | 8 | adantl | |
10 | 1 2 7 9 | idsrngd | |
11 | 10 | mptru | |