Theorem itsclc0xyqsolr

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 2-May-2023) (Revised by AV, 14-May-2023)

	Ref	Expression
Hypotheses	itsclc0xyqsolr.q	|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
	itsclc0xyqsolr.d	|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
Assertion	itsclc0xyqsolr	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) ) )

Proof

Step	Hyp	Ref	Expression
1		itsclc0xyqsolr.q	|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
2		itsclc0xyqsolr.d	|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
3		recn	|- ( A e. RR -> A e. CC )
4	3	3ad2ant1	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
5	4	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> A e. CC )
6		recn	|- ( C e. RR -> C e. CC )
7	6	3ad2ant3	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. CC )
8	7	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> C e. CC )
9	5 8	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. C ) e. CC )
10		recn	|- ( B e. RR -> B e. CC )
11	10	3ad2ant2	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
12	11	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B e. CC )
13		rpre	|- ( R e. RR+ -> R e. RR )
14	13	adantr	|- ( ( R e. RR+ /\ 0 <_ D ) -> R e. RR )
15	14	anim2i	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) )
16	15	3adant2	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) )
17	1 2	itsclc0lem3	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> D e. RR )
18	16 17	syl	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> D e. RR )
19	18	recnd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> D e. CC )
20	19	sqrtcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( sqrt ` D ) e. CC )
21	12 20	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( sqrt ` D ) ) e. CC )
22	9 21	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) e. CC )
23	1	resum2sqcl	|- ( ( A e. RR /\ B e. RR ) -> Q e. RR )
24	23	3adant3	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> Q e. RR )
25	24	recnd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> Q e. CC )
26	25	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q e. CC )
27		simp11	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> A e. RR )
28		simp12	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B e. RR )
29		simp2	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A =/= 0 \/ B =/= 0 ) )
30	1	resum2sqorgt0	|- ( ( A e. RR /\ B e. RR /\ ( A =/= 0 \/ B =/= 0 ) ) -> 0 < Q )
31	27 28 29 30	syl3anc	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> 0 < Q )
32	31	gt0ne0d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q =/= 0 )
33	22 26 32	sqdivd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) = ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ^ 2 ) / ( Q ^ 2 ) ) )
34	4 7	mulcld	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. C ) e. CC )
35	34	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. C ) e. CC )
36		binom2	|- ( ( ( A x. C ) e. CC /\ ( B x. ( sqrt ` D ) ) e. CC ) -> ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( A x. C ) ^ 2 ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B x. ( sqrt ` D ) ) ^ 2 ) ) )
37	35 21 36	syl2anc	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( A x. C ) ^ 2 ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B x. ( sqrt ` D ) ) ^ 2 ) ) )
38	4 7	sqmuld	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) ^ 2 ) = ( ( A ^ 2 ) x. ( C ^ 2 ) ) )
39	38	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) ^ 2 ) = ( ( A ^ 2 ) x. ( C ^ 2 ) ) )
40	39	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) ^ 2 ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) = ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) )
41	12 20	sqmuld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( sqrt ` D ) ) ^ 2 ) = ( ( B ^ 2 ) x. ( ( sqrt ` D ) ^ 2 ) ) )
42		simp3r	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> 0 <_ D )
43		resqrtth	|- ( ( D e. RR /\ 0 <_ D ) -> ( ( sqrt ` D ) ^ 2 ) = D )
44	18 42 43	syl2anc	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( sqrt ` D ) ^ 2 ) = D )
45	44	oveq2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B ^ 2 ) x. ( ( sqrt ` D ) ^ 2 ) ) = ( ( B ^ 2 ) x. D ) )
46	41 45	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( sqrt ` D ) ) ^ 2 ) = ( ( B ^ 2 ) x. D ) )
47	40 46	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A x. C ) ^ 2 ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B x. ( sqrt ` D ) ) ^ 2 ) ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) )
48	37 47	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) )
49	48	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ^ 2 ) / ( Q ^ 2 ) ) = ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) )
50	33 49	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) = ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) )
51	12 8	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. C ) e. CC )
52	5 20	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( sqrt ` D ) ) e. CC )
53	51 52	subcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) e. CC )
54	53 26 32	sqdivd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) = ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ^ 2 ) / ( Q ^ 2 ) ) )
55	27	recnd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> A e. CC )
56	55 20	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( sqrt ` D ) ) e. CC )
57		binom2sub	|- ( ( ( B x. C ) e. CC /\ ( A x. ( sqrt ` D ) ) e. CC ) -> ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( B x. C ) ^ 2 ) - ( 2 x. ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) ) ) + ( ( A x. ( sqrt ` D ) ) ^ 2 ) ) )
58	51 56 57	syl2anc	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( B x. C ) ^ 2 ) - ( 2 x. ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) ) ) + ( ( A x. ( sqrt ` D ) ) ^ 2 ) ) )
59	11 7	sqmuld	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B x. C ) ^ 2 ) = ( ( B ^ 2 ) x. ( C ^ 2 ) ) )
60	59	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) ^ 2 ) = ( ( B ^ 2 ) x. ( C ^ 2 ) ) )
61	12 8 55 20	mul4d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) = ( ( B x. A ) x. ( C x. ( sqrt ` D ) ) ) )
62	12 55	mulcomd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. A ) = ( A x. B ) )
63	62	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. A ) x. ( C x. ( sqrt ` D ) ) ) = ( ( A x. B ) x. ( C x. ( sqrt ` D ) ) ) )
64	55 12 8 20	mul4d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. B ) x. ( C x. ( sqrt ` D ) ) ) = ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) )
65	63 64	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. A ) x. ( C x. ( sqrt ` D ) ) ) = ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) )
66	61 65	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) = ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) )
67	66	oveq2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( 2 x. ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) ) = ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) )
68	60 67	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) ^ 2 ) - ( 2 x. ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) ) ) = ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) )
69	55 20	sqmuld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( sqrt ` D ) ) ^ 2 ) = ( ( A ^ 2 ) x. ( ( sqrt ` D ) ^ 2 ) ) )
70	44	oveq2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) x. ( ( sqrt ` D ) ^ 2 ) ) = ( ( A ^ 2 ) x. D ) )
71	69 70	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( sqrt ` D ) ) ^ 2 ) = ( ( A ^ 2 ) x. D ) )
72	68 71	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B x. C ) ^ 2 ) - ( 2 x. ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) ) ) + ( ( A x. ( sqrt ` D ) ) ^ 2 ) ) = ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) )
73	58 72	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) )
74	73	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ^ 2 ) / ( Q ^ 2 ) ) = ( ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) )
75	54 74	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) = ( ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) )
76	50 75	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) + ( ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) ) )
77	5	sqcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A ^ 2 ) e. CC )
78	8	sqcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( C ^ 2 ) e. CC )
79	77 78	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) x. ( C ^ 2 ) ) e. CC )
80		2cnd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> 2 e. CC )
81	9 21	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) e. CC )
82	80 81	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) e. CC )
83	79 82	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) e. CC )
84	12	sqcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B ^ 2 ) e. CC )
85	84 19	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B ^ 2 ) x. D ) e. CC )
86	83 85	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) e. CC )
87	84 78	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B ^ 2 ) x. ( C ^ 2 ) ) e. CC )
88	87 82	subcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) e. CC )
89	77 19	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) x. D ) e. CC )
90	88 89	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) e. CC )
91	26	sqcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Q ^ 2 ) e. CC )
92		2z	|- 2 e. ZZ
93	92	a1i	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> 2 e. ZZ )
94	26 32 93	expne0d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Q ^ 2 ) =/= 0 )
95	86 90 91 94	divdird	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) + ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) ) / ( Q ^ 2 ) ) = ( ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) + ( ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) ) )
96	83 85 88 89	add4d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) + ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) ) = ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) ) + ( ( ( B ^ 2 ) x. D ) + ( ( A ^ 2 ) x. D ) ) ) )
97	79 82 87	ppncand	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) ) = ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) )
98	55	sqcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A ^ 2 ) e. CC )
99	98 84 78	adddird	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( C ^ 2 ) ) = ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) )
100	1	eqcomi	|- ( ( A ^ 2 ) + ( B ^ 2 ) ) = Q
101	100	a1i	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = Q )
102	101	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( C ^ 2 ) ) = ( Q x. ( C ^ 2 ) ) )
103	97 99 102	3eqtr2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) ) = ( Q x. ( C ^ 2 ) ) )
104	84 98 19	adddird	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B ^ 2 ) + ( A ^ 2 ) ) x. D ) = ( ( ( B ^ 2 ) x. D ) + ( ( A ^ 2 ) x. D ) ) )
105	84 98	addcomd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
106	105 101	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = Q )
107	106	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B ^ 2 ) + ( A ^ 2 ) ) x. D ) = ( Q x. D ) )
108	104 107	eqtr3d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B ^ 2 ) x. D ) + ( ( A ^ 2 ) x. D ) ) = ( Q x. D ) )
109	103 108	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) ) + ( ( ( B ^ 2 ) x. D ) + ( ( A ^ 2 ) x. D ) ) ) = ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) )
110	96 109	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) + ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) ) = ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) )
111	110	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) + ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) ) / ( Q ^ 2 ) ) = ( ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) / ( Q ^ 2 ) ) )
112	26 78 19	adddid	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Q x. ( ( C ^ 2 ) + D ) ) = ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) )
113	112	eqcomd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) = ( Q x. ( ( C ^ 2 ) + D ) ) )
114	26	sqvald	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Q ^ 2 ) = ( Q x. Q ) )
115	113 114	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) / ( Q ^ 2 ) ) = ( ( Q x. ( ( C ^ 2 ) + D ) ) / ( Q x. Q ) ) )
116	78 19	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( C ^ 2 ) + D ) e. CC )
117	116 26 26 32 32	divcan5d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( Q x. ( ( C ^ 2 ) + D ) ) / ( Q x. Q ) ) = ( ( ( C ^ 2 ) + D ) / Q ) )
118	115 117	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) / ( Q ^ 2 ) ) = ( ( ( C ^ 2 ) + D ) / Q ) )
119	2	a1i	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) )
120	119	oveq2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( C ^ 2 ) + D ) = ( ( C ^ 2 ) + ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) ) )
121		rpcn	|- ( R e. RR+ -> R e. CC )
122	121	adantr	|- ( ( R e. RR+ /\ 0 <_ D ) -> R e. CC )
123	122	3ad2ant3	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> R e. CC )
124	123	sqcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( R ^ 2 ) e. CC )
125	124 26	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( R ^ 2 ) x. Q ) e. CC )
126	78 125	pncan3d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( C ^ 2 ) + ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) ) = ( ( R ^ 2 ) x. Q ) )
127	120 126	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( C ^ 2 ) + D ) = ( ( R ^ 2 ) x. Q ) )
128	116 124 26 32	divmul3d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( C ^ 2 ) + D ) / Q ) = ( R ^ 2 ) <-> ( ( C ^ 2 ) + D ) = ( ( R ^ 2 ) x. Q ) ) )
129	127 128	mpbird	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( C ^ 2 ) + D ) / Q ) = ( R ^ 2 ) )
130	118 129	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) / ( Q ^ 2 ) ) = ( R ^ 2 ) )
131	111 130	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) + ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) ) / ( Q ^ 2 ) ) = ( R ^ 2 ) )
132	76 95 131	3eqtr2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( R ^ 2 ) )
133	5 22 26 32	divassd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ) / Q ) = ( A x. ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) )
134	5 9 21	adddid	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ) = ( ( A x. ( A x. C ) ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) )
135	3	adantr	|- ( ( A e. RR /\ C e. RR ) -> A e. CC )
136	6	adantl	|- ( ( A e. RR /\ C e. RR ) -> C e. CC )
137	135 135 136	mulassd	|- ( ( A e. RR /\ C e. RR ) -> ( ( A x. A ) x. C ) = ( A x. ( A x. C ) ) )
138	135	sqvald	|- ( ( A e. RR /\ C e. RR ) -> ( A ^ 2 ) = ( A x. A ) )
139	138	eqcomd	|- ( ( A e. RR /\ C e. RR ) -> ( A x. A ) = ( A ^ 2 ) )
140	139	oveq1d	|- ( ( A e. RR /\ C e. RR ) -> ( ( A x. A ) x. C ) = ( ( A ^ 2 ) x. C ) )
141	137 140	eqtr3d	|- ( ( A e. RR /\ C e. RR ) -> ( A x. ( A x. C ) ) = ( ( A ^ 2 ) x. C ) )
142	141	3adant2	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( A x. C ) ) = ( ( A ^ 2 ) x. C ) )
143	142	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( A x. C ) ) = ( ( A ^ 2 ) x. C ) )
144	5 12 20	mulassd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. B ) x. ( sqrt ` D ) ) = ( A x. ( B x. ( sqrt ` D ) ) ) )
145	144	eqcomd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( B x. ( sqrt ` D ) ) ) = ( ( A x. B ) x. ( sqrt ` D ) ) )
146	143 145	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( A x. C ) ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) = ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) )
147	134 146	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ) = ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) )
148	147	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ) / Q ) = ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) )
149	133 148	eqtr3d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) = ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) )
150	12 53 26 32	divassd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) = ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) )
151	12 51 52	subdid	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) = ( ( B x. ( B x. C ) ) - ( B x. ( A x. ( sqrt ` D ) ) ) ) )
152		simpl	|- ( ( B e. RR /\ C e. RR ) -> B e. RR )
153	152	recnd	|- ( ( B e. RR /\ C e. RR ) -> B e. CC )
154		simpr	|- ( ( B e. RR /\ C e. RR ) -> C e. RR )
155	154	recnd	|- ( ( B e. RR /\ C e. RR ) -> C e. CC )
156	153 153 155	mulassd	|- ( ( B e. RR /\ C e. RR ) -> ( ( B x. B ) x. C ) = ( B x. ( B x. C ) ) )
157	10	sqvald	|- ( B e. RR -> ( B ^ 2 ) = ( B x. B ) )
158	157	eqcomd	|- ( B e. RR -> ( B x. B ) = ( B ^ 2 ) )
159	158	adantr	|- ( ( B e. RR /\ C e. RR ) -> ( B x. B ) = ( B ^ 2 ) )
160	159	oveq1d	|- ( ( B e. RR /\ C e. RR ) -> ( ( B x. B ) x. C ) = ( ( B ^ 2 ) x. C ) )
161	156 160	eqtr3d	|- ( ( B e. RR /\ C e. RR ) -> ( B x. ( B x. C ) ) = ( ( B ^ 2 ) x. C ) )
162	161	3adant1	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B x. ( B x. C ) ) = ( ( B ^ 2 ) x. C ) )
163	162	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( B x. C ) ) = ( ( B ^ 2 ) x. C ) )
164	12 5 20	mulassd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. A ) x. ( sqrt ` D ) ) = ( B x. ( A x. ( sqrt ` D ) ) ) )
165	11 4	mulcomd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B x. A ) = ( A x. B ) )
166	165	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. A ) = ( A x. B ) )
167	166	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. A ) x. ( sqrt ` D ) ) = ( ( A x. B ) x. ( sqrt ` D ) ) )
168	164 167	eqtr3d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( A x. ( sqrt ` D ) ) ) = ( ( A x. B ) x. ( sqrt ` D ) ) )
169	163 168	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( B x. C ) ) - ( B x. ( A x. ( sqrt ` D ) ) ) ) = ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) )
170	151 169	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) = ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) )
171	170	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) = ( ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) )
172	150 171	eqtr3d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) = ( ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) )
173	149 172	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = ( ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) + ( ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) ) )
174	77 8	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) x. C ) e. CC )
175	5 12	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. B ) e. CC )
176	175 20	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. B ) x. ( sqrt ` D ) ) e. CC )
177	174 176	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) e. CC )
178	84 8	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B ^ 2 ) x. C ) e. CC )
179	178 176	subcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) e. CC )
180	177 179 26 32	divdird	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) ) / Q ) = ( ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) + ( ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) ) )
181	174 176 178	ppncand	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) ) = ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) )
182	77 84 8	adddird	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. C ) = ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) )
183	1	a1i	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
184	183	eqcomd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = Q )
185	184	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. C ) = ( Q x. C ) )
186	181 182 185	3eqtr2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) ) = ( Q x. C ) )
187	177 179	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) ) e. CC )
188	187 8 26 32	divmul2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) ) / Q ) = C <-> ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) ) = ( Q x. C ) ) )
189	186 188	mpbird	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) ) / Q ) = C )
190	173 180 189	3eqtr2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C )
191	132 190	jca	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C ) )
192		oveq1	|- ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) -> ( X ^ 2 ) = ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) )
193		oveq1	|- ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) -> ( Y ^ 2 ) = ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) )
194	192 193	oveqan12d	|- ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) )
195	194	eqeq1d	|- ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) <-> ( ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( R ^ 2 ) ) )
196		oveq2	|- ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) -> ( A x. X ) = ( A x. ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) )
197		oveq2	|- ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) -> ( B x. Y ) = ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) )
198	196 197	oveqan12d	|- ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( A x. X ) + ( B x. Y ) ) = ( ( A x. ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
199	198	eqeq1d	|- ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C <-> ( ( A x. ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C ) )
200	195 199	anbi12d	|- ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) <-> ( ( ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C ) ) )
201	191 200	syl5ibrcom	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) ) )
202	35 21	subcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) e. CC )
203	202 26 32	sqdivd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) = ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ^ 2 ) / ( Q ^ 2 ) ) )
204		binom2sub	|- ( ( ( A x. C ) e. CC /\ ( B x. ( sqrt ` D ) ) e. CC ) -> ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B x. ( sqrt ` D ) ) ^ 2 ) ) )
205	35 21 204	syl2anc	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B x. ( sqrt ` D ) ) ^ 2 ) ) )
206	39	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) = ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) )
207	206 46	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A x. C ) ^ 2 ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B x. ( sqrt ` D ) ) ^ 2 ) ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) )
208	205 207	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) )
209	208	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ^ 2 ) / ( Q ^ 2 ) ) = ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) )
210	203 209	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) = ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) )
211	51 56	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) e. CC )
212	211 26 32	sqdivd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) = ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ^ 2 ) / ( Q ^ 2 ) ) )
213		binom2	|- ( ( ( B x. C ) e. CC /\ ( A x. ( sqrt ` D ) ) e. CC ) -> ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( B x. C ) ^ 2 ) + ( 2 x. ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) ) ) + ( ( A x. ( sqrt ` D ) ) ^ 2 ) ) )
214	51 56 213	syl2anc	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( B x. C ) ^ 2 ) + ( 2 x. ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) ) ) + ( ( A x. ( sqrt ` D ) ) ^ 2 ) ) )
215	60 67	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) ^ 2 ) + ( 2 x. ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) ) ) = ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) )
216	215 71	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B x. C ) ^ 2 ) + ( 2 x. ( ( B x. C ) x. ( A x. ( sqrt ` D ) ) ) ) ) + ( ( A x. ( sqrt ` D ) ) ^ 2 ) ) = ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) )
217	214 216	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ^ 2 ) = ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) )
218	217	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ^ 2 ) / ( Q ^ 2 ) ) = ( ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) )
219	212 218	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) = ( ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) )
220	210 219	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) + ( ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) ) )
221	98 78	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) x. ( C ^ 2 ) ) e. CC )
222	35 21	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) e. CC )
223	80 222	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) e. CC )
224	221 223	subcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) e. CC )
225	224 85	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) e. CC )
226	87 223	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) e. CC )
227	98 19	mulcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) x. D ) e. CC )
228	226 227	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) e. CC )
229	225 228 91 94	divdird	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) + ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) ) / ( Q ^ 2 ) ) = ( ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) + ( ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) / ( Q ^ 2 ) ) ) )
230	224 85 226 227	add4d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) + ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) ) = ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) ) + ( ( ( B ^ 2 ) x. D ) + ( ( A ^ 2 ) x. D ) ) ) )
231	221 223 87	nppcan3d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) ) = ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) + ( ( B ^ 2 ) x. ( C ^ 2 ) ) ) )
232	231 99 102	3eqtr2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) ) = ( Q x. ( C ^ 2 ) ) )
233	232 108	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) ) + ( ( ( B ^ 2 ) x. D ) + ( ( A ^ 2 ) x. D ) ) ) = ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) )
234	230 233	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) + ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) ) = ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) )
235	234	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( ( A ^ 2 ) x. ( C ^ 2 ) ) - ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( B ^ 2 ) x. D ) ) + ( ( ( ( B ^ 2 ) x. ( C ^ 2 ) ) + ( 2 x. ( ( A x. C ) x. ( B x. ( sqrt ` D ) ) ) ) ) + ( ( A ^ 2 ) x. D ) ) ) / ( Q ^ 2 ) ) = ( ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) / ( Q ^ 2 ) ) )
236	220 229 235	3eqtr2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( ( ( Q x. ( C ^ 2 ) ) + ( Q x. D ) ) / ( Q ^ 2 ) ) )
237	236 130	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( R ^ 2 ) )
238		simp1	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
239		simp3	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
240	238 239	remulcld	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
241	240	recnd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. C ) e. CC )
242	241	3ad2ant1	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. C ) e. CC )
243	242 21	subcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) e. CC )
244	5 243 26 32	divassd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ) / Q ) = ( A x. ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) )
245	5 242 21	subdid	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ) = ( ( A x. ( A x. C ) ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) )
246	143 145	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( A x. C ) ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) = ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) )
247	245 246	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ) = ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) )
248	247	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ) / Q ) = ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) )
249	244 248	eqtr3d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) = ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) )
250	51 52	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) e. CC )
251	12 250 26 32	divassd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) = ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) )
252	12 51 52	adddid	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) = ( ( B x. ( B x. C ) ) + ( B x. ( A x. ( sqrt ` D ) ) ) ) )
253	163 168	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( B x. C ) ) + ( B x. ( A x. ( sqrt ` D ) ) ) ) = ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) )
254	252 253	eqtrd	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) = ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) )
255	254	oveq1d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) = ( ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) )
256	251 255	eqtr3d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) = ( ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) )
257	249 256	oveq12d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = ( ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) + ( ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) ) )
258	174 176	subcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) e. CC )
259	178 176	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) e. CC )
260	258 259 26 32	divdird	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) ) / Q ) = ( ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) + ( ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) / Q ) ) )
261	174 176 178	nppcan3d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) ) = ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) )
262	261 182 185	3eqtr2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) ) = ( Q x. C ) )
263	258 259	addcld	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) ) e. CC )
264	263 8 26 32	divmul2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) ) / Q ) = C <-> ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) ) = ( Q x. C ) ) )
265	262 264	mpbird	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( A ^ 2 ) x. C ) - ( ( A x. B ) x. ( sqrt ` D ) ) ) + ( ( ( B ^ 2 ) x. C ) + ( ( A x. B ) x. ( sqrt ` D ) ) ) ) / Q ) = C )
266	257 260 265	3eqtr2d	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C )
267	237 266	jca	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C ) )
268		oveq1	|- ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) -> ( X ^ 2 ) = ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) )
269		oveq1	|- ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) -> ( Y ^ 2 ) = ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) )
270	268 269	oveqan12d	|- ( ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) )
271	270	eqeq1d	|- ( ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) <-> ( ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( R ^ 2 ) ) )
272		oveq2	|- ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) -> ( A x. X ) = ( A x. ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) )
273		oveq2	|- ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) -> ( B x. Y ) = ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) )
274	272 273	oveqan12d	|- ( ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( A x. X ) + ( B x. Y ) ) = ( ( A x. ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
275	274	eqeq1d	|- ( ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C <-> ( ( A x. ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C ) )
276	271 275	anbi12d	|- ( ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) <-> ( ( ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) + ( ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C ) ) )
277	267 276	syl5ibrcom	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) ) )
278	201 277	jaod	|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) ) )