Metamath Proof Explorer


Theorem itsclc0lem1

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
Assertion itsclc0lem1 S T U V 0 V W W 0 S U + T V W

Proof

Step Hyp Ref Expression
1 remulcl S U S U
2 1 3adant2 S T U S U
3 2 adantr S T U V 0 V S U
4 simpl2 S T U V 0 V T
5 resqrtcl V 0 V V
6 5 adantl S T U V 0 V V
7 4 6 remulcld S T U V 0 V T V
8 3 7 readdcld S T U V 0 V S U + T V
9 8 3adant3 S T U V 0 V W W 0 S U + T V
10 simp3l S T U V 0 V W W 0 W
11 simp3r S T U V 0 V W W 0 W 0
12 9 10 11 redivcld S T U V 0 V W W 0 S U + T V W