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 ⊢ 𝑆 ∈ ℂ
normlem1.2 ⊢ 𝐹 ∈ ℋ
normlem1.3 ⊢ 𝐺 ∈ ℋ
normlem2.4 ⊢ 𝐵 = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
normlem3.5 ⊢ 𝐴 = ( 𝐺 ·ih 𝐺 )
normlem3.6 ⊢ 𝐶 = ( 𝐹 ·ih 𝐹 )
normlem6.7 ⊢ ( abs ‘ 𝑆 ) = 1
Assertion normlem6 ( abs ‘ 𝐵 ) ≤ ( 2 · ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 normlem1.1 ⊢ 𝑆 ∈ ℂ
2 normlem1.2 ⊢ 𝐹 ∈ ℋ
3 normlem1.3 ⊢ 𝐺 ∈ ℋ
4 normlem2.4 ⊢ 𝐵 = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
5 normlem3.5 ⊢ 𝐴 = ( 𝐺 ·ih 𝐺 )
6 normlem3.6 ⊢ 𝐶 = ( 𝐹 ·ih 𝐹 )
7 normlem6.7 ⊢ ( abs ‘ 𝑆 ) = 1
8 hiidrcl ⊢ ( 𝐺 ∈ ℋ → ( 𝐺 ·ih 𝐺 ) ∈ ℝ )
9 3 8 ax-mp ⊢ ( 𝐺 ·ih 𝐺 ) ∈ ℝ
10 5 9 eqeltri ⊢ 𝐴 ∈ ℝ
11 10 a1i ⊢ ( ⊤ → 𝐴 ∈ ℝ )
12 1 2 3 4 normlem2 ⊢ 𝐵 ∈ ℝ
13 12 a1i ⊢ ( ⊤ → 𝐵 ∈ ℝ )
14 hiidrcl ⊢ ( 𝐹 ∈ ℋ → ( 𝐹 ·ih 𝐹 ) ∈ ℝ )
15 2 14 ax-mp ⊢ ( 𝐹 ·ih 𝐹 ) ∈ ℝ
16 6 15 eqeltri ⊢ 𝐶 ∈ ℝ
17 16 a1i ⊢ ( ⊤ → 𝐶 ∈ ℝ )
18 oveq1 ⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( 𝑥 ↑ 2 ) = ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) )
19 18 oveq2d ⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( 𝐴 · ( 𝑥 ↑ 2 ) ) = ( 𝐴 · ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) ) )
20 oveq2 ⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ) )
21 19 20 oveq12d ⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) = ( ( 𝐴 · ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) ) + ( 𝐵 · if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ) ) )
22 21 oveq1d ⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) = ( ( ( 𝐴 · ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) ) + ( 𝐵 · if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ) ) + 𝐶 ) )
23 22 breq2d ⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) ↔ 0 ≤ ( ( ( 𝐴 · ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) ) + ( 𝐵 · if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ) ) + 𝐶 ) ) )
24 0re ⊢ 0 ∈ ℝ
25 24 elimel ⊢ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ∈ ℝ
26 1 2 3 4 5 6 25 7 normlem5 ⊢ 0 ≤ ( ( ( 𝐴 · ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) ) + ( 𝐵 · if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ) ) + 𝐶 )
27 23 26 dedth ⊢ ( 𝑥 ∈ ℝ → 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) )
28 27 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) )
29 11 13 17 28 discr ⊢ ( ⊤ → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ≤ 0 )
30 29 mptru ⊢ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ≤ 0
31 12 resqcli ⊢ ( 𝐵 ↑ 2 ) ∈ ℝ
32 4re ⊢ 4 ∈ ℝ
33 10 16 remulcli ⊢ ( 𝐴 · 𝐶 ) ∈ ℝ
34 32 33 remulcli ⊢ ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℝ
35 31 34 24 lesubadd2i ⊢ ( ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ≤ 0 ↔ ( 𝐵 ↑ 2 ) ≤ ( ( 4 · ( 𝐴 · 𝐶 ) ) + 0 ) )
36 30 35 mpbi ⊢ ( 𝐵 ↑ 2 ) ≤ ( ( 4 · ( 𝐴 · 𝐶 ) ) + 0 )
37 34 recni ⊢ ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℂ
38 37 addid1i ⊢ ( ( 4 · ( 𝐴 · 𝐶 ) ) + 0 ) = ( 4 · ( 𝐴 · 𝐶 ) )
39 36 38 breqtri ⊢ ( 𝐵 ↑ 2 ) ≤ ( 4 · ( 𝐴 · 𝐶 ) )
40 12 sqge0i ⊢ 0 ≤ ( 𝐵 ↑ 2 )
41 4pos ⊢ 0 < 4
42 24 32 41 ltleii ⊢ 0 ≤ 4
43 hiidge0 ⊢ ( 𝐺 ∈ ℋ → 0 ≤ ( 𝐺 ·ih 𝐺 ) )
44 3 43 ax-mp ⊢ 0 ≤ ( 𝐺 ·ih 𝐺 )
45 44 5 breqtrri ⊢ 0 ≤ 𝐴
46 hiidge0 ⊢ ( 𝐹 ∈ ℋ → 0 ≤ ( 𝐹 ·ih 𝐹 ) )
47 2 46 ax-mp ⊢ 0 ≤ ( 𝐹 ·ih 𝐹 )
48 47 6 breqtrri ⊢ 0 ≤ 𝐶
49 10 16 mulge0i ⊢ ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) → 0 ≤ ( 𝐴 · 𝐶 ) )
50 45 48 49 mp2an ⊢ 0 ≤ ( 𝐴 · 𝐶 )
51 32 33 mulge0i ⊢ ( ( 0 ≤ 4 ∧ 0 ≤ ( 𝐴 · 𝐶 ) ) → 0 ≤ ( 4 · ( 𝐴 · 𝐶 ) ) )
52 42 50 51 mp2an ⊢ 0 ≤ ( 4 · ( 𝐴 · 𝐶 ) )
53 31 34 sqrtlei ⊢ ( ( 0 ≤ ( 𝐵 ↑ 2 ) ∧ 0 ≤ ( 4 · ( 𝐴 · 𝐶 ) ) ) → ( ( 𝐵 ↑ 2 ) ≤ ( 4 · ( 𝐴 · 𝐶 ) ) ↔ ( √ ‘ ( 𝐵 ↑ 2 ) ) ≤ ( √ ‘ ( 4 · ( 𝐴 · 𝐶 ) ) ) ) )
54 40 52 53 mp2an ⊢ ( ( 𝐵 ↑ 2 ) ≤ ( 4 · ( 𝐴 · 𝐶 ) ) ↔ ( √ ‘ ( 𝐵 ↑ 2 ) ) ≤ ( √ ‘ ( 4 · ( 𝐴 · 𝐶 ) ) ) )
55 39 54 mpbi ⊢ ( √ ‘ ( 𝐵 ↑ 2 ) ) ≤ ( √ ‘ ( 4 · ( 𝐴 · 𝐶 ) ) )
56 12 absrei ⊢ ( abs ‘ 𝐵 ) = ( √ ‘ ( 𝐵 ↑ 2 ) )
57 32 33 42 50 sqrtmulii ⊢ ( √ ‘ ( 4 · ( 𝐴 · 𝐶 ) ) ) = ( ( √ ‘ 4 ) · ( √ ‘ ( 𝐴 · 𝐶 ) ) )
58 sqrt4 ⊢ ( √ ‘ 4 ) = 2
59 10 16 45 48 sqrtmulii ⊢ ( √ ‘ ( 𝐴 · 𝐶 ) ) = ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐶 ) )
60 58 59 oveq12i ⊢ ( ( √ ‘ 4 ) · ( √ ‘ ( 𝐴 · 𝐶 ) ) ) = ( 2 · ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐶 ) ) )
61 57 60 eqtr2i ⊢ ( 2 · ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐶 ) ) ) = ( √ ‘ ( 4 · ( 𝐴 · 𝐶 ) ) )
62 55 56 61 3brtr4i ⊢ ( abs ‘ 𝐵 ) ≤ ( 2 · ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐶 ) ) )