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 15281

Description: Lemma for sqreu 15282: 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 7366	. . . 4 ⊢ (𝐵↑2) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2)
3		abscl 15199	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
4		absge0 15208	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
5		resqrtcl 15174	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → (√‘(abs‘𝐴)) ∈ ℝ)
6	3, 4, 5	syl2anc 584	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℝ)
7	6	recnd 11158	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℂ)
8	7	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (√‘(abs‘𝐴)) ∈ ℂ)
9	3	recnd 11158	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℂ)
10		addcl 11106	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) + 𝐴) ∈ ℂ)
11	9, 10	mpancom 688	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + 𝐴) ∈ ℂ)
12	11	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) + 𝐴) ∈ ℂ)
13		abscl 15199	. . . . . . . . 9 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
14	11, 13	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
15	14	recnd 11158	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
16	15	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
17	11	abs00ad 15211	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴)) = 0 ↔ ((abs‘𝐴) + 𝐴) = 0))
18	17	necon3bid 2974	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴)) ≠ 0 ↔ ((abs‘𝐴) + 𝐴) ≠ 0))
19	18	biimpar 477	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ≠ 0)
20	12, 16, 19	divcld 11915	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℂ)
21	8, 20	sqmuld 14079	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)))
22	2, 21	eqtrid 2781	. . 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 15176	. . . . 5 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → ((√‘(abs‘𝐴))↑2) = (abs‘𝐴))
26	23, 24, 25	syl2anc 584	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴))↑2) = (abs‘𝐴))
27	12, 16, 19	sqdivd 14080	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2) = ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)))
28		absvalsq 15201	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
29		2cn 12218	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
30		mulass 11112	. . . . . . . . . . . . . 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 11108	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (2 · (abs‘𝐴)) ∈ ℂ)
34	29, 9, 33	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (2 · (abs‘𝐴)) ∈ ℂ)
35		mulcom 11110	. . . . . . . . . . . . 13 ⊢ (((2 · (abs‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (𝐴 · (2 · (abs‘𝐴))))
36	34, 35	mpancom 688	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) · 𝐴) = (𝐴 · (2 · (abs‘𝐴))))
37	32, 36	eqtr3d 2771	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · 𝐴)) = (𝐴 · (2 · (abs‘𝐴))))
38	28, 37	oveq12d 7374	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
39		cjcl 15026	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘𝐴) ∈ ℂ)
40		adddi 11113	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ ∧ (2 · (abs‘𝐴)) ∈ ℂ) → (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
41	39, 34, 40	mpd3an23 1465	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
42	38, 41	eqtr4d 2772	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) = (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))))
43		sqval 14035	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴))
44	42, 43	oveq12d 7374	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)) = ((𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + (𝐴 · 𝐴)))
45		binom2 14138	. . . . . . . . 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 11149	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((∗‘𝐴) + (2 · (abs‘𝐴))) ∈ ℂ)
49	47, 48, 47	adddid 11154	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = ((𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + (𝐴 · 𝐴)))
50	44, 46, 49	3eqtr4d 2779	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴)↑2) = (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))
51	9, 34	mulcld 11150	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (2 · (abs‘𝐴))) ∈ ℂ)
52	9, 39	mulcld 11150	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (∗‘𝐴)) ∈ ℂ)
53	51, 52	addcomd 11333	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (2 · (abs‘𝐴))) + ((abs‘𝐴) · (∗‘𝐴))) = (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · (2 · (abs‘𝐴)))))
54	9, 9	mulcld 11150	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (abs‘𝐴)) ∈ ℂ)
55	54	2timesd 12382	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · (abs‘𝐴))) = (((abs‘𝐴) · (abs‘𝐴)) + ((abs‘𝐴) · (abs‘𝐴))))
56		mul12 11296	. . . . . . . . . . . . 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 14064	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = ((abs‘𝐴) · (abs‘𝐴)))
59		mulcom 11110	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ) → (𝐴 · (∗‘𝐴)) = ((∗‘𝐴) · 𝐴))
60	39, 59	mpdan 687	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = ((∗‘𝐴) · 𝐴))
61	28, 58, 60	3eqtr3d 2777	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (abs‘𝐴)) = ((∗‘𝐴) · 𝐴))
62	61	oveq2d 7372	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((abs‘𝐴) · (abs‘𝐴))) = (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)))
63	55, 57, 62	3eqtr3rd 2778	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
64	63	oveq1d 7371	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) = (((abs‘𝐴) · (2 · (abs‘𝐴))) + ((abs‘𝐴) · (∗‘𝐴))))
65	9, 39, 34	adddid 11154	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · (2 · (abs‘𝐴)))))
66	53, 64, 65	3eqtr4d 2779	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) = ((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))))
67	66	oveq1d 7371	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)) = (((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + ((abs‘𝐴) · 𝐴)))
68		cjadd 15062	. . . . . . . . . . . . 13 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (∗‘((abs‘𝐴) + 𝐴)) = ((∗‘(abs‘𝐴)) + (∗‘𝐴)))
69	9, 68	mpancom 688	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (∗‘((abs‘𝐴) + 𝐴)) = ((∗‘(abs‘𝐴)) + (∗‘𝐴)))
70	3	cjred 15147	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (∗‘(abs‘𝐴)) = (abs‘𝐴))
71	70	oveq1d 7371	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((∗‘(abs‘𝐴)) + (∗‘𝐴)) = ((abs‘𝐴) + (∗‘𝐴)))
72	69, 71	eqtrd 2769	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘((abs‘𝐴) + 𝐴)) = ((abs‘𝐴) + (∗‘𝐴)))
73	72	oveq2d 7372	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))) = (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) + (∗‘𝐴))))
74	9, 47, 9, 39	muladdd 11593	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) + (∗‘𝐴))) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
75	73, 74	eqtrd 2769	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
76		absvalsq 15201	. . . . . . . . . 10 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))))
77	11, 76	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))))
78		mulcl 11108	. . . . . . . . . . . 12 ⊢ (((∗‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((∗‘𝐴) · 𝐴) ∈ ℂ)
79	39, 78	mpancom 688	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((∗‘𝐴) · 𝐴) ∈ ℂ)
80	54, 79	addcld 11149	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) ∈ ℂ)
81		mulcl 11108	. . . . . . . . . . 11 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) · 𝐴) ∈ ℂ)
82	9, 81	mpancom 688	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · 𝐴) ∈ ℂ)
83	80, 52, 82	addassd 11152	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
84	75, 77, 83	3eqtr4d 2779	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)))
85	9, 48, 47	adddid 11154	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = (((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + ((abs‘𝐴) · 𝐴)))
86	67, 84, 85	3eqtr4d 2779	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))
87	50, 86	oveq12d 7374	. . . . . 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 2769	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
90	26, 89	oveq12d 7374	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)) = ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))))
91		addcl 11106	. . . . . . . 8 ⊢ ((((∗‘𝐴) + (2 · (abs‘𝐴))) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ)
92	48, 91	mpancom 688	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ)
93	9, 47, 92	mul12d 11340	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = (𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
94	93	oveq1d 7371	. . . . 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 11108	. . . . . . 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 11150	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
101	100	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
102		sqeq0 14041	. . . . . . . . 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 2736	. . . . . . . 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 2974	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) ≠ 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ≠ 0))
107	106	biimpa 476	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ≠ 0)
108	96, 99, 101, 107	divassd 11950	. . . 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 11921	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = 𝐴)
111	95, 108, 110	3eqtr3d 2777	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))) = 𝐴)
112	22, 90, 111	3eqtrd 2773	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵↑2) = 𝐴)
113	6	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (√‘(abs‘𝐴)) ∈ ℝ)
114	11	addcjd 15133	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) = (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
115		2re 12217	. . . . . . . . 9 ⊢ 2 ∈ ℝ
116	11	recld 15115	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
117		remulcl 11109	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ) → (2 · (ℜ‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
118	115, 116, 117	sylancr 587	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (2 · (ℜ‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
119	114, 118	eqeltrd 2834	. . . . . . 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 11967	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
123	113, 122	remulcld 11160	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ)
124		sqrtge0 15178	. . . . . . 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 11378	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
128		releabs 15243	. . . . . . . . . . . 12 ⊢ (-𝐴 ∈ ℂ → (ℜ‘-𝐴) ≤ (abs‘-𝐴))
129	127, 128	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ≤ (abs‘-𝐴))
130		abscl 15199	. . . . . . . . . . . . 13 ⊢ (-𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℝ)
131	127, 130	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℝ)
132	127	recld 15115	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ∈ ℝ)
133	131, 132	subge0d 11725	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (0 ≤ ((abs‘-𝐴) − (ℜ‘-𝐴)) ↔ (ℜ‘-𝐴) ≤ (abs‘-𝐴)))
134	129, 133	mpbird 257	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → 0 ≤ ((abs‘-𝐴) − (ℜ‘-𝐴)))
135		readd 15047	. . . . . . . . . . . 12 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (ℜ‘((abs‘𝐴) + 𝐴)) = ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)))
136	9, 135	mpancom 688	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) = ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)))
137	3	rered 15145	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘(abs‘𝐴)) = (abs‘𝐴))
138		absneg 15198	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴))
139	137, 138	eqtr4d 2772	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘(abs‘𝐴)) = (abs‘-𝐴))
140		negneg 11429	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴)
141	140	fveq2d 6836	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘--𝐴) = (ℜ‘𝐴))
142	127	renegd 15130	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘--𝐴) = -(ℜ‘-𝐴))
143	141, 142	eqtr3d 2771	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = -(ℜ‘-𝐴))
144	139, 143	oveq12d 7374	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)) = ((abs‘-𝐴) + -(ℜ‘-𝐴)))
145	131	recnd 11158	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℂ)
146	132	recnd 11158	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ∈ ℂ)
147	145, 146	negsubd 11496	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘-𝐴) + -(ℜ‘-𝐴)) = ((abs‘-𝐴) − (ℜ‘-𝐴)))
148	136, 144, 147	3eqtrd 2773	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) = ((abs‘-𝐴) − (ℜ‘-𝐴)))
149	134, 148	breqtrrd 5124	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴)))
150		0le2 12245	. . . . . . . . . 10 ⊢ 0 ≤ 2
151		mulge0 11653	. . . . . . . . . 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 5124	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))))
155	154	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))))
156		absge0 15208	. . . . . . . 8 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → 0 ≤ (abs‘((abs‘𝐴) + 𝐴)))
157	12, 156	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (abs‘((abs‘𝐴) + 𝐴)))
158	121, 157, 19	ne0gt0d 11268	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 < (abs‘((abs‘𝐴) + 𝐴)))
159		divge0 12009	. . . . . 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 11712	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))))
162		2pos 12246	. . . . 5 ⊢ 0 < 2
163		divge0 12009	. . . . 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 11150	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℂ)
167	1, 166	eqeltrid 2838	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 𝐵 ∈ ℂ)
168		reval 15027	. . . . 5 ⊢ (𝐵 ∈ ℂ → (ℜ‘𝐵) = ((𝐵 + (∗‘𝐵)) / 2))
169	167, 168	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (ℜ‘𝐵) = ((𝐵 + (∗‘𝐵)) / 2))
170	1	oveq1i 7366	. . . . . . 7 ⊢ (𝐵 + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
171	1	fveq2i 6835	. . . . . . . . . 10 ⊢ (∗‘𝐵) = (∗‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))))
172	8, 20	cjmuld 15142	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) = ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))))
173	171, 172	eqtrid 2781	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘𝐵) = ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))))
174	6	cjred 15147	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘(√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
175	174	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
176	12, 16, 19	cjdivd 15144	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (∗‘(abs‘((abs‘𝐴) + 𝐴)))))
177	121	cjred 15147	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(abs‘((abs‘𝐴) + 𝐴))) = (abs‘((abs‘𝐴) + 𝐴)))
178	177	oveq2d 7372	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘((abs‘𝐴) + 𝐴)) / (∗‘(abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))
179	176, 178	eqtrd 2769	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))
180	175, 179	oveq12d 7374	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) = ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
181	173, 180	eqtrd 2769	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘𝐵) = ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
182	181	oveq2d 7372	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = (𝐵 + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
183	12	cjcld 15117	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
184	183, 16, 19	divcld 11915	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℂ)
185	8, 20, 184	adddid 11154	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
186	170, 182, 185	3eqtr4a 2795	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
187	12, 183, 16, 19	divdird 11953	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))) = ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
188	187	oveq2d 7372	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
189	186, 188	eqtr4d 2772	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))))
190	189	oveq1d 7371	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵 + (∗‘𝐵)) / 2) = (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
191	169, 190	eqtrd 2769	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (ℜ‘𝐵) = (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
192	165, 191	breqtrrd 5124	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (ℜ‘𝐵))
193		subneg 11428	. . . . . . . . . 10 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) − -𝐴) = ((abs‘𝐴) + 𝐴))
194	9, 193	mpancom 688	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -𝐴) = ((abs‘𝐴) + 𝐴))
195	194	eqeq1d 2736	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − -𝐴) = 0 ↔ ((abs‘𝐴) + 𝐴) = 0))
196	9, 127	subeq0ad 11500	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − -𝐴) = 0 ↔ (abs‘𝐴) = -𝐴))
197	195, 196	bitr3d 281	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) = 0 ↔ (abs‘𝐴) = -𝐴))
198	197	necon3bid 2974	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) ≠ 0 ↔ (abs‘𝐴) ≠ -𝐴))
199	198	biimpa 476	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘𝐴) ≠ -𝐴)
200		resqcl 14045	. . . . . . . . . 10 ⊢ ((i · 𝐵) ∈ ℝ → ((i · 𝐵)↑2) ∈ ℝ)
201		ax-icn 11083	. . . . . . . . . . . . 13 ⊢ i ∈ ℂ
202		sqmul 14040	. . . . . . . . . . . . 13 ⊢ ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i · 𝐵)↑2) = ((i↑2) · (𝐵↑2)))
203	201, 167, 202	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵)↑2) = ((i↑2) · (𝐵↑2)))
204		i2 14123	. . . . . . . . . . . . . 14 ⊢ (i↑2) = -1
205	204	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (i↑2) = -1)
206	205, 112	oveq12d 7374	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i↑2) · (𝐵↑2)) = (-1 · 𝐴))
207		mulm1 11576	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴)
208	207	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (-1 · 𝐴) = -𝐴)
209	203, 206, 208	3eqtrd 2773	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵)↑2) = -𝐴)
210	209	eleq1d 2819	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((i · 𝐵)↑2) ∈ ℝ ↔ -𝐴 ∈ ℝ))
211	200, 210	imbitrid 244	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → -𝐴 ∈ ℝ))
212		renegcl 11442	. . . . . . . . . 10 ⊢ (-𝐴 ∈ ℝ → --𝐴 ∈ ℝ)
213	140	eleq1d 2819	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (--𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ))
214	212, 213	imbitrid 244	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ → 𝐴 ∈ ℝ))
215	109, 211, 214	sylsyld 61	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 𝐴 ∈ ℝ))
216		sqge0 14057	. . . . . . . . . 10 ⊢ ((i · 𝐵) ∈ ℝ → 0 ≤ ((i · 𝐵)↑2))
217	209	breq2d 5108	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (0 ≤ ((i · 𝐵)↑2) ↔ 0 ≤ -𝐴))
218	216, 217	imbitrid 244	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 0 ≤ -𝐴))
219		le0neg1 11643	. . . . . . . . . 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 15219	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴)
224	222, 223	syl6 35	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → (abs‘𝐴) = -𝐴))
225	224	necon3ad 2943	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) ≠ -𝐴 → ¬ (i · 𝐵) ∈ ℝ))
226	199, 225	mpd 15	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ¬ (i · 𝐵) ∈ ℝ)
227		rpre 12912	. . . 4 ⊢ ((i · 𝐵) ∈ ℝ⁺ → (i · 𝐵) ∈ ℝ)
228	226, 227	nsyl 140	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ¬ (i · 𝐵) ∈ ℝ⁺)
229		df-nel 3035	. . 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 2930 ∉ wnel 3034 class class class wbr 5096 ‘cfv 6490 (class class class)co 7356 ℂcc 11022 ℝcr 11023 0cc0 11024 1c1 11025 ici 11026 + caddc 11027 · cmul 11029 < clt 11164 ≤ cle 11165 − cmin 11362 -cneg 11363 / cdiv 11792 2c2 12198 ℝ⁺crp 12903 ↑cexp 13982 ∗ccj 15017 ℜcre 15018 √csqrt 15154 abscabs 15155

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 2182 ax-ext 2706 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101 ax-pre-sup 11102

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 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-iun 4946 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-er 8633 df-en 8882 df-dom 8883 df-sdom 8884 df-sup 9343 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-div 11793 df-nn 12144 df-2 12206 df-3 12207 df-n0 12400 df-z 12487 df-uz 12750 df-rp 12904 df-seq 13923 df-exp 13983 df-cj 15020 df-re 15021 df-im 15022 df-sqrt 15156 df-abs 15157

This theorem is referenced by: sqreu 15282 cphsqrtcl2 25140 constrsqrtcl 33885

W3C validator