itsclc0yqsollem2

	Ref	Expression
Hypotheses	itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
	itscnhlc0yqe.t	$⊢ T = - 2 B C$
	itscnhlc0yqe.u	$⊢ U = C^{2} - A^{2} R^{2}$
	itsclc0yqsollem1.d	$⊢ D = R^{2} Q - C^{2}$
Assertion	itsclc0yqsollem2	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{T^{2} - 4 Q U} = 2 \|A\| \sqrt{D}$

Proof

Step	Hyp	Ref	Expression
1		itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
2		itscnhlc0yqe.t	$⊢ T = - 2 B C$
3		itscnhlc0yqe.u	$⊢ U = C^{2} - A^{2} R^{2}$
4		itsclc0yqsollem1.d	$⊢ D = R^{2} Q - C^{2}$
5		recn	$⊢ A \in ℝ \to A \in ℂ$
6		recn	$⊢ B \in ℝ \to B \in ℂ$
7		recn	$⊢ C \in ℝ \to C \in ℂ$
8	5 6 7	3anim123i	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A \in ℂ \land B \in ℂ \land C \in ℂ)$
9		recn	$⊢ R \in ℝ \to R \in ℂ$
10	8 9	anim12i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ)$
11	10	3adant3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ)$
12	1 2 3 4	itsclc0yqsollem1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land R \in ℂ) \to T^{2} - 4 Q U = 4 A^{2} D$
13	11 12	syl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to T^{2} - 4 Q U = 4 A^{2} D$
14	13	fveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{T^{2} - 4 Q U} = \sqrt{4 A^{2} D}$
15		4re	$⊢ 4 \in ℝ$
16	15	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to 4 \in ℝ$
17		simp1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℝ$
18	17	resqcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A^{2} \in ℝ$
19	18	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to A^{2} \in ℝ$
20	16 19	remulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to 4 A^{2} \in ℝ$
21		0re	$⊢ 0 \in ℝ$
22		4pos	$⊢ 0 < 4$
23	21 15 22	ltleii	$⊢ 0 \leq 4$
24	23	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to 0 \leq 4$
25	17	sqge0d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to 0 \leq A^{2}$
26	25	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to 0 \leq A^{2}$
27	16 19 24 26	mulge0d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to 0 \leq 4 A^{2}$
28		simp2	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to R \in ℝ$
29	28	resqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to R^{2} \in ℝ$
30	1	resum2sqcl	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℝ$
31	30	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to Q \in ℝ$
32	31	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to Q \in ℝ$
33	29 32	remulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to R^{2} Q \in ℝ$
34		simp3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to C \in ℝ$
35	34	resqcld	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to C^{2} \in ℝ$
36	35	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to C^{2} \in ℝ$
37	33 36	resubcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to R^{2} Q - C^{2} \in ℝ$
38	4 37	eqeltrid	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to D \in ℝ$
39		simp3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to 0 \leq D$
40	20 27 38 39	sqrtmuld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{4 A^{2} D} = \sqrt{4 A^{2}} \sqrt{D}$
41	15 23	pm3.2i	$⊢ (4 \in ℝ \land 0 \leq 4)$
42	41	a1i	$⊢ A \in ℝ \to (4 \in ℝ \land 0 \leq 4)$
43		resqcl	$⊢ A \in ℝ \to A^{2} \in ℝ$
44		sqge0	$⊢ A \in ℝ \to 0 \leq A^{2}$
45		sqrtmul	$⊢ ((4 \in ℝ \land 0 \leq 4) \land (A^{2} \in ℝ \land 0 \leq A^{2})) \to \sqrt{4 A^{2}} = \sqrt{4} \sqrt{A^{2}}$
46	42 43 44 45	syl12anc	$⊢ A \in ℝ \to \sqrt{4 A^{2}} = \sqrt{4} \sqrt{A^{2}}$
47	46	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to \sqrt{4 A^{2}} = \sqrt{4} \sqrt{A^{2}}$
48	47	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{4 A^{2}} = \sqrt{4} \sqrt{A^{2}}$
49		sqrt4	$⊢ \sqrt{4} = 2$
50	49	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{4} = 2$
51		absre	$⊢ A \in ℝ \to \|A\| = \sqrt{A^{2}}$
52	51	eqcomd	$⊢ A \in ℝ \to \sqrt{A^{2}} = \|A\|$
53	52	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to \sqrt{A^{2}} = \|A\|$
54	53	3ad2ant1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{A^{2}} = \|A\|$
55	50 54	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{4} \sqrt{A^{2}} = 2 \|A\|$
56	48 55	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{4 A^{2}} = 2 \|A\|$
57	56	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{4 A^{2}} \sqrt{D} = 2 \|A\| \sqrt{D}$
58	14 40 57	3eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ \land 0 \leq D) \to \sqrt{T^{2} - 4 Q U} = 2 \|A\| \sqrt{D}$

Metamath Proof Explorer

Theorem itsclc0yqsollem2

Proof