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 15316

Description: Lemma for sqreu 15317: 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 7371	. . . 4 ⊢ (𝐵↑2) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2)
3		abscl 15234	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
4		absge0 15243	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
5		resqrtcl 15209	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → (√‘(abs‘𝐴)) ∈ ℝ)
6	3, 4, 5	syl2anc 585	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℝ)
7	6	recnd 11167	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℂ)
8	7	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (√‘(abs‘𝐴)) ∈ ℂ)
9	3	recnd 11167	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℂ)
10		addcl 11114	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) + 𝐴) ∈ ℂ)
11	9, 10	mpancom 689	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + 𝐴) ∈ ℂ)
12	11	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) + 𝐴) ∈ ℂ)
13		abscl 15234	. . . . . . . . 9 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
14	11, 13	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
15	14	recnd 11167	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
16	15	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
17	11	abs00ad 15246	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴)) = 0 ↔ ((abs‘𝐴) + 𝐴) = 0))
18	17	necon3bid 2977	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴)) ≠ 0 ↔ ((abs‘𝐴) + 𝐴) ≠ 0))
19	18	biimpar 477	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ≠ 0)
20	12, 16, 19	divcld 11925	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℂ)
21	8, 20	sqmuld 14114	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)))
22	2, 21	eqtrid 2784	. . 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 15211	. . . . 5 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → ((√‘(abs‘𝐴))↑2) = (abs‘𝐴))
26	23, 24, 25	syl2anc 585	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴))↑2) = (abs‘𝐴))
27	12, 16, 19	sqdivd 14115	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2) = ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)))
28		absvalsq 15236	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
29		2cn 12250	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
30		mulass 11120	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
31	29, 30	mp3an1 1451	. . . . . . . . . . . . 13 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
32	9, 31	mpancom 689	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
33		mulcl 11116	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (2 · (abs‘𝐴)) ∈ ℂ)
34	29, 9, 33	sylancr 588	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (2 · (abs‘𝐴)) ∈ ℂ)
35		mulcom 11118	. . . . . . . . . . . . 13 ⊢ (((2 · (abs‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (𝐴 · (2 · (abs‘𝐴))))
36	34, 35	mpancom 689	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) · 𝐴) = (𝐴 · (2 · (abs‘𝐴))))
37	32, 36	eqtr3d 2774	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · 𝐴)) = (𝐴 · (2 · (abs‘𝐴))))
38	28, 37	oveq12d 7379	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
39		cjcl 15061	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘𝐴) ∈ ℂ)
40		adddi 11121	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ ∧ (2 · (abs‘𝐴)) ∈ ℂ) → (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
41	39, 34, 40	mpd3an23 1466	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
42	38, 41	eqtr4d 2775	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) = (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))))
43		sqval 14070	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴))
44	42, 43	oveq12d 7379	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)) = ((𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + (𝐴 · 𝐴)))
45		binom2 14173	. . . . . . . . 9 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((abs‘𝐴) + 𝐴)↑2) = ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)))
46	9, 45	mpancom 689	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴)↑2) = ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)))
47		id 22	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
48	39, 34	addcld 11158	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((∗‘𝐴) + (2 · (abs‘𝐴))) ∈ ℂ)
49	47, 48, 47	adddid 11163	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = ((𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + (𝐴 · 𝐴)))
50	44, 46, 49	3eqtr4d 2782	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴)↑2) = (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))
51	9, 34	mulcld 11159	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (2 · (abs‘𝐴))) ∈ ℂ)
52	9, 39	mulcld 11159	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (∗‘𝐴)) ∈ ℂ)
53	51, 52	addcomd 11342	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (2 · (abs‘𝐴))) + ((abs‘𝐴) · (∗‘𝐴))) = (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · (2 · (abs‘𝐴)))))
54	9, 9	mulcld 11159	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (abs‘𝐴)) ∈ ℂ)
55	54	2timesd 12414	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · (abs‘𝐴))) = (((abs‘𝐴) · (abs‘𝐴)) + ((abs‘𝐴) · (abs‘𝐴))))
56		mul12 11305	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (2 · ((abs‘𝐴) · (abs‘𝐴))) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
57	29, 9, 9, 56	mp3an2i 1469	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · (abs‘𝐴))) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
58	9	sqvald 14099	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = ((abs‘𝐴) · (abs‘𝐴)))
59		mulcom 11118	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ) → (𝐴 · (∗‘𝐴)) = ((∗‘𝐴) · 𝐴))
60	39, 59	mpdan 688	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = ((∗‘𝐴) · 𝐴))
61	28, 58, 60	3eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (abs‘𝐴)) = ((∗‘𝐴) · 𝐴))
62	61	oveq2d 7377	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((abs‘𝐴) · (abs‘𝐴))) = (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)))
63	55, 57, 62	3eqtr3rd 2781	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
64	63	oveq1d 7376	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) = (((abs‘𝐴) · (2 · (abs‘𝐴))) + ((abs‘𝐴) · (∗‘𝐴))))
65	9, 39, 34	adddid 11163	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · (2 · (abs‘𝐴)))))
66	53, 64, 65	3eqtr4d 2782	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) = ((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))))
67	66	oveq1d 7376	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)) = (((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + ((abs‘𝐴) · 𝐴)))
68		cjadd 15097	. . . . . . . . . . . . 13 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (∗‘((abs‘𝐴) + 𝐴)) = ((∗‘(abs‘𝐴)) + (∗‘𝐴)))
69	9, 68	mpancom 689	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (∗‘((abs‘𝐴) + 𝐴)) = ((∗‘(abs‘𝐴)) + (∗‘𝐴)))
70	3	cjred 15182	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (∗‘(abs‘𝐴)) = (abs‘𝐴))
71	70	oveq1d 7376	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((∗‘(abs‘𝐴)) + (∗‘𝐴)) = ((abs‘𝐴) + (∗‘𝐴)))
72	69, 71	eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘((abs‘𝐴) + 𝐴)) = ((abs‘𝐴) + (∗‘𝐴)))
73	72	oveq2d 7377	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))) = (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) + (∗‘𝐴))))
74	9, 47, 9, 39	muladdd 11602	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) + (∗‘𝐴))) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
75	73, 74	eqtrd 2772	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
76		absvalsq 15236	. . . . . . . . . 10 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))))
77	11, 76	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))))
78		mulcl 11116	. . . . . . . . . . . 12 ⊢ (((∗‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((∗‘𝐴) · 𝐴) ∈ ℂ)
79	39, 78	mpancom 689	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((∗‘𝐴) · 𝐴) ∈ ℂ)
80	54, 79	addcld 11158	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) ∈ ℂ)
81		mulcl 11116	. . . . . . . . . . 11 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) · 𝐴) ∈ ℂ)
82	9, 81	mpancom 689	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · 𝐴) ∈ ℂ)
83	80, 52, 82	addassd 11161	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
84	75, 77, 83	3eqtr4d 2782	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)))
85	9, 48, 47	adddid 11163	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = (((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + ((abs‘𝐴) · 𝐴)))
86	67, 84, 85	3eqtr4d 2782	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))
87	50, 86	oveq12d 7379	. . . . . 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 2772	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
90	26, 89	oveq12d 7379	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)) = ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))))
91		addcl 11114	. . . . . . . 8 ⊢ ((((∗‘𝐴) + (2 · (abs‘𝐴))) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ)
92	48, 91	mpancom 689	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ)
93	9, 47, 92	mul12d 11349	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = (𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
94	93	oveq1d 7376	. . . . 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 11116	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ) → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
98	92, 97	mpdan 688	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
99	98	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
100	9, 92	mulcld 11159	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
101	100	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
102		sqeq0 14076	. . . . . . . . 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 2739	. . . . . . . 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 2977	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) ≠ 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ≠ 0))
107	106	biimpa 476	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ≠ 0)
108	96, 99, 101, 107	divassd 11960	. . . 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 11931	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = 𝐴)
111	95, 108, 110	3eqtr3d 2780	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))) = 𝐴)
112	22, 90, 111	3eqtrd 2776	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵↑2) = 𝐴)
113	6	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (√‘(abs‘𝐴)) ∈ ℝ)
114	11	addcjd 15168	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) = (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
115		2re 12249	. . . . . . . . 9 ⊢ 2 ∈ ℝ
116	11	recld 15150	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
117		remulcl 11117	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ) → (2 · (ℜ‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
118	115, 116, 117	sylancr 588	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (2 · (ℜ‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
119	114, 118	eqeltrd 2837	. . . . . . 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 11977	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
123	113, 122	remulcld 11169	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ)
124		sqrtge0 15213	. . . . . . 7 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → 0 ≤ (√‘(abs‘𝐴)))
125	3, 4, 124	syl2anc 585	. . . . . 6 ⊢ (𝐴 ∈ ℂ → 0 ≤ (√‘(abs‘𝐴)))
126	125	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (√‘(abs‘𝐴)))
127		negcl 11387	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
128		releabs 15278	. . . . . . . . . . . 12 ⊢ (-𝐴 ∈ ℂ → (ℜ‘-𝐴) ≤ (abs‘-𝐴))
129	127, 128	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ≤ (abs‘-𝐴))
130		abscl 15234	. . . . . . . . . . . . 13 ⊢ (-𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℝ)
131	127, 130	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℝ)
132	127	recld 15150	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ∈ ℝ)
133	131, 132	subge0d 11734	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (0 ≤ ((abs‘-𝐴) − (ℜ‘-𝐴)) ↔ (ℜ‘-𝐴) ≤ (abs‘-𝐴)))
134	129, 133	mpbird 257	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → 0 ≤ ((abs‘-𝐴) − (ℜ‘-𝐴)))
135		readd 15082	. . . . . . . . . . . 12 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (ℜ‘((abs‘𝐴) + 𝐴)) = ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)))
136	9, 135	mpancom 689	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) = ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)))
137	3	rered 15180	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘(abs‘𝐴)) = (abs‘𝐴))
138		absneg 15233	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴))
139	137, 138	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘(abs‘𝐴)) = (abs‘-𝐴))
140		negneg 11438	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴)
141	140	fveq2d 6839	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘--𝐴) = (ℜ‘𝐴))
142	127	renegd 15165	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘--𝐴) = -(ℜ‘-𝐴))
143	141, 142	eqtr3d 2774	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = -(ℜ‘-𝐴))
144	139, 143	oveq12d 7379	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)) = ((abs‘-𝐴) + -(ℜ‘-𝐴)))
145	131	recnd 11167	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℂ)
146	132	recnd 11167	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ∈ ℂ)
147	145, 146	negsubd 11505	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘-𝐴) + -(ℜ‘-𝐴)) = ((abs‘-𝐴) − (ℜ‘-𝐴)))
148	136, 144, 147	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) = ((abs‘-𝐴) − (ℜ‘-𝐴)))
149	134, 148	breqtrrd 5114	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴)))
150		0le2 12277	. . . . . . . . . 10 ⊢ 0 ≤ 2
151		mulge0 11662	. . . . . . . . . 10 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ ((ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴)))) → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
152	115, 150, 151	mpanl12 703	. . . . . . . . 9 ⊢ (((ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴))) → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
153	116, 149, 152	syl2anc 585	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
154	153, 114	breqtrrd 5114	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))))
155	154	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))))
156		absge0 15243	. . . . . . . 8 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → 0 ≤ (abs‘((abs‘𝐴) + 𝐴)))
157	12, 156	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (abs‘((abs‘𝐴) + 𝐴)))
158	121, 157, 19	ne0gt0d 11277	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 < (abs‘((abs‘𝐴) + 𝐴)))
159		divge0 12019	. . . . . 6 ⊢ ((((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) ∈ ℝ ∧ 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴)))) ∧ ((abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 < (abs‘((abs‘𝐴) + 𝐴)))) → 0 ≤ ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))
160	120, 155, 121, 158, 159	syl22anc 839	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))
161	113, 122, 126, 160	mulge0d 11721	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))))
162		2pos 12278	. . . . 5 ⊢ 0 < 2
163		divge0 12019	. . . . 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 706	. . . 4 ⊢ ((((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ ∧ 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))) → 0 ≤ (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
165	123, 161, 164	syl2anc 585	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
166	8, 20	mulcld 11159	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℂ)
167	1, 166	eqeltrid 2841	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 𝐵 ∈ ℂ)
168		reval 15062	. . . . 5 ⊢ (𝐵 ∈ ℂ → (ℜ‘𝐵) = ((𝐵 + (∗‘𝐵)) / 2))
169	167, 168	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (ℜ‘𝐵) = ((𝐵 + (∗‘𝐵)) / 2))
170	1	oveq1i 7371	. . . . . . 7 ⊢ (𝐵 + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
171	1	fveq2i 6838	. . . . . . . . . 10 ⊢ (∗‘𝐵) = (∗‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))))
172	8, 20	cjmuld 15177	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) = ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))))
173	171, 172	eqtrid 2784	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘𝐵) = ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))))
174	6	cjred 15182	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘(√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
175	174	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
176	12, 16, 19	cjdivd 15179	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (∗‘(abs‘((abs‘𝐴) + 𝐴)))))
177	121	cjred 15182	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(abs‘((abs‘𝐴) + 𝐴))) = (abs‘((abs‘𝐴) + 𝐴)))
178	177	oveq2d 7377	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘((abs‘𝐴) + 𝐴)) / (∗‘(abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))
179	176, 178	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))
180	175, 179	oveq12d 7379	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) = ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
181	173, 180	eqtrd 2772	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘𝐵) = ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
182	181	oveq2d 7377	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = (𝐵 + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
183	12	cjcld 15152	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
184	183, 16, 19	divcld 11925	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℂ)
185	8, 20, 184	adddid 11163	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
186	170, 182, 185	3eqtr4a 2798	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
187	12, 183, 16, 19	divdird 11963	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))) = ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
188	187	oveq2d 7377	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
189	186, 188	eqtr4d 2775	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))))
190	189	oveq1d 7376	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵 + (∗‘𝐵)) / 2) = (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
191	169, 190	eqtrd 2772	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (ℜ‘𝐵) = (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
192	165, 191	breqtrrd 5114	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (ℜ‘𝐵))
193		subneg 11437	. . . . . . . . . 10 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) − -𝐴) = ((abs‘𝐴) + 𝐴))
194	9, 193	mpancom 689	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -𝐴) = ((abs‘𝐴) + 𝐴))
195	194	eqeq1d 2739	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − -𝐴) = 0 ↔ ((abs‘𝐴) + 𝐴) = 0))
196	9, 127	subeq0ad 11509	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − -𝐴) = 0 ↔ (abs‘𝐴) = -𝐴))
197	195, 196	bitr3d 281	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) = 0 ↔ (abs‘𝐴) = -𝐴))
198	197	necon3bid 2977	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) ≠ 0 ↔ (abs‘𝐴) ≠ -𝐴))
199	198	biimpa 476	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘𝐴) ≠ -𝐴)
200		resqcl 14080	. . . . . . . . . 10 ⊢ ((i · 𝐵) ∈ ℝ → ((i · 𝐵)↑2) ∈ ℝ)
201		ax-icn 11091	. . . . . . . . . . . . 13 ⊢ i ∈ ℂ
202		sqmul 14075	. . . . . . . . . . . . 13 ⊢ ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i · 𝐵)↑2) = ((i↑2) · (𝐵↑2)))
203	201, 167, 202	sylancr 588	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵)↑2) = ((i↑2) · (𝐵↑2)))
204		i2 14158	. . . . . . . . . . . . . 14 ⊢ (i↑2) = -1
205	204	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (i↑2) = -1)
206	205, 112	oveq12d 7379	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i↑2) · (𝐵↑2)) = (-1 · 𝐴))
207		mulm1 11585	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴)
208	207	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (-1 · 𝐴) = -𝐴)
209	203, 206, 208	3eqtrd 2776	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵)↑2) = -𝐴)
210	209	eleq1d 2822	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((i · 𝐵)↑2) ∈ ℝ ↔ -𝐴 ∈ ℝ))
211	200, 210	imbitrid 244	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → -𝐴 ∈ ℝ))
212		renegcl 11451	. . . . . . . . . 10 ⊢ (-𝐴 ∈ ℝ → --𝐴 ∈ ℝ)
213	140	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (--𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ))
214	212, 213	imbitrid 244	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ → 𝐴 ∈ ℝ))
215	109, 211, 214	sylsyld 61	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 𝐴 ∈ ℝ))
216		sqge0 14092	. . . . . . . . . 10 ⊢ ((i · 𝐵) ∈ ℝ → 0 ≤ ((i · 𝐵)↑2))
217	209	breq2d 5098	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (0 ≤ ((i · 𝐵)↑2) ↔ 0 ≤ -𝐴))
218	216, 217	imbitrid 244	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 0 ≤ -𝐴))
219		le0neg1 11652	. . . . . . . . . 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 15254	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴)
224	222, 223	syl6 35	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → (abs‘𝐴) = -𝐴))
225	224	necon3ad 2946	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) ≠ -𝐴 → ¬ (i · 𝐵) ∈ ℝ))
226	199, 225	mpd 15	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ¬ (i · 𝐵) ∈ ℝ)
227		rpre 12945	. . . 4 ⊢ ((i · 𝐵) ∈ ℝ⁺ → (i · 𝐵) ∈ ℝ)
228	226, 227	nsyl 140	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ¬ (i · 𝐵) ∈ ℝ⁺)
229		df-nel 3038	. . 3 ⊢ ((i · 𝐵) ∉ ℝ⁺ ↔ ¬ (i · 𝐵) ∈ ℝ⁺)
230	228, 229	sylibr 234	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (i · 𝐵) ∉ ℝ⁺)
231	112, 192, 230	3jca 1129	1 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝐵) ∧ (i · 𝐵) ∉ ℝ⁺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∉ wnel 3037 class class class wbr 5086 ‘cfv 6493 (class class class)co 7361 ℂcc 11030 ℝcr 11031 0cc0 11032 1c1 11033 ici 11034 + caddc 11035 · cmul 11037 < clt 11173 ≤ cle 11174 − cmin 11371 -cneg 11372 / cdiv 11801 2c2 12230 ℝ⁺crp 12936 ↑cexp 14017 ∗ccj 15052 ℜcre 15053 √csqrt 15189 abscabs 15190

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7812 df-2nd 7937 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-sup 9349 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-n0 12432 df-z 12519 df-uz 12783 df-rp 12937 df-seq 13958 df-exp 14018 df-cj 15055 df-re 15056 df-im 15057 df-sqrt 15191 df-abs 15192

This theorem is referenced by: sqreu 15317 cphsqrtcl2 25166 constrsqrtcl 33942

W3C validator