Theorem xrecex

Description: Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016)

	Ref	Expression
Assertion	xrecex	|- ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A *e x ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		ax-rrecex	|- ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A x. x ) = 1 )
2		rexmul	|- ( ( A e. RR /\ x e. RR ) -> ( A *e x ) = ( A x. x ) )
3	2	eqeq1d	|- ( ( A e. RR /\ x e. RR ) -> ( ( A *e x ) = 1 <-> ( A x. x ) = 1 ) )
4	3	ex	|- ( A e. RR -> ( x e. RR -> ( ( A *e x ) = 1 <-> ( A x. x ) = 1 ) ) )
5	4	adantr	|- ( ( A e. RR /\ A =/= 0 ) -> ( x e. RR -> ( ( A *e x ) = 1 <-> ( A x. x ) = 1 ) ) )
6	5	pm5.32d	|- ( ( A e. RR /\ A =/= 0 ) -> ( ( x e. RR /\ ( A *e x ) = 1 ) <-> ( x e. RR /\ ( A x. x ) = 1 ) ) )
7	6	rexbidv2	|- ( ( A e. RR /\ A =/= 0 ) -> ( E. x e. RR ( A *e x ) = 1 <-> E. x e. RR ( A x. x ) = 1 ) )
8	1 7	mpbird	|- ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A *e x ) = 1 )