sqreulem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > sqreulem		Structured version Visualization version GIF version

Theorem sqreulem 15314

Description: Lemma for sqreu 15315: write a general complex square root in terms of the square root function over nonnegative reals. (Contributed by Mario Carneiro, 9-Jul-2013.)

**Hypothesis**
Ref	Expression
sqrteulem.1	⊢ 𝐵 = ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))

**Assertion**
Ref	Expression
sqreulem	⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝐵) ∧ (i · 𝐵) ∉ ℝ⁺))

**Proof of Theorem sqreulem**
Step	Hyp	Ref	Expression
1		sqrteulem.1	. . . . 5 ⊢ 𝐵 = ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))
2	1	oveq1i 7367	. . . 4 ⊢ (𝐵↑2) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2)
3		abscl 15232	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
4		absge0 15241	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
5		resqrtcl 15207	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → (√‘(abs‘𝐴)) ∈ ℝ)
6	3, 4, 5	syl2anc 590	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℝ)
7	6	recnd 11165	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℂ)
8	7	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (√‘(abs‘𝐴)) ∈ ℂ)
9	3	recnd 11165	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℂ)
10		addcl 11112	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) + 𝐴) ∈ ℂ)
11	9, 10	mpancom 694	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + 𝐴) ∈ ℂ)
12	11	adantr 481	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) + 𝐴) ∈ ℂ)
13		abscl 15232	. . . . . . . . 9 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
14	11, 13	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
15	14	recnd 11165	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
16	15	adantr 481	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
17	11	abs00ad 15244	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴)) = 0 ↔ ((abs‘𝐴) + 𝐴) = 0))
18	17	necon3bid 2978	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴)) ≠ 0 ↔ ((abs‘𝐴) + 𝐴) ≠ 0))
19	18	biimpar 478	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ≠ 0)
20	12, 16, 19	divcld 11923	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℂ)
21	8, 20	sqmuld 14112	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)))
22	2, 21	eqtrid 2786	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵↑2) = (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)))
23	3	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘𝐴) ∈ ℝ)
24	4	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (abs‘𝐴))
25		resqrtth 15209	. . . . 5 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → ((√‘(abs‘𝐴))↑2) = (abs‘𝐴))
26	23, 24, 25	syl2anc 590	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴))↑2) = (abs‘𝐴))
27	12, 16, 19	sqdivd 14113	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2) = ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)))
28		absvalsq 15234	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
29		2cn 12248	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
30		mulass 11118	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
31	29, 30	mp3an1 1456	. . . . . . . . . . . . 13 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
32	9, 31	mpancom 694	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
33		mulcl 11114	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (2 · (abs‘𝐴)) ∈ ℂ)
34	29, 9, 33	sylancr 593	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (2 · (abs‘𝐴)) ∈ ℂ)
35		mulcom 11116	. . . . . . . . . . . . 13 ⊢ (((2 · (abs‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (𝐴 · (2 · (abs‘𝐴))))
36	34, 35	mpancom 694	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) · 𝐴) = (𝐴 · (2 · (abs‘𝐴))))
37	32, 36	eqtr3d 2776	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · 𝐴)) = (𝐴 · (2 · (abs‘𝐴))))
38	28, 37	oveq12d 7375	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
39		cjcl 15059	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘𝐴) ∈ ℂ)
40		adddi 11119	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ ∧ (2 · (abs‘𝐴)) ∈ ℂ) → (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
41	39, 34, 40	mpd3an23 1471	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
42	38, 41	eqtr4d 2777	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) = (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))))
43		sqval 14068	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴))
44	42, 43	oveq12d 7375	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)) = ((𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + (𝐴 · 𝐴)))
45		binom2 14171	. . . . . . . . 9 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((abs‘𝐴) + 𝐴)↑2) = ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)))
46	9, 45	mpancom 694	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴)↑2) = ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)))
47		id 22	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
48	39, 34	addcld 11156	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((∗‘𝐴) + (2 · (abs‘𝐴))) ∈ ℂ)
49	47, 48, 47	adddid 11161	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = ((𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + (𝐴 · 𝐴)))
50	44, 46, 49	3eqtr4d 2784	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴)↑2) = (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))
51	9, 34	mulcld 11157	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (2 · (abs‘𝐴))) ∈ ℂ)
52	9, 39	mulcld 11157	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (∗‘𝐴)) ∈ ℂ)
53	51, 52	addcomd 11340	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (2 · (abs‘𝐴))) + ((abs‘𝐴) · (∗‘𝐴))) = (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · (2 · (abs‘𝐴)))))
54	9, 9	mulcld 11157	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (abs‘𝐴)) ∈ ℂ)
55	54	2timesd 12412	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · (abs‘𝐴))) = (((abs‘𝐴) · (abs‘𝐴)) + ((abs‘𝐴) · (abs‘𝐴))))
56		mul12 11303	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (2 · ((abs‘𝐴) · (abs‘𝐴))) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
57	29, 9, 9, 56	mp3an2i 1474	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · (abs‘𝐴))) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
58	9	sqvald 14097	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = ((abs‘𝐴) · (abs‘𝐴)))
59		mulcom 11116	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ) → (𝐴 · (∗‘𝐴)) = ((∗‘𝐴) · 𝐴))
60	39, 59	mpdan 693	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = ((∗‘𝐴) · 𝐴))
61	28, 58, 60	3eqtr3d 2782	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (abs‘𝐴)) = ((∗‘𝐴) · 𝐴))
62	61	oveq2d 7373	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((abs‘𝐴) · (abs‘𝐴))) = (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)))
63	55, 57, 62	3eqtr3rd 2783	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
64	63	oveq1d 7372	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) = (((abs‘𝐴) · (2 · (abs‘𝐴))) + ((abs‘𝐴) · (∗‘𝐴))))
65	9, 39, 34	adddid 11161	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · (2 · (abs‘𝐴)))))
66	53, 64, 65	3eqtr4d 2784	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) = ((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))))
67	66	oveq1d 7372	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)) = (((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + ((abs‘𝐴) · 𝐴)))
68		cjadd 15095	. . . . . . . . . . . . 13 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (∗‘((abs‘𝐴) + 𝐴)) = ((∗‘(abs‘𝐴)) + (∗‘𝐴)))
69	9, 68	mpancom 694	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (∗‘((abs‘𝐴) + 𝐴)) = ((∗‘(abs‘𝐴)) + (∗‘𝐴)))
70	3	cjred 15180	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (∗‘(abs‘𝐴)) = (abs‘𝐴))
71	70	oveq1d 7372	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((∗‘(abs‘𝐴)) + (∗‘𝐴)) = ((abs‘𝐴) + (∗‘𝐴)))
72	69, 71	eqtrd 2774	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘((abs‘𝐴) + 𝐴)) = ((abs‘𝐴) + (∗‘𝐴)))
73	72	oveq2d 7373	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))) = (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) + (∗‘𝐴))))
74	9, 47, 9, 39	muladdd 11600	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) + (∗‘𝐴))) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
75	73, 74	eqtrd 2774	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
76		absvalsq 15234	. . . . . . . . . 10 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))))
77	11, 76	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))))
78		mulcl 11114	. . . . . . . . . . . 12 ⊢ (((∗‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((∗‘𝐴) · 𝐴) ∈ ℂ)
79	39, 78	mpancom 694	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((∗‘𝐴) · 𝐴) ∈ ℂ)
80	54, 79	addcld 11156	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) ∈ ℂ)
81		mulcl 11114	. . . . . . . . . . 11 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) · 𝐴) ∈ ℂ)
82	9, 81	mpancom 694	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · 𝐴) ∈ ℂ)
83	80, 52, 82	addassd 11159	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
84	75, 77, 83	3eqtr4d 2784	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)))
85	9, 48, 47	adddid 11161	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = (((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + ((abs‘𝐴) · 𝐴)))
86	67, 84, 85	3eqtr4d 2784	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))
87	50, 86	oveq12d 7375	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
88	87	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
89	27, 88	eqtrd 2774	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
90	26, 89	oveq12d 7375	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)) = ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))))
91		addcl 11112	. . . . . . . 8 ⊢ ((((∗‘𝐴) + (2 · (abs‘𝐴))) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ)
92	48, 91	mpancom 694	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ)
93	9, 47, 92	mul12d 11347	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = (𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
94	93	oveq1d 7372	. . . . 5 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
95	94	adantr 481	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
96	9	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘𝐴) ∈ ℂ)
97		mulcl 11114	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ) → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
98	92, 97	mpdan 693	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
99	98	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
100	9, 92	mulcld 11157	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
101	100	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
102		sqeq0 14074	. . . . . . . . 9 ⊢ ((abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ → (((abs‘((abs‘𝐴) + 𝐴))↑2) = 0 ↔ (abs‘((abs‘𝐴) + 𝐴)) = 0))
103	15, 102	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘((abs‘𝐴) + 𝐴))↑2) = 0 ↔ (abs‘((abs‘𝐴) + 𝐴)) = 0))
104	86	eqeq1d 2741	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘((abs‘𝐴) + 𝐴))↑2) = 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = 0))
105	103, 104, 17	3bitr3rd 311	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) = 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = 0))
106	105	necon3bid 2978	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) ≠ 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ≠ 0))
107	106	biimpa 477	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ≠ 0)
108	96, 99, 101, 107	divassd 11958	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))))
109		simpl 483	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 𝐴 ∈ ℂ)
110	109, 101, 107	divcan4d 11929	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = 𝐴)
111	95, 108, 110	3eqtr3d 2782	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))) = 𝐴)
112	22, 90, 111	3eqtrd 2778	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵↑2) = 𝐴)
113	6	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (√‘(abs‘𝐴)) ∈ ℝ)
114	11	addcjd 15166	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) = (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
115		2re 12247	. . . . . . . . 9 ⊢ 2 ∈ ℝ
116	11	recld 15148	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
117		remulcl 11115	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ) → (2 · (ℜ‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
118	115, 116, 117	sylancr 593	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (2 · (ℜ‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
119	114, 118	eqeltrd 2839	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
120	119	adantr 481	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
121	14	adantr 481	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
122	120, 121, 19	redivcld 11975	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
123	113, 122	remulcld 11167	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ)
124		sqrtge0 15211	. . . . . . 7 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → 0 ≤ (√‘(abs‘𝐴)))
125	3, 4, 124	syl2anc 590	. . . . . 6 ⊢ (𝐴 ∈ ℂ → 0 ≤ (√‘(abs‘𝐴)))
126	125	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (√‘(abs‘𝐴)))
127		negcl 11385	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
128		releabs 15276	. . . . . . . . . . . 12 ⊢ (-𝐴 ∈ ℂ → (ℜ‘-𝐴) ≤ (abs‘-𝐴))
129	127, 128	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ≤ (abs‘-𝐴))
130		abscl 15232	. . . . . . . . . . . . 13 ⊢ (-𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℝ)
131	127, 130	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℝ)
132	127	recld 15148	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ∈ ℝ)
133	131, 132	subge0d 11732	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (0 ≤ ((abs‘-𝐴) − (ℜ‘-𝐴)) ↔ (ℜ‘-𝐴) ≤ (abs‘-𝐴)))
134	129, 133	mpbird 258	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → 0 ≤ ((abs‘-𝐴) − (ℜ‘-𝐴)))
135		readd 15080	. . . . . . . . . . . 12 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (ℜ‘((abs‘𝐴) + 𝐴)) = ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)))
136	9, 135	mpancom 694	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) = ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)))
137	3	rered 15178	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘(abs‘𝐴)) = (abs‘𝐴))
138		absneg 15231	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴))
139	137, 138	eqtr4d 2777	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘(abs‘𝐴)) = (abs‘-𝐴))
140		negneg 11436	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴)
141	140	fveq2d 6832	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘--𝐴) = (ℜ‘𝐴))
142	127	renegd 15163	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘--𝐴) = -(ℜ‘-𝐴))
143	141, 142	eqtr3d 2776	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = -(ℜ‘-𝐴))
144	139, 143	oveq12d 7375	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)) = ((abs‘-𝐴) + -(ℜ‘-𝐴)))
145	131	recnd 11165	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℂ)
146	132	recnd 11165	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ∈ ℂ)
147	145, 146	negsubd 11503	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘-𝐴) + -(ℜ‘-𝐴)) = ((abs‘-𝐴) − (ℜ‘-𝐴)))
148	136, 144, 147	3eqtrd 2778	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) = ((abs‘-𝐴) − (ℜ‘-𝐴)))
149	134, 148	breqtrrd 5101	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴)))
150		0le2 12275	. . . . . . . . . 10 ⊢ 0 ≤ 2
151		mulge0 11660	. . . . . . . . . 10 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ ((ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴)))) → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
152	115, 150, 151	mpanl12 708	. . . . . . . . 9 ⊢ (((ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴))) → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
153	116, 149, 152	syl2anc 590	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
154	153, 114	breqtrrd 5101	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))))
155	154	adantr 481	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))))
156		absge0 15241	. . . . . . . 8 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → 0 ≤ (abs‘((abs‘𝐴) + 𝐴)))
157	12, 156	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (abs‘((abs‘𝐴) + 𝐴)))
158	121, 157, 19	ne0gt0d 11275	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 < (abs‘((abs‘𝐴) + 𝐴)))
159		divge0 12017	. . . . . 6 ⊢ ((((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) ∈ ℝ ∧ 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴)))) ∧ ((abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 < (abs‘((abs‘𝐴) + 𝐴)))) → 0 ≤ ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))
160	120, 155, 121, 158, 159	syl22anc 844	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))
161	113, 122, 126, 160	mulge0d 11719	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))))
162		2pos 12276	. . . . 5 ⊢ 0 < 2
163		divge0 12017	. . . . 5 ⊢ (((((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ ∧ 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
164	115, 162, 163	mpanr12 711	. . . 4 ⊢ ((((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ ∧ 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))) → 0 ≤ (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
165	123, 161, 164	syl2anc 590	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
166	8, 20	mulcld 11157	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℂ)
167	1, 166	eqeltrid 2843	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 𝐵 ∈ ℂ)
168		reval 15060	. . . . 5 ⊢ (𝐵 ∈ ℂ → (ℜ‘𝐵) = ((𝐵 + (∗‘𝐵)) / 2))
169	167, 168	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (ℜ‘𝐵) = ((𝐵 + (∗‘𝐵)) / 2))
170	1	oveq1i 7367	. . . . . . 7 ⊢ (𝐵 + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
171	1	fveq2i 6831	. . . . . . . . . 10 ⊢ (∗‘𝐵) = (∗‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))))
172	8, 20	cjmuld 15175	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) = ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))))
173	171, 172	eqtrid 2786	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘𝐵) = ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))))
174	6	cjred 15180	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘(√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
175	174	adantr 481	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
176	12, 16, 19	cjdivd 15177	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (∗‘(abs‘((abs‘𝐴) + 𝐴)))))
177	121	cjred 15180	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(abs‘((abs‘𝐴) + 𝐴))) = (abs‘((abs‘𝐴) + 𝐴)))
178	177	oveq2d 7373	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘((abs‘𝐴) + 𝐴)) / (∗‘(abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))
179	176, 178	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))
180	175, 179	oveq12d 7375	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) = ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
181	173, 180	eqtrd 2774	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘𝐵) = ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
182	181	oveq2d 7373	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = (𝐵 + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
183	12	cjcld 15150	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
184	183, 16, 19	divcld 11923	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℂ)
185	8, 20, 184	adddid 11161	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
186	170, 182, 185	3eqtr4a 2800	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
187	12, 183, 16, 19	divdird 11961	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))) = ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
188	187	oveq2d 7373	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
189	186, 188	eqtr4d 2777	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))))
190	189	oveq1d 7372	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵 + (∗‘𝐵)) / 2) = (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
191	169, 190	eqtrd 2774	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (ℜ‘𝐵) = (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
192	165, 191	breqtrrd 5101	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (ℜ‘𝐵))
193		subneg 11435	. . . . . . . . . 10 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) − -𝐴) = ((abs‘𝐴) + 𝐴))
194	9, 193	mpancom 694	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -𝐴) = ((abs‘𝐴) + 𝐴))
195	194	eqeq1d 2741	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − -𝐴) = 0 ↔ ((abs‘𝐴) + 𝐴) = 0))
196	9, 127	subeq0ad 11507	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − -𝐴) = 0 ↔ (abs‘𝐴) = -𝐴))
197	195, 196	bitr3d 282	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) = 0 ↔ (abs‘𝐴) = -𝐴))
198	197	necon3bid 2978	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) ≠ 0 ↔ (abs‘𝐴) ≠ -𝐴))
199	198	biimpa 477	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘𝐴) ≠ -𝐴)
200		resqcl 14078	. . . . . . . . . 10 ⊢ ((i · 𝐵) ∈ ℝ → ((i · 𝐵)↑2) ∈ ℝ)
201		ax-icn 11089	. . . . . . . . . . . . 13 ⊢ i ∈ ℂ
202		sqmul 14073	. . . . . . . . . . . . 13 ⊢ ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i · 𝐵)↑2) = ((i↑2) · (𝐵↑2)))
203	201, 167, 202	sylancr 593	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵)↑2) = ((i↑2) · (𝐵↑2)))
204		i2 14156	. . . . . . . . . . . . . 14 ⊢ (i↑2) = -1
205	204	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (i↑2) = -1)
206	205, 112	oveq12d 7375	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i↑2) · (𝐵↑2)) = (-1 · 𝐴))
207		mulm1 11583	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴)
208	207	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (-1 · 𝐴) = -𝐴)
209	203, 206, 208	3eqtrd 2778	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵)↑2) = -𝐴)
210	209	eleq1d 2824	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((i · 𝐵)↑2) ∈ ℝ ↔ -𝐴 ∈ ℝ))
211	200, 210	imbitrid 245	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → -𝐴 ∈ ℝ))
212		renegcl 11449	. . . . . . . . . 10 ⊢ (-𝐴 ∈ ℝ → --𝐴 ∈ ℝ)
213	140	eleq1d 2824	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (--𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ))
214	212, 213	imbitrid 245	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ → 𝐴 ∈ ℝ))
215	109, 211, 214	sylsyld 61	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 𝐴 ∈ ℝ))
216		sqge0 14090	. . . . . . . . . 10 ⊢ ((i · 𝐵) ∈ ℝ → 0 ≤ ((i · 𝐵)↑2))
217	209	breq2d 5085	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (0 ≤ ((i · 𝐵)↑2) ↔ 0 ≤ -𝐴))
218	216, 217	imbitrid 245	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 0 ≤ -𝐴))
219		le0neg1 11650	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴))
220	219	biimprcd 251	. . . . . . . . 9 ⊢ (0 ≤ -𝐴 → (𝐴 ∈ ℝ → 𝐴 ≤ 0))
221	218, 215, 220	syl6c 70	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 𝐴 ≤ 0))
222	215, 221	jcad 517	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐴 ≤ 0)))
223		absnid 15252	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴)
224	222, 223	syl6 35	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → (abs‘𝐴) = -𝐴))
225	224	necon3ad 2947	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) ≠ -𝐴 → ¬ (i · 𝐵) ∈ ℝ))
226	199, 225	mpd 15	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ¬ (i · 𝐵) ∈ ℝ)
227		rpre 12943	. . . 4 ⊢ ((i · 𝐵) ∈ ℝ⁺ → (i · 𝐵) ∈ ℝ)
228	226, 227	nsyl 140	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ¬ (i · 𝐵) ∈ ℝ⁺)
229		df-nel 3039	. . 3 ⊢ ((i · 𝐵) ∉ ℝ⁺ ↔ ¬ (i · 𝐵) ∈ ℝ⁺)
230	228, 229	sylibr 235	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (i · 𝐵) ∉ ℝ⁺)
231	112, 192, 230	3jca 1134	1 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝐵) ∧ (i · 𝐵) ∉ ℝ⁺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∉ wnel 3038 class class class wbr 5073 ‘cfv 6486 (class class class)co 7357 ℂcc 11028 ℝcr 11029 0cc0 11030 1c1 11031 ici 11032 + caddc 11033 · cmul 11035 < clt 11171 ≤ cle 11172 − cmin 11369 -cneg 11370 / cdiv 11799 2c2 12228 ℝ⁺crp 12934 ↑cexp 14015 ∗ccj 15050 ℜcre 15051 √csqrt 15187 abscabs 15188

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5219 ax-nul 5229 ax-pow 5295 ax-pr 5363 ax-un 7679 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-pre-sup 11108

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4263 df-if 4456 df-pw 4532 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4840 df-iun 4924 df-br 5074 df-opab 5136 df-mpt 5155 df-tr 5181 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7314 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7808 df-2nd 7933 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-er 8634 df-en 8885 df-dom 8886 df-sdom 8887 df-sup 9346 df-pnf 11173 df-mnf 11174 df-xr 11175 df-ltxr 11176 df-le 11177 df-sub 11371 df-neg 11372 df-div 11800 df-nn 12167 df-2 12236 df-3 12237 df-n0 12430 df-z 12517 df-uz 12781 df-rp 12935 df-seq 13956 df-exp 14016 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190

This theorem is referenced by: sqreu 15315 cphsqrtcl2 25172 constrsqrtcl 33972

W3C validator