sqrmo

Description: Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013) (Revised by NM, 17-Jun-2017)

		Ref	Expression
	Assertion	sqrmo	$⊢ A \in ℂ \to \exists^{*} x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$

Proof

Step	Hyp	Ref	Expression
1		simplr1	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to x^{2} = A$
2		simprr1	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to y^{2} = A$
3	1 2	eqtr4d	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to x^{2} = y^{2}$
4		sqeqor	$⊢ (x \in ℂ \land y \in ℂ) \to (x^{2} = y^{2} \leftrightarrow (x = y \lor x = - y))$
5	4	ad2ant2r	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to (x^{2} = y^{2} \leftrightarrow (x = y \lor x = - y))$
6	3 5	mpbid	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to (x = y \lor x = - y)$
7	6	ord	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to (\neg x = y \to x = - y)$
8		3simpc	$⊢ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \to (0 \leq ℜ (x) \land i x \notin ℝ^{+})$
9		fveq2	$⊢ x = - y \to ℜ (x) = ℜ (- y)$
10	9	breq2d	$⊢ x = - y \to (0 \leq ℜ (x) \leftrightarrow 0 \leq ℜ (- y))$
11		oveq2	$⊢ x = - y \to i x = i (- y)$
12		neleq1	$⊢ i x = i (- y) \to (i x \notin ℝ^{+} \leftrightarrow i (- y) \notin ℝ^{+})$
13	11 12	syl	$⊢ x = - y \to (i x \notin ℝ^{+} \leftrightarrow i (- y) \notin ℝ^{+})$
14	10 13	anbi12d	$⊢ x = - y \to ((0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow (0 \leq ℜ (- y) \land i (- y) \notin ℝ^{+}))$
15	8 14	syl5ibcom	$⊢ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \to (x = - y \to (0 \leq ℜ (- y) \land i (- y) \notin ℝ^{+}))$
16	15	ad2antlr	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to (x = - y \to (0 \leq ℜ (- y) \land i (- y) \notin ℝ^{+}))$
17	7 16	syld	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to (\neg x = y \to (0 \leq ℜ (- y) \land i (- y) \notin ℝ^{+}))$
18		negeq	$⊢ y = 0 \to - y = - 0$
19		neg0	$⊢ - 0 = 0$
20	18 19	eqtrdi	$⊢ y = 0 \to - y = 0$
21	20	eqeq2d	$⊢ y = 0 \to (x = - y \leftrightarrow x = 0)$
22		eqeq2	$⊢ y = 0 \to (x = y \leftrightarrow x = 0)$
23	21 22	bitr4d	$⊢ y = 0 \to (x = - y \leftrightarrow x = y)$
24	23	biimpcd	$⊢ x = - y \to (y = 0 \to x = y)$
25	24	necon3bd	$⊢ x = - y \to (\neg x = y \to y \neq 0)$
26	7 25	syli	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to (\neg x = y \to y \neq 0)$
27		3simpc	$⊢ (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}) \to (0 \leq ℜ (y) \land i y \notin ℝ^{+})$
28		cnpart	$⊢ (y \in ℂ \land y \neq 0) \to ((0 \leq ℜ (y) \land i y \notin ℝ^{+}) \leftrightarrow \neg (0 \leq ℜ (- y) \land i (- y) \notin ℝ^{+}))$
29	27 28	syl5ib	$⊢ (y \in ℂ \land y \neq 0) \to ((y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}) \to \neg (0 \leq ℜ (- y) \land i (- y) \notin ℝ^{+}))$
30	29	impancom	$⊢ (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+})) \to (y \neq 0 \to \neg (0 \leq ℜ (- y) \land i (- y) \notin ℝ^{+}))$
31	30	adantl	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to (y \neq 0 \to \neg (0 \leq ℜ (- y) \land i (- y) \notin ℝ^{+}))$
32	26 31	syld	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to (\neg x = y \to \neg (0 \leq ℜ (- y) \land i (- y) \notin ℝ^{+}))$
33	17 32	pm2.65d	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to \neg \neg x = y$
34	33	notnotrd	$⊢ ((x \in ℂ \land (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \land (y \in ℂ \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to x = y$
35	34	an4s	$⊢ ((x \in ℂ \land y \in ℂ) \land ((x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))) \to x = y$
36	35	ex	$⊢ (x \in ℂ \land y \in ℂ) \to (((x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+})) \to x = y)$
37	36	a1i	$⊢ A \in ℂ \to ((x \in ℂ \land y \in ℂ) \to (((x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+})) \to x = y))$
38	37	ralrimivv	$⊢ A \in ℂ \to \forall x \in ℂ \forall y \in ℂ (((x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+})) \to x = y)$
39		oveq1	$⊢ x = y \to x^{2} = y^{2}$
40	39	eqeq1d	$⊢ x = y \to (x^{2} = A \leftrightarrow y^{2} = A)$
41		fveq2	$⊢ x = y \to ℜ (x) = ℜ (y)$
42	41	breq2d	$⊢ x = y \to (0 \leq ℜ (x) \leftrightarrow 0 \leq ℜ (y))$
43		oveq2	$⊢ x = y \to i x = i y$
44		neleq1	$⊢ i x = i y \to (i x \notin ℝ^{+} \leftrightarrow i y \notin ℝ^{+})$
45	43 44	syl	$⊢ x = y \to (i x \notin ℝ^{+} \leftrightarrow i y \notin ℝ^{+})$
46	40 42 45	3anbi123d	$⊢ x = y \to ((x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))$
47	46	rmo4	$⊢ \exists^{*} x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow \forall x \in ℂ \forall y \in ℂ (((x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \land (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+})) \to x = y)$
48	38 47	sylibr	$⊢ A \in ℂ \to \exists^{*} x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$

Metamath Proof Explorer

Theorem sqrmo

Proof