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 13947

Description: Lemma for sqreu 13948: 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 6559	. . . 4 ⊢ (𝐵↑2) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2)
3		abscl 13866	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
4		absge0 13875	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
5		resqrtcl 13842	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → (√‘(abs‘𝐴)) ∈ ℝ)
6	3, 4, 5	syl2anc 691	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℝ)
7	6	recnd 9947	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℂ)
8	7	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (√‘(abs‘𝐴)) ∈ ℂ)
9	3	recnd 9947	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℂ)
10		addcl 9897	. . . . . . . 8 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) + 𝐴) ∈ ℂ)
11	9, 10	mpancom 700	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + 𝐴) ∈ ℂ)
12	11	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) + 𝐴) ∈ ℂ)
13		abscl 13866	. . . . . . . . 9 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
14	11, 13	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
15	14	recnd 9947	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
16	15	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
17	11	abs00ad 13878	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴)) = 0 ↔ ((abs‘𝐴) + 𝐴) = 0))
18	17	necon3bid 2826	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴)) ≠ 0 ↔ ((abs‘𝐴) + 𝐴) ≠ 0))
19	18	biimpar 501	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ≠ 0)
20	12, 16, 19	divcld 10680	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℂ)
21	8, 20	sqmuld 12882	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))↑2) = (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)))
22	2, 21	syl5eq 2656	. . 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 13844	. . . . 5 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → ((√‘(abs‘𝐴))↑2) = (abs‘𝐴))
26	23, 24, 25	syl2anc 691	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴))↑2) = (abs‘𝐴))
27	12, 16, 19	sqdivd 12883	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2) = ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)))
28		absvalsq 13868	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
29		2cn 10968	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
30		mulass 9903	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
31	29, 30	mp3an1 1403	. . . . . . . . . . . . 13 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
32	9, 31	mpancom 700	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) · 𝐴) = (2 · ((abs‘𝐴) · 𝐴)))
33		mulcl 9899	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (2 · (abs‘𝐴)) ∈ ℂ)
34	29, 9, 33	sylancr 694	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (2 · (abs‘𝐴)) ∈ ℂ)
35		mulcom 9901	. . . . . . . . . . . . 13 ⊢ (((2 · (abs‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · (abs‘𝐴)) · 𝐴) = (𝐴 · (2 · (abs‘𝐴))))
36	34, 35	mpancom 700	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) · 𝐴) = (𝐴 · (2 · (abs‘𝐴))))
37	32, 36	eqtr3d 2646	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · 𝐴)) = (𝐴 · (2 · (abs‘𝐴))))
38	28, 37	oveq12d 6567	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
39		cjcl 13693	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘𝐴) ∈ ℂ)
40		adddi 9904	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ ∧ (2 · (abs‘𝐴)) ∈ ℂ) → (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
41	39, 34, 40	mpd3an23 1418	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = ((𝐴 · (∗‘𝐴)) + (𝐴 · (2 · (abs‘𝐴)))))
42	38, 41	eqtr4d 2647	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) = (𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))))
43		sqval 12784	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴))
44	42, 43	oveq12d 6567	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)) = ((𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + (𝐴 · 𝐴)))
45		binom2 12841	. . . . . . . . 9 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((abs‘𝐴) + 𝐴)↑2) = ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)))
46	9, 45	mpancom 700	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴)↑2) = ((((abs‘𝐴)↑2) + (2 · ((abs‘𝐴) · 𝐴))) + (𝐴↑2)))
47		id 22	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
48	39, 34	addcld 9938	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((∗‘𝐴) + (2 · (abs‘𝐴))) ∈ ℂ)
49	47, 48, 47	adddid 9943	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = ((𝐴 · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + (𝐴 · 𝐴)))
50	44, 46, 49	3eqtr4d 2654	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴)↑2) = (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))
51	9, 34	mulcld 9939	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (2 · (abs‘𝐴))) ∈ ℂ)
52	9, 39	mulcld 9939	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (∗‘𝐴)) ∈ ℂ)
53	51, 52	addcomd 10117	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (2 · (abs‘𝐴))) + ((abs‘𝐴) · (∗‘𝐴))) = (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · (2 · (abs‘𝐴)))))
54	9, 9	mulcld 9939	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (abs‘𝐴)) ∈ ℂ)
55	54	2timesd 11152	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · (abs‘𝐴))) = (((abs‘𝐴) · (abs‘𝐴)) + ((abs‘𝐴) · (abs‘𝐴))))
56		mul12 10081	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (2 · ((abs‘𝐴) · (abs‘𝐴))) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
57	29, 56	mp3an1 1403	. . . . . . . . . . . . 13 ⊢ (((abs‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (2 · ((abs‘𝐴) · (abs‘𝐴))) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
58	9, 9, 57	syl2anc 691	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (2 · ((abs‘𝐴) · (abs‘𝐴))) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
59	9	sqvald 12867	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = ((abs‘𝐴) · (abs‘𝐴)))
60		mulcom 9901	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (∗‘𝐴) ∈ ℂ) → (𝐴 · (∗‘𝐴)) = ((∗‘𝐴) · 𝐴))
61	39, 60	mpdan 699	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = ((∗‘𝐴) · 𝐴))
62	28, 59, 61	3eqtr3d 2652	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (abs‘𝐴)) = ((∗‘𝐴) · 𝐴))
63	62	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((abs‘𝐴) · (abs‘𝐴))) = (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)))
64	55, 58, 63	3eqtr3rd 2653	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) = ((abs‘𝐴) · (2 · (abs‘𝐴))))
65	64	oveq1d 6564	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) = (((abs‘𝐴) · (2 · (abs‘𝐴))) + ((abs‘𝐴) · (∗‘𝐴))))
66	9, 39, 34	adddid 9943	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) = (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · (2 · (abs‘𝐴)))))
67	53, 65, 66	3eqtr4d 2654	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) = ((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))))
68	67	oveq1d 6564	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)) = (((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + ((abs‘𝐴) · 𝐴)))
69		cjadd 13729	. . . . . . . . . . . . 13 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (∗‘((abs‘𝐴) + 𝐴)) = ((∗‘(abs‘𝐴)) + (∗‘𝐴)))
70	9, 69	mpancom 700	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (∗‘((abs‘𝐴) + 𝐴)) = ((∗‘(abs‘𝐴)) + (∗‘𝐴)))
71	3	cjred 13814	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (∗‘(abs‘𝐴)) = (abs‘𝐴))
72	71	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((∗‘(abs‘𝐴)) + (∗‘𝐴)) = ((abs‘𝐴) + (∗‘𝐴)))
73	70, 72	eqtrd 2644	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘((abs‘𝐴) + 𝐴)) = ((abs‘𝐴) + (∗‘𝐴)))
74	73	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))) = (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) + (∗‘𝐴))))
75	9, 47, 9, 39	muladdd 10368	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) + (∗‘𝐴))) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
76	74, 75	eqtrd 2644	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
77		absvalsq 13868	. . . . . . . . . 10 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))))
78	11, 77	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((abs‘𝐴) + 𝐴) · (∗‘((abs‘𝐴) + 𝐴))))
79		mulcl 9899	. . . . . . . . . . . 12 ⊢ (((∗‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((∗‘𝐴) · 𝐴) ∈ ℂ)
80	39, 79	mpancom 700	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((∗‘𝐴) · 𝐴) ∈ ℂ)
81	54, 80	addcld 9938	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) ∈ ℂ)
82		mulcl 9899	. . . . . . . . . . 11 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) · 𝐴) ∈ ℂ)
83	9, 82	mpancom 700	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · 𝐴) ∈ ℂ)
84	81, 52, 83	addassd 9941	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)) = ((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + (((abs‘𝐴) · (∗‘𝐴)) + ((abs‘𝐴) · 𝐴))))
85	76, 78, 84	3eqtr4d 2654	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = (((((abs‘𝐴) · (abs‘𝐴)) + ((∗‘𝐴) · 𝐴)) + ((abs‘𝐴) · (∗‘𝐴))) + ((abs‘𝐴) · 𝐴)))
86	9, 48, 47	adddid 9943	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = (((abs‘𝐴) · ((∗‘𝐴) + (2 · (abs‘𝐴)))) + ((abs‘𝐴) · 𝐴)))
87	68, 85, 86	3eqtr4d 2654	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((abs‘((abs‘𝐴) + 𝐴))↑2) = ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))
88	50, 87	oveq12d 6567	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
89	88	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴)↑2) / ((abs‘((abs‘𝐴) + 𝐴))↑2)) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
90	27, 89	eqtrd 2644	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2) = ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
91	26, 90	oveq12d 6567	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((√‘(abs‘𝐴))↑2) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))↑2)) = ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))))
92		addcl 9897	. . . . . . . 8 ⊢ ((((∗‘𝐴) + (2 · (abs‘𝐴))) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ)
93	48, 92	mpancom 700	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ)
94	9, 47, 93	mul12d 10124	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = (𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
95	94	oveq1d 6564	. . . . 5 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
96	95	adantr 480	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))))
97	9	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘𝐴) ∈ ℂ)
98		mulcl 9899	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴) ∈ ℂ) → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
99	93, 98	mpdan 699	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
100	99	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
101	9, 93	mulcld 9939	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
102	101	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ∈ ℂ)
103		sqeq0 12789	. . . . . . . . 9 ⊢ ((abs‘((abs‘𝐴) + 𝐴)) ∈ ℂ → (((abs‘((abs‘𝐴) + 𝐴))↑2) = 0 ↔ (abs‘((abs‘𝐴) + 𝐴)) = 0))
104	15, 103	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘((abs‘𝐴) + 𝐴))↑2) = 0 ↔ (abs‘((abs‘𝐴) + 𝐴)) = 0))
105	87	eqeq1d 2612	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘((abs‘𝐴) + 𝐴))↑2) = 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = 0))
106	104, 105, 17	3bitr3rd 298	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) = 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) = 0))
107	106	necon3bid 2826	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) ≠ 0 ↔ ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ≠ 0))
108	107	biimpa 500	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) ≠ 0)
109	97, 100, 102, 108	divassd 10715	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) · (𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))))
110		simpl 472	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 𝐴 ∈ ℂ)
111	110, 102, 108	divcan4d 10686	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐴 · ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴))) = 𝐴)
112	96, 109, 111	3eqtr3d 2652	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) · ((𝐴 · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)) / ((abs‘𝐴) · (((∗‘𝐴) + (2 · (abs‘𝐴))) + 𝐴)))) = 𝐴)
113	22, 91, 112	3eqtrd 2648	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵↑2) = 𝐴)
114	6	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (√‘(abs‘𝐴)) ∈ ℝ)
115	11	addcjd 13800	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) = (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
116		2re 10967	. . . . . . . . 9 ⊢ 2 ∈ ℝ
117	11	recld 13782	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
118		remulcl 9900	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ) → (2 · (ℜ‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
119	116, 117, 118	sylancr 694	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (2 · (ℜ‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
120	115, 119	eqeltrd 2688	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
121	120	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
122	14	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ)
123	121, 122, 19	redivcld 10732	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℝ)
124	114, 123	remulcld 9949	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ)
125		sqrtge0 13846	. . . . . . 7 ⊢ (((abs‘𝐴) ∈ ℝ ∧ 0 ≤ (abs‘𝐴)) → 0 ≤ (√‘(abs‘𝐴)))
126	3, 4, 125	syl2anc 691	. . . . . 6 ⊢ (𝐴 ∈ ℂ → 0 ≤ (√‘(abs‘𝐴)))
127	126	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (√‘(abs‘𝐴)))
128		negcl 10160	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
129		releabs 13909	. . . . . . . . . . . 12 ⊢ (-𝐴 ∈ ℂ → (ℜ‘-𝐴) ≤ (abs‘-𝐴))
130	128, 129	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ≤ (abs‘-𝐴))
131		abscl 13866	. . . . . . . . . . . . 13 ⊢ (-𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℝ)
132	128, 131	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℝ)
133	128	recld 13782	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ∈ ℝ)
134	132, 133	subge0d 10496	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (0 ≤ ((abs‘-𝐴) − (ℜ‘-𝐴)) ↔ (ℜ‘-𝐴) ≤ (abs‘-𝐴)))
135	130, 134	mpbird 246	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → 0 ≤ ((abs‘-𝐴) − (ℜ‘-𝐴)))
136		readd 13714	. . . . . . . . . . . 12 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (ℜ‘((abs‘𝐴) + 𝐴)) = ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)))
137	9, 136	mpancom 700	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) = ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)))
138	3	rered 13812	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘(abs‘𝐴)) = (abs‘𝐴))
139		absneg 13865	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴))
140	138, 139	eqtr4d 2647	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘(abs‘𝐴)) = (abs‘-𝐴))
141		negneg 10210	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴)
142	141	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘--𝐴) = (ℜ‘𝐴))
143	128	renegd 13797	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (ℜ‘--𝐴) = -(ℜ‘-𝐴))
144	142, 143	eqtr3d 2646	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = -(ℜ‘-𝐴))
145	140, 144	oveq12d 6567	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((ℜ‘(abs‘𝐴)) + (ℜ‘𝐴)) = ((abs‘-𝐴) + -(ℜ‘-𝐴)))
146	132	recnd 9947	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) ∈ ℂ)
147	133	recnd 9947	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) ∈ ℂ)
148	146, 147	negsubd 10277	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘-𝐴) + -(ℜ‘-𝐴)) = ((abs‘-𝐴) − (ℜ‘-𝐴)))
149	137, 145, 148	3eqtrd 2648	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (ℜ‘((abs‘𝐴) + 𝐴)) = ((abs‘-𝐴) − (ℜ‘-𝐴)))
150	135, 149	breqtrrd 4611	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴)))
151		0le2 10988	. . . . . . . . . 10 ⊢ 0 ≤ 2
152		mulge0 10425	. . . . . . . . . 10 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ ((ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴)))) → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
153	116, 151, 152	mpanl12 714	. . . . . . . . 9 ⊢ (((ℜ‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 ≤ (ℜ‘((abs‘𝐴) + 𝐴))) → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
154	117, 150, 153	syl2anc 691	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → 0 ≤ (2 · (ℜ‘((abs‘𝐴) + 𝐴))))
155	154, 115	breqtrrd 4611	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))))
156	155	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))))
157		absge0 13875	. . . . . . . 8 ⊢ (((abs‘𝐴) + 𝐴) ∈ ℂ → 0 ≤ (abs‘((abs‘𝐴) + 𝐴)))
158	12, 157	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (abs‘((abs‘𝐴) + 𝐴)))
159	122, 158, 19	ne0gt0d 10053	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 < (abs‘((abs‘𝐴) + 𝐴)))
160		divge0 10771	. . . . . 6 ⊢ ((((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) ∈ ℝ ∧ 0 ≤ (((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴)))) ∧ ((abs‘((abs‘𝐴) + 𝐴)) ∈ ℝ ∧ 0 < (abs‘((abs‘𝐴) + 𝐴)))) → 0 ≤ ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))
161	121, 156, 122, 159, 160	syl22anc 1319	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))
162	114, 123, 127, 161	mulge0d 10483	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))))
163		2pos 10989	. . . . 5 ⊢ 0 < 2
164		divge0 10771	. . . . 5 ⊢ (((((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ ∧ 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
165	116, 163, 164	mpanr12 717	. . . 4 ⊢ ((((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℝ ∧ 0 ≤ ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))))) → 0 ≤ (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
166	124, 162, 165	syl2anc 691	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
167	8, 20	mulcld 9939	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ∈ ℂ)
168	1, 167	syl5eqel 2692	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 𝐵 ∈ ℂ)
169		reval 13694	. . . . 5 ⊢ (𝐵 ∈ ℂ → (ℜ‘𝐵) = ((𝐵 + (∗‘𝐵)) / 2))
170	168, 169	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (ℜ‘𝐵) = ((𝐵 + (∗‘𝐵)) / 2))
171	1	oveq1i 6559	. . . . . . 7 ⊢ (𝐵 + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
172	1	fveq2i 6106	. . . . . . . . . 10 ⊢ (∗‘𝐵) = (∗‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))))
173	8, 20	cjmuld 13809	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) = ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))))
174	172, 173	syl5eq 2656	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘𝐵) = ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))))
175	6	cjred 13814	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (∗‘(√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
176	175	adantr 480	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
177	12, 16, 19	cjdivd 13811	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (∗‘(abs‘((abs‘𝐴) + 𝐴)))))
178	122	cjred 13814	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(abs‘((abs‘𝐴) + 𝐴))) = (abs‘((abs‘𝐴) + 𝐴)))
179	178	oveq2d 6565	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘((abs‘𝐴) + 𝐴)) / (∗‘(abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))
180	177, 179	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) = ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))
181	176, 180	oveq12d 6567	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘(√‘(abs‘𝐴))) · (∗‘(((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))))) = ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
182	174, 181	eqtrd 2644	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘𝐵) = ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
183	182	oveq2d 6565	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = (𝐵 + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
184	12	cjcld 13784	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (∗‘((abs‘𝐴) + 𝐴)) ∈ ℂ)
185	184, 16, 19	divcld 10680	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))) ∈ ℂ)
186	8, 20, 185	adddid 9943	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))) = (((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) + ((√‘(abs‘𝐴)) · ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
187	171, 183, 186	3eqtr4a 2670	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
188	12, 184, 16, 19	divdird 10718	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴))) = ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴)))))
189	188	oveq2d 6565	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴))) + ((∗‘((abs‘𝐴) + 𝐴)) / (abs‘((abs‘𝐴) + 𝐴))))))
190	187, 189	eqtr4d 2647	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (𝐵 + (∗‘𝐵)) = ((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))))
191	190	oveq1d 6564	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵 + (∗‘𝐵)) / 2) = (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
192	170, 191	eqtrd 2644	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (ℜ‘𝐵) = (((√‘(abs‘𝐴)) · ((((abs‘𝐴) + 𝐴) + (∗‘((abs‘𝐴) + 𝐴))) / (abs‘((abs‘𝐴) + 𝐴)))) / 2))
193	166, 192	breqtrrd 4611	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → 0 ≤ (ℜ‘𝐵))
194		subneg 10209	. . . . . . . . . 10 ⊢ (((abs‘𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((abs‘𝐴) − -𝐴) = ((abs‘𝐴) + 𝐴))
195	9, 194	mpancom 700	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -𝐴) = ((abs‘𝐴) + 𝐴))
196	195	eqeq1d 2612	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − -𝐴) = 0 ↔ ((abs‘𝐴) + 𝐴) = 0))
197	9, 128	subeq0ad 10281	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − -𝐴) = 0 ↔ (abs‘𝐴) = -𝐴))
198	196, 197	bitr3d 269	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) = 0 ↔ (abs‘𝐴) = -𝐴))
199	198	necon3bid 2826	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + 𝐴) ≠ 0 ↔ (abs‘𝐴) ≠ -𝐴))
200	199	biimpa 500	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (abs‘𝐴) ≠ -𝐴)
201		resqcl 12793	. . . . . . . . . 10 ⊢ ((i · 𝐵) ∈ ℝ → ((i · 𝐵)↑2) ∈ ℝ)
202		ax-icn 9874	. . . . . . . . . . . . 13 ⊢ i ∈ ℂ
203		sqmul 12788	. . . . . . . . . . . . 13 ⊢ ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i · 𝐵)↑2) = ((i↑2) · (𝐵↑2)))
204	202, 168, 203	sylancr 694	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵)↑2) = ((i↑2) · (𝐵↑2)))
205		i2 12827	. . . . . . . . . . . . . 14 ⊢ (i↑2) = -1
206	205	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (i↑2) = -1)
207	206, 113	oveq12d 6567	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i↑2) · (𝐵↑2)) = (-1 · 𝐴))
208		mulm1 10350	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴)
209	208	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (-1 · 𝐴) = -𝐴)
210	204, 207, 209	3eqtrd 2648	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵)↑2) = -𝐴)
211	210	eleq1d 2672	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (((i · 𝐵)↑2) ∈ ℝ ↔ -𝐴 ∈ ℝ))
212	201, 211	syl5ib 233	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → -𝐴 ∈ ℝ))
213		renegcl 10223	. . . . . . . . . 10 ⊢ (-𝐴 ∈ ℝ → --𝐴 ∈ ℝ)
214	141	eleq1d 2672	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (--𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ))
215	213, 214	syl5ib 233	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ → 𝐴 ∈ ℝ))
216	110, 212, 215	sylsyld 59	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 𝐴 ∈ ℝ))
217		sqge0 12802	. . . . . . . . . 10 ⊢ ((i · 𝐵) ∈ ℝ → 0 ≤ ((i · 𝐵)↑2))
218	210	breq2d 4595	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (0 ≤ ((i · 𝐵)↑2) ↔ 0 ≤ -𝐴))
219	217, 218	syl5ib 233	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 0 ≤ -𝐴))
220		le0neg1 10415	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴))
221	220	biimprcd 239	. . . . . . . . 9 ⊢ (0 ≤ -𝐴 → (𝐴 ∈ ℝ → 𝐴 ≤ 0))
222	219, 216, 221	syl6c 68	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → 𝐴 ≤ 0))
223	216, 222	jcad 554	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐴 ≤ 0)))
224		absnid 13886	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴)
225	223, 224	syl6 34	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((i · 𝐵) ∈ ℝ → (abs‘𝐴) = -𝐴))
226	225	necon3ad 2795	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((abs‘𝐴) ≠ -𝐴 → ¬ (i · 𝐵) ∈ ℝ))
227	200, 226	mpd 15	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ¬ (i · 𝐵) ∈ ℝ)
228		rpre 11715	. . . 4 ⊢ ((i · 𝐵) ∈ ℝ⁺ → (i · 𝐵) ∈ ℝ)
229	227, 228	nsyl 134	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ¬ (i · 𝐵) ∈ ℝ⁺)
230		df-nel 2783	. . 3 ⊢ ((i · 𝐵) ∉ ℝ⁺ ↔ ¬ (i · 𝐵) ∈ ℝ⁺)
231	229, 230	sylibr 223	. 2 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → (i · 𝐵) ∉ ℝ⁺)
232	113, 193, 231	3jca 1235	1 ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝐵) ∧ (i · 𝐵) ∉ ℝ⁺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∉ wnel 2781 class class class wbr 4583 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 ici 9817 + caddc 9818 · cmul 9820 < clt 9953 ≤ cle 9954 − cmin 10145 -cneg 10146 / cdiv 10563 2c2 10947 ℝ⁺crp 11708 ↑cexp 12722 ∗ccj 13684 ℜcre 13685 √csqrt 13821 abscabs 13822

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-sup 8231 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-seq 12664 df-exp 12723 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824

This theorem is referenced by: sqreu 13948 cphsqrtcl2 22794

W3C validator