Metamath Proof Explorer

Theorem itsclc0yqsollem2

Description: Lemma 2 for itsclc0yqsol . (Contributed by AV, 6-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itscnhlc0yqe.t 
|- T = -u ( 2 x. ( B x. C ) )
itscnhlc0yqe.u 
|- U = ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
itsclc0yqsollem1.d 
|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
Assertion itsclc0yqsollem2 
|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( sqrt ` ( ( T ^ 2 ) - ( 4 x. ( Q x. U ) ) ) ) = ( ( 2 x. ( abs ` A ) ) x. ( sqrt ` D ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q 
 |-  Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
2 itscnhlc0yqe.t 
 |-  T = -u ( 2 x. ( B x. C ) )
3 itscnhlc0yqe.u 
 |-  U = ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
4 itsclc0yqsollem1.d 
 |-  D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
5 recn 
 |-  ( A e. RR -> A e. CC )
6 recn 
 |-  ( B e. RR -> B e. CC )
7 recn 
 |-  ( C e. RR -> C e. CC )
8 5 6 7 3anim123i 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A e. CC /\ B e. CC /\ C e. CC ) )
9 recn 
 |-  ( R e. RR -> R e. CC )
10 8 9 anim12i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) )
11 10 3adant3 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) )
12 1 2 3 4 itsclc0yqsollem1 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ R e. CC ) -> ( ( T ^ 2 ) - ( 4 x. ( Q x. U ) ) ) = ( ( 4 x. ( A ^ 2 ) ) x. D ) )
13 11 12 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( ( T ^ 2 ) - ( 4 x. ( Q x. U ) ) ) = ( ( 4 x. ( A ^ 2 ) ) x. D ) )
14 13 fveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( sqrt ` ( ( T ^ 2 ) - ( 4 x. ( Q x. U ) ) ) ) = ( sqrt ` ( ( 4 x. ( A ^ 2 ) ) x. D ) ) )
15 4re 
 |-  4 e. RR
16 15 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> 4 e. RR )
17 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
18 17 resqcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A ^ 2 ) e. RR )
19 18 3ad2ant1 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( A ^ 2 ) e. RR )
20 16 19 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( 4 x. ( A ^ 2 ) ) e. RR )
21 0re 
 |-  0 e. RR
22 4pos 
 |-  0 < 4
23 21 15 22 ltleii 
 |-  0 <_ 4
24 23 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> 0 <_ 4 )
25 17 sqge0d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> 0 <_ ( A ^ 2 ) )
26 25 3ad2ant1 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> 0 <_ ( A ^ 2 ) )
27 16 19 24 26 mulge0d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> 0 <_ ( 4 x. ( A ^ 2 ) ) )
28 simp2 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> R e. RR )
29 28 resqcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( R ^ 2 ) e. RR )
30 1 resum2sqcl 
 |-  ( ( A e. RR /\ B e. RR ) -> Q e. RR )
31 30 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> Q e. RR )
32 31 3ad2ant1 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> Q e. RR )
33 29 32 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( ( R ^ 2 ) x. Q ) e. RR )
34 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
35 34 resqcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C ^ 2 ) e. RR )
36 35 3ad2ant1 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( C ^ 2 ) e. RR )
37 33 36 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) e. RR )
38 4 37 eqeltrid 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> D e. RR )
39 simp3 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> 0 <_ D )
40 20 27 38 39 sqrtmuld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( sqrt ` ( ( 4 x. ( A ^ 2 ) ) x. D ) ) = ( ( sqrt ` ( 4 x. ( A ^ 2 ) ) ) x. ( sqrt ` D ) ) )
41 15 23 pm3.2i 
 |-  ( 4 e. RR /\ 0 <_ 4 )
42 41 a1i 
 |-  ( A e. RR -> ( 4 e. RR /\ 0 <_ 4 ) )
43 resqcl 
 |-  ( A e. RR -> ( A ^ 2 ) e. RR )
44 sqge0 
 |-  ( A e. RR -> 0 <_ ( A ^ 2 ) )
45 sqrtmul 
 |-  ( ( ( 4 e. RR /\ 0 <_ 4 ) /\ ( ( A ^ 2 ) e. RR /\ 0 <_ ( A ^ 2 ) ) ) -> ( sqrt ` ( 4 x. ( A ^ 2 ) ) ) = ( ( sqrt ` 4 ) x. ( sqrt ` ( A ^ 2 ) ) ) )
46 42 43 44 45 syl12anc 
 |-  ( A e. RR -> ( sqrt ` ( 4 x. ( A ^ 2 ) ) ) = ( ( sqrt ` 4 ) x. ( sqrt ` ( A ^ 2 ) ) ) )
47 46 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( sqrt ` ( 4 x. ( A ^ 2 ) ) ) = ( ( sqrt ` 4 ) x. ( sqrt ` ( A ^ 2 ) ) ) )
48 47 3ad2ant1 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( sqrt ` ( 4 x. ( A ^ 2 ) ) ) = ( ( sqrt ` 4 ) x. ( sqrt ` ( A ^ 2 ) ) ) )
49 sqrt4 
 |-  ( sqrt ` 4 ) = 2
50 49 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( sqrt ` 4 ) = 2 )
51 absre 
 |-  ( A e. RR -> ( abs ` A ) = ( sqrt ` ( A ^ 2 ) ) )
52 51 eqcomd 
 |-  ( A e. RR -> ( sqrt ` ( A ^ 2 ) ) = ( abs ` A ) )
53 52 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( sqrt ` ( A ^ 2 ) ) = ( abs ` A ) )
54 53 3ad2ant1 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( sqrt ` ( A ^ 2 ) ) = ( abs ` A ) )
55 50 54 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( ( sqrt ` 4 ) x. ( sqrt ` ( A ^ 2 ) ) ) = ( 2 x. ( abs ` A ) ) )
56 48 55 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( sqrt ` ( 4 x. ( A ^ 2 ) ) ) = ( 2 x. ( abs ` A ) ) )
57 56 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( ( sqrt ` ( 4 x. ( A ^ 2 ) ) ) x. ( sqrt ` D ) ) = ( ( 2 x. ( abs ` A ) ) x. ( sqrt ` D ) ) )
58 14 40 57 3eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( sqrt ` ( ( T ^ 2 ) - ( 4 x. ( Q x. U ) ) ) ) = ( ( 2 x. ( abs ` A ) ) x. ( sqrt ` D ) ) )