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

Theorem rrndstprj1 26539
 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 731 . . . . 5
2 simprl 733 . . . . . . . . . 10
3 rrnval.1 . . . . . . . . . 10
42, 3syl6eleq 2526 . . . . . . . . 9
5 elmapi 7038 . . . . . . . . 9
64, 5syl 16 . . . . . . . 8
76ffvelrnda 5870 . . . . . . 7
8 simprr 734 . . . . . . . . . 10
98, 3syl6eleq 2526 . . . . . . . . 9
10 elmapi 7038 . . . . . . . . 9
119, 10syl 16 . . . . . . . 8
1211ffvelrnda 5870 . . . . . . 7
137, 12resubcld 9465 . . . . . 6
1413resqcld 11549 . . . . 5
1513sqge0d 11550 . . . . 5
16 fveq2 5728 . . . . . . 7
17 fveq2 5728 . . . . . . 7
1816, 17oveq12d 6099 . . . . . 6
1918oveq1d 6096 . . . . 5
20 simplr 732 . . . . 5
211, 14, 15, 19, 20fsumge1 12576 . . . 4
226, 20ffvelrnd 5871 . . . . . 6
2311, 20ffvelrnd 5871 . . . . . 6
2422, 23resubcld 9465 . . . . 5
25 absresq 12107 . . . . 5
2624, 25syl 16 . . . 4
271, 14fsumrecl 12528 . . . . 5
281, 14, 15fsumge0 12574 . . . . 5
29 resqrth 12061 . . . . 5
3027, 28, 29syl2anc 643 . . . 4
3121, 26, 303brtr4d 4242 . . 3
3224recnd 9114 . . . . 5
3332abscld 12238 . . . 4
3427, 28resqrcld 12220 . . . 4
3532absge0d 12246 . . . 4
3627, 28sqrge0d 12223 . . . 4
3733, 34, 35, 36le2sqd 11558 . . 3
3831, 37mpbird 224 . 2
39 rrndstprj1.1 . . . 4
4039remetdval 18820 . . 3
4122, 23, 40syl2anc 643 . 2
423rrnmval 26537 . . . 4
43423expb 1154 . . 3