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 A A 0 0 < norm A

Proof

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