Metamath Proof Explorer


Theorem normpyc

Description: Corollary to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of Beran p. 98. (Contributed by NM, 26-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion normpyc A B A ih B = 0 norm A norm A + B

Proof

Step Hyp Ref Expression
1 normcl A norm A
2 1 resqcld A norm A 2
3 2 recnd A norm A 2
4 3 addid1d A norm A 2 + 0 = norm A 2
5 4 adantr A B norm A 2 + 0 = norm A 2
6 normcl B norm B
7 6 sqge0d B 0 norm B 2
8 7 adantl A B 0 norm B 2
9 6 resqcld B norm B 2
10 0re 0
11 leadd2 0 norm B 2 norm A 2 0 norm B 2 norm A 2 + 0 norm A 2 + norm B 2
12 10 11 mp3an1 norm B 2 norm A 2 0 norm B 2 norm A 2 + 0 norm A 2 + norm B 2
13 9 2 12 syl2anr A B 0 norm B 2 norm A 2 + 0 norm A 2 + norm B 2
14 8 13 mpbid A B norm A 2 + 0 norm A 2 + norm B 2
15 5 14 eqbrtrrd A B norm A 2 norm A 2 + norm B 2
16 15 adantr A B A ih B = 0 norm A 2 norm A 2 + norm B 2
17 normpyth A B A ih B = 0 norm A + B 2 = norm A 2 + norm B 2
18 17 imp A B A ih B = 0 norm A + B 2 = norm A 2 + norm B 2
19 16 18 breqtrrd A B A ih B = 0 norm A 2 norm A + B 2
20 19 ex A B A ih B = 0 norm A 2 norm A + B 2
21 1 adantr A B norm A
22 hvaddcl A B A + B
23 normcl A + B norm A + B
24 22 23 syl A B norm A + B
25 normge0 A 0 norm A
26 25 adantr A B 0 norm A
27 normge0 A + B 0 norm A + B
28 22 27 syl A B 0 norm A + B
29 21 24 26 28 le2sqd A B norm A norm A + B norm A 2 norm A + B 2
30 20 29 sylibrd A B A ih B = 0 norm A norm A + B