Metamath Proof Explorer

Theorem normlem6

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 2-Aug-1999) (Revised by Mario Carneiro, 4-Jun-2014) (New usage is discouraged.)

Ref Expression
Hypotheses normlem1.1 
|- S e. CC
normlem1.2 
|- F e. ~H
normlem1.3 
|- G e. ~H
normlem2.4 
|- B = -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
normlem3.5 
|- A = ( G .ih G )
normlem3.6 
|- C = ( F .ih F )
normlem6.7 
|- ( abs ` S ) = 1
Assertion normlem6 
|- ( abs ` B ) <_ ( 2 x. ( ( sqrt ` A ) x. ( sqrt ` C ) ) )

Proof

Step Hyp Ref Expression
1 normlem1.1 
 |-  S e. CC
2 normlem1.2 
 |-  F e. ~H
3 normlem1.3 
 |-  G e. ~H
4 normlem2.4 
 |-  B = -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
5 normlem3.5 
 |-  A = ( G .ih G )
6 normlem3.6 
 |-  C = ( F .ih F )
7 normlem6.7 
 |-  ( abs ` S ) = 1
8 hiidrcl 
 |-  ( G e. ~H -> ( G .ih G ) e. RR )
9 3 8 ax-mp 
 |-  ( G .ih G ) e. RR
10 5 9 eqeltri 
 |-  A e. RR
11 10 a1i 
 |-  ( T. -> A e. RR )
12 1 2 3 4 normlem2 
 |-  B e. RR
13 12 a1i 
 |-  ( T. -> B e. RR )
14 hiidrcl 
 |-  ( F e. ~H -> ( F .ih F ) e. RR )
15 2 14 ax-mp 
 |-  ( F .ih F ) e. RR
16 6 15 eqeltri 
 |-  C e. RR
17 16 a1i 
 |-  ( T. -> C e. RR )
18 oveq1 
 |-  ( x = if ( x e. RR , x , 0 ) -> ( x ^ 2 ) = ( if ( x e. RR , x , 0 ) ^ 2 ) )
19 18 oveq2d 
 |-  ( x = if ( x e. RR , x , 0 ) -> ( A x. ( x ^ 2 ) ) = ( A x. ( if ( x e. RR , x , 0 ) ^ 2 ) ) )
20 oveq2 
 |-  ( x = if ( x e. RR , x , 0 ) -> ( B x. x ) = ( B x. if ( x e. RR , x , 0 ) ) )
21 19 20 oveq12d 
 |-  ( x = if ( x e. RR , x , 0 ) -> ( ( A x. ( x ^ 2 ) ) + ( B x. x ) ) = ( ( A x. ( if ( x e. RR , x , 0 ) ^ 2 ) ) + ( B x. if ( x e. RR , x , 0 ) ) ) )
22 21 oveq1d 
 |-  ( x = if ( x e. RR , x , 0 ) -> ( ( ( A x. ( x ^ 2 ) ) + ( B x. x ) ) + C ) = ( ( ( A x. ( if ( x e. RR , x , 0 ) ^ 2 ) ) + ( B x. if ( x e. RR , x , 0 ) ) ) + C ) )
23 22 breq2d 
 |-  ( x = if ( x e. RR , x , 0 ) -> ( 0 <_ ( ( ( A x. ( x ^ 2 ) ) + ( B x. x ) ) + C ) <-> 0 <_ ( ( ( A x. ( if ( x e. RR , x , 0 ) ^ 2 ) ) + ( B x. if ( x e. RR , x , 0 ) ) ) + C ) ) )
24 0re 
 |-  0 e. RR
25 24 elimel 
 |-  if ( x e. RR , x , 0 ) e. RR
26 1 2 3 4 5 6 25 7 normlem5 
 |-  0 <_ ( ( ( A x. ( if ( x e. RR , x , 0 ) ^ 2 ) ) + ( B x. if ( x e. RR , x , 0 ) ) ) + C )
27 23 26 dedth 
 |-  ( x e. RR -> 0 <_ ( ( ( A x. ( x ^ 2 ) ) + ( B x. x ) ) + C ) )
28 27 adantl 
 |-  ( ( T. /\ x e. RR ) -> 0 <_ ( ( ( A x. ( x ^ 2 ) ) + ( B x. x ) ) + C ) )
29 11 13 17 28 discr 
 |-  ( T. -> ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) <_ 0 )
30 29 mptru 
 |-  ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) <_ 0
31 12 resqcli 
 |-  ( B ^ 2 ) e. RR
32 4re 
 |-  4 e. RR
33 10 16 remulcli 
 |-  ( A x. C ) e. RR
34 32 33 remulcli 
 |-  ( 4 x. ( A x. C ) ) e. RR
35 31 34 24 lesubadd2i 
 |-  ( ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) <_ 0 <-> ( B ^ 2 ) <_ ( ( 4 x. ( A x. C ) ) + 0 ) )
36 30 35 mpbi 
 |-  ( B ^ 2 ) <_ ( ( 4 x. ( A x. C ) ) + 0 )
37 34 recni 
 |-  ( 4 x. ( A x. C ) ) e. CC
38 37 addridi 
 |-  ( ( 4 x. ( A x. C ) ) + 0 ) = ( 4 x. ( A x. C ) )
39 36 38 breqtri 
 |-  ( B ^ 2 ) <_ ( 4 x. ( A x. C ) )
40 12 sqge0i 
 |-  0 <_ ( B ^ 2 )
41 4pos 
 |-  0 < 4
42 24 32 41 ltleii 
 |-  0 <_ 4
43 hiidge0 
 |-  ( G e. ~H -> 0 <_ ( G .ih G ) )
44 3 43 ax-mp 
 |-  0 <_ ( G .ih G )
45 44 5 breqtrri 
 |-  0 <_ A
46 hiidge0 
 |-  ( F e. ~H -> 0 <_ ( F .ih F ) )
47 2 46 ax-mp 
 |-  0 <_ ( F .ih F )
48 47 6 breqtrri 
 |-  0 <_ C
49 10 16 mulge0i 
 |-  ( ( 0 <_ A /\ 0 <_ C ) -> 0 <_ ( A x. C ) )
50 45 48 49 mp2an 
 |-  0 <_ ( A x. C )
51 32 33 mulge0i 
 |-  ( ( 0 <_ 4 /\ 0 <_ ( A x. C ) ) -> 0 <_ ( 4 x. ( A x. C ) ) )
52 42 50 51 mp2an 
 |-  0 <_ ( 4 x. ( A x. C ) )
53 31 34 sqrtlei 
 |-  ( ( 0 <_ ( B ^ 2 ) /\ 0 <_ ( 4 x. ( A x. C ) ) ) -> ( ( B ^ 2 ) <_ ( 4 x. ( A x. C ) ) <-> ( sqrt ` ( B ^ 2 ) ) <_ ( sqrt ` ( 4 x. ( A x. C ) ) ) ) )
54 40 52 53 mp2an 
 |-  ( ( B ^ 2 ) <_ ( 4 x. ( A x. C ) ) <-> ( sqrt ` ( B ^ 2 ) ) <_ ( sqrt ` ( 4 x. ( A x. C ) ) ) )
55 39 54 mpbi 
 |-  ( sqrt ` ( B ^ 2 ) ) <_ ( sqrt ` ( 4 x. ( A x. C ) ) )
56 12 absrei 
 |-  ( abs ` B ) = ( sqrt ` ( B ^ 2 ) )
57 32 33 42 50 sqrtmulii 
 |-  ( sqrt ` ( 4 x. ( A x. C ) ) ) = ( ( sqrt ` 4 ) x. ( sqrt ` ( A x. C ) ) )
58 sqrt4 
 |-  ( sqrt ` 4 ) = 2
59 10 16 45 48 sqrtmulii 
 |-  ( sqrt ` ( A x. C ) ) = ( ( sqrt ` A ) x. ( sqrt ` C ) )
60 58 59 oveq12i 
 |-  ( ( sqrt ` 4 ) x. ( sqrt ` ( A x. C ) ) ) = ( 2 x. ( ( sqrt ` A ) x. ( sqrt ` C ) ) )
61 57 60 eqtr2i 
 |-  ( 2 x. ( ( sqrt ` A ) x. ( sqrt ` C ) ) ) = ( sqrt ` ( 4 x. ( A x. C ) ) )
62 55 56 61 3brtr4i 
 |-  ( abs ` B ) <_ ( 2 x. ( ( sqrt ` A ) x. ( sqrt ` C ) ) )