Metamath Proof Explorer


Theorem inlinecirc02plem

Description: Lemma for inlinecirc02p . (Contributed by AV, 7-May-2023) (Revised by AV, 15-May-2023)

Ref Expression
Hypotheses inlinecirc02p.i โŠข ๐ผ = { 1 , 2 }
inlinecirc02p.e โŠข ๐ธ = ( โ„^ โ€˜ ๐ผ )
inlinecirc02p.p โŠข ๐‘ƒ = ( โ„ โ†‘m ๐ผ )
inlinecirc02p.s โŠข ๐‘† = ( Sphere โ€˜ ๐ธ )
inlinecirc02p.0 โŠข 0 = ( ๐ผ ร— { 0 } )
inlinecirc02p.l โŠข ๐ฟ = ( LineM โ€˜ ๐ธ )
inlinecirc02plem.q โŠข ๐‘„ = ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) )
inlinecirc02plem.d โŠข ๐ท = ( ( ( ๐‘… โ†‘ 2 ) ยท ๐‘„ ) โˆ’ ( ๐ถ โ†‘ 2 ) )
inlinecirc02plem.a โŠข ๐ด = ( ( ๐‘‹ โ€˜ 2 ) โˆ’ ( ๐‘Œ โ€˜ 2 ) )
inlinecirc02plem.b โŠข ๐ต = ( ( ๐‘Œ โ€˜ 1 ) โˆ’ ( ๐‘‹ โ€˜ 1 ) )
inlinecirc02plem.c โŠข ๐ถ = ( ( ( ๐‘‹ โ€˜ 2 ) ยท ( ๐‘Œ โ€˜ 1 ) ) โˆ’ ( ( ๐‘‹ โ€˜ 1 ) ยท ( ๐‘Œ โ€˜ 2 ) ) )
Assertion inlinecirc02plem ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ โˆƒ ๐‘Ž โˆˆ ๐‘ƒ โˆƒ ๐‘ โˆˆ ๐‘ƒ ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { ๐‘Ž , ๐‘ } โˆง ๐‘Ž โ‰  ๐‘ ) )

Proof

Step Hyp Ref Expression
1 inlinecirc02p.i โŠข ๐ผ = { 1 , 2 }
2 inlinecirc02p.e โŠข ๐ธ = ( โ„^ โ€˜ ๐ผ )
3 inlinecirc02p.p โŠข ๐‘ƒ = ( โ„ โ†‘m ๐ผ )
4 inlinecirc02p.s โŠข ๐‘† = ( Sphere โ€˜ ๐ธ )
5 inlinecirc02p.0 โŠข 0 = ( ๐ผ ร— { 0 } )
6 inlinecirc02p.l โŠข ๐ฟ = ( LineM โ€˜ ๐ธ )
7 inlinecirc02plem.q โŠข ๐‘„ = ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) )
8 inlinecirc02plem.d โŠข ๐ท = ( ( ( ๐‘… โ†‘ 2 ) ยท ๐‘„ ) โˆ’ ( ๐ถ โ†‘ 2 ) )
9 inlinecirc02plem.a โŠข ๐ด = ( ( ๐‘‹ โ€˜ 2 ) โˆ’ ( ๐‘Œ โ€˜ 2 ) )
10 inlinecirc02plem.b โŠข ๐ต = ( ( ๐‘Œ โ€˜ 1 ) โˆ’ ( ๐‘‹ โ€˜ 1 ) )
11 inlinecirc02plem.c โŠข ๐ถ = ( ( ( ๐‘‹ โ€˜ 2 ) ยท ( ๐‘Œ โ€˜ 1 ) ) โˆ’ ( ( ๐‘‹ โ€˜ 1 ) ยท ( ๐‘Œ โ€˜ 2 ) ) )
12 simprr โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ 0 < ๐ท )
13 12 gt0ne0d โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐ท โ‰  0 )
14 1 3 rrx2pyel โŠข ( ๐‘‹ โˆˆ ๐‘ƒ โ†’ ( ๐‘‹ โ€˜ 2 ) โˆˆ โ„ )
15 14 adantr โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ๐‘‹ โ€˜ 2 ) โˆˆ โ„ )
16 1 3 rrx2pyel โŠข ( ๐‘Œ โˆˆ ๐‘ƒ โ†’ ( ๐‘Œ โ€˜ 2 ) โˆˆ โ„ )
17 16 adantl โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ๐‘Œ โ€˜ 2 ) โˆˆ โ„ )
18 15 17 resubcld โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ( ๐‘‹ โ€˜ 2 ) โˆ’ ( ๐‘Œ โ€˜ 2 ) ) โˆˆ โ„ )
19 9 18 eqeltrid โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ๐ด โˆˆ โ„ )
20 19 3adant3 โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ ๐ด โˆˆ โ„ )
21 20 adantr โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐ด โˆˆ โ„ )
22 1 3 rrx2pxel โŠข ( ๐‘Œ โˆˆ ๐‘ƒ โ†’ ( ๐‘Œ โ€˜ 1 ) โˆˆ โ„ )
23 22 adantl โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ๐‘Œ โ€˜ 1 ) โˆˆ โ„ )
24 1 3 rrx2pxel โŠข ( ๐‘‹ โˆˆ ๐‘ƒ โ†’ ( ๐‘‹ โ€˜ 1 ) โˆˆ โ„ )
25 24 adantr โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ๐‘‹ โ€˜ 1 ) โˆˆ โ„ )
26 23 25 resubcld โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ( ๐‘Œ โ€˜ 1 ) โˆ’ ( ๐‘‹ โ€˜ 1 ) ) โˆˆ โ„ )
27 10 26 eqeltrid โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ๐ต โˆˆ โ„ )
28 27 3adant3 โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ ๐ต โˆˆ โ„ )
29 28 adantr โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐ต โˆˆ โ„ )
30 15 23 remulcld โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ( ๐‘‹ โ€˜ 2 ) ยท ( ๐‘Œ โ€˜ 1 ) ) โˆˆ โ„ )
31 25 17 remulcld โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ( ๐‘‹ โ€˜ 1 ) ยท ( ๐‘Œ โ€˜ 2 ) ) โˆˆ โ„ )
32 30 31 resubcld โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ( ( ๐‘‹ โ€˜ 2 ) ยท ( ๐‘Œ โ€˜ 1 ) ) โˆ’ ( ( ๐‘‹ โ€˜ 1 ) ยท ( ๐‘Œ โ€˜ 2 ) ) ) โˆˆ โ„ )
33 11 32 eqeltrid โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ๐ถ โˆˆ โ„ )
34 33 3adant3 โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ ๐ถ โˆˆ โ„ )
35 34 adantr โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐ถ โˆˆ โ„ )
36 19 27 33 3jca โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) )
37 36 3adant3 โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) )
38 rpre โŠข ( ๐‘… โˆˆ โ„+ โ†’ ๐‘… โˆˆ โ„ )
39 38 adantr โŠข ( ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) โ†’ ๐‘… โˆˆ โ„ )
40 7 8 itsclc0lem3 โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐‘… โˆˆ โ„ ) โ†’ ๐ท โˆˆ โ„ )
41 37 39 40 syl2an โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐ท โˆˆ โ„ )
42 41 12 elrpd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐ท โˆˆ โ„+ )
43 42 rprege0d โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ๐ท โˆˆ โ„ โˆง 0 โ‰ค ๐ท ) )
44 7 resum2sqcl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ๐‘„ โˆˆ โ„ )
45 19 27 44 syl2anc โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ๐‘„ โˆˆ โ„ )
46 45 3adant3 โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ ๐‘„ โˆˆ โ„ )
47 1 3 10 9 rrx2pnedifcoorneorr โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ ( ๐ต โ‰  0 โˆจ ๐ด โ‰  0 ) )
48 47 orcomd โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ ( ๐ด โ‰  0 โˆจ ๐ต โ‰  0 ) )
49 7 resum2sqorgt0 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ( ๐ด โ‰  0 โˆจ ๐ต โ‰  0 ) ) โ†’ 0 < ๐‘„ )
50 20 28 48 49 syl3anc โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ 0 < ๐‘„ )
51 50 gt0ne0d โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ ๐‘„ โ‰  0 )
52 46 51 jca โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ ( ๐‘„ โˆˆ โ„ โˆง ๐‘„ โ‰  0 ) )
53 52 adantr โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ๐‘„ โˆˆ โ„ โˆง ๐‘„ โ‰  0 ) )
54 itsclc0lem1 โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ท โˆˆ โ„ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘„ โˆˆ โ„ โˆง ๐‘„ โ‰  0 ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ )
55 21 29 35 43 53 54 syl311anc โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ )
56 itsclc0lem2 โŠข ( ( ( ๐ต โˆˆ โ„ โˆง ๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ท โˆˆ โ„ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘„ โˆˆ โ„ โˆง ๐‘„ โ‰  0 ) ) โ†’ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ )
57 29 21 35 43 53 56 syl311anc โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ )
58 55 57 jca โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ โˆง ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ ) )
59 58 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ โˆง ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ ) )
60 1 3 prelrrx2 โŠข ( ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ โˆง ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ ) โ†’ { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โˆˆ ๐‘ƒ )
61 59 60 syl โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โˆˆ ๐‘ƒ )
62 itsclc0lem2 โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ท โˆˆ โ„ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘„ โˆˆ โ„ โˆง ๐‘„ โ‰  0 ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ )
63 21 29 35 43 53 62 syl311anc โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ )
64 itsclc0lem1 โŠข ( ( ( ๐ต โˆˆ โ„ โˆง ๐ด โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โˆง ( ๐ท โˆˆ โ„ โˆง 0 โ‰ค ๐ท ) โˆง ( ๐‘„ โˆˆ โ„ โˆง ๐‘„ โ‰  0 ) ) โ†’ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ )
65 29 21 35 43 53 64 syl311anc โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ )
66 63 65 jca โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ โˆง ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ ) )
67 66 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ โˆง ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ ) )
68 1 3 prelrrx2 โŠข ( ( ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ โˆง ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ โ„ ) โ†’ { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โˆˆ ๐‘ƒ )
69 67 68 syl โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โˆˆ ๐‘ƒ )
70 simpl โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) )
71 simprl โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐‘… โˆˆ โ„+ )
72 0red โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ 0 โˆˆ โ„ )
73 72 41 12 ltled โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ 0 โ‰ค ๐ท )
74 70 71 73 jca32 โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) )
75 74 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) )
76 1 2 3 4 5 7 8 6 9 10 11 itsclinecirc0in โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 โ‰ค ๐ท ) ) โ†’ ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } } )
77 75 76 syl โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } } )
78 opex โŠข โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V
79 opex โŠข โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V
80 opex โŠข โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V
81 opex โŠข โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V
82 80 81 pm3.2i โŠข ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V )
83 48 adantr โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ๐ด โ‰  0 โˆจ ๐ต โ‰  0 ) )
84 83 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ๐ด โ‰  0 โˆจ ๐ต โ‰  0 ) )
85 orcom โŠข ( ( ๐ด โ‰  0 โˆจ ๐ต โ‰  0 ) โ†” ( ๐ต โ‰  0 โˆจ ๐ด โ‰  0 ) )
86 21 recnd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐ด โˆˆ โ„‚ )
87 86 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ๐ด โˆˆ โ„‚ )
88 35 recnd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐ถ โˆˆ โ„‚ )
89 88 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ๐ถ โˆˆ โ„‚ )
90 87 89 mulcld โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ๐ด ยท ๐ถ ) โˆˆ โ„‚ )
91 29 recnd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐ต โˆˆ โ„‚ )
92 91 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ๐ต โˆˆ โ„‚ )
93 41 recnd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐ท โˆˆ โ„‚ )
94 93 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ๐ท โˆˆ โ„‚ )
95 94 sqrtcld โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( โˆš โ€˜ ๐ท ) โˆˆ โ„‚ )
96 92 95 mulcld โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) โˆˆ โ„‚ )
97 90 96 addcld โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„‚ )
98 90 96 subcld โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„‚ )
99 46 adantr โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐‘„ โˆˆ โ„ )
100 99 recnd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐‘„ โˆˆ โ„‚ )
101 51 adantr โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ๐‘„ โ‰  0 )
102 100 101 jca โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ๐‘„ โˆˆ โ„‚ โˆง ๐‘„ โ‰  0 ) )
103 102 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ๐‘„ โˆˆ โ„‚ โˆง ๐‘„ โ‰  0 ) )
104 div11 โŠข ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„‚ โˆง ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„‚ โˆง ( ๐‘„ โˆˆ โ„‚ โˆง ๐‘„ โ‰  0 ) ) โ†’ ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ†” ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) ) )
105 97 98 103 104 syl3anc โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ†” ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) ) )
106 addsubeq0 โŠข ( ( ( ๐ด ยท ๐ถ ) โˆˆ โ„‚ โˆง ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) โˆˆ โ„‚ ) โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) โ†” ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) = 0 ) )
107 90 96 106 syl2anc โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) โ†” ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) = 0 ) )
108 41 73 resqrtcld โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( โˆš โ€˜ ๐ท ) โˆˆ โ„ )
109 108 recnd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( โˆš โ€˜ ๐ท ) โˆˆ โ„‚ )
110 91 109 mul0ord โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) = 0 โ†” ( ๐ต = 0 โˆจ ( โˆš โ€˜ ๐ท ) = 0 ) ) )
111 110 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) = 0 โ†” ( ๐ต = 0 โˆจ ( โˆš โ€˜ ๐ท ) = 0 ) ) )
112 eqneqall โŠข ( ๐ต = 0 โ†’ ( ๐ต โ‰  0 โ†’ ๐ท = 0 ) )
113 112 com12 โŠข ( ๐ต โ‰  0 โ†’ ( ๐ต = 0 โ†’ ๐ท = 0 ) )
114 113 adantl โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ๐ต = 0 โ†’ ๐ท = 0 ) )
115 sqrt00 โŠข ( ( ๐ท โˆˆ โ„ โˆง 0 โ‰ค ๐ท ) โ†’ ( ( โˆš โ€˜ ๐ท ) = 0 โ†” ๐ท = 0 ) )
116 41 73 115 syl2anc โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( โˆš โ€˜ ๐ท ) = 0 โ†” ๐ท = 0 ) )
117 116 biimpd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( โˆš โ€˜ ๐ท ) = 0 โ†’ ๐ท = 0 ) )
118 117 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ( โˆš โ€˜ ๐ท ) = 0 โ†’ ๐ท = 0 ) )
119 114 118 jaod โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ( ๐ต = 0 โˆจ ( โˆš โ€˜ ๐ท ) = 0 ) โ†’ ๐ท = 0 ) )
120 111 119 sylbid โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) = 0 โ†’ ๐ท = 0 ) )
121 107 120 sylbid โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) โ†’ ๐ท = 0 ) )
122 105 121 sylbid โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ†’ ๐ท = 0 ) )
123 122 necon3d โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ต โ‰  0 ) โ†’ ( ๐ท โ‰  0 โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
124 123 impancom โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ๐ต โ‰  0 โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
125 124 imp โŠข ( ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โˆง ๐ต โ‰  0 ) โ†’ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) )
126 125 olcd โŠข ( ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โˆง ๐ต โ‰  0 ) โ†’ ( 1 โ‰  1 โˆจ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
127 1ex โŠข 1 โˆˆ V
128 ovex โŠข ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ V
129 127 128 opthne โŠข ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ†” ( 1 โ‰  1 โˆจ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
130 126 129 sylibr โŠข ( ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โˆง ๐ต โ‰  0 ) โ†’ โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ )
131 1ne2 โŠข 1 โ‰  2
132 131 orci โŠข ( 1 โ‰  2 โˆจ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) )
133 127 128 opthne โŠข ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ†” ( 1 โ‰  2 โˆจ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
134 132 133 mpbir โŠข โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ
135 130 134 jctir โŠข ( ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โˆง ๐ต โ‰  0 ) โ†’ ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) )
136 135 ex โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ๐ต โ‰  0 โ†’ ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) ) )
137 27 33 remulcld โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ๐ต ยท ๐ถ ) โˆˆ โ„ )
138 137 3adant3 โŠข ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โ†’ ( ๐ต ยท ๐ถ ) โˆˆ โ„ )
139 138 adantr โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ๐ต ยท ๐ถ ) โˆˆ โ„ )
140 21 108 remulcld โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) โˆˆ โ„ )
141 139 140 resubcld โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„ )
142 141 recnd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„‚ )
143 142 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„‚ )
144 29 35 remulcld โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ๐ต ยท ๐ถ ) โˆˆ โ„ )
145 144 140 readdcld โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„ )
146 145 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„ )
147 146 recnd โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„‚ )
148 102 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ๐‘„ โˆˆ โ„‚ โˆง ๐‘„ โ‰  0 ) )
149 div11 โŠข ( ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„‚ โˆง ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โˆˆ โ„‚ โˆง ( ๐‘„ โˆˆ โ„‚ โˆง ๐‘„ โ‰  0 ) ) โ†’ ( ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ†” ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) ) )
150 143 147 148 149 syl3anc โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ†” ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) ) )
151 139 recnd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ๐ต ยท ๐ถ ) โˆˆ โ„‚ )
152 140 recnd โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) โˆˆ โ„‚ )
153 151 152 jca โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ๐ต ยท ๐ถ ) โˆˆ โ„‚ โˆง ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) โˆˆ โ„‚ ) )
154 153 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ๐ต ยท ๐ถ ) โˆˆ โ„‚ โˆง ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) โˆˆ โ„‚ ) )
155 eqcom โŠข ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โ†” ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) )
156 addsubeq0 โŠข ( ( ( ๐ต ยท ๐ถ ) โˆˆ โ„‚ โˆง ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) โˆˆ โ„‚ ) โ†’ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โ†” ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = 0 ) )
157 155 156 bitrid โŠข ( ( ( ๐ต ยท ๐ถ ) โˆˆ โ„‚ โˆง ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) โˆˆ โ„‚ ) โ†’ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โ†” ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = 0 ) )
158 154 157 syl โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โ†” ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = 0 ) )
159 86 109 mul0ord โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = 0 โ†” ( ๐ด = 0 โˆจ ( โˆš โ€˜ ๐ท ) = 0 ) ) )
160 159 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = 0 โ†” ( ๐ด = 0 โˆจ ( โˆš โ€˜ ๐ท ) = 0 ) ) )
161 eqneqall โŠข ( ๐ด = 0 โ†’ ( ๐ด โ‰  0 โ†’ ๐ท = 0 ) )
162 161 com12 โŠข ( ๐ด โ‰  0 โ†’ ( ๐ด = 0 โ†’ ๐ท = 0 ) )
163 162 adantl โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ๐ด = 0 โ†’ ๐ท = 0 ) )
164 117 adantr โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( โˆš โ€˜ ๐ท ) = 0 โ†’ ๐ท = 0 ) )
165 163 164 jaod โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ๐ด = 0 โˆจ ( โˆš โ€˜ ๐ท ) = 0 ) โ†’ ๐ท = 0 ) )
166 160 165 sylbid โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) = 0 โ†’ ๐ท = 0 ) )
167 158 166 sylbid โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) โ†’ ๐ท = 0 ) )
168 150 167 sylbid โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ†’ ๐ท = 0 ) )
169 168 necon3d โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ด โ‰  0 ) โ†’ ( ๐ท โ‰  0 โ†’ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
170 169 impancom โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ๐ด โ‰  0 โ†’ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
171 170 imp โŠข ( ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โˆง ๐ด โ‰  0 ) โ†’ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) )
172 171 olcd โŠข ( ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โˆง ๐ด โ‰  0 ) โ†’ ( 2 โ‰  2 โˆจ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
173 2ex โŠข 2 โˆˆ V
174 ovex โŠข ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โˆˆ V
175 173 174 opthne โŠข ( โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ†” ( 2 โ‰  2 โˆจ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
176 172 175 sylibr โŠข ( ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โˆง ๐ด โ‰  0 ) โ†’ โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ )
177 131 necomi โŠข 2 โ‰  1
178 177 orci โŠข ( 2 โ‰  1 โˆจ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) )
179 173 174 opthne โŠข ( โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ†” ( 2 โ‰  1 โˆจ ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โ‰  ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) ) )
180 178 179 mpbir โŠข โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ
181 176 180 jctil โŠข ( ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โˆง ๐ด โ‰  0 ) โ†’ ( โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) )
182 181 ex โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ๐ด โ‰  0 โ†’ ( โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) ) )
183 136 182 orim12d โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ( ๐ต โ‰  0 โˆจ ๐ด โ‰  0 ) โ†’ ( ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) โˆจ ( โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) ) ) )
184 85 183 biimtrid โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ( ๐ด โ‰  0 โˆจ ๐ต โ‰  0 ) โ†’ ( ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) โˆจ ( โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) ) ) )
185 84 184 mpd โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) โˆจ ( โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) ) )
186 prneimg โŠข ( ( ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V ) โˆง ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V ) ) โ†’ ( ( ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) โˆจ ( โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) ) โ†’ { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } ) )
187 186 imp โŠข ( ( ( ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V ) โˆง ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆˆ V ) ) โˆง ( ( โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) โˆจ ( โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โˆง โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ โ‰  โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ ) ) ) โ†’ { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } )
188 78 79 82 185 187 mpsyl4anc โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } )
189 77 188 jca โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } } โˆง { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } ) )
190 61 69 189 3jca โŠข ( ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โˆง ๐ท โ‰  0 ) โ†’ ( { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โˆˆ ๐‘ƒ โˆง { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โˆˆ ๐‘ƒ โˆง ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } } โˆง { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } ) ) )
191 13 190 mpdan โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ ( { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โˆˆ ๐‘ƒ โˆง { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โˆˆ ๐‘ƒ โˆง ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } } โˆง { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } ) ) )
192 preq1 โŠข ( ๐‘Ž = { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ†’ { ๐‘Ž , ๐‘ } = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , ๐‘ } )
193 192 eqeq2d โŠข ( ๐‘Ž = { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ†’ ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { ๐‘Ž , ๐‘ } โ†” ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , ๐‘ } ) )
194 neeq1 โŠข ( ๐‘Ž = { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ†’ ( ๐‘Ž โ‰  ๐‘ โ†” { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  ๐‘ ) )
195 193 194 anbi12d โŠข ( ๐‘Ž = { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ†’ ( ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { ๐‘Ž , ๐‘ } โˆง ๐‘Ž โ‰  ๐‘ ) โ†” ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , ๐‘ } โˆง { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  ๐‘ ) ) )
196 preq2 โŠข ( ๐‘ = { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ†’ { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , ๐‘ } = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } } )
197 196 eqeq2d โŠข ( ๐‘ = { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ†’ ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , ๐‘ } โ†” ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } } ) )
198 neeq2 โŠข ( ๐‘ = { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ†’ ( { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  ๐‘ โ†” { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } ) )
199 197 198 anbi12d โŠข ( ๐‘ = { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ†’ ( ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , ๐‘ } โˆง { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  ๐‘ ) โ†” ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } } โˆง { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } ) ) )
200 195 199 rspc2ev โŠข ( ( { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โˆˆ ๐‘ƒ โˆง { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โˆˆ ๐‘ƒ โˆง ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } , { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } } โˆง { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) โˆ’ ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } โ‰  { โŸจ 1 , ( ( ( ๐ด ยท ๐ถ ) โˆ’ ( ๐ต ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ , โŸจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โˆš โ€˜ ๐ท ) ) ) / ๐‘„ ) โŸฉ } ) ) โ†’ โˆƒ ๐‘Ž โˆˆ ๐‘ƒ โˆƒ ๐‘ โˆˆ ๐‘ƒ ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { ๐‘Ž , ๐‘ } โˆง ๐‘Ž โ‰  ๐‘ ) )
201 191 200 syl โŠข ( ( ( ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ โˆง ๐‘‹ โ‰  ๐‘Œ ) โˆง ( ๐‘… โˆˆ โ„+ โˆง 0 < ๐ท ) ) โ†’ โˆƒ ๐‘Ž โˆˆ ๐‘ƒ โˆƒ ๐‘ โˆˆ ๐‘ƒ ( ( ( 0 ๐‘† ๐‘… ) โˆฉ ( ๐‘‹ ๐ฟ ๐‘Œ ) ) = { ๐‘Ž , ๐‘ } โˆง ๐‘Ž โ‰  ๐‘ ) )