Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rrndstprj1 Unicode version

Theorem rrndstprj1 26554
 Description: The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
Hypotheses
Ref Expression
rrnval.1
rrndstprj1.1
Assertion
Ref Expression
rrndstprj1

Proof of Theorem rrndstprj1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpll 730 . . . . 5
2 simprl 732 . . . . . . . . . 10
3 rrnval.1 . . . . . . . . . 10
42, 3syl6eleq 2373 . . . . . . . . 9
5 elmapi 6792 . . . . . . . . 9
64, 5syl 15 . . . . . . . 8
7 ffvelrn 5663 . . . . . . . 8
86, 7sylan 457 . . . . . . 7
9 simprr 733 . . . . . . . . . 10
109, 3syl6eleq 2373 . . . . . . . . 9
11 elmapi 6792 . . . . . . . . 9
1210, 11syl 15 . . . . . . . 8
13 ffvelrn 5663 . . . . . . . 8
1412, 13sylan 457 . . . . . . 7
158, 14resubcld 9211 . . . . . 6
1615resqcld 11271 . . . . 5
1715sqge0d 11272 . . . . 5
18 fveq2 5525 . . . . . . 7
19 fveq2 5525 . . . . . . 7
2018, 19oveq12d 5876 . . . . . 6
2120oveq1d 5873 . . . . 5
22 simplr 731 . . . . 5
231, 16, 17, 21, 22fsumge1 12255 . . . 4
24 ffvelrn 5663 . . . . . . 7
256, 22, 24syl2anc 642 . . . . . 6
26 ffvelrn 5663 . . . . . . 7
2712, 22, 26syl2anc 642 . . . . . 6
2825, 27resubcld 9211 . . . . 5
29 absresq 11787 . . . . 5
3028, 29syl 15 . . . 4
311, 16fsumrecl 12207 . . . . 5
321, 16, 17fsumge0 12253 . . . . 5
33 resqrth 11741 . . . . 5
3431, 32, 33syl2anc 642 . . . 4
3523, 30, 343brtr4d 4053 . . 3
3628recnd 8861 . . . . 5
3736abscld 11918 . . . 4
3831, 32resqrcld 11900 . . . 4
3936absge0d 11926 . . . 4
4031, 32sqrge0d 11903 . . . 4
4137, 38, 39, 40le2sqd 11280 . . 3
4235, 41mpbird 223 . 2
43 rrndstprj1.1 . . . 4
4443remetdval 18295 . . 3
4525, 27, 44syl2anc 642 . 2
463rrnmval 26552 . . . 4
47463expb 1152 . . 3