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

Theorem rrndstprj1 31608
 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 752 . . . . 5
2 simprl 756 . . . . . . . . . 10
3 rrnval.1 . . . . . . . . . 10
42, 3syl6eleq 2500 . . . . . . . . 9
5 elmapi 7478 . . . . . . . . 9
64, 5syl 17 . . . . . . . 8
76ffvelrnda 6009 . . . . . . 7
8 simprr 758 . . . . . . . . . 10
98, 3syl6eleq 2500 . . . . . . . . 9
10 elmapi 7478 . . . . . . . . 9
119, 10syl 17 . . . . . . . 8
1211ffvelrnda 6009 . . . . . . 7
137, 12resubcld 10028 . . . . . 6
1413resqcld 12380 . . . . 5
1513sqge0d 12381 . . . . 5
16 fveq2 5849 . . . . . . 7
17 fveq2 5849 . . . . . . 7
1816, 17oveq12d 6296 . . . . . 6
1918oveq1d 6293 . . . . 5
20 simplr 754 . . . . 5
211, 14, 15, 19, 20fsumge1 13762 . . . 4
226, 20ffvelrnd 6010 . . . . . 6
2311, 20ffvelrnd 6010 . . . . . 6
2422, 23resubcld 10028 . . . . 5
25 absresq 13284 . . . . 5
2624, 25syl 17 . . . 4
271, 14fsumrecl 13705 . . . . 5
281, 14, 15fsumge0 13760 . . . . 5
29 resqrtth 13238 . . . . 5
3027, 28, 29syl2anc 659 . . . 4
3121, 26, 303brtr4d 4425 . . 3
3224recnd 9652 . . . . 5
3332abscld 13416 . . . 4
3427, 28resqrtcld 13398 . . . 4
3532absge0d 13424 . . . 4
3627, 28sqrtge0d 13401 . . . 4
3733, 34, 35, 36le2sqd 12389 . . 3
3831, 37mpbird 232 . 2
39 rrndstprj1.1 . . . 4
4039remetdval 21586 . . 3
4122, 23, 40syl2anc 659 . 2
423rrnmval 31606 . . . 4
43423expb 1198 . . 3