Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  normpyc Structured version   Unicode version

Theorem normpyc 22640
 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.)
Assertion
Ref Expression
normpyc

Proof of Theorem normpyc
StepHypRef Expression
1 normcl 22619 . . . . . . . . . 10
21resqcld 11541 . . . . . . . . 9
32recnd 9106 . . . . . . . 8
43addid1d 9258 . . . . . . 7
54adantr 452 . . . . . 6
6 normcl 22619 . . . . . . . . 9
76sqge0d 11542 . . . . . . . 8
87adantl 453 . . . . . . 7
96resqcld 11541 . . . . . . . 8
10 0re 9083 . . . . . . . . 9
11 leadd2 9489 . . . . . . . . 9
1210, 11mp3an1 1266 . . . . . . . 8
139, 2, 12syl2anr 465 . . . . . . 7
148, 13mpbid 202 . . . . . 6
155, 14eqbrtrrd 4226 . . . . 5
1615adantr 452 . . . 4
17 normpyth 22639 . . . . 5
1817imp 419 . . . 4
1916, 18breqtrrd 4230 . . 3
2019ex 424 . 2