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

Theorem pjhthlem1 26879
Description: Lemma for pjhth 26881. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
pjhth.1  |-  H  e. 
CH
pjhth.2  |-  ( ph  ->  A  e.  ~H )
pjhth.3  |-  ( ph  ->  B  e.  H )
pjhth.4  |-  ( ph  ->  C  e.  H )
pjhth.5  |-  ( ph  ->  A. x  e.  H  ( normh `  ( A  -h  B ) )  <_ 
( normh `  ( A  -h  x ) ) )
pjhth.6  |-  T  =  ( ( ( A  -h  B )  .ih  C )  /  ( ( C  .ih  C )  +  1 ) )
Assertion
Ref Expression
pjhthlem1  |-  ( ph  ->  ( ( A  -h  B )  .ih  C
)  =  0 )
Distinct variable groups:    x, A    x, B    x, C    x, H    x, T
Allowed substitution hint:    ph( x)

Proof of Theorem pjhthlem1
StepHypRef Expression
1 pjhth.2 . . . 4  |-  ( ph  ->  A  e.  ~H )
2 pjhth.3 . . . . 5  |-  ( ph  ->  B  e.  H )
3 pjhth.1 . . . . . 6  |-  H  e. 
CH
43cheli 26720 . . . . 5  |-  ( B  e.  H  ->  B  e.  ~H )
52, 4syl 17 . . . 4  |-  ( ph  ->  B  e.  ~H )
6 hvsubcl 26505 . . . 4  |-  ( ( A  e.  ~H  /\  B  e.  ~H )  ->  ( A  -h  B
)  e.  ~H )
71, 5, 6syl2anc 665 . . 3  |-  ( ph  ->  ( A  -h  B
)  e.  ~H )
8 pjhth.4 . . . 4  |-  ( ph  ->  C  e.  H )
93cheli 26720 . . . 4  |-  ( C  e.  H  ->  C  e.  ~H )
108, 9syl 17 . . 3  |-  ( ph  ->  C  e.  ~H )
11 hicl 26568 . . 3  |-  ( ( ( A  -h  B
)  e.  ~H  /\  C  e.  ~H )  ->  ( ( A  -h  B )  .ih  C
)  e.  CC )
127, 10, 11syl2anc 665 . 2  |-  ( ph  ->  ( ( A  -h  B )  .ih  C
)  e.  CC )
1312abscld 13476 . . . 4  |-  ( ph  ->  ( abs `  (
( A  -h  B
)  .ih  C )
)  e.  RR )
1413recnd 9668 . . 3  |-  ( ph  ->  ( abs `  (
( A  -h  B
)  .ih  C )
)  e.  CC )
1513resqcld 12439 . . . . . . 7  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  e.  RR )
1615renegcld 10045 . . . . . 6  |-  ( ph  -> 
-u ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  e.  RR )
17 hiidrcl 26583 . . . . . . . 8  |-  ( C  e.  ~H  ->  ( C  .ih  C )  e.  RR )
1810, 17syl 17 . . . . . . 7  |-  ( ph  ->  ( C  .ih  C
)  e.  RR )
19 2re 10679 . . . . . . 7  |-  2  e.  RR
20 readdcl 9621 . . . . . . 7  |-  ( ( ( C  .ih  C
)  e.  RR  /\  2  e.  RR )  ->  ( ( C  .ih  C )  +  2 )  e.  RR )
2118, 19, 20sylancl 666 . . . . . 6  |-  ( ph  ->  ( ( C  .ih  C )  +  2 )  e.  RR )
22 0red 9643 . . . . . . 7  |-  ( ph  ->  0  e.  RR )
23 peano2re 9805 . . . . . . . 8  |-  ( ( C  .ih  C )  e.  RR  ->  (
( C  .ih  C
)  +  1 )  e.  RR )
2418, 23syl 17 . . . . . . 7  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  e.  RR )
25 hiidge0 26586 . . . . . . . . 9  |-  ( C  e.  ~H  ->  0  <_  ( C  .ih  C
) )
2610, 25syl 17 . . . . . . . 8  |-  ( ph  ->  0  <_  ( C  .ih  C ) )
2718ltp1d 10537 . . . . . . . 8  |-  ( ph  ->  ( C  .ih  C
)  <  ( ( C  .ih  C )  +  1 ) )
2822, 18, 24, 26, 27lelttrd 9792 . . . . . . 7  |-  ( ph  ->  0  <  ( ( C  .ih  C )  +  1 ) )
2924ltp1d 10537 . . . . . . . 8  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  <  ( ( ( C  .ih  C )  +  1 )  +  1 ) )
3018recnd 9668 . . . . . . . . . 10  |-  ( ph  ->  ( C  .ih  C
)  e.  CC )
31 ax-1cn 9596 . . . . . . . . . . 11  |-  1  e.  CC
32 addass 9625 . . . . . . . . . . 11  |-  ( ( ( C  .ih  C
)  e.  CC  /\  1  e.  CC  /\  1  e.  CC )  ->  (
( ( C  .ih  C )  +  1 )  +  1 )  =  ( ( C  .ih  C )  +  ( 1  +  1 ) ) )
3331, 31, 32mp3an23 1352 . . . . . . . . . 10  |-  ( ( C  .ih  C )  e.  CC  ->  (
( ( C  .ih  C )  +  1 )  +  1 )  =  ( ( C  .ih  C )  +  ( 1  +  1 ) ) )
3430, 33syl 17 . . . . . . . . 9  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 )  +  1 )  =  ( ( C  .ih  C )  +  ( 1  +  1 ) ) )
35 df-2 10668 . . . . . . . . . 10  |-  2  =  ( 1  +  1 )
3635oveq2i 6316 . . . . . . . . 9  |-  ( ( C  .ih  C )  +  2 )  =  ( ( C  .ih  C )  +  ( 1  +  1 ) )
3734, 36syl6reqr 2489 . . . . . . . 8  |-  ( ph  ->  ( ( C  .ih  C )  +  2 )  =  ( ( ( C  .ih  C )  +  1 )  +  1 ) )
3829, 37breqtrrd 4452 . . . . . . 7  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  <  ( ( C 
.ih  C )  +  2 ) )
3922, 24, 21, 28, 38lttrd 9795 . . . . . 6  |-  ( ph  ->  0  <  ( ( C  .ih  C )  +  2 ) )
403chshii 26715 . . . . . . . . . . . . . . 15  |-  H  e.  SH
4140a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  H  e.  SH )
42 pjhth.6 . . . . . . . . . . . . . . . 16  |-  T  =  ( ( ( A  -h  B )  .ih  C )  /  ( ( C  .ih  C )  +  1 ) )
4324recnd 9668 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  e.  CC )
4418, 26ge0p1rpd 11368 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  e.  RR+ )
4544rpne0d 11346 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  =/=  0 )
4612, 43, 45divcld 10382 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  C )  /  ( ( C  .ih  C )  +  1 ) )  e.  CC )
4742, 46syl5eqel 2521 . . . . . . . . . . . . . . 15  |-  ( ph  ->  T  e.  CC )
48 shmulcl 26706 . . . . . . . . . . . . . . 15  |-  ( ( H  e.  SH  /\  T  e.  CC  /\  C  e.  H )  ->  ( T  .h  C )  e.  H )
4941, 47, 8, 48syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  .h  C
)  e.  H )
50 shaddcl 26705 . . . . . . . . . . . . . 14  |-  ( ( H  e.  SH  /\  B  e.  H  /\  ( T  .h  C
)  e.  H )  ->  ( B  +h  ( T  .h  C
) )  e.  H
)
5141, 2, 49, 50syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  +h  ( T  .h  C )
)  e.  H )
52 pjhth.5 . . . . . . . . . . . . 13  |-  ( ph  ->  A. x  e.  H  ( normh `  ( A  -h  B ) )  <_ 
( normh `  ( A  -h  x ) ) )
53 oveq2 6313 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( B  +h  ( T  .h  C
) )  ->  ( A  -h  x )  =  ( A  -h  ( B  +h  ( T  .h  C ) ) ) )
5453fveq2d 5885 . . . . . . . . . . . . . . 15  |-  ( x  =  ( B  +h  ( T  .h  C
) )  ->  ( normh `  ( A  -h  x ) )  =  ( normh `  ( A  -h  ( B  +h  ( T  .h  C )
) ) ) )
5554breq2d 4438 . . . . . . . . . . . . . 14  |-  ( x  =  ( B  +h  ( T  .h  C
) )  ->  (
( normh `  ( A  -h  B ) )  <_ 
( normh `  ( A  -h  x ) )  <->  ( normh `  ( A  -h  B
) )  <_  ( normh `  ( A  -h  ( B  +h  ( T  .h  C )
) ) ) ) )
5655rspcv 3184 . . . . . . . . . . . . 13  |-  ( ( B  +h  ( T  .h  C ) )  e.  H  ->  ( A. x  e.  H  ( normh `  ( A  -h  B ) )  <_ 
( normh `  ( A  -h  x ) )  -> 
( normh `  ( A  -h  B ) )  <_ 
( normh `  ( A  -h  ( B  +h  ( T  .h  C )
) ) ) ) )
5751, 52, 56sylc 62 . . . . . . . . . . . 12  |-  ( ph  ->  ( normh `  ( A  -h  B ) )  <_ 
( normh `  ( A  -h  ( B  +h  ( T  .h  C )
) ) ) )
583cheli 26720 . . . . . . . . . . . . . . 15  |-  ( ( T  .h  C )  e.  H  ->  ( T  .h  C )  e.  ~H )
5949, 58syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  .h  C
)  e.  ~H )
60 hvsubass 26532 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ~H  /\  B  e.  ~H  /\  ( T  .h  C )  e.  ~H )  ->  (
( A  -h  B
)  -h  ( T  .h  C ) )  =  ( A  -h  ( B  +h  ( T  .h  C )
) ) )
611, 5, 59, 60syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A  -h  B )  -h  ( T  .h  C )
)  =  ( A  -h  ( B  +h  ( T  .h  C
) ) ) )
6261fveq2d 5885 . . . . . . . . . . . 12  |-  ( ph  ->  ( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) )  =  ( normh `  ( A  -h  ( B  +h  ( T  .h  C )
) ) ) )
6357, 62breqtrrd 4452 . . . . . . . . . . 11  |-  ( ph  ->  ( normh `  ( A  -h  B ) )  <_ 
( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) )
64 normcl 26613 . . . . . . . . . . . . 13  |-  ( ( A  -h  B )  e.  ~H  ->  ( normh `  ( A  -h  B ) )  e.  RR )
657, 64syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( normh `  ( A  -h  B ) )  e.  RR )
66 hvsubcl 26505 . . . . . . . . . . . . . 14  |-  ( ( ( A  -h  B
)  e.  ~H  /\  ( T  .h  C
)  e.  ~H )  ->  ( ( A  -h  B )  -h  ( T  .h  C )
)  e.  ~H )
677, 59, 66syl2anc 665 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A  -h  B )  -h  ( T  .h  C )
)  e.  ~H )
68 normcl 26613 . . . . . . . . . . . . 13  |-  ( ( ( A  -h  B
)  -h  ( T  .h  C ) )  e.  ~H  ->  ( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) )  e.  RR )
6967, 68syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) )  e.  RR )
70 normge0 26614 . . . . . . . . . . . . 13  |-  ( ( A  -h  B )  e.  ~H  ->  0  <_  ( normh `  ( A  -h  B ) ) )
717, 70syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( normh `  ( A  -h  B
) ) )
7222, 65, 69, 71, 63letrd 9791 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( normh `  ( ( A  -h  B )  -h  ( T  .h  C )
) ) )
7365, 69, 71, 72le2sqd 12448 . . . . . . . . . . 11  |-  ( ph  ->  ( ( normh `  ( A  -h  B ) )  <_  ( normh `  (
( A  -h  B
)  -h  ( T  .h  C ) ) )  <->  ( ( normh `  ( A  -h  B
) ) ^ 2 )  <_  ( ( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) ^
2 ) ) )
7463, 73mpbid 213 . . . . . . . . . 10  |-  ( ph  ->  ( ( normh `  ( A  -h  B ) ) ^ 2 )  <_ 
( ( normh `  (
( A  -h  B
)  -h  ( T  .h  C ) ) ) ^ 2 ) )
7569resqcld 12439 . . . . . . . . . . 11  |-  ( ph  ->  ( ( normh `  (
( A  -h  B
)  -h  ( T  .h  C ) ) ) ^ 2 )  e.  RR )
7665resqcld 12439 . . . . . . . . . . 11  |-  ( ph  ->  ( ( normh `  ( A  -h  B ) ) ^ 2 )  e.  RR )
7775, 76subge0d 10202 . . . . . . . . . 10  |-  ( ph  ->  ( 0  <_  (
( ( normh `  (
( A  -h  B
)  -h  ( T  .h  C ) ) ) ^ 2 )  -  ( ( normh `  ( A  -h  B
) ) ^ 2 ) )  <->  ( ( normh `  ( A  -h  B ) ) ^
2 )  <_  (
( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) ^
2 ) ) )
7874, 77mpbird 235 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( (
( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) ^
2 )  -  (
( normh `  ( A  -h  B ) ) ^
2 ) ) )
79 2z 10969 . . . . . . . . . . . . . . . 16  |-  2  e.  ZZ
80 rpexpcl 12288 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( C  .ih  C )  +  1 )  e.  RR+  /\  2  e.  ZZ )  ->  (
( ( C  .ih  C )  +  1 ) ^ 2 )  e.  RR+ )
8144, 79, 80sylancl 666 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 ) ^ 2 )  e.  RR+ )
8215, 81rerpdivcld 11369 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  e.  RR )
8382, 21remulcld 9670 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  2 ) )  e.  RR )
8483recnd 9668 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  2 ) )  e.  CC )
8584negcld 9972 . . . . . . . . . . 11  |-  ( ph  -> 
-u ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  2 ) )  e.  CC )
86 hicl 26568 . . . . . . . . . . . 12  |-  ( ( ( A  -h  B
)  e.  ~H  /\  ( A  -h  B
)  e.  ~H )  ->  ( ( A  -h  B )  .ih  ( A  -h  B ) )  e.  CC )
877, 7, 86syl2anc 665 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( A  -h  B ) )  e.  CC )
8885, 87pncand 9986 . . . . . . . . . 10  |-  ( ph  ->  ( ( -u (
( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  x.  ( ( C 
.ih  C )  +  2 ) )  +  ( ( A  -h  B )  .ih  ( A  -h  B ) ) )  -  ( ( A  -h  B ) 
.ih  ( A  -h  B ) ) )  =  -u ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  2 ) ) )
89 normsq 26622 . . . . . . . . . . . . . 14  |-  ( ( ( A  -h  B
)  -h  ( T  .h  C ) )  e.  ~H  ->  (
( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) ^
2 )  =  ( ( ( A  -h  B )  -h  ( T  .h  C )
)  .ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) )
9067, 89syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( normh `  (
( A  -h  B
)  -h  ( T  .h  C ) ) ) ^ 2 )  =  ( ( ( A  -h  B )  -h  ( T  .h  C ) )  .ih  ( ( A  -h  B )  -h  ( T  .h  C )
) ) )
91 his2sub 26580 . . . . . . . . . . . . . 14  |-  ( ( ( A  -h  B
)  e.  ~H  /\  ( T  .h  C
)  e.  ~H  /\  ( ( A  -h  B )  -h  ( T  .h  C )
)  e.  ~H )  ->  ( ( ( A  -h  B )  -h  ( T  .h  C
) )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) )  =  ( ( ( A  -h  B
)  .ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) )  -  ( ( T  .h  C )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) ) ) )
927, 59, 67, 91syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( A  -h  B )  -h  ( T  .h  C
) )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) )  =  ( ( ( A  -h  B
)  .ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) )  -  ( ( T  .h  C )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) ) ) )
93 his2sub2 26581 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  -h  B
)  e.  ~H  /\  ( A  -h  B
)  e.  ~H  /\  ( T  .h  C
)  e.  ~H )  ->  ( ( A  -h  B )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) )  =  ( ( ( A  -h  B
)  .ih  ( A  -h  B ) )  -  ( ( A  -h  B )  .ih  ( T  .h  C )
) ) )
947, 7, 59, 93syl3anc 1264 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  -h  B )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) )  =  ( ( ( A  -h  B
)  .ih  ( A  -h  B ) )  -  ( ( A  -h  B )  .ih  ( T  .h  C )
) ) )
9594oveq1d 6320 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  ( ( A  -h  B )  -h  ( T  .h  C )
) )  -  (
( T  .h  C
)  .ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) )  =  ( ( ( ( A  -h  B
)  .ih  ( A  -h  B ) )  -  ( ( A  -h  B )  .ih  ( T  .h  C )
) )  -  (
( T  .h  C
)  .ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) ) )
96 hicl 26568 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  -h  B
)  e.  ~H  /\  ( T  .h  C
)  e.  ~H )  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  e.  CC )
977, 59, 96syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  e.  CC )
98 his2sub2 26581 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T  .h  C
)  e.  ~H  /\  ( A  -h  B
)  e.  ~H  /\  ( T  .h  C
)  e.  ~H )  ->  ( ( T  .h  C )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) )  =  ( ( ( T  .h  C
)  .ih  ( A  -h  B ) )  -  ( ( T  .h  C )  .ih  ( T  .h  C )
) ) )
9959, 7, 59, 98syl3anc 1264 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( T  .h  C )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) )  =  ( ( ( T  .h  C
)  .ih  ( A  -h  B ) )  -  ( ( T  .h  C )  .ih  ( T  .h  C )
) ) )
100 hicl 26568 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T  .h  C
)  e.  ~H  /\  ( A  -h  B
)  e.  ~H )  ->  ( ( T  .h  C )  .ih  ( A  -h  B ) )  e.  CC )
10159, 7, 100syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( T  .h  C )  .ih  ( A  -h  B ) )  e.  CC )
102 hicl 26568 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T  .h  C
)  e.  ~H  /\  ( T  .h  C
)  e.  ~H )  ->  ( ( T  .h  C )  .ih  ( T  .h  C )
)  e.  CC )
10359, 59, 102syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( T  .h  C )  .ih  ( T  .h  C )
)  e.  CC )
104101, 103subcld 9985 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( T  .h  C )  .ih  ( A  -h  B
) )  -  (
( T  .h  C
)  .ih  ( T  .h  C ) ) )  e.  CC )
10599, 104eqeltrd 2517 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( T  .h  C )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) )  e.  CC )
10687, 97, 105subsub4d 10016 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( A  -h  B ) 
.ih  ( A  -h  B ) )  -  ( ( A  -h  B )  .ih  ( T  .h  C )
) )  -  (
( T  .h  C
)  .ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) )  =  ( ( ( A  -h  B ) 
.ih  ( A  -h  B ) )  -  ( ( ( A  -h  B )  .ih  ( T  .h  C
) )  +  ( ( T  .h  C
)  .ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) ) ) )
10782recnd 9668 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  e.  CC )
10831a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  CC )
109107, 43, 108adddid 9666 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( ( C  .ih  C )  +  1 )  +  1 ) )  =  ( ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  1 ) )  +  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  1 ) ) )
11037oveq2d 6321 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  2 ) )  =  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( ( C 
.ih  C )  +  1 )  +  1 ) ) )
111 his5 26574 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T  e.  CC  /\  ( A  -h  B
)  e.  ~H  /\  C  e.  ~H )  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  =  ( ( * `  T )  x.  ( ( A  -h  B )  .ih  C ) ) )
11247, 7, 10, 111syl3anc 1264 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  =  ( ( * `  T )  x.  ( ( A  -h  B )  .ih  C ) ) )
11347cjcld 13238 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( * `  T
)  e.  CC )
114113, 12mulcomd 9663 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( * `  T )  x.  (
( A  -h  B
)  .ih  C )
)  =  ( ( ( A  -h  B
)  .ih  C )  x.  ( * `  T
) ) )
11512cjcld 13238 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( * `  (
( A  -h  B
)  .ih  C )
)  e.  CC )
11612, 115, 43, 45divassd 10417 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( ( A  -h  B ) 
.ih  C )  x.  ( * `  (
( A  -h  B
)  .ih  C )
) )  /  (
( C  .ih  C
)  +  1 ) )  =  ( ( ( A  -h  B
)  .ih  C )  x.  ( ( * `  ( ( A  -h  B )  .ih  C
) )  /  (
( C  .ih  C
)  +  1 ) ) ) )
11712absvalsqd 13482 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  =  ( ( ( A  -h  B ) 
.ih  C )  x.  ( * `  (
( A  -h  B
)  .ih  C )
) ) )
118117oveq1d 6320 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  /  ( ( C  .ih  C )  +  1 ) )  =  ( ( ( ( A  -h  B
)  .ih  C )  x.  ( * `  (
( A  -h  B
)  .ih  C )
) )  /  (
( C  .ih  C
)  +  1 ) ) )
11942fveq2i 5884 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( * `
 T )  =  ( * `  (
( ( A  -h  B )  .ih  C
)  /  ( ( C  .ih  C )  +  1 ) ) )
12012, 43, 45cjdivd 13265 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( * `  (
( ( A  -h  B )  .ih  C
)  /  ( ( C  .ih  C )  +  1 ) ) )  =  ( ( * `  ( ( A  -h  B ) 
.ih  C ) )  /  ( * `  ( ( C  .ih  C )  +  1 ) ) ) )
12124cjred 13268 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( * `  (
( C  .ih  C
)  +  1 ) )  =  ( ( C  .ih  C )  +  1 ) )
122121oveq2d 6321 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( * `  ( ( A  -h  B )  .ih  C
) )  /  (
* `  ( ( C  .ih  C )  +  1 ) ) )  =  ( ( * `
 ( ( A  -h  B )  .ih  C ) )  /  (
( C  .ih  C
)  +  1 ) ) )
123120, 122eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( * `  (
( ( A  -h  B )  .ih  C
)  /  ( ( C  .ih  C )  +  1 ) ) )  =  ( ( * `  ( ( A  -h  B ) 
.ih  C ) )  /  ( ( C 
.ih  C )  +  1 ) ) )
124119, 123syl5eq 2482 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( * `  T
)  =  ( ( * `  ( ( A  -h  B ) 
.ih  C ) )  /  ( ( C 
.ih  C )  +  1 ) ) )
125124oveq2d 6321 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  C )  x.  ( * `
 T ) )  =  ( ( ( A  -h  B ) 
.ih  C )  x.  ( ( * `  ( ( A  -h  B )  .ih  C
) )  /  (
( C  .ih  C
)  +  1 ) ) ) )
126116, 118, 1253eqtr4rd 2481 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  C )  x.  ( * `
 T ) )  =  ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( C  .ih  C )  +  1 ) ) )
127112, 114, 1263eqtrd 2474 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  =  ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( C 
.ih  C )  +  1 ) ) )
12815recnd 9668 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  e.  CC )
129128, 43mulcomd 9663 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  x.  ( ( C  .ih  C )  +  1 ) )  =  ( ( ( C  .ih  C )  +  1 )  x.  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 ) ) )
13043sqvald 12410 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 ) ^ 2 )  =  ( ( ( C  .ih  C
)  +  1 )  x.  ( ( C 
.ih  C )  +  1 ) ) )
131129, 130oveq12d 6323 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  x.  ( ( C  .ih  C )  +  1 ) )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  =  ( ( ( ( C  .ih  C
)  +  1 )  x.  ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 ) )  /  (
( ( C  .ih  C )  +  1 )  x.  ( ( C 
.ih  C )  +  1 ) ) ) )
132128, 43, 43, 45, 45divcan5d 10408 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( ( C  .ih  C )  +  1 )  x.  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 ) )  /  ( ( ( C  .ih  C
)  +  1 )  x.  ( ( C 
.ih  C )  +  1 ) ) )  =  ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( C  .ih  C )  +  1 ) ) )
133131, 132eqtr2d 2471 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  /  ( ( C  .ih  C )  +  1 ) )  =  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  x.  ( ( C 
.ih  C )  +  1 ) )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) ) )
13424resqcld 12439 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 ) ^ 2 )  e.  RR )
135134recnd 9668 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 ) ^ 2 )  e.  CC )
13681rpne0d 11346 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 ) ^ 2 )  =/=  0 )
137128, 43, 135, 136div23d 10419 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  x.  ( ( C  .ih  C )  +  1 ) )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  =  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  1 ) ) )
138127, 133, 1373eqtrd 2474 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  =  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  1 ) ) )
13982, 24remulcld 9670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  1 ) )  e.  RR )
140138, 139eqeltrd 2517 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  e.  RR )
141 hire 26582 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  -h  B
)  e.  ~H  /\  ( T  .h  C
)  e.  ~H )  ->  ( ( ( A  -h  B )  .ih  ( T  .h  C
) )  e.  RR  <->  ( ( A  -h  B
)  .ih  ( T  .h  C ) )  =  ( ( T  .h  C )  .ih  ( A  -h  B ) ) ) )
1427, 59, 141syl2anc 665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  ( T  .h  C
) )  e.  RR  <->  ( ( A  -h  B
)  .ih  ( T  .h  C ) )  =  ( ( T  .h  C )  .ih  ( A  -h  B ) ) ) )
143140, 142mpbid 213 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  =  ( ( T  .h  C ) 
.ih  ( A  -h  B ) ) )
144143, 138eqtr3d 2472 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( T  .h  C )  .ih  ( A  -h  B ) )  =  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  1 ) ) )
145 his35 26576 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T  e.  CC  /\  T  e.  CC )  /\  ( C  e. 
~H  /\  C  e.  ~H ) )  ->  (
( T  .h  C
)  .ih  ( T  .h  C ) )  =  ( ( T  x.  ( * `  T
) )  x.  ( C  .ih  C ) ) )
14647, 47, 10, 10, 145syl22anc 1265 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( T  .h  C )  .ih  ( T  .h  C )
)  =  ( ( T  x.  ( * `
 T ) )  x.  ( C  .ih  C ) ) )
14742fveq2i 5884 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( abs `  T )  =  ( abs `  ( ( ( A  -h  B
)  .ih  C )  /  ( ( C 
.ih  C )  +  1 ) ) )
14812, 43, 45absdivd 13495 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( abs `  (
( ( A  -h  B )  .ih  C
)  /  ( ( C  .ih  C )  +  1 ) ) )  =  ( ( abs `  ( ( A  -h  B ) 
.ih  C ) )  /  ( abs `  (
( C  .ih  C
)  +  1 ) ) ) )
14944rpge0d 11345 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  0  <_  ( ( C  .ih  C )  +  1 ) )
15024, 149absidd 13463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( abs `  (
( C  .ih  C
)  +  1 ) )  =  ( ( C  .ih  C )  +  1 ) )
151150oveq2d 6321 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
)  /  ( abs `  ( ( C  .ih  C )  +  1 ) ) )  =  ( ( abs `  (
( A  -h  B
)  .ih  C )
)  /  ( ( C  .ih  C )  +  1 ) ) )
152148, 151eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( abs `  (
( ( A  -h  B )  .ih  C
)  /  ( ( C  .ih  C )  +  1 ) ) )  =  ( ( abs `  ( ( A  -h  B ) 
.ih  C ) )  /  ( ( C 
.ih  C )  +  1 ) ) )
153147, 152syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( abs `  T
)  =  ( ( abs `  ( ( A  -h  B ) 
.ih  C ) )  /  ( ( C 
.ih  C )  +  1 ) ) )
154153oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( abs `  T
) ^ 2 )  =  ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) )  /  ( ( C 
.ih  C )  +  1 ) ) ^
2 ) )
15547absvalsqd 13482 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( abs `  T
) ^ 2 )  =  ( T  x.  ( * `  T
) ) )
15614, 43, 45sqdivd 12426 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) )  /  (
( C  .ih  C
)  +  1 ) ) ^ 2 )  =  ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) ) )
157154, 155, 1563eqtr3d 2478 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( T  x.  (
* `  T )
)  =  ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) ) )
158157oveq1d 6320 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( T  x.  ( * `  T
) )  x.  ( C  .ih  C ) )  =  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( C  .ih  C
) ) )
159146, 158eqtrd 2470 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( T  .h  C )  .ih  ( T  .h  C )
)  =  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( C  .ih  C
) ) )
160144, 159oveq12d 6323 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( T  .h  C )  .ih  ( A  -h  B
) )  -  (
( T  .h  C
)  .ih  ( T  .h  C ) ) )  =  ( ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  1 ) )  -  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( C  .ih  C
) ) ) )
161 pncan2 9881 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( C  .ih  C
)  e.  CC  /\  1  e.  CC )  ->  ( ( ( C 
.ih  C )  +  1 )  -  ( C  .ih  C ) )  =  1 )
16230, 31, 161sylancl 666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 )  -  ( C  .ih  C ) )  =  1 )
163162oveq2d 6321 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( ( C  .ih  C )  +  1 )  -  ( C  .ih  C ) ) )  =  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  1 ) )
164107, 43, 30subdid 10073 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( ( C  .ih  C )  +  1 )  -  ( C  .ih  C ) ) )  =  ( ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  1 ) )  -  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( C  .ih  C
) ) ) )
165163, 164eqtr3d 2472 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  1 )  =  ( ( ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  x.  ( ( C 
.ih  C )  +  1 ) )  -  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  ( C  .ih  C ) ) ) )
166160, 99, 1653eqtr4d 2480 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( T  .h  C )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) )  =  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  1 ) )
167138, 166oveq12d 6323 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  ( T  .h  C
) )  +  ( ( T  .h  C
)  .ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) )  =  ( ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  1 ) )  +  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  1 ) ) )
168109, 110, 1673eqtr4rd 2481 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  ( T  .h  C
) )  +  ( ( T  .h  C
)  .ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) )  =  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  2 ) ) )
169168oveq2d 6321 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  ( A  -h  B
) )  -  (
( ( A  -h  B )  .ih  ( T  .h  C )
)  +  ( ( T  .h  C ) 
.ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) ) )  =  ( ( ( A  -h  B
)  .ih  ( A  -h  B ) )  -  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  2 ) ) ) )
17095, 106, 1693eqtrd 2474 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  ( ( A  -h  B )  -h  ( T  .h  C )
) )  -  (
( T  .h  C
)  .ih  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) )  =  ( ( ( A  -h  B ) 
.ih  ( A  -h  B ) )  -  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  2 ) ) ) )
17190, 92, 1703eqtrd 2474 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( normh `  (
( A  -h  B
)  -h  ( T  .h  C ) ) ) ^ 2 )  =  ( ( ( A  -h  B ) 
.ih  ( A  -h  B ) )  -  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  2 ) ) ) )
17287, 84negsubd 9991 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  ( A  -h  B
) )  +  -u ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  2 ) ) )  =  ( ( ( A  -h  B )  .ih  ( A  -h  B ) )  -  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  2 ) ) ) )
17387, 85addcomd 9834 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  ( A  -h  B
) )  +  -u ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  2 ) ) )  =  (
-u ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  2 ) )  +  ( ( A  -h  B ) 
.ih  ( A  -h  B ) ) ) )
174171, 172, 1733eqtr2d 2476 . . . . . . . . . . 11  |-  ( ph  ->  ( ( normh `  (
( A  -h  B
)  -h  ( T  .h  C ) ) ) ^ 2 )  =  ( -u (
( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  x.  ( ( C 
.ih  C )  +  2 ) )  +  ( ( A  -h  B )  .ih  ( A  -h  B ) ) ) )
175 normsq 26622 . . . . . . . . . . . 12  |-  ( ( A  -h  B )  e.  ~H  ->  (
( normh `  ( A  -h  B ) ) ^
2 )  =  ( ( A  -h  B
)  .ih  ( A  -h  B ) ) )
1767, 175syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( normh `  ( A  -h  B ) ) ^ 2 )  =  ( ( A  -h  B )  .ih  ( A  -h  B ) ) )
177174, 176oveq12d 6323 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( normh `  ( ( A  -h  B )  -h  ( T  .h  C )
) ) ^ 2 )  -  ( (
normh `  ( A  -h  B ) ) ^
2 ) )  =  ( ( -u (
( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  x.  ( ( C 
.ih  C )  +  2 ) )  +  ( ( A  -h  B )  .ih  ( A  -h  B ) ) )  -  ( ( A  -h  B ) 
.ih  ( A  -h  B ) ) ) )
17821renegcld 10045 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u ( ( C 
.ih  C )  +  2 )  e.  RR )
179178recnd 9668 . . . . . . . . . . . 12  |-  ( ph  -> 
-u ( ( C 
.ih  C )  +  2 )  e.  CC )
180128, 179, 135, 136div23d 10419 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  x.  -u ( ( C  .ih  C )  +  2 ) )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  =  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  -u ( ( C  .ih  C )  +  2 ) ) )
18121recnd 9668 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( C  .ih  C )  +  2 )  e.  CC )
182107, 181mulneg2d 10071 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  -u (
( C  .ih  C
)  +  2 ) )  =  -u (
( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  x.  ( ( C 
.ih  C )  +  2 ) ) )
183180, 182eqtrd 2470 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  x.  -u ( ( C  .ih  C )  +  2 ) )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  =  -u ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  2 ) ) )
18488, 177, 1833eqtr4rd 2481 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  x.  -u ( ( C  .ih  C )  +  2 ) )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  =  ( ( (
normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) ^
2 )  -  (
( normh `  ( A  -h  B ) ) ^
2 ) ) )
18578, 184breqtrrd 4452 . . . . . . . 8  |-  ( ph  ->  0  <_  ( (
( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  x.  -u ( ( C 
.ih  C )  +  2 ) )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) ) )
18615, 178remulcld 9670 . . . . . . . . 9  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  x.  -u (
( C  .ih  C
)  +  2 ) )  e.  RR )
187186, 81ge0divd 11376 . . . . . . . 8  |-  ( ph  ->  ( 0  <_  (
( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  x.  -u ( ( C 
.ih  C )  +  2 ) )  <->  0  <_  ( ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  x.  -u (
( C  .ih  C
)  +  2 ) )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) ) ) )
188185, 187mpbird 235 . . . . . . 7  |-  ( ph  ->  0  <_  ( (
( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  x.  -u ( ( C 
.ih  C )  +  2 ) ) )
189 mulneg12 10056 . . . . . . . 8  |-  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  e.  CC  /\  (
( C  .ih  C
)  +  2 )  e.  CC )  -> 
( -u ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  x.  ( ( C  .ih  C )  +  2 ) )  =  ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  x.  -u ( ( C  .ih  C )  +  2 ) ) )
190128, 181, 189syl2anc 665 . . . . . . 7  |-  ( ph  ->  ( -u ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  x.  ( ( C  .ih  C )  +  2 ) )  =  ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  x.  -u ( ( C 
.ih  C )  +  2 ) ) )
191188, 190breqtrrd 4452 . . . . . 6  |-  ( ph  ->  0  <_  ( -u (
( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  x.  ( ( C 
.ih  C )  +  2 ) ) )
192 prodge02 10452 . . . . . 6  |-  ( ( ( -u ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  e.  RR  /\  ( ( C  .ih  C )  +  2 )  e.  RR )  /\  (
0  <  ( ( C  .ih  C )  +  2 )  /\  0  <_  ( -u ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  x.  ( ( C  .ih  C )  +  2 ) ) ) )  -> 
0  <_  -u ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 ) )
19316, 21, 39, 191, 192syl22anc 1265 . . . . 5  |-  ( ph  ->  0  <_  -u ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 ) )
19415le0neg1d 10184 . . . . 5  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  <_  0  <->  0  <_  -u ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 ) ) )
195193, 194mpbird 235 . . . 4  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  <_  0 )
19613sqge0d 12440 . . . 4  |-  ( ph  ->  0  <_  ( ( abs `  ( ( A  -h  B )  .ih  C ) ) ^ 2 ) )
197 0re 9642 . . . . 5  |-  0  e.  RR
198 letri3 9718 . . . . 5  |-  ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  e.  RR  /\  0  e.  RR )  ->  (
( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  =  0  <->  ( (
( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  <_  0  /\  0  <_  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 ) ) ) )
19915, 197, 198sylancl 666 . . . 4  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  =  0  <->  (
( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  <_  0  /\  0  <_  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 ) ) ) )
200195, 196, 199mpbir2and 930 . . 3  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  =  0 )
20114, 200sqeq0d 12412 . 2  |-  ( ph  ->  ( abs `  (
( A  -h  B
)  .ih  C )
)  =  0 )
20212, 201abs00d 13486 1  |-  ( ph  ->  ( ( A  -h  B )  .ih  C
)  =  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1870   A.wral 2782   class class class wbr 4426   ` cfv 5601  (class class class)co 6305   CCcc 9536   RRcr 9537   0cc0 9538   1c1 9539    + caddc 9541    x. cmul 9543    < clt 9674    <_ cle 9675    - cmin 9859   -ucneg 9860    / cdiv 10268   2c2 10659   ZZcz 10937   RR+crp 11302   ^cexp 12269   *ccj 13138   abscabs 13276   ~Hchil 26407    +h cva 26408    .h csm 26409    .ih csp 26410   normhcno 26411    -h cmv 26413   SHcsh 26416   CHcch 26417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615  ax-pre-sup 9616  ax-hilex 26487  ax-hfvadd 26488  ax-hvass 26490  ax-hv0cl 26491  ax-hfvmul 26493  ax-hvdistr1 26496  ax-hvmul0 26498  ax-hfi 26567  ax-his1 26570  ax-his2 26571  ax-his3 26572  ax-his4 26573
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-sup 7962  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-rp 11303  df-seq 12211  df-exp 12270  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-hnorm 26456  df-hvsub 26459  df-sh 26695  df-ch 26709
This theorem is referenced by:  pjhthlem2  26880
  Copyright terms: Public domain W3C validator