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 ( ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โˆง ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) โˆง ( ๐‘Š โˆˆ โ„ โˆง ๐‘Š โ‰  0 ) ) โ†’ ( ( ( ๐‘† ยท ๐‘ˆ ) + ( ๐‘‡ ยท ( โˆš โ€˜ ๐‘‰ ) ) ) / ๐‘Š ) โˆˆ โ„ )

Proof

Step Hyp Ref Expression
1 remulcl โŠข ( ( ๐‘† โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โ†’ ( ๐‘† ยท ๐‘ˆ ) โˆˆ โ„ )
2 1 3adant2 โŠข ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โ†’ ( ๐‘† ยท ๐‘ˆ ) โˆˆ โ„ )
3 2 adantr โŠข ( ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โˆง ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) ) โ†’ ( ๐‘† ยท ๐‘ˆ ) โˆˆ โ„ )
4 simpl2 โŠข ( ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โˆง ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) ) โ†’ ๐‘‡ โˆˆ โ„ )
5 resqrtcl โŠข ( ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) โ†’ ( โˆš โ€˜ ๐‘‰ ) โˆˆ โ„ )
6 5 adantl โŠข ( ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โˆง ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) ) โ†’ ( โˆš โ€˜ ๐‘‰ ) โˆˆ โ„ )
7 4 6 remulcld โŠข ( ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โˆง ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) ) โ†’ ( ๐‘‡ ยท ( โˆš โ€˜ ๐‘‰ ) ) โˆˆ โ„ )
8 3 7 readdcld โŠข ( ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โˆง ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) ) โ†’ ( ( ๐‘† ยท ๐‘ˆ ) + ( ๐‘‡ ยท ( โˆš โ€˜ ๐‘‰ ) ) ) โˆˆ โ„ )
9 8 3adant3 โŠข ( ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โˆง ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) โˆง ( ๐‘Š โˆˆ โ„ โˆง ๐‘Š โ‰  0 ) ) โ†’ ( ( ๐‘† ยท ๐‘ˆ ) + ( ๐‘‡ ยท ( โˆš โ€˜ ๐‘‰ ) ) ) โˆˆ โ„ )
10 simp3l โŠข ( ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โˆง ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) โˆง ( ๐‘Š โˆˆ โ„ โˆง ๐‘Š โ‰  0 ) ) โ†’ ๐‘Š โˆˆ โ„ )
11 simp3r โŠข ( ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โˆง ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) โˆง ( ๐‘Š โˆˆ โ„ โˆง ๐‘Š โ‰  0 ) ) โ†’ ๐‘Š โ‰  0 )
12 9 10 11 redivcld โŠข ( ( ( ๐‘† โˆˆ โ„ โˆง ๐‘‡ โˆˆ โ„ โˆง ๐‘ˆ โˆˆ โ„ ) โˆง ( ๐‘‰ โˆˆ โ„ โˆง 0 โ‰ค ๐‘‰ ) โˆง ( ๐‘Š โˆˆ โ„ โˆง ๐‘Š โ‰  0 ) ) โ†’ ( ( ( ๐‘† ยท ๐‘ˆ ) + ( ๐‘‡ ยท ( โˆš โ€˜ ๐‘‰ ) ) ) / ๐‘Š ) โˆˆ โ„ )