This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem normlem5

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 10-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses normlem1.1 ⊢ S ∈ ℂ
normlem1.2 ⊢ F ∈ ℋ
normlem1.3 ⊢ G ∈ ℋ
normlem2.4 ⊢ B = − S ‾ ⁢ F ⋅ ih G + S ⁢ G ⋅ ih F
normlem3.5 ⊢ A = G ⋅ ih G
normlem3.6 ⊢ C = F ⋅ ih F
normlem4.7 ⊢ R ∈ ℝ
normlem4.8 ⊢ S = 1
Assertion normlem5 ⊢ 0 ≤ A ⁢ R 2 + B ⁢ R + C

Proof

Step Hyp Ref Expression
1 normlem1.1 ⊢ S ∈ ℂ
2 normlem1.2 ⊢ F ∈ ℋ
3 normlem1.3 ⊢ G ∈ ℋ
4 normlem2.4 ⊢ B = − S ‾ ⁢ F ⋅ ih G + S ⁢ G ⋅ ih F
5 normlem3.5 ⊢ A = G ⋅ ih G
6 normlem3.6 ⊢ C = F ⋅ ih F
7 normlem4.7 ⊢ R ∈ ℝ
8 normlem4.8 ⊢ S = 1
9 7 recni ⊢ R ∈ ℂ
10 1 9 mulcli ⊢ S ⁢ R ∈ ℂ
11 10 3 hvmulcli ⊢ S ⁢ R ⋅ ℎ G ∈ ℋ
12 2 11 hvsubcli ⊢ F - ℎ S ⁢ R ⋅ ℎ G ∈ ℋ
13 hiidge0 ⊢ F - ℎ S ⁢ R ⋅ ℎ G ∈ ℋ → 0 ≤ F - ℎ S ⁢ R ⋅ ℎ G ⋅ ih F - ℎ S ⁢ R ⋅ ℎ G
14 12 13 ax-mp ⊢ 0 ≤ F - ℎ S ⁢ R ⋅ ℎ G ⋅ ih F - ℎ S ⁢ R ⋅ ℎ G
15 1 2 3 4 5 6 7 8 normlem4 ⊢ F - ℎ S ⁢ R ⋅ ℎ G ⋅ ih F - ℎ S ⁢ R ⋅ ℎ G = A ⁢ R 2 + B ⁢ R + C
16 14 15 breqtri ⊢ 0 ≤ A ⁢ R 2 + B ⁢ R + C