Metamath Proof Explorer


Theorem 2itscp

Description: A condition for a quadratic equation with real coefficients (for the intersection points of a line with a circle) to have (exactly) two different real solutions. (Contributed by AV, 5-Mar-2023) (Revised by AV, 16-May-2023)

Ref Expression
Hypotheses 2itscp.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
2itscp.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
2itscp.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„ )
2itscp.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ โ„ )
2itscp.d โŠข ๐ท = ( ๐‘‹ โˆ’ ๐ด )
2itscp.e โŠข ๐ธ = ( ๐ต โˆ’ ๐‘Œ )
2itscp.c โŠข ๐ถ = ( ( ๐ท ยท ๐ต ) + ( ๐ธ ยท ๐ด ) )
2itscp.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ โ„ )
2itscp.l โŠข ( ๐œ‘ โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) < ( ๐‘… โ†‘ 2 ) )
2itscp.n โŠข ( ๐œ‘ โ†’ ( ๐ต โ‰  ๐‘Œ โˆจ ๐ด โ‰  ๐‘‹ ) )
2itscp.q โŠข ๐‘„ = ( ( ๐ธ โ†‘ 2 ) + ( ๐ท โ†‘ 2 ) )
2itscp.s โŠข ๐‘† = ( ( ( ๐‘… โ†‘ 2 ) ยท ๐‘„ ) โˆ’ ( ๐ถ โ†‘ 2 ) )
Assertion 2itscp ( ๐œ‘ โ†’ 0 < ๐‘† )

Proof

Step Hyp Ref Expression
1 2itscp.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
2 2itscp.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
3 2itscp.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„ )
4 2itscp.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ โ„ )
5 2itscp.d โŠข ๐ท = ( ๐‘‹ โˆ’ ๐ด )
6 2itscp.e โŠข ๐ธ = ( ๐ต โˆ’ ๐‘Œ )
7 2itscp.c โŠข ๐ถ = ( ( ๐ท ยท ๐ต ) + ( ๐ธ ยท ๐ด ) )
8 2itscp.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ โ„ )
9 2itscp.l โŠข ( ๐œ‘ โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) < ( ๐‘… โ†‘ 2 ) )
10 2itscp.n โŠข ( ๐œ‘ โ†’ ( ๐ต โ‰  ๐‘Œ โˆจ ๐ด โ‰  ๐‘‹ ) )
11 2itscp.q โŠข ๐‘„ = ( ( ๐ธ โ†‘ 2 ) + ( ๐ท โ†‘ 2 ) )
12 2itscp.s โŠข ๐‘† = ( ( ( ๐‘… โ†‘ 2 ) ยท ๐‘„ ) โˆ’ ( ๐ถ โ†‘ 2 ) )
13 2 recnd โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
14 13 adantr โŠข ( ( ๐œ‘ โˆง ๐ต โ‰  ๐‘Œ ) โ†’ ๐ต โˆˆ โ„‚ )
15 4 recnd โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ โ„‚ )
16 15 adantr โŠข ( ( ๐œ‘ โˆง ๐ต โ‰  ๐‘Œ ) โ†’ ๐‘Œ โˆˆ โ„‚ )
17 simpr โŠข ( ( ๐œ‘ โˆง ๐ต โ‰  ๐‘Œ ) โ†’ ๐ต โ‰  ๐‘Œ )
18 14 16 17 subne0d โŠข ( ( ๐œ‘ โˆง ๐ต โ‰  ๐‘Œ ) โ†’ ( ๐ต โˆ’ ๐‘Œ ) โ‰  0 )
19 18 ex โŠข ( ๐œ‘ โ†’ ( ๐ต โ‰  ๐‘Œ โ†’ ( ๐ต โˆ’ ๐‘Œ ) โ‰  0 ) )
20 3 recnd โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚ )
21 20 adantr โŠข ( ( ๐œ‘ โˆง ๐ด โ‰  ๐‘‹ ) โ†’ ๐‘‹ โˆˆ โ„‚ )
22 1 recnd โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
23 22 adantr โŠข ( ( ๐œ‘ โˆง ๐ด โ‰  ๐‘‹ ) โ†’ ๐ด โˆˆ โ„‚ )
24 simpr โŠข ( ( ๐œ‘ โˆง ๐ด โ‰  ๐‘‹ ) โ†’ ๐ด โ‰  ๐‘‹ )
25 24 necomd โŠข ( ( ๐œ‘ โˆง ๐ด โ‰  ๐‘‹ ) โ†’ ๐‘‹ โ‰  ๐ด )
26 21 23 25 subne0d โŠข ( ( ๐œ‘ โˆง ๐ด โ‰  ๐‘‹ ) โ†’ ( ๐‘‹ โˆ’ ๐ด ) โ‰  0 )
27 26 ex โŠข ( ๐œ‘ โ†’ ( ๐ด โ‰  ๐‘‹ โ†’ ( ๐‘‹ โˆ’ ๐ด ) โ‰  0 ) )
28 6 neeq1i โŠข ( ๐ธ โ‰  0 โ†” ( ๐ต โˆ’ ๐‘Œ ) โ‰  0 )
29 5 neeq1i โŠข ( ๐ท โ‰  0 โ†” ( ๐‘‹ โˆ’ ๐ด ) โ‰  0 )
30 28 29 anbi12i โŠข ( ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) โ†” ( ( ๐ต โˆ’ ๐‘Œ ) โ‰  0 โˆง ( ๐‘‹ โˆ’ ๐ด ) โ‰  0 ) )
31 2re โŠข 2 โˆˆ โ„
32 31 a1i โŠข ( ๐œ‘ โ†’ 2 โˆˆ โ„ )
33 3 1 resubcld โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆ’ ๐ด ) โˆˆ โ„ )
34 5 33 eqeltrid โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„ )
35 34 1 remulcld โŠข ( ๐œ‘ โ†’ ( ๐ท ยท ๐ด ) โˆˆ โ„ )
36 2 4 resubcld โŠข ( ๐œ‘ โ†’ ( ๐ต โˆ’ ๐‘Œ ) โˆˆ โ„ )
37 6 36 eqeltrid โŠข ( ๐œ‘ โ†’ ๐ธ โˆˆ โ„ )
38 37 2 remulcld โŠข ( ๐œ‘ โ†’ ( ๐ธ ยท ๐ต ) โˆˆ โ„ )
39 35 38 remulcld โŠข ( ๐œ‘ โ†’ ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) โˆˆ โ„ )
40 32 39 remulcld โŠข ( ๐œ‘ โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) โˆˆ โ„ )
41 40 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) โˆˆ โ„ )
42 37 resqcld โŠข ( ๐œ‘ โ†’ ( ๐ธ โ†‘ 2 ) โˆˆ โ„ )
43 2 resqcld โŠข ( ๐œ‘ โ†’ ( ๐ต โ†‘ 2 ) โˆˆ โ„ )
44 42 43 remulcld โŠข ( ๐œ‘ โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) โˆˆ โ„ )
45 34 resqcld โŠข ( ๐œ‘ โ†’ ( ๐ท โ†‘ 2 ) โˆˆ โ„ )
46 1 resqcld โŠข ( ๐œ‘ โ†’ ( ๐ด โ†‘ 2 ) โˆˆ โ„ )
47 45 46 remulcld โŠข ( ๐œ‘ โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) โˆˆ โ„ )
48 44 47 readdcld โŠข ( ๐œ‘ โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) ) โˆˆ โ„ )
49 48 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) ) โˆˆ โ„ )
50 8 resqcld โŠข ( ๐œ‘ โ†’ ( ๐‘… โ†‘ 2 ) โˆˆ โ„ )
51 50 46 resubcld โŠข ( ๐œ‘ โ†’ ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) โˆˆ โ„ )
52 42 51 remulcld โŠข ( ๐œ‘ โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) โˆˆ โ„ )
53 50 43 resubcld โŠข ( ๐œ‘ โ†’ ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) โˆˆ โ„ )
54 45 53 remulcld โŠข ( ๐œ‘ โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) โˆˆ โ„ )
55 52 54 readdcld โŠข ( ๐œ‘ โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) โˆˆ โ„ )
56 55 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) โˆˆ โ„ )
57 35 38 resubcld โŠข ( ๐œ‘ โ†’ ( ( ๐ท ยท ๐ด ) โˆ’ ( ๐ธ ยท ๐ต ) ) โˆˆ โ„ )
58 57 sqge0d โŠข ( ๐œ‘ โ†’ 0 โ‰ค ( ( ( ๐ท ยท ๐ด ) โˆ’ ( ๐ธ ยท ๐ต ) ) โ†‘ 2 ) )
59 1 2 3 4 5 6 2itscplem1 โŠข ( ๐œ‘ โ†’ ( ( ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) ) โˆ’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) ) = ( ( ( ๐ท ยท ๐ด ) โˆ’ ( ๐ธ ยท ๐ต ) ) โ†‘ 2 ) )
60 58 59 breqtrrd โŠข ( ๐œ‘ โ†’ 0 โ‰ค ( ( ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) ) โˆ’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) ) )
61 48 40 subge0d โŠข ( ๐œ‘ โ†’ ( 0 โ‰ค ( ( ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) ) โˆ’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) ) โ†” ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) โ‰ค ( ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) ) ) )
62 60 61 mpbid โŠข ( ๐œ‘ โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) โ‰ค ( ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) ) )
63 62 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) โ‰ค ( ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) ) )
64 44 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) โˆˆ โ„ )
65 47 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) โˆˆ โ„ )
66 52 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) โˆˆ โ„ )
67 54 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) โˆˆ โ„ )
68 43 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ต โ†‘ 2 ) โˆˆ โ„ )
69 51 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) โˆˆ โ„ )
70 simpl โŠข ( ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) โ†’ ๐ธ โ‰  0 )
71 sqn0rp โŠข ( ( ๐ธ โˆˆ โ„ โˆง ๐ธ โ‰  0 ) โ†’ ( ๐ธ โ†‘ 2 ) โˆˆ โ„+ )
72 37 70 71 syl2an โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ธ โ†‘ 2 ) โˆˆ โ„+ )
73 46 43 50 ltaddsub2d โŠข ( ๐œ‘ โ†’ ( ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) < ( ๐‘… โ†‘ 2 ) โ†” ( ๐ต โ†‘ 2 ) < ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) )
74 9 73 mpbid โŠข ( ๐œ‘ โ†’ ( ๐ต โ†‘ 2 ) < ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) )
75 74 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ต โ†‘ 2 ) < ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) )
76 68 69 72 75 ltmul2dd โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) < ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) )
77 46 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ด โ†‘ 2 ) โˆˆ โ„ )
78 53 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) โˆˆ โ„ )
79 simpr โŠข ( ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) โ†’ ๐ท โ‰  0 )
80 sqn0rp โŠข ( ( ๐ท โˆˆ โ„ โˆง ๐ท โ‰  0 ) โ†’ ( ๐ท โ†‘ 2 ) โˆˆ โ„+ )
81 34 79 80 syl2an โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ท โ†‘ 2 ) โˆˆ โ„+ )
82 46 43 50 ltaddsubd โŠข ( ๐œ‘ โ†’ ( ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) < ( ๐‘… โ†‘ 2 ) โ†” ( ๐ด โ†‘ 2 ) < ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) )
83 9 82 mpbid โŠข ( ๐œ‘ โ†’ ( ๐ด โ†‘ 2 ) < ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) )
84 83 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ด โ†‘ 2 ) < ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) )
85 77 78 81 84 ltmul2dd โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) < ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) )
86 64 65 66 67 76 85 lt2addd โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) )
87 41 49 56 63 86 lelttrd โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) )
88 87 ex โŠข ( ๐œ‘ โ†’ ( ( ๐ธ โ‰  0 โˆง ๐ท โ‰  0 ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
89 30 88 biimtrrid โŠข ( ๐œ‘ โ†’ ( ( ( ๐ต โˆ’ ๐‘Œ ) โ‰  0 โˆง ( ๐‘‹ โˆ’ ๐ด ) โ‰  0 ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
90 19 27 89 syl2and โŠข ( ๐œ‘ โ†’ ( ( ๐ต โ‰  ๐‘Œ โˆง ๐ด โ‰  ๐‘‹ ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
91 90 imp โŠข ( ( ๐œ‘ โˆง ( ๐ต โ‰  ๐‘Œ โˆง ๐ด โ‰  ๐‘‹ ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) )
92 nne โŠข ( ยฌ ๐ด โ‰  ๐‘‹ โ†” ๐ด = ๐‘‹ )
93 eqcom โŠข ( ๐ด = ๐‘‹ โ†” ๐‘‹ = ๐ด )
94 20 22 subeq0ad โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆ’ ๐ด ) = 0 โ†” ๐‘‹ = ๐ด ) )
95 94 biimprd โŠข ( ๐œ‘ โ†’ ( ๐‘‹ = ๐ด โ†’ ( ๐‘‹ โˆ’ ๐ด ) = 0 ) )
96 93 95 biimtrid โŠข ( ๐œ‘ โ†’ ( ๐ด = ๐‘‹ โ†’ ( ๐‘‹ โˆ’ ๐ด ) = 0 ) )
97 92 96 biimtrid โŠข ( ๐œ‘ โ†’ ( ยฌ ๐ด โ‰  ๐‘‹ โ†’ ( ๐‘‹ โˆ’ ๐ด ) = 0 ) )
98 5 eqeq1i โŠข ( ๐ท = 0 โ†” ( ๐‘‹ โˆ’ ๐ด ) = 0 )
99 28 98 anbi12i โŠข ( ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) โ†” ( ( ๐ต โˆ’ ๐‘Œ ) โ‰  0 โˆง ( ๐‘‹ โˆ’ ๐ด ) = 0 ) )
100 0red โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ 0 โˆˆ โ„ )
101 44 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) โˆˆ โ„ )
102 52 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) โˆˆ โ„ )
103 37 sqge0d โŠข ( ๐œ‘ โ†’ 0 โ‰ค ( ๐ธ โ†‘ 2 ) )
104 2 sqge0d โŠข ( ๐œ‘ โ†’ 0 โ‰ค ( ๐ต โ†‘ 2 ) )
105 42 43 103 104 mulge0d โŠข ( ๐œ‘ โ†’ 0 โ‰ค ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) )
106 105 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ 0 โ‰ค ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) )
107 43 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ๐ต โ†‘ 2 ) โˆˆ โ„ )
108 51 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) โˆˆ โ„ )
109 simprl โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ๐ธ โ‰  0 )
110 37 109 71 syl2an2r โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ๐ธ โ†‘ 2 ) โˆˆ โ„+ )
111 74 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ๐ต โ†‘ 2 ) < ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) )
112 107 108 110 111 ltmul2dd โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ๐ต โ†‘ 2 ) ) < ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) )
113 100 101 102 106 112 lelttrd โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ 0 < ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) )
114 oveq1 โŠข ( ๐ท = 0 โ†’ ( ๐ท ยท ๐ด ) = ( 0 ยท ๐ด ) )
115 114 adantl โŠข ( ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) โ†’ ( ๐ท ยท ๐ด ) = ( 0 ยท ๐ด ) )
116 22 mul02d โŠข ( ๐œ‘ โ†’ ( 0 ยท ๐ด ) = 0 )
117 115 116 sylan9eqr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ๐ท ยท ๐ด ) = 0 )
118 117 oveq1d โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) = ( 0 ยท ( ๐ธ ยท ๐ต ) ) )
119 38 recnd โŠข ( ๐œ‘ โ†’ ( ๐ธ ยท ๐ต ) โˆˆ โ„‚ )
120 119 mul02d โŠข ( ๐œ‘ โ†’ ( 0 ยท ( ๐ธ ยท ๐ต ) ) = 0 )
121 120 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( 0 ยท ( ๐ธ ยท ๐ต ) ) = 0 )
122 118 121 eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) = 0 )
123 122 oveq2d โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) = ( 2 ยท 0 ) )
124 2t0e0 โŠข ( 2 ยท 0 ) = 0
125 123 124 eqtrdi โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) = 0 )
126 sq0i โŠข ( ๐ท = 0 โ†’ ( ๐ท โ†‘ 2 ) = 0 )
127 126 adantl โŠข ( ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) โ†’ ( ๐ท โ†‘ 2 ) = 0 )
128 127 adantl โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ๐ท โ†‘ 2 ) = 0 )
129 128 oveq1d โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) = ( 0 ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) )
130 53 recnd โŠข ( ๐œ‘ โ†’ ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) โˆˆ โ„‚ )
131 130 mul02d โŠข ( ๐œ‘ โ†’ ( 0 ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) = 0 )
132 131 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( 0 ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) = 0 )
133 129 132 eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) = 0 )
134 133 oveq2d โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) = ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + 0 ) )
135 52 recnd โŠข ( ๐œ‘ โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) โˆˆ โ„‚ )
136 135 addridd โŠข ( ๐œ‘ โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + 0 ) = ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) )
137 136 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + 0 ) = ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) )
138 134 137 eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) = ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) )
139 113 125 138 3brtr4d โŠข ( ( ๐œ‘ โˆง ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) )
140 139 ex โŠข ( ๐œ‘ โ†’ ( ( ๐ธ โ‰  0 โˆง ๐ท = 0 ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
141 99 140 biimtrrid โŠข ( ๐œ‘ โ†’ ( ( ( ๐ต โˆ’ ๐‘Œ ) โ‰  0 โˆง ( ๐‘‹ โˆ’ ๐ด ) = 0 ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
142 19 97 141 syl2and โŠข ( ๐œ‘ โ†’ ( ( ๐ต โ‰  ๐‘Œ โˆง ยฌ ๐ด โ‰  ๐‘‹ ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
143 142 imp โŠข ( ( ๐œ‘ โˆง ( ๐ต โ‰  ๐‘Œ โˆง ยฌ ๐ด โ‰  ๐‘‹ ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) )
144 nne โŠข ( ยฌ ๐ต โ‰  ๐‘Œ โ†” ๐ต = ๐‘Œ )
145 13 15 subeq0ad โŠข ( ๐œ‘ โ†’ ( ( ๐ต โˆ’ ๐‘Œ ) = 0 โ†” ๐ต = ๐‘Œ ) )
146 145 biimprd โŠข ( ๐œ‘ โ†’ ( ๐ต = ๐‘Œ โ†’ ( ๐ต โˆ’ ๐‘Œ ) = 0 ) )
147 144 146 biimtrid โŠข ( ๐œ‘ โ†’ ( ยฌ ๐ต โ‰  ๐‘Œ โ†’ ( ๐ต โˆ’ ๐‘Œ ) = 0 ) )
148 6 eqeq1i โŠข ( ๐ธ = 0 โ†” ( ๐ต โˆ’ ๐‘Œ ) = 0 )
149 148 29 anbi12i โŠข ( ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) โ†” ( ( ๐ต โˆ’ ๐‘Œ ) = 0 โˆง ( ๐‘‹ โˆ’ ๐ด ) โ‰  0 ) )
150 0red โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ 0 โˆˆ โ„ )
151 47 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) โˆˆ โ„ )
152 54 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) โˆˆ โ„ )
153 34 sqge0d โŠข ( ๐œ‘ โ†’ 0 โ‰ค ( ๐ท โ†‘ 2 ) )
154 1 sqge0d โŠข ( ๐œ‘ โ†’ 0 โ‰ค ( ๐ด โ†‘ 2 ) )
155 45 46 153 154 mulge0d โŠข ( ๐œ‘ โ†’ 0 โ‰ค ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) )
156 155 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ 0 โ‰ค ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) )
157 46 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ด โ†‘ 2 ) โˆˆ โ„ )
158 53 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) โˆˆ โ„ )
159 simprr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ๐ท โ‰  0 )
160 34 159 80 syl2an2r โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ท โ†‘ 2 ) โˆˆ โ„+ )
161 43 recnd โŠข ( ๐œ‘ โ†’ ( ๐ต โ†‘ 2 ) โˆˆ โ„‚ )
162 46 recnd โŠข ( ๐œ‘ โ†’ ( ๐ด โ†‘ 2 ) โˆˆ โ„‚ )
163 161 162 addcomd โŠข ( ๐œ‘ โ†’ ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) = ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) )
164 163 9 eqbrtrd โŠข ( ๐œ‘ โ†’ ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) < ( ๐‘… โ†‘ 2 ) )
165 43 46 50 ltaddsub2d โŠข ( ๐œ‘ โ†’ ( ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) < ( ๐‘… โ†‘ 2 ) โ†” ( ๐ด โ†‘ 2 ) < ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) )
166 164 165 mpbid โŠข ( ๐œ‘ โ†’ ( ๐ด โ†‘ 2 ) < ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) )
167 166 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ด โ†‘ 2 ) < ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) )
168 157 158 160 167 ltmul2dd โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ๐ด โ†‘ 2 ) ) < ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) )
169 150 151 152 156 168 lelttrd โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ 0 < ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) )
170 oveq1 โŠข ( ๐ธ = 0 โ†’ ( ๐ธ ยท ๐ต ) = ( 0 ยท ๐ต ) )
171 170 adantr โŠข ( ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) โ†’ ( ๐ธ ยท ๐ต ) = ( 0 ยท ๐ต ) )
172 13 mul02d โŠข ( ๐œ‘ โ†’ ( 0 ยท ๐ต ) = 0 )
173 171 172 sylan9eqr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ธ ยท ๐ต ) = 0 )
174 173 oveq2d โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) = ( ( ๐ท ยท ๐ด ) ยท 0 ) )
175 34 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ๐ท โˆˆ โ„ )
176 175 recnd โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ๐ท โˆˆ โ„‚ )
177 22 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ๐ด โˆˆ โ„‚ )
178 176 177 mulcld โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ท ยท ๐ด ) โˆˆ โ„‚ )
179 178 mul01d โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ท ยท ๐ด ) ยท 0 ) = 0 )
180 174 179 eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) = 0 )
181 180 oveq2d โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) = ( 2 ยท 0 ) )
182 181 124 eqtrdi โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) = 0 )
183 sq0i โŠข ( ๐ธ = 0 โ†’ ( ๐ธ โ†‘ 2 ) = 0 )
184 183 adantr โŠข ( ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) โ†’ ( ๐ธ โ†‘ 2 ) = 0 )
185 184 adantl โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ๐ธ โ†‘ 2 ) = 0 )
186 185 oveq1d โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) = ( 0 ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) )
187 51 recnd โŠข ( ๐œ‘ โ†’ ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) โˆˆ โ„‚ )
188 187 mul02d โŠข ( ๐œ‘ โ†’ ( 0 ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) = 0 )
189 188 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( 0 ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) = 0 )
190 186 189 eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) = 0 )
191 190 oveq1d โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) = ( 0 + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) )
192 54 recnd โŠข ( ๐œ‘ โ†’ ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) โˆˆ โ„‚ )
193 192 addlidd โŠข ( ๐œ‘ โ†’ ( 0 + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) = ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) )
194 193 adantr โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( 0 + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) = ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) )
195 191 194 eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) = ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) )
196 169 182 195 3brtr4d โŠข ( ( ๐œ‘ โˆง ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) )
197 196 ex โŠข ( ๐œ‘ โ†’ ( ( ๐ธ = 0 โˆง ๐ท โ‰  0 ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
198 149 197 biimtrrid โŠข ( ๐œ‘ โ†’ ( ( ( ๐ต โˆ’ ๐‘Œ ) = 0 โˆง ( ๐‘‹ โˆ’ ๐ด ) โ‰  0 ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
199 147 27 198 syl2and โŠข ( ๐œ‘ โ†’ ( ( ยฌ ๐ต โ‰  ๐‘Œ โˆง ๐ด โ‰  ๐‘‹ ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
200 199 imp โŠข ( ( ๐œ‘ โˆง ( ยฌ ๐ต โ‰  ๐‘Œ โˆง ๐ด โ‰  ๐‘‹ ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) )
201 ioran โŠข ( ยฌ ( ๐ต โ‰  ๐‘Œ โˆจ ๐ด โ‰  ๐‘‹ ) โ†” ( ยฌ ๐ต โ‰  ๐‘Œ โˆง ยฌ ๐ด โ‰  ๐‘‹ ) )
202 10 pm2.24d โŠข ( ๐œ‘ โ†’ ( ยฌ ( ๐ต โ‰  ๐‘Œ โˆจ ๐ด โ‰  ๐‘‹ ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
203 201 202 biimtrrid โŠข ( ๐œ‘ โ†’ ( ( ยฌ ๐ต โ‰  ๐‘Œ โˆง ยฌ ๐ด โ‰  ๐‘‹ ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) ) )
204 203 imp โŠข ( ( ๐œ‘ โˆง ( ยฌ ๐ต โ‰  ๐‘Œ โˆง ยฌ ๐ด โ‰  ๐‘‹ ) ) โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) )
205 91 143 200 204 4casesdan โŠข ( ๐œ‘ โ†’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) )
206 40 55 posdifd โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) < ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) โ†” 0 < ( ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) โˆ’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) ) ) )
207 205 206 mpbid โŠข ( ๐œ‘ โ†’ 0 < ( ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) โˆ’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) ) )
208 1 2 3 4 5 6 7 8 11 12 2itscplem3 โŠข ( ๐œ‘ โ†’ ๐‘† = ( ( ( ( ๐ธ โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ด โ†‘ 2 ) ) ) + ( ( ๐ท โ†‘ 2 ) ยท ( ( ๐‘… โ†‘ 2 ) โˆ’ ( ๐ต โ†‘ 2 ) ) ) ) โˆ’ ( 2 ยท ( ( ๐ท ยท ๐ด ) ยท ( ๐ธ ยท ๐ต ) ) ) ) )
209 207 208 breqtrrd โŠข ( ๐œ‘ โ†’ 0 < ๐‘† )