Metamath Proof Explorer

Theorem itsclc0lem3

Description: Lemma for theorems about intersections of lines and circles in a real Euclidean space of dimension 2 . (Contributed by AV, 2-May-2023)

		Ref	Expression
	Hypotheses	itsclc0lem3.q	\|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
		itsclc0lem3.d	\|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
	Assertion	itsclc0lem3	\|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> D e. RR )

Proof

Step	Hyp	Ref	Expression
1		itsclc0lem3.q	\|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
2		itsclc0lem3.d	\|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
3		simpr	\|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> R e. RR )
4	3	resqcld	\|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> ( R ^ 2 ) e. RR )
5	1	resum2sqcl	\|- ( ( A e. RR /\ B e. RR ) -> Q e. RR )
6	5	3adant3	\|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> Q e. RR )
7	6	adantr	\|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> Q e. RR )
8	4 7	remulcld	\|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> ( ( R ^ 2 ) x. Q ) e. RR )
9		simpl3	\|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> C e. RR )
10	9	resqcld	\|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> ( C ^ 2 ) e. RR )
11	8 10	resubcld	\|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) e. RR )
12	2 11	eqeltrid	\|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> D e. RR )