receu

Description: Existential uniqueness of reciprocals. Theorem I.8 of Apostol p. 18. (Contributed by NM, 29-Jan-1995) (Revised by Mario Carneiro, 17-Feb-2014)

		Ref	Expression
	Assertion	receu	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \exists! x \in ℂ B x = A$

Proof

Step	Hyp	Ref	Expression
1		recex	$⊢ (B \in ℂ \land B \neq 0) \to \exists y \in ℂ B y = 1$
2	1	3adant1	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \exists y \in ℂ B y = 1$
3		simprl	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land B y = 1)) \to y \in ℂ$
4		simpll	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land B y = 1)) \to A \in ℂ$
5	3 4	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land B y = 1)) \to y A \in ℂ$
6		oveq1	$⊢ B y = 1 \to B y A = 1 A$
7	6	ad2antll	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land B y = 1)) \to B y A = 1 A$
8		simplr	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land B y = 1)) \to B \in ℂ$
9	8 3 4	mulassd	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land B y = 1)) \to B y A = B y A$
10	4	mulid2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land B y = 1)) \to 1 A = A$
11	7 9 10	3eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land B y = 1)) \to B y A = A$
12		oveq2	$⊢ x = y A \to B x = B y A$
13	12	eqeq1d	$⊢ x = y A \to (B x = A \leftrightarrow B y A = A)$
14	13	rspcev	$⊢ (y A \in ℂ \land B y A = A) \to \exists x \in ℂ B x = A$
15	5 11 14	syl2anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (y \in ℂ \land B y = 1)) \to \exists x \in ℂ B x = A$
16	15	rexlimdvaa	$⊢ (A \in ℂ \land B \in ℂ) \to (\exists y \in ℂ B y = 1 \to \exists x \in ℂ B x = A)$
17	16	3adant3	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to (\exists y \in ℂ B y = 1 \to \exists x \in ℂ B x = A)$
18	2 17	mpd	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \exists x \in ℂ B x = A$
19		eqtr3	$⊢ (B x = A \land B y = A) \to B x = B y$
20		mulcan	$⊢ (x \in ℂ \land y \in ℂ \land (B \in ℂ \land B \neq 0)) \to (B x = B y \leftrightarrow x = y)$
21	19 20	syl5ib	$⊢ (x \in ℂ \land y \in ℂ \land (B \in ℂ \land B \neq 0)) \to ((B x = A \land B y = A) \to x = y)$
22	21	3expa	$⊢ ((x \in ℂ \land y \in ℂ) \land (B \in ℂ \land B \neq 0)) \to ((B x = A \land B y = A) \to x = y)$
23	22	expcom	$⊢ (B \in ℂ \land B \neq 0) \to ((x \in ℂ \land y \in ℂ) \to ((B x = A \land B y = A) \to x = y))$
24	23	3adant1	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to ((x \in ℂ \land y \in ℂ) \to ((B x = A \land B y = A) \to x = y))$
25	24	ralrimivv	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \forall x \in ℂ \forall y \in ℂ ((B x = A \land B y = A) \to x = y)$
26		oveq2	$⊢ x = y \to B x = B y$
27	26	eqeq1d	$⊢ x = y \to (B x = A \leftrightarrow B y = A)$
28	27	reu4	$⊢ \exists! x \in ℂ B x = A \leftrightarrow (\exists x \in ℂ B x = A \land \forall x \in ℂ \forall y \in ℂ ((B x = A \land B y = A) \to x = y))$
29	18 25 28	sylanbrc	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \exists! x \in ℂ B x = A$

Metamath Proof Explorer

Theorem receu

Proof