Metamath Proof Explorer


Theorem itschlc0xyqsol

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a horizontal line and a circle. (Contributed by AV, 8-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q โŠข ๐‘„ = ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) )
itsclc0yqsol.d โŠข ๐ท = ( ( ( ๐‘… โ†‘ 2 ) ยท ๐‘„ ) โˆ’ ( ๐ถ โ†‘ 2 ) )
Assertion itschlc0xyqsol ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ( ( ๐‘‹ โ†‘ 2 ) + ( ๐‘Œ โ†‘ 2 ) ) = ( ๐‘… โ†‘ 2 ) โˆง ( ( ๐ด ยท ๐‘‹ ) + ( ๐ต ยท ๐‘Œ ) ) = ๐ถ ) โ†’ ( ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) โˆจ ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q โŠข ๐‘„ = ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) )
2 itsclc0yqsol.d โŠข ๐ท = ( ( ( ๐‘… โ†‘ 2 ) ยท ๐‘„ ) โˆ’ ( ๐ถ โ†‘ 2 ) )
3 1 2 itschlc0xyqsol1 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ( ( ๐‘‹ โ†‘ 2 ) + ( ๐‘Œ โ†‘ 2 ) ) = ( ๐‘… โ†‘ 2 ) โˆง ( ( ๐ด ยท ๐‘‹ ) + ( ๐ต ยท ๐‘Œ ) ) = ๐ถ ) โ†’ ( ๐‘Œ = ( ๐ถ / ๐ต ) โˆง ( ๐‘‹ = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โˆจ ๐‘‹ = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) ) ) ) )
4 orcom โŠข ( ( ๐‘‹ = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โˆจ ๐‘‹ = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) ) โ†” ( ๐‘‹ = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โˆจ ๐‘‹ = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) ) )
5 oveq1 โŠข ( ๐ด = 0 โ†’ ( ๐ด ยท ๐ถ ) = ( 0 ยท ๐ถ ) )
6 5 ad2antrl โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โ†’ ( ๐ด ยท ๐ถ ) = ( 0 ยท ๐ถ ) )
7 6 adantr โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ๐ด ยท ๐ถ ) = ( 0 ยท ๐ถ ) )
8 simpll3 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ๐ถ โˆˆ โ„ )
9 8 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ๐ถ โˆˆ โ„‚ )
10 9 mul02d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( 0 ยท ๐ถ ) = 0 )
11 7 10 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ๐ด ยท ๐ถ ) = 0 )
12 11 oveq1d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) = ( 0 + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) )
13 simpll2 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ๐ต โˆˆ โ„ )
14 13 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ๐ต โˆˆ โ„‚ )
15 rpre โŠข ( ๐‘… โˆˆ โ„+ โ†’ ๐‘… โˆˆ โ„ )
16 15 adantr โŠข ( ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โ†’ ๐‘… โˆˆ โ„ )
17 16 recnd โŠข ( ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โ†’ ๐‘… โˆˆ โ„‚ )
18 17 adantl โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ๐‘… โˆˆ โ„‚ )
19 18 sqcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ๐‘… โ†‘ 2 ) โˆˆ โ„‚ )
20 1 resum2sqcl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ๐‘„ โˆˆ โ„ )
21 20 recnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ๐‘„ โˆˆ โ„‚ )
22 21 3adant3 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โ†’ ๐‘„ โˆˆ โ„‚ )
23 22 adantr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โ†’ ๐‘„ โˆˆ โ„‚ )
24 23 adantr โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ๐‘„ โˆˆ โ„‚ )
25 19 24 mulcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐‘… โ†‘ 2 ) ยท ๐‘„ ) โˆˆ โ„‚ )
26 9 sqcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ๐ถ โ†‘ 2 ) โˆˆ โ„‚ )
27 25 26 subcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ( ๐‘… โ†‘ 2 ) ยท ๐‘„ ) โˆ’ ( ๐ถ โ†‘ 2 ) ) โˆˆ โ„‚ )
28 2 27 eqeltrid โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ๐ท โˆˆ โ„‚ )
29 28 sqrtcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( โˆš โ€˜ ๐ท ) โˆˆ โ„‚ )
30 14 29 mulcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) โˆˆ โ„‚ )
31 30 addlidd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( 0 + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) )
32 12 31 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) )
33 32 oveq1d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) / ๐‘„ ) )
34 sq0i โŠข ( ๐ด = 0 โ†’ ( ๐ด โ†‘ 2 ) = 0 )
35 34 ad2antrl โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โ†’ ( ๐ด โ†‘ 2 ) = 0 )
36 35 oveq1d โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( 0 + ( ๐ต โ†‘ 2 ) ) )
37 simp2 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โ†’ ๐ต โˆˆ โ„ )
38 37 recnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โ†’ ๐ต โˆˆ โ„‚ )
39 38 sqcld โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ๐ต โ†‘ 2 ) โˆˆ โ„‚ )
40 39 addlidd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( 0 + ( ๐ต โ†‘ 2 ) ) = ( ๐ต โ†‘ 2 ) )
41 38 sqvald โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ๐ต โ†‘ 2 ) = ( ๐ต ยท ๐ต ) )
42 40 41 eqtrd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( 0 + ( ๐ต โ†‘ 2 ) ) = ( ๐ต ยท ๐ต ) )
43 42 adantr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โ†’ ( 0 + ( ๐ต โ†‘ 2 ) ) = ( ๐ต ยท ๐ต ) )
44 36 43 eqtrd โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ต ยท ๐ต ) )
45 1 44 eqtrid โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โ†’ ๐‘„ = ( ๐ต ยท ๐ต ) )
46 45 adantr โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ๐‘„ = ( ๐ต ยท ๐ต ) )
47 46 oveq2d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) / ๐‘„ ) = ( ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) / ( ๐ต ยท ๐ต ) ) )
48 simplrr โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ๐ต โ‰  0 )
49 29 14 14 48 48 divcan5d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) / ( ๐ต ยท ๐ต ) ) = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) )
50 47 49 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) / ๐‘„ ) = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) )
51 33 50 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) )
52 51 3adant3 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) )
53 52 adantr โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) )
54 53 eqcomd โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ( โˆš โ€˜ ๐ท ) / ๐ต ) = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) )
55 54 eqeq2d โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ๐‘‹ = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โ†” ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
56 55 biimpd โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ๐‘‹ = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โ†’ ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
57 oveq1 โŠข ( ๐ด = 0 โ†’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = ( 0 ยท ( โˆš โ€˜ ๐ท ) ) )
58 57 ad2antrl โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โ†’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = ( 0 ยท ( โˆš โ€˜ ๐ท ) ) )
59 58 adantr โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = ( 0 ยท ( โˆš โ€˜ ๐ท ) ) )
60 29 mul02d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( 0 ยท ( โˆš โ€˜ ๐ท ) ) = 0 )
61 59 60 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = 0 )
62 61 oveq2d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) โˆ’ 0 ) )
63 14 9 mulcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ๐ต ยท ๐ถ ) โˆˆ โ„‚ )
64 63 subid1d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ต ยท ๐ถ ) โˆ’ 0 ) = ( ๐ต ยท ๐ถ ) )
65 62 64 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ๐ต ยท ๐ถ ) )
66 65 46 oveq12d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( ๐ต ยท ๐ถ ) / ( ๐ต ยท ๐ต ) ) )
67 66 3adant3 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( ๐ต ยท ๐ถ ) / ( ๐ต ยท ๐ต ) ) )
68 9 3adant3 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐ถ โˆˆ โ„‚ )
69 14 3adant3 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐ต โˆˆ โ„‚ )
70 simp1rr โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐ต โ‰  0 )
71 68 69 69 70 70 divcan5d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ๐ต ยท ๐ถ ) / ( ๐ต ยท ๐ต ) ) = ( ๐ถ / ๐ต ) )
72 67 71 eqtr2d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ๐ถ / ๐ต ) = ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) )
73 72 eqeq2d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ๐‘Œ = ( ๐ถ / ๐ต ) โ†” ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
74 73 biimpa โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) )
75 56 74 jctird โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ๐‘‹ = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โ†’ ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) ) )
76 14 29 mulneg2d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ๐ต ยท - ( โˆš โ€˜ ๐ท ) ) = - ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) )
77 76 eqcomd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ - ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) = ( ๐ต ยท - ( โˆš โ€˜ ๐ท ) ) )
78 77 46 oveq12d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( - ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) / ๐‘„ ) = ( ( ๐ต ยท - ( โˆš โ€˜ ๐ท ) ) / ( ๐ต ยท ๐ต ) ) )
79 29 negcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ - ( โˆš โ€˜ ๐ท ) โˆˆ โ„‚ )
80 79 14 14 48 48 divcan5d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ต ยท - ( โˆš โ€˜ ๐ท ) ) / ( ๐ต ยท ๐ต ) ) = ( - ( โˆš โ€˜ ๐ท ) / ๐ต ) )
81 78 80 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( - ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) / ๐‘„ ) = ( - ( โˆš โ€˜ ๐ท ) / ๐ต ) )
82 11 oveq1d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) = ( 0 โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) )
83 df-neg โŠข - ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) = ( 0 โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) )
84 82 83 eqtr4di โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) = - ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) )
85 84 oveq1d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( - ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) / ๐‘„ ) )
86 29 14 48 divnegd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) = ( - ( โˆš โ€˜ ๐ท ) / ๐ต ) )
87 81 85 86 3eqtr4d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) )
88 87 3adant3 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) )
89 88 adantr โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) )
90 89 eqcomd โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) )
91 90 eqeq2d โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ๐‘‹ = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โ†” ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
92 91 biimpd โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ๐‘‹ = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โ†’ ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
93 58 3ad2ant1 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = ( 0 ยท ( โˆš โ€˜ ๐ท ) ) )
94 17 3ad2ant2 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐‘… โˆˆ โ„‚ )
95 94 sqcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ๐‘… โ†‘ 2 ) โˆˆ โ„‚ )
96 23 3ad2ant1 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐‘„ โˆˆ โ„‚ )
97 95 96 mulcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ๐‘… โ†‘ 2 ) ยท ๐‘„ ) โˆˆ โ„‚ )
98 simp1l3 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐ถ โˆˆ โ„ )
99 98 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐ถ โˆˆ โ„‚ )
100 99 sqcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ๐ถ โ†‘ 2 ) โˆˆ โ„‚ )
101 97 100 subcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ( ๐‘… โ†‘ 2 ) ยท ๐‘„ ) โˆ’ ( ๐ถ โ†‘ 2 ) ) โˆˆ โ„‚ )
102 2 101 eqeltrid โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐ท โˆˆ โ„‚ )
103 102 sqrtcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( โˆš โ€˜ ๐ท ) โˆˆ โ„‚ )
104 103 mul02d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( 0 ยท ( โˆš โ€˜ ๐ท ) ) = 0 )
105 93 104 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = 0 )
106 105 oveq2d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + 0 ) )
107 simp1l2 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐ต โˆˆ โ„ )
108 107 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐ต โˆˆ โ„‚ )
109 108 99 mulcld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ๐ต ยท ๐ถ ) โˆˆ โ„‚ )
110 109 addridd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ๐ต ยท ๐ถ ) + 0 ) = ( ๐ต ยท ๐ถ ) )
111 106 110 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ๐ต ยท ๐ถ ) )
112 45 3ad2ant1 โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ๐‘„ = ( ๐ต ยท ๐ต ) )
113 111 112 oveq12d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( ๐ต ยท ๐ถ ) / ( ๐ต ยท ๐ต ) ) )
114 99 108 108 70 70 divcan5d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ๐ต ยท ๐ถ ) / ( ๐ต ยท ๐ต ) ) = ( ๐ถ / ๐ต ) )
115 113 114 eqtr2d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ๐ถ / ๐ต ) = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) )
116 115 eqeq2d โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ๐‘Œ = ( ๐ถ / ๐ต ) โ†” ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
117 116 biimpa โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) )
118 92 117 jctird โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ๐‘‹ = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โ†’ ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) ) )
119 75 118 orim12d โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ( ๐‘‹ = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โˆจ ๐‘‹ = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) ) โ†’ ( ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) โˆจ ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) ) ) )
120 4 119 biimtrid โŠข ( ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โˆง ๐‘Œ = ( ๐ถ / ๐ต ) ) โ†’ ( ( ๐‘‹ = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โˆจ ๐‘‹ = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) ) โ†’ ( ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) โˆจ ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) ) ) )
121 120 expimpd โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ๐‘Œ = ( ๐ถ / ๐ต ) โˆง ( ๐‘‹ = - ( ( โˆš โ€˜ ๐ท ) / ๐ต ) โˆจ ๐‘‹ = ( ( โˆš โ€˜ ๐ท ) / ๐ต ) ) ) โ†’ ( ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) โˆจ ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) ) ) )
122 3 121 syld โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ด = 0 โˆง ๐ต โ‰  0 ) ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ ) ) โ†’ ( ( ( ( ๐‘‹ โ†‘ 2 ) + ( ๐‘Œ โ†‘ 2 ) ) = ( ๐‘… โ†‘ 2 ) โˆง ( ( ๐ด ยท ๐‘‹ ) + ( ๐ต ยท ๐‘Œ ) ) = ๐ถ ) โ†’ ( ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) โˆจ ( ๐‘‹ = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆง ๐‘Œ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) ) ) )