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