Metamath Proof Explorer


Theorem normgt0

Description: The norm of nonzero vector is positive. (Contributed by NM, 10-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion normgt0 ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0 ↔ 0 < ( norm𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 hiidrcl ( 𝐴 ∈ ℋ → ( 𝐴 ·ih 𝐴 ) ∈ ℝ )
2 1 adantr ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ·ih 𝐴 ) ∈ ℝ )
3 ax-his4 ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 ·ih 𝐴 ) )
4 sqrtgt0 ( ( ( 𝐴 ·ih 𝐴 ) ∈ ℝ ∧ 0 < ( 𝐴 ·ih 𝐴 ) ) → 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) )
5 2 3 4 syl2anc ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0 ) → 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) )
6 5 ex ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0 → 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) )
7 oveq1 ( 𝐴 = 0 → ( 𝐴 ·ih 𝐴 ) = ( 0 ·ih 𝐴 ) )
8 hi01 ( 𝐴 ∈ ℋ → ( 0 ·ih 𝐴 ) = 0 )
9 7 8 sylan9eqr ( ( 𝐴 ∈ ℋ ∧ 𝐴 = 0 ) → ( 𝐴 ·ih 𝐴 ) = 0 )
10 9 fveq2d ( ( 𝐴 ∈ ℋ ∧ 𝐴 = 0 ) → ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) = ( √ ‘ 0 ) )
11 sqrt0 ( √ ‘ 0 ) = 0
12 10 11 syl6eq ( ( 𝐴 ∈ ℋ ∧ 𝐴 = 0 ) → ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) = 0 )
13 12 ex ( 𝐴 ∈ ℋ → ( 𝐴 = 0 → ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) = 0 ) )
14 hiidge0 ( 𝐴 ∈ ℋ → 0 ≤ ( 𝐴 ·ih 𝐴 ) )
15 1 14 resqrtcld ( 𝐴 ∈ ℋ → ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ∈ ℝ )
16 0re 0 ∈ ℝ
17 lttri3 ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) = 0 ↔ ( ¬ ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) < 0 ∧ ¬ 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) )
18 15 16 17 sylancl ( 𝐴 ∈ ℋ → ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) = 0 ↔ ( ¬ ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) < 0 ∧ ¬ 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) ) )
19 simpr ( ( ¬ ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) < 0 ∧ ¬ 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) → ¬ 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) )
20 18 19 syl6bi ( 𝐴 ∈ ℋ → ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) = 0 → ¬ 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) )
21 13 20 syld ( 𝐴 ∈ ℋ → ( 𝐴 = 0 → ¬ 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) )
22 21 necon2ad ( 𝐴 ∈ ℋ → ( 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) → 𝐴 ≠ 0 ) )
23 6 22 impbid ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0 ↔ 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) )
24 normval ( 𝐴 ∈ ℋ → ( norm𝐴 ) = ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) )
25 24 breq2d ( 𝐴 ∈ ℋ → ( 0 < ( norm𝐴 ) ↔ 0 < ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ) )
26 23 25 bitr4d ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0 ↔ 0 < ( norm𝐴 ) ) )