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

Theorem pjhthlem1 24762
Description: Lemma for pjhth 24764. (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 24603 . . . . 5  |-  ( B  e.  H  ->  B  e.  ~H )
52, 4syl 16 . . . 4  |-  ( ph  ->  B  e.  ~H )
6 hvsubcl 24387 . . . 4  |-  ( ( A  e.  ~H  /\  B  e.  ~H )  ->  ( A  -h  B
)  e.  ~H )
71, 5, 6syl2anc 661 . . 3  |-  ( ph  ->  ( A  -h  B
)  e.  ~H )
8 pjhth.4 . . . 4  |-  ( ph  ->  C  e.  H )
93cheli 24603 . . . 4  |-  ( C  e.  H  ->  C  e.  ~H )
108, 9syl 16 . . 3  |-  ( ph  ->  C  e.  ~H )
11 hicl 24450 . . 3  |-  ( ( ( A  -h  B
)  e.  ~H  /\  C  e.  ~H )  ->  ( ( A  -h  B )  .ih  C
)  e.  CC )
127, 10, 11syl2anc 661 . 2  |-  ( ph  ->  ( ( A  -h  B )  .ih  C
)  e.  CC )
1312abscld 12914 . . . 4  |-  ( ph  ->  ( abs `  (
( A  -h  B
)  .ih  C )
)  e.  RR )
1413recnd 9404 . . 3  |-  ( ph  ->  ( abs `  (
( A  -h  B
)  .ih  C )
)  e.  CC )
1513resqcld 12026 . . . . . . 7  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  e.  RR )
1615renegcld 9767 . . . . . 6  |-  ( ph  -> 
-u ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  e.  RR )
17 hiidrcl 24465 . . . . . . . 8  |-  ( C  e.  ~H  ->  ( C  .ih  C )  e.  RR )
1810, 17syl 16 . . . . . . 7  |-  ( ph  ->  ( C  .ih  C
)  e.  RR )
19 2re 10383 . . . . . . 7  |-  2  e.  RR
20 readdcl 9357 . . . . . . 7  |-  ( ( ( C  .ih  C
)  e.  RR  /\  2  e.  RR )  ->  ( ( C  .ih  C )  +  2 )  e.  RR )
2118, 19, 20sylancl 662 . . . . . 6  |-  ( ph  ->  ( ( C  .ih  C )  +  2 )  e.  RR )
22 0red 9379 . . . . . . 7  |-  ( ph  ->  0  e.  RR )
23 peano2re 9534 . . . . . . . 8  |-  ( ( C  .ih  C )  e.  RR  ->  (
( C  .ih  C
)  +  1 )  e.  RR )
2418, 23syl 16 . . . . . . 7  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  e.  RR )
25 hiidge0 24468 . . . . . . . . 9  |-  ( C  e.  ~H  ->  0  <_  ( C  .ih  C
) )
2610, 25syl 16 . . . . . . . 8  |-  ( ph  ->  0  <_  ( C  .ih  C ) )
2718ltp1d 10255 . . . . . . . 8  |-  ( ph  ->  ( C  .ih  C
)  <  ( ( C  .ih  C )  +  1 ) )
2822, 18, 24, 26, 27lelttrd 9521 . . . . . . 7  |-  ( ph  ->  0  <  ( ( C  .ih  C )  +  1 ) )
2924ltp1d 10255 . . . . . . . 8  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  <  ( ( ( C  .ih  C )  +  1 )  +  1 ) )
3018recnd 9404 . . . . . . . . . 10  |-  ( ph  ->  ( C  .ih  C
)  e.  CC )
31 ax-1cn 9332 . . . . . . . . . . 11  |-  1  e.  CC
32 addass 9361 . . . . . . . . . . 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 1306 . . . . . . . . . 10  |-  ( ( C  .ih  C )  e.  CC  ->  (
( ( C  .ih  C )  +  1 )  +  1 )  =  ( ( C  .ih  C )  +  ( 1  +  1 ) ) )
3430, 33syl 16 . . . . . . . . 9  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 )  +  1 )  =  ( ( C  .ih  C )  +  ( 1  +  1 ) ) )
35 df-2 10372 . . . . . . . . . 10  |-  2  =  ( 1  +  1 )
3635oveq2i 6097 . . . . . . . . 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 4313 . . . . . . 7  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  <  ( ( C 
.ih  C )  +  2 ) )
3922, 24, 21, 28, 38lttrd 9524 . . . . . 6  |-  ( ph  ->  0  <  ( ( C  .ih  C )  +  2 ) )
403chshii 24598 . . . . . . . . . . . . . . 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 9404 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  e.  CC )
4418, 26ge0p1rpd 11045 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  e.  RR+ )
4544rpne0d 11024 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( C  .ih  C )  +  1 )  =/=  0 )
4612, 43, 45divcld 10099 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A  -h  B )  .ih  C )  /  ( ( C  .ih  C )  +  1 ) )  e.  CC )
4742, 46syl5eqel 2522 . . . . . . . . . . . . . . 15  |-  ( ph  ->  T  e.  CC )
48 shmulcl 24588 . . . . . . . . . . . . . . 15  |-  ( ( H  e.  SH  /\  T  e.  CC  /\  C  e.  H )  ->  ( T  .h  C )  e.  H )
4941, 47, 8, 48syl3anc 1218 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  .h  C
)  e.  H )
50 shaddcl 24587 . . . . . . . . . . . . . 14  |-  ( ( H  e.  SH  /\  B  e.  H  /\  ( T  .h  C
)  e.  H )  ->  ( B  +h  ( T  .h  C
) )  e.  H
)
5141, 2, 49, 50syl3anc 1218 . . . . . . . . . . . . 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 6094 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( B  +h  ( T  .h  C
) )  ->  ( A  -h  x )  =  ( A  -h  ( B  +h  ( T  .h  C ) ) ) )
5453fveq2d 5690 . . . . . . . . . . . . . . 15  |-  ( x  =  ( B  +h  ( T  .h  C
) )  ->  ( normh `  ( A  -h  x ) )  =  ( normh `  ( A  -h  ( B  +h  ( T  .h  C )
) ) ) )
5554breq2d 4299 . . . . . . . . . . . . . 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 3064 . . . . . . . . . . . . 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 60 . . . . . . . . . . . 12  |-  ( ph  ->  ( normh `  ( A  -h  B ) )  <_ 
( normh `  ( A  -h  ( B  +h  ( T  .h  C )
) ) ) )
583cheli 24603 . . . . . . . . . . . . . . 15  |-  ( ( T  .h  C )  e.  H  ->  ( T  .h  C )  e.  ~H )
5949, 58syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  .h  C
)  e.  ~H )
60 hvsubass 24414 . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A  -h  B )  -h  ( T  .h  C )
)  =  ( A  -h  ( B  +h  ( T  .h  C
) ) ) )
6261fveq2d 5690 . . . . . . . . . . . 12  |-  ( ph  ->  ( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) )  =  ( normh `  ( A  -h  ( B  +h  ( T  .h  C )
) ) ) )
6357, 62breqtrrd 4313 . . . . . . . . . . 11  |-  ( ph  ->  ( normh `  ( A  -h  B ) )  <_ 
( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) )
64 normcl 24495 . . . . . . . . . . . . 13  |-  ( ( A  -h  B )  e.  ~H  ->  ( normh `  ( A  -h  B ) )  e.  RR )
657, 64syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( normh `  ( A  -h  B ) )  e.  RR )
66 hvsubcl 24387 . . . . . . . . . . . . . 14  |-  ( ( ( A  -h  B
)  e.  ~H  /\  ( T  .h  C
)  e.  ~H )  ->  ( ( A  -h  B )  -h  ( T  .h  C )
)  e.  ~H )
677, 59, 66syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A  -h  B )  -h  ( T  .h  C )
)  e.  ~H )
68 normcl 24495 . . . . . . . . . . . . 13  |-  ( ( ( A  -h  B
)  -h  ( T  .h  C ) )  e.  ~H  ->  ( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) )  e.  RR )
6967, 68syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) )  e.  RR )
70 normge0 24496 . . . . . . . . . . . . 13  |-  ( ( A  -h  B )  e.  ~H  ->  0  <_  ( normh `  ( A  -h  B ) ) )
717, 70syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( normh `  ( A  -h  B
) ) )
7222, 65, 69, 71, 63letrd 9520 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( normh `  ( ( A  -h  B )  -h  ( T  .h  C )
) ) )
7365, 69, 71, 72le2sqd 12035 . . . . . . . . . . 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 210 . . . . . . . . . 10  |-  ( ph  ->  ( ( normh `  ( A  -h  B ) ) ^ 2 )  <_ 
( ( normh `  (
( A  -h  B
)  -h  ( T  .h  C ) ) ) ^ 2 ) )
7569resqcld 12026 . . . . . . . . . . 11  |-  ( ph  ->  ( ( normh `  (
( A  -h  B
)  -h  ( T  .h  C ) ) ) ^ 2 )  e.  RR )
7665resqcld 12026 . . . . . . . . . . 11  |-  ( ph  ->  ( ( normh `  ( A  -h  B ) ) ^ 2 )  e.  RR )
7775, 76subge0d 9921 . . . . . . . . . 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 232 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( (
( normh `  ( ( A  -h  B )  -h  ( T  .h  C
) ) ) ^
2 )  -  (
( normh `  ( A  -h  B ) ) ^
2 ) ) )
79 2z 10670 . . . . . . . . . . . . . . . 16  |-  2  e.  ZZ
80 rpexpcl 11876 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( C  .ih  C )  +  1 )  e.  RR+  /\  2  e.  ZZ )  ->  (
( ( C  .ih  C )  +  1 ) ^ 2 )  e.  RR+ )
8144, 79, 80sylancl 662 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 ) ^ 2 )  e.  RR+ )
8215, 81rerpdivcld 11046 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  /  ( ( ( C  .ih  C
)  +  1 ) ^ 2 ) )  e.  RR )
8382, 21remulcld 9406 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  2 ) )  e.  RR )
8483recnd 9404 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  2 ) )  e.  CC )
8584negcld 9698 . . . . . . . . . . 11  |-  ( ph  -> 
-u ( ( ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  /  ( ( ( C  .ih  C )  +  1 ) ^
2 ) )  x.  ( ( C  .ih  C )  +  2 ) )  e.  CC )
86 hicl 24450 . . . . . . . . . . . 12  |-  ( ( ( A  -h  B
)  e.  ~H  /\  ( A  -h  B
)  e.  ~H )  ->  ( ( A  -h  B )  .ih  ( A  -h  B ) )  e.  CC )
877, 7, 86syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( A  -h  B ) )  e.  CC )
8885, 87pncand 9712 . . . . . . . . . 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 24504 . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . 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 24462 . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . 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 24463 . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . 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 24450 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  -h  B
)  e.  ~H  /\  ( T  .h  C
)  e.  ~H )  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  e.  CC )
977, 59, 96syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  e.  CC )
98 his2sub2 24463 . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . 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 24450 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T  .h  C
)  e.  ~H  /\  ( A  -h  B
)  e.  ~H )  ->  ( ( T  .h  C )  .ih  ( A  -h  B ) )  e.  CC )
10159, 7, 100syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( T  .h  C )  .ih  ( A  -h  B ) )  e.  CC )
102 hicl 24450 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T  .h  C
)  e.  ~H  /\  ( T  .h  C
)  e.  ~H )  ->  ( ( T  .h  C )  .ih  ( T  .h  C )
)  e.  CC )
10359, 59, 102syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( T  .h  C )  .ih  ( T  .h  C )
)  e.  CC )
104101, 103subcld 9711 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( T  .h  C )  .ih  ( A  -h  B
) )  -  (
( T  .h  C
)  .ih  ( T  .h  C ) ) )  e.  CC )
10599, 104eqeltrd 2512 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( T  .h  C )  .ih  (
( A  -h  B
)  -h  ( T  .h  C ) ) )  e.  CC )
10687, 97, 105subsub4d 9742 . . . . . . . . . . . . . 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 9404 . . . . . . . . . . . . . . . . 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 9402 . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . . . 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 24456 . . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  =  ( ( * `  T )  x.  ( ( A  -h  B )  .ih  C ) ) )
11347cjcld 12677 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( * `  T
)  e.  CC )
114113, 12mulcomd 9399 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( * `  T )  x.  (
( A  -h  B
)  .ih  C )
)  =  ( ( ( A  -h  B
)  .ih  C )  x.  ( * `  T
) ) )
11512cjcld 12677 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( * `  (
( A  -h  B
)  .ih  C )
)  e.  CC )
11612, 115, 43, 45divassd 10134 . . . . . . . . . . . . . . . . . . . 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 12920 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  =  ( ( ( A  -h  B ) 
.ih  C )  x.  ( * `  (
( A  -h  B
)  .ih  C )
) ) )
118117oveq1d 6101 . . . . . . . . . . . . . . . . . . . 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 5689 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( * `
 T )  =  ( * `  (
( ( A  -h  B )  .ih  C
)  /  ( ( C  .ih  C )  +  1 ) ) )
12012, 43, 45cjdivd 12704 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( * `  (
( ( A  -h  B )  .ih  C
)  /  ( ( C  .ih  C )  +  1 ) ) )  =  ( ( * `  ( ( A  -h  B ) 
.ih  C ) )  /  ( * `  ( ( C  .ih  C )  +  1 ) ) ) )
12124cjred 12707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( * `  (
( C  .ih  C
)  +  1 ) )  =  ( ( C  .ih  C )  +  1 ) )
122121oveq2d 6102 . . . . . . . . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . . . . . . . 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 9404 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  e.  CC )
129128, 43mulcomd 9399 . . . . . . . . . . . . . . . . . . . 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 11997 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 ) ^ 2 )  =  ( ( ( C  .ih  C
)  +  1 )  x.  ( ( C 
.ih  C )  +  1 ) ) )
131129, 130oveq12d 6104 . . . . . . . . . . . . . . . . . . 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 10125 . . . . . . . . . . . . . . . . . . 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 12026 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 ) ^ 2 )  e.  RR )
135134recnd 9404 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 ) ^ 2 )  e.  CC )
13681rpne0d 11024 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 ) ^ 2 )  =/=  0 )
137128, 43, 135, 136div23d 10136 . . . . . . . . . . . . . . . . . 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 9406 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) )  x.  (
( C  .ih  C
)  +  1 ) )  e.  RR )
140138, 139eqeltrd 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( A  -h  B )  .ih  ( T  .h  C )
)  e.  RR )
141 hire 24464 . . . . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . . . . . 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 24458 . . . . . . . . . . . . . . . . . . . . 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 1219 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( T  .h  C )  .ih  ( T  .h  C )
)  =  ( ( T  x.  ( * `
 T ) )  x.  ( C  .ih  C ) ) )
14742fveq2i 5689 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( abs `  T )  =  ( abs `  ( ( ( A  -h  B
)  .ih  C )  /  ( ( C 
.ih  C )  +  1 ) ) )
14812, 43, 45absdivd 12933 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( abs `  (
( ( A  -h  B )  .ih  C
)  /  ( ( C  .ih  C )  +  1 ) ) )  =  ( ( abs `  ( ( A  -h  B ) 
.ih  C ) )  /  ( abs `  (
( C  .ih  C
)  +  1 ) ) ) )
14944rpge0d 11023 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  0  <_  ( ( C  .ih  C )  +  1 ) )
15024, 149absidd 12901 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( abs `  (
( C  .ih  C
)  +  1 ) )  =  ( ( C  .ih  C )  +  1 ) )
151150oveq2d 6102 . . . . . . . . . . . . . . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( abs `  T
) ^ 2 )  =  ( ( ( abs `  ( ( A  -h  B ) 
.ih  C ) )  /  ( ( C 
.ih  C )  +  1 ) ) ^
2 ) )
15547absvalsqd 12920 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( abs `  T
) ^ 2 )  =  ( T  x.  ( * `  T
) ) )
15614, 43, 45sqdivd 12013 . . . . . . . . . . . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . . . . . . . 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 6104 . . . . . . . . . . . . . . . . . 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 9609 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( C  .ih  C
)  e.  CC  /\  1  e.  CC )  ->  ( ( ( C 
.ih  C )  +  1 )  -  ( C  .ih  C ) )  =  1 )
16230, 31, 161sylancl 662 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( C 
.ih  C )  +  1 )  -  ( C  .ih  C ) )  =  1 )
163162oveq2d 6102 . . . . . . . . . . . . . . . . . . 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 9792 . . . . . . . . . . . . . . . . . . 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 6104 . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . 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 9717 . . . . . . . . . . . 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 9563 . . . . . . . . . . . 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 24504 . . . . . . . . . . . 12  |-  ( ( A  -h  B )  e.  ~H  ->  (
( normh `  ( A  -h  B ) ) ^
2 )  =  ( ( A  -h  B
)  .ih  ( A  -h  B ) ) )
1767, 175syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( normh `  ( A  -h  B ) ) ^ 2 )  =  ( ( A  -h  B )  .ih  ( A  -h  B ) ) )
177174, 176oveq12d 6104 . . . . . . . . . 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 9767 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u ( ( C 
.ih  C )  +  2 )  e.  RR )
179178recnd 9404 . . . . . . . . . . . 12  |-  ( ph  -> 
-u ( ( C 
.ih  C )  +  2 )  e.  CC )
180128, 179, 135, 136div23d 10136 . . . . . . . . . . 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 9404 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( C  .ih  C )  +  2 )  e.  CC )
182107, 181mulneg2d 9790 . . . . . . . . . . 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 4313 . . . . . . . 8  |-  ( ph  ->  0  <_  ( (
( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  x.  -u ( ( C 
.ih  C )  +  2 ) )  / 
( ( ( C 
.ih  C )  +  1 ) ^ 2 ) ) )
18615, 178remulcld 9406 . . . . . . . . 9  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  x.  -u (
( C  .ih  C
)  +  2 ) )  e.  RR )
187186, 81ge0divd 11053 . . . . . . . 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 232 . . . . . . 7  |-  ( ph  ->  0  <_  ( (
( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  x.  -u ( ( C 
.ih  C )  +  2 ) ) )
189 mulneg12 9775 . . . . . . . 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 661 . . . . . . 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 4313 . . . . . 6  |-  ( ph  ->  0  <_  ( -u (
( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  x.  ( ( C 
.ih  C )  +  2 ) ) )
192 prodge02 10169 . . . . . 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 1219 . . . . 5  |-  ( ph  ->  0  <_  -u ( ( abs `  ( ( A  -h  B ) 
.ih  C ) ) ^ 2 ) )
19415le0neg1d 9903 . . . . 5  |-  ( ph  ->  ( ( ( abs `  ( ( A  -h  B )  .ih  C
) ) ^ 2 )  <_  0  <->  0  <_  -u ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 ) ) )
195193, 194mpbird 232 . . . 4  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  <_  0 )
19613sqge0d 12027 . . . 4  |-  ( ph  ->  0  <_  ( ( abs `  ( ( A  -h  B )  .ih  C ) ) ^ 2 ) )
197 0re 9378 . . . . 5  |-  0  e.  RR
198 letri3 9452 . . . . 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 662 . . . 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 913 . . 3  |-  ( ph  ->  ( ( abs `  (
( A  -h  B
)  .ih  C )
) ^ 2 )  =  0 )
20114, 200sqeq0d 11999 . 2  |-  ( ph  ->  ( abs `  (
( A  -h  B
)  .ih  C )
)  =  0 )
20212, 201abs00d 12924 1  |-  ( ph  ->  ( ( A  -h  B )  .ih  C
)  =  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2710   class class class wbr 4287   ` cfv 5413  (class class class)co 6086   CCcc 9272   RRcr 9273   0cc0 9274   1c1 9275    + caddc 9277    x. cmul 9279    < clt 9410    <_ cle 9411    - cmin 9587   -ucneg 9588    / cdiv 9985   2c2 10363   ZZcz 10638   RR+crp 10983   ^cexp 11857   *ccj 12577   abscabs 12715   ~Hchil 24289    +h cva 24290    .h csm 24291    .ih csp 24292   normhcno 24293    -h cmv 24295   SHcsh 24298   CHcch 24299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352  ax-hilex 24369  ax-hfvadd 24370  ax-hvass 24372  ax-hv0cl 24373  ax-hfvmul 24375  ax-hvdistr1 24378  ax-hvmul0 24380  ax-hfi 24449  ax-his1 24452  ax-his2 24453  ax-his3 24454  ax-his4 24455
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-2nd 6573  df-recs 6824  df-rdg 6858  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-sup 7683  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-n0 10572  df-z 10639  df-uz 10854  df-rp 10984  df-seq 11799  df-exp 11858  df-cj 12580  df-re 12581  df-im 12582  df-sqr 12716  df-abs 12717  df-hnorm 24338  df-hvsub 24341  df-sh 24577  df-ch 24592
This theorem is referenced by:  pjhthlem2  24763
  Copyright terms: Public domain W3C validator