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

Metamath Proof Explorer

Theorem hiidge0

Description: Inner product with self is not negative. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion hiidge0 ⊢ A ∈ ℋ → 0 ≤ A ⋅ ih A

Proof

Step Hyp Ref Expression
1 pm2.1 ⊢ ¬ A = 0 ℎ ∨ A = 0 ℎ
2 df-ne ⊢ A ≠ 0 ℎ ↔ ¬ A = 0 ℎ
3 ax-his4 ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < A ⋅ ih A
4 2 3 sylan2br ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 0 < A ⋅ ih A
5 4 ex ⊢ A ∈ ℋ → ¬ A = 0 ℎ → 0 < A ⋅ ih A
6 oveq1 ⊢ A = 0 ℎ → A ⋅ ih A = 0 ℎ ⋅ ih A
7 hi01 ⊢ A ∈ ℋ → 0 ℎ ⋅ ih A = 0
8 6 7 sylan9eqr ⊢ A ∈ ℋ ∧ A = 0 ℎ → A ⋅ ih A = 0
9 8 eqcomd ⊢ A ∈ ℋ ∧ A = 0 ℎ → 0 = A ⋅ ih A
10 9 ex ⊢ A ∈ ℋ → A = 0 ℎ → 0 = A ⋅ ih A
11 5 10 orim12d ⊢ A ∈ ℋ → ¬ A = 0 ℎ ∨ A = 0 ℎ → 0 < A ⋅ ih A ∨ 0 = A ⋅ ih A
12 1 11 mpi ⊢ A ∈ ℋ → 0 < A ⋅ ih A ∨ 0 = A ⋅ ih A
13 0re ⊢ 0 ∈ ℝ
14 hiidrcl ⊢ A ∈ ℋ → A ⋅ ih A ∈ ℝ
15 leloe ⊢ 0 ∈ ℝ ∧ A ⋅ ih A ∈ ℝ → 0 ≤ A ⋅ ih A ↔ 0 < A ⋅ ih A ∨ 0 = A ⋅ ih A
16 13 14 15 sylancr ⊢ A ∈ ℋ → 0 ≤ A ⋅ ih A ↔ 0 < A ⋅ ih A ∨ 0 = A ⋅ ih A
17 12 16 mpbird ⊢ A ∈ ℋ → 0 ≤ A ⋅ ih A