Description: Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by Theorem axrrecex . (Contributed by Eric Schmidt, 11-Apr-2007)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-rrecex | |- ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A x. x ) = 1 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | cr | |- RR |
|
| 2 | 0 1 | wcel | |- A e. RR |
| 3 | cc0 | |- 0 |
|
| 4 | 0 3 | wne | |- A =/= 0 |
| 5 | 2 4 | wa | |- ( A e. RR /\ A =/= 0 ) |
| 6 | vx | |- x |
|
| 7 | cmul | |- x. |
|
| 8 | 6 | cv | |- x |
| 9 | 0 8 7 | co | |- ( A x. x ) |
| 10 | c1 | |- 1 |
|
| 11 | 9 10 | wceq | |- ( A x. x ) = 1 |
| 12 | 11 6 1 | wrex | |- E. x e. RR ( A x. x ) = 1 |
| 13 | 5 12 | wi | |- ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A x. x ) = 1 ) |