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 15285

Description: Lemma for sqreu 15286: 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 7368	. . . 4 ⊢ (𝐵↑2) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2)
3		abscl 15203	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
4		absge0 15212	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
5		resqrtcl 15178	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → (√‘(abs‘𝐴)) ∈ ℝ)
6	3, 4, 5	syl2anc 584	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℝ)
7	6	recnd 11162	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℂ)
8	7	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (√‘(abs‘𝐴)) ∈ ℂ)
9	3	recnd 11162	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℂ)
10		addcl 11110	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) + 𝐴) ∈ ℂ)
11	9, 10	mpancom 688	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + 𝐴) ∈ ℂ)
12	11	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) + 𝐴) ∈ ℂ)
13		abscl 15203	. . . . . . . . 9 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
14	11, 13	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
15	14	recnd 11162	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
16	15	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
17	11	abs00ad 15215	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴)) = 0 ↔ ((abs‘𝐴) + 𝐴) = 0))
18	17	necon3bid 2976	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴)) ≠ 0 ↔ ((abs‘𝐴) + 𝐴) ≠ 0))
19	18	biimpar 477	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ≠ 0)
20	12, 16, 19	divcld 11919	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℂ)
21	8, 20	sqmuld 14083	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)))
22	2, 21	eqtrid 2783	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵↑2) = (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)))
23	3	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘𝐴) ∈ ℝ)
24	4	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (abs‘𝐴))
25		resqrtth 15180	. . . . 5 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → ((√‘(abs‘𝐴))↑2) = (abs‘𝐴))
26	23, 24, 25	syl2anc 584	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴))↑2) = (abs‘𝐴))
27	12, 16, 19	sqdivd 14084	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2) = ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)))
28		absvalsq 15205	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
29		2cn 12222	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
30		mulass 11116	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
31	29, 30	mp3an1 1450	. . . . . . . . . . . . 13 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
32	9, 31	mpancom 688	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
33		mulcl 11112	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (2 · (abs‘𝐴)) ∈ ℂ)
34	29, 9, 33	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (2 · (abs‘𝐴)) ∈ ℂ)
35		mulcom 11114	. . . . . . . . . . . . 13 ⊢ (((2 · (abs‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (𝐴 · (2 · (abs‘𝐴))))
36	34, 35	mpancom 688	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) · 𝐴) = (𝐴 · (2 · (abs‘𝐴))))
37	32, 36	eqtr3d 2773	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · 𝐴)) = (𝐴 · (2 · (abs‘𝐴))))
38	28, 37	oveq12d 7376	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
39		cjcl 15030	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘𝐴) ∈ ℂ)
40		adddi 11117	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ ∧ (2 · (abs‘𝐴)) ∈ ℂ) → (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
41	39, 34, 40	mpd3an23 1465	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
42	38, 41	eqtr4d 2774	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) = (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))))
43		sqval 14039	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴))
44	42, 43	oveq12d 7376	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)) = ((𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + (𝐴 · 𝐴)))
45		binom2 14142	. . . . . . . . 9 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((abs‘𝐴) + 𝐴)↑2) = ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)))
46	9, 45	mpancom 688	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴)↑2) = ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)))
47		id 22	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
48	39, 34	addcld 11153	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((∗‘𝐴) + (2 · (abs‘𝐴))) ∈ ℂ)
49	47, 48, 47	adddid 11158	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = ((𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + (𝐴 · 𝐴)))
50	44, 46, 49	3eqtr4d 2781	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴)↑2) = (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))
51	9, 34	mulcld 11154	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (2 · (abs‘𝐴))) ∈ ℂ)
52	9, 39	mulcld 11154	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (∗‘𝐴)) ∈ ℂ)
53	51, 52	addcomd 11337	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (2 · (abs‘𝐴))) + ((abs‘𝐴) · (∗‘𝐴))) = (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · (2 · (abs‘𝐴)))))
54	9, 9	mulcld 11154	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (abs‘𝐴)) ∈ ℂ)
55	54	2timesd 12386	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · (abs‘𝐴))) = (((abs‘𝐴) · (abs‘𝐴)) + ((abs‘𝐴) · (abs‘𝐴))))
56		mul12 11300	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (2 · ((abs‘𝐴) · (abs‘𝐴))) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
57	29, 9, 9, 56	mp3an2i 1468	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · (abs‘𝐴))) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
58	9	sqvald 14068	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = ((abs‘𝐴) · (abs‘𝐴)))
59		mulcom 11114	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ) → (𝐴 · (∗‘𝐴)) = ((∗‘𝐴) · 𝐴))
60	39, 59	mpdan 687	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = ((∗‘𝐴) · 𝐴))
61	28, 58, 60	3eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (abs‘𝐴)) = ((∗‘𝐴) · 𝐴))
62	61	oveq2d 7374	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((abs‘𝐴) · (abs‘𝐴))) = (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)))
63	55, 57, 62	3eqtr3rd 2780	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
64	63	oveq1d 7373	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) = (((abs‘𝐴) · (2 · (abs‘𝐴))) + ((abs‘𝐴) · (∗‘𝐴))))
65	9, 39, 34	adddid 11158	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · (2 · (abs‘𝐴)))))
66	53, 64, 65	3eqtr4d 2781	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) = ((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))))
67	66	oveq1d 7373	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)) = (((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + ((abs‘𝐴) · 𝐴)))
68		cjadd 15066	. . . . . . . . . . . . 13 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (∗‘((abs‘𝐴) + 𝐴)) = ((∗‘(abs‘𝐴)) + (∗‘𝐴)))
69	9, 68	mpancom 688	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (∗‘((abs‘𝐴) + 𝐴)) = ((∗‘(abs‘𝐴)) + (∗‘𝐴)))
70	3	cjred 15151	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (∗‘(abs‘𝐴)) = (abs‘𝐴))
71	70	oveq1d 7373	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((∗‘(abs‘𝐴)) + (∗‘𝐴)) = ((abs‘𝐴) + (∗‘𝐴)))
72	69, 71	eqtrd 2771	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘((abs‘𝐴) + 𝐴)) = ((abs‘𝐴) + (∗‘𝐴)))
73	72	oveq2d 7374	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))) = (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) + (∗‘𝐴))))
74	9, 47, 9, 39	muladdd 11597	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) + (∗‘𝐴))) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
75	73, 74	eqtrd 2771	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
76		absvalsq 15205	. . . . . . . . . 10 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))))
77	11, 76	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))))
78		mulcl 11112	. . . . . . . . . . . 12 ⊢ (((∗‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((∗‘𝐴) · 𝐴) ∈ ℂ)
79	39, 78	mpancom 688	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((∗‘𝐴) · 𝐴) ∈ ℂ)
80	54, 79	addcld 11153	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) ∈ ℂ)
81		mulcl 11112	. . . . . . . . . . 11 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) · 𝐴) ∈ ℂ)
82	9, 81	mpancom 688	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · 𝐴) ∈ ℂ)
83	80, 52, 82	addassd 11156	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
84	75, 77, 83	3eqtr4d 2781	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)))
85	9, 48, 47	adddid 11158	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = (((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + ((abs‘𝐴) · 𝐴)))
86	67, 84, 85	3eqtr4d 2781	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))
87	50, 86	oveq12d 7376	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
88	87	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
89	27, 88	eqtrd 2771	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
90	26, 89	oveq12d 7376	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)) = ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))))
91		addcl 11110	. . . . . . . 8 ⊢ ((((∗‘𝐴) + (2 · (abs‘𝐴))) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ)
92	48, 91	mpancom 688	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ)
93	9, 47, 92	mul12d 11344	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = (𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
94	93	oveq1d 7373	. . . . 5 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
95	94	adantr 480	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
96	9	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘𝐴) ∈ ℂ)
97		mulcl 11112	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ) → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
98	92, 97	mpdan 687	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
99	98	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
100	9, 92	mulcld 11154	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
101	100	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
102		sqeq0 14045	. . . . . . . . 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 2738	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘((abs‘𝐴) + 𝐴))↑2) = 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = 0))
105	103, 104, 17	3bitr3rd 310	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) = 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = 0))
106	105	necon3bid 2976	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) ≠ 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ≠ 0))
107	106	biimpa 476	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ≠ 0)
108	96, 99, 101, 107	divassd 11954	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))))
109		simpl 482	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 𝐴 ∈ ℂ)
110	109, 101, 107	divcan4d 11925	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = 𝐴)
111	95, 108, 110	3eqtr3d 2779	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))) = 𝐴)
112	22, 90, 111	3eqtrd 2775	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵↑2) = 𝐴)
113	6	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (√‘(abs‘𝐴)) ∈ ℝ)
114	11	addcjd 15137	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) = (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
115		2re 12221	. . . . . . . . 9 ⊢ 2 ∈ ℝ
116	11	recld 15119	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
117		remulcl 11113	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ) → (2 · (ℜ‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
118	115, 116, 117	sylancr 587	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (2 · (ℜ‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
119	114, 118	eqeltrd 2836	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
120	119	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
121	14	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
122	120, 121, 19	redivcld 11971	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
123	113, 122	remulcld 11164	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ)
124		sqrtge0 15182	. . . . . . 7 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → 0 ≤ (√‘(abs‘𝐴)))
125	3, 4, 124	syl2anc 584	. . . . . 6 ⊢ (𝐴 ∈ ℂ → 0 ≤ (√‘(abs‘𝐴)))
126	125	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (√‘(abs‘𝐴)))
127		negcl 11382	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
128		releabs 15247	. . . . . . . . . . . 12 ⊢ (-𝐴 ∈ ℂ → (ℜ‘-𝐴) ≤ (abs‘-𝐴))
129	127, 128	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ≤ (abs‘-𝐴))
130		abscl 15203	. . . . . . . . . . . . 13 ⊢ (-𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℝ)
131	127, 130	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℝ)
132	127	recld 15119	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ∈ ℝ)
133	131, 132	subge0d 11729	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (0 ≤ ((abs‘-𝐴) − (ℜ‘-𝐴)) ↔ (ℜ‘-𝐴) ≤ (abs‘-𝐴)))
134	129, 133	mpbird 257	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → 0 ≤ ((abs‘-𝐴) − (ℜ‘-𝐴)))
135		readd 15051	. . . . . . . . . . . 12 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (ℜ‘((abs‘𝐴) + 𝐴)) = ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)))
136	9, 135	mpancom 688	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) = ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)))
137	3	rered 15149	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘(abs‘𝐴)) = (abs‘𝐴))
138		absneg 15202	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴))
139	137, 138	eqtr4d 2774	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘(abs‘𝐴)) = (abs‘-𝐴))
140		negneg 11433	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴)
141	140	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘--𝐴) = (ℜ‘𝐴))
142	127	renegd 15134	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘--𝐴) = -(ℜ‘-𝐴))
143	141, 142	eqtr3d 2773	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = -(ℜ‘-𝐴))
144	139, 143	oveq12d 7376	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)) = ((abs‘-𝐴) + -(ℜ‘-𝐴)))
145	131	recnd 11162	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℂ)
146	132	recnd 11162	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ∈ ℂ)
147	145, 146	negsubd 11500	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘-𝐴) + -(ℜ‘-𝐴)) = ((abs‘-𝐴) − (ℜ‘-𝐴)))
148	136, 144, 147	3eqtrd 2775	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) = ((abs‘-𝐴) − (ℜ‘-𝐴)))
149	134, 148	breqtrrd 5126	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴)))
150		0le2 12249	. . . . . . . . . 10 ⊢ 0 ≤ 2
151		mulge0 11657	. . . . . . . . . 10 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ ((ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴)))) → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
152	115, 150, 151	mpanl12 702	. . . . . . . . 9 ⊢ (((ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴))) → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
153	116, 149, 152	syl2anc 584	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
154	153, 114	breqtrrd 5126	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))))
155	154	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))))
156		absge0 15212	. . . . . . . 8 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → 0 ≤ (abs‘((abs‘𝐴) + 𝐴)))
157	12, 156	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (abs‘((abs‘𝐴) + 𝐴)))
158	121, 157, 19	ne0gt0d 11272	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 < (abs‘((abs‘𝐴) + 𝐴)))
159		divge0 12013	. . . . . 6 ⊢ ((((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) ∈ ℝ ∧ 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴)))) ∧ ((abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 < (abs‘((abs‘𝐴) + 𝐴)))) → 0 ≤ ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))
160	120, 155, 121, 158, 159	syl22anc 838	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))
161	113, 122, 126, 160	mulge0d 11716	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))))
162		2pos 12250	. . . . 5 ⊢ 0 < 2
163		divge0 12013	. . . . 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 705	. . . 4 ⊢ ((((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ ∧ 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))) → 0 ≤ (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
165	123, 161, 164	syl2anc 584	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
166	8, 20	mulcld 11154	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℂ)
167	1, 166	eqeltrid 2840	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 𝐵 ∈ ℂ)
168		reval 15031	. . . . 5 ⊢ (𝐵 ∈ ℂ → (ℜ‘𝐵) = ((𝐵 + (∗‘𝐵)) / 2))
169	167, 168	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (ℜ‘𝐵) = ((𝐵 + (∗‘𝐵)) / 2))
170	1	oveq1i 7368	. . . . . . 7 ⊢ (𝐵 + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
171	1	fveq2i 6837	. . . . . . . . . 10 ⊢ (∗‘𝐵) = (∗‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))))
172	8, 20	cjmuld 15146	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) = ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))))
173	171, 172	eqtrid 2783	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘𝐵) = ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))))
174	6	cjred 15151	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘(√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
175	174	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
176	12, 16, 19	cjdivd 15148	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (∗‘(abs‘((abs‘𝐴) + 𝐴)))))
177	121	cjred 15151	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(abs‘((abs‘𝐴) + 𝐴))) = (abs‘((abs‘𝐴) + 𝐴)))
178	177	oveq2d 7374	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘((abs‘𝐴) + 𝐴)) / (∗‘(abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))
179	176, 178	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))
180	175, 179	oveq12d 7376	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) = ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
181	173, 180	eqtrd 2771	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘𝐵) = ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
182	181	oveq2d 7374	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = (𝐵 + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
183	12	cjcld 15121	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
184	183, 16, 19	divcld 11919	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℂ)
185	8, 20, 184	adddid 11158	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
186	170, 182, 185	3eqtr4a 2797	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
187	12, 183, 16, 19	divdird 11957	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))) = ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
188	187	oveq2d 7374	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
189	186, 188	eqtr4d 2774	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))))
190	189	oveq1d 7373	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵 + (∗‘𝐵)) / 2) = (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
191	169, 190	eqtrd 2771	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (ℜ‘𝐵) = (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
192	165, 191	breqtrrd 5126	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (ℜ‘𝐵))
193		subneg 11432	. . . . . . . . . 10 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) − -𝐴) = ((abs‘𝐴) + 𝐴))
194	9, 193	mpancom 688	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -𝐴) = ((abs‘𝐴) + 𝐴))
195	194	eqeq1d 2738	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − -𝐴) = 0 ↔ ((abs‘𝐴) + 𝐴) = 0))
196	9, 127	subeq0ad 11504	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − -𝐴) = 0 ↔ (abs‘𝐴) = -𝐴))
197	195, 196	bitr3d 281	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) = 0 ↔ (abs‘𝐴) = -𝐴))
198	197	necon3bid 2976	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) ≠ 0 ↔ (abs‘𝐴) ≠ -𝐴))
199	198	biimpa 476	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘𝐴) ≠ -𝐴)
200		resqcl 14049	. . . . . . . . . 10 ⊢ ((i · 𝐵) ∈ ℝ → ((i · 𝐵)↑2) ∈ ℝ)
201		ax-icn 11087	. . . . . . . . . . . . 13 ⊢ i ∈ ℂ
202		sqmul 14044	. . . . . . . . . . . . 13 ⊢ ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i · 𝐵)↑2) = ((i↑2) · (𝐵↑2)))
203	201, 167, 202	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵)↑2) = ((i↑2) · (𝐵↑2)))
204		i2 14127	. . . . . . . . . . . . . 14 ⊢ (i↑2) = -1
205	204	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (i↑2) = -1)
206	205, 112	oveq12d 7376	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i↑2) · (𝐵↑2)) = (-1 · 𝐴))
207		mulm1 11580	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴)
208	207	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (-1 · 𝐴) = -𝐴)
209	203, 206, 208	3eqtrd 2775	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵)↑2) = -𝐴)
210	209	eleq1d 2821	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((i · 𝐵)↑2) ∈ ℝ ↔ -𝐴 ∈ ℝ))
211	200, 210	imbitrid 244	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → -𝐴 ∈ ℝ))
212		renegcl 11446	. . . . . . . . . 10 ⊢ (-𝐴 ∈ ℝ → --𝐴 ∈ ℝ)
213	140	eleq1d 2821	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (--𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ))
214	212, 213	imbitrid 244	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ → 𝐴 ∈ ℝ))
215	109, 211, 214	sylsyld 61	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 𝐴 ∈ ℝ))
216		sqge0 14061	. . . . . . . . . 10 ⊢ ((i · 𝐵) ∈ ℝ → 0 ≤ ((i · 𝐵)↑2))
217	209	breq2d 5110	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (0 ≤ ((i · 𝐵)↑2) ↔ 0 ≤ -𝐴))
218	216, 217	imbitrid 244	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 0 ≤ -𝐴))
219		le0neg1 11647	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴))
220	219	biimprcd 250	. . . . . . . . 9 ⊢ (0 ≤ -𝐴 → (𝐴 ∈ ℝ → 𝐴 ≤ 0))
221	218, 215, 220	syl6c 70	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 𝐴 ≤ 0))
222	215, 221	jcad 512	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐴 ≤ 0)))
223		absnid 15223	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴)
224	222, 223	syl6 35	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → (abs‘𝐴) = -𝐴))
225	224	necon3ad 2945	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) ≠ -𝐴 → ¬ (i · 𝐵) ∈ ℝ))
226	199, 225	mpd 15	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ¬ (i · 𝐵) ∈ ℝ)
227		rpre 12916	. . . 4 ⊢ ((i · 𝐵) ∈ ℝ⁺ → (i · 𝐵) ∈ ℝ)
228	226, 227	nsyl 140	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ¬ (i · 𝐵) ∈ ℝ⁺)
229		df-nel 3037	. . 3 ⊢ ((i · 𝐵) ∉ ℝ⁺ ↔ ¬ (i · 𝐵) ∈ ℝ⁺)
230	228, 229	sylibr 234	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (i · 𝐵) ∉ ℝ⁺)
231	112, 192, 230	3jca 1128	1 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝐵) ∧ (i · 𝐵) ∉ ℝ⁺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 ∉ wnel 3036 class class class wbr 5098 ‘cfv 6492 (class class class)co 7358 ℂcc 11026 ℝcr 11027 0cc0 11028 1c1 11029 ici 11030 + caddc 11031 · cmul 11033 < clt 11168 ≤ cle 11169 − cmin 11366 -cneg 11367 / cdiv 11796 2c2 12202 ℝ⁺crp 12907 ↑cexp 13986 ∗ccj 15021 ℜcre 15022 √csqrt 15158 abscabs 15159

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-er 8635 df-en 8886 df-dom 8887 df-sdom 8888 df-sup 9347 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-n0 12404 df-z 12491 df-uz 12754 df-rp 12908 df-seq 13927 df-exp 13987 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161

This theorem is referenced by: sqreu 15286 cphsqrtcl2 25144 constrsqrtcl 33938

W3C validator