Metamath Proof Explorer

Theorem itscnhlinecirc02plem1

Description: Lemma 1 for itscnhlinecirc02p . (Contributed by AV, 6-Mar-2023)

Ref Expression
Hypotheses 2itscp.a 
|- ( ph -> A e. RR )
2itscp.b 
|- ( ph -> B e. RR )
2itscp.x 
|- ( ph -> X e. RR )
2itscp.y 
|- ( ph -> Y e. RR )
2itscp.d 
|- D = ( X - A )
2itscp.e 
|- E = ( B - Y )
2itscp.c 
|- C = ( ( D x. B ) + ( E x. A ) )
2itscp.r 
|- ( ph -> R e. RR )
2itscp.l 
|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) )
itscnhlinecirc02plem1.n 
|- ( ph -> B =/= Y )
Assertion itscnhlinecirc02plem1 
|- ( ph -> 0 < ( ( -u ( 2 x. ( D x. C ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 2itscp.a 
 |-  ( ph -> A e. RR )
2 2itscp.b 
 |-  ( ph -> B e. RR )
3 2itscp.x 
 |-  ( ph -> X e. RR )
4 2itscp.y 
 |-  ( ph -> Y e. RR )
5 2itscp.d 
 |-  D = ( X - A )
6 2itscp.e 
 |-  E = ( B - Y )
7 2itscp.c 
 |-  C = ( ( D x. B ) + ( E x. A ) )
8 2itscp.r 
 |-  ( ph -> R e. RR )
9 2itscp.l 
 |-  ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) < ( R ^ 2 ) )
10 itscnhlinecirc02plem1.n 
 |-  ( ph -> B =/= Y )
11 4re 
 |-  4 e. RR
12 11 a1i 
 |-  ( ph -> 4 e. RR )
13 3 1 resubcld 
 |-  ( ph -> ( X - A ) e. RR )
14 5 13 eqeltrid 
 |-  ( ph -> D e. RR )
15 14 resqcld 
 |-  ( ph -> ( D ^ 2 ) e. RR )
16 14 2 remulcld 
 |-  ( ph -> ( D x. B ) e. RR )
17 2 4 resubcld 
 |-  ( ph -> ( B - Y ) e. RR )
18 6 17 eqeltrid 
 |-  ( ph -> E e. RR )
19 18 1 remulcld 
 |-  ( ph -> ( E x. A ) e. RR )
20 16 19 readdcld 
 |-  ( ph -> ( ( D x. B ) + ( E x. A ) ) e. RR )
21 7 20 eqeltrid 
 |-  ( ph -> C e. RR )
22 21 resqcld 
 |-  ( ph -> ( C ^ 2 ) e. RR )
23 15 22 remulcld 
 |-  ( ph -> ( ( D ^ 2 ) x. ( C ^ 2 ) ) e. RR )
24 18 resqcld 
 |-  ( ph -> ( E ^ 2 ) e. RR )
25 24 15 readdcld 
 |-  ( ph -> ( ( E ^ 2 ) + ( D ^ 2 ) ) e. RR )
26 8 resqcld 
 |-  ( ph -> ( R ^ 2 ) e. RR )
27 24 26 remulcld 
 |-  ( ph -> ( ( E ^ 2 ) x. ( R ^ 2 ) ) e. RR )
28 22 27 resubcld 
 |-  ( ph -> ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) e. RR )
29 25 28 remulcld 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) e. RR )
30 23 29 resubcld 
 |-  ( ph -> ( ( ( D ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) e. RR )
31 4pos 
 |-  0 < 4
32 31 a1i 
 |-  ( ph -> 0 < 4 )
33 15 26 remulcld 
 |-  ( ph -> ( ( D ^ 2 ) x. ( R ^ 2 ) ) e. RR )
34 27 33 readdcld 
 |-  ( ph -> ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) e. RR )
35 34 22 resubcld 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( C ^ 2 ) ) e. RR )
36 6 a1i 
 |-  ( ph -> E = ( B - Y ) )
37 2 recnd 
 |-  ( ph -> B e. CC )
38 4 recnd 
 |-  ( ph -> Y e. CC )
39 37 38 10 subne0d 
 |-  ( ph -> ( B - Y ) =/= 0 )
40 36 39 eqnetrd 
 |-  ( ph -> E =/= 0 )
41 18 40 sqgt0d 
 |-  ( ph -> 0 < ( E ^ 2 ) )
42 10 orcd 
 |-  ( ph -> ( B =/= Y \/ A =/= X ) )
43 eqid 
 |-  ( ( E ^ 2 ) + ( D ^ 2 ) ) = ( ( E ^ 2 ) + ( D ^ 2 ) )
44 eqid 
 |-  ( ( ( R ^ 2 ) x. ( ( E ^ 2 ) + ( D ^ 2 ) ) ) - ( C ^ 2 ) ) = ( ( ( R ^ 2 ) x. ( ( E ^ 2 ) + ( D ^ 2 ) ) ) - ( C ^ 2 ) )
45 1 2 3 4 5 6 7 8 9 42 43 44 2itscp 
 |-  ( ph -> 0 < ( ( ( R ^ 2 ) x. ( ( E ^ 2 ) + ( D ^ 2 ) ) ) - ( C ^ 2 ) ) )
46 24 recnd 
 |-  ( ph -> ( E ^ 2 ) e. CC )
47 15 recnd 
 |-  ( ph -> ( D ^ 2 ) e. CC )
48 26 recnd 
 |-  ( ph -> ( R ^ 2 ) e. CC )
49 46 47 48 adddird 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( R ^ 2 ) ) = ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) )
50 46 47 addcld 
 |-  ( ph -> ( ( E ^ 2 ) + ( D ^ 2 ) ) e. CC )
51 50 48 mulcomd 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( R ^ 2 ) ) = ( ( R ^ 2 ) x. ( ( E ^ 2 ) + ( D ^ 2 ) ) ) )
52 49 51 eqtr3d 
 |-  ( ph -> ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) = ( ( R ^ 2 ) x. ( ( E ^ 2 ) + ( D ^ 2 ) ) ) )
53 52 oveq1d 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( C ^ 2 ) ) = ( ( ( R ^ 2 ) x. ( ( E ^ 2 ) + ( D ^ 2 ) ) ) - ( C ^ 2 ) ) )
54 45 53 breqtrrd 
 |-  ( ph -> 0 < ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( C ^ 2 ) ) )
55 24 35 41 54 mulgt0d 
 |-  ( ph -> 0 < ( ( E ^ 2 ) x. ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( C ^ 2 ) ) ) )
56 47 46 48 mul12d 
 |-  ( ph -> ( ( D ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) = ( ( E ^ 2 ) x. ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) )
57 56 oveq2d 
 |-  ( ph -> ( ( ( E ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( ( E ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( E ^ 2 ) x. ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) ) )
58 46 48 mulcld 
 |-  ( ph -> ( ( E ^ 2 ) x. ( R ^ 2 ) ) e. CC )
59 47 48 mulcld 
 |-  ( ph -> ( ( D ^ 2 ) x. ( R ^ 2 ) ) e. CC )
60 46 58 59 adddid 
 |-  ( ph -> ( ( E ^ 2 ) x. ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( ( E ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( E ^ 2 ) x. ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) ) )
61 57 60 eqtr4d 
 |-  ( ph -> ( ( ( E ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( E ^ 2 ) x. ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) ) )
62 61 oveq1d 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( E ^ 2 ) x. ( C ^ 2 ) ) ) = ( ( ( E ^ 2 ) x. ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( E ^ 2 ) x. ( C ^ 2 ) ) ) )
63 58 59 addcld 
 |-  ( ph -> ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) e. CC )
64 22 recnd 
 |-  ( ph -> ( C ^ 2 ) e. CC )
65 46 63 64 subdid 
 |-  ( ph -> ( ( E ^ 2 ) x. ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( C ^ 2 ) ) ) = ( ( ( E ^ 2 ) x. ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( E ^ 2 ) x. ( C ^ 2 ) ) ) )
66 62 65 eqtr4d 
 |-  ( ph -> ( ( ( ( E ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( E ^ 2 ) x. ( C ^ 2 ) ) ) = ( ( E ^ 2 ) x. ( ( ( ( E ^ 2 ) x. ( R ^ 2 ) ) + ( ( D ^ 2 ) x. ( R ^ 2 ) ) ) - ( C ^ 2 ) ) ) )
67 55 66 breqtrrd 
 |-  ( ph -> 0 < ( ( ( ( E ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( E ^ 2 ) x. ( C ^ 2 ) ) ) )
68 18 recnd 
 |-  ( ph -> E e. CC )
69 68 sqcld 
 |-  ( ph -> ( E ^ 2 ) e. CC )
70 14 recnd 
 |-  ( ph -> D e. CC )
71 70 sqcld 
 |-  ( ph -> ( D ^ 2 ) e. CC )
72 27 recnd 
 |-  ( ph -> ( ( E ^ 2 ) x. ( R ^ 2 ) ) e. CC )
73 mulsubaddmulsub 
 |-  ( ( ( ( E ^ 2 ) e. CC /\ ( D ^ 2 ) e. CC ) /\ ( ( C ^ 2 ) e. CC /\ ( ( E ^ 2 ) x. ( R ^ 2 ) ) e. CC ) ) -> ( ( ( D ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = ( ( ( ( E ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( E ^ 2 ) x. ( C ^ 2 ) ) ) )
74 69 71 64 72 73 syl22anc 
 |-  ( ph -> ( ( ( D ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = ( ( ( ( E ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) + ( ( D ^ 2 ) x. ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) - ( ( E ^ 2 ) x. ( C ^ 2 ) ) ) )
75 67 74 breqtrrd 
 |-  ( ph -> 0 < ( ( ( D ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) )
76 12 30 32 75 mulgt0d 
 |-  ( ph -> 0 < ( 4 x. ( ( ( D ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
77 4cn 
 |-  4 e. CC
78 77 a1i 
 |-  ( ph -> 4 e. CC )
79 21 recnd 
 |-  ( ph -> C e. CC )
80 79 sqcld 
 |-  ( ph -> ( C ^ 2 ) e. CC )
81 71 80 mulcld 
 |-  ( ph -> ( ( D ^ 2 ) x. ( C ^ 2 ) ) e. CC )
82 69 71 addcld 
 |-  ( ph -> ( ( E ^ 2 ) + ( D ^ 2 ) ) e. CC )
83 8 recnd 
 |-  ( ph -> R e. CC )
84 83 sqcld 
 |-  ( ph -> ( R ^ 2 ) e. CC )
85 69 84 mulcld 
 |-  ( ph -> ( ( E ^ 2 ) x. ( R ^ 2 ) ) e. CC )
86 80 85 subcld 
 |-  ( ph -> ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) e. CC )
87 82 86 mulcld 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) e. CC )
88 78 81 87 subdid 
 |-  ( ph -> ( 4 x. ( ( ( D ^ 2 ) x. ( C ^ 2 ) ) - ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( ( 4 x. ( ( D ^ 2 ) x. ( C ^ 2 ) ) ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
89 76 88 breqtrd 
 |-  ( ph -> 0 < ( ( 4 x. ( ( D ^ 2 ) x. ( C ^ 2 ) ) ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
90 2cnd 
 |-  ( ph -> 2 e. CC )
91 70 79 mulcld 
 |-  ( ph -> ( D x. C ) e. CC )
92 90 91 mulcld 
 |-  ( ph -> ( 2 x. ( D x. C ) ) e. CC )
93 sqneg 
 |-  ( ( 2 x. ( D x. C ) ) e. CC -> ( -u ( 2 x. ( D x. C ) ) ^ 2 ) = ( ( 2 x. ( D x. C ) ) ^ 2 ) )
94 92 93 syl 
 |-  ( ph -> ( -u ( 2 x. ( D x. C ) ) ^ 2 ) = ( ( 2 x. ( D x. C ) ) ^ 2 ) )
95 90 91 sqmuld 
 |-  ( ph -> ( ( 2 x. ( D x. C ) ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( ( D x. C ) ^ 2 ) ) )
96 sq2 
 |-  ( 2 ^ 2 ) = 4
97 96 a1i 
 |-  ( ph -> ( 2 ^ 2 ) = 4 )
98 70 79 sqmuld 
 |-  ( ph -> ( ( D x. C ) ^ 2 ) = ( ( D ^ 2 ) x. ( C ^ 2 ) ) )
99 97 98 oveq12d 
 |-  ( ph -> ( ( 2 ^ 2 ) x. ( ( D x. C ) ^ 2 ) ) = ( 4 x. ( ( D ^ 2 ) x. ( C ^ 2 ) ) ) )
100 94 95 99 3eqtrd 
 |-  ( ph -> ( -u ( 2 x. ( D x. C ) ) ^ 2 ) = ( 4 x. ( ( D ^ 2 ) x. ( C ^ 2 ) ) ) )
101 100 oveq1d 
 |-  ( ph -> ( ( -u ( 2 x. ( D x. C ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( ( 4 x. ( ( D ^ 2 ) x. ( C ^ 2 ) ) ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
102 89 101 breqtrrd 
 |-  ( ph -> 0 < ( ( -u ( 2 x. ( D x. C ) ) ^ 2 ) - ( 4 x. ( ( ( E ^ 2 ) + ( D ^ 2 ) ) x. ( ( C ^ 2 ) - ( ( E ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )