Metamath Proof Explorer

Theorem axpaschlem

Description: Lemma for axpasch . Set up coefficents used in the proof. (Contributed by Scott Fenton, 5-Jun-2013)

Ref Expression
Assertion axpaschlem 
|- ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) -> E. r e. ( 0 [,] 1 ) E. p e. ( 0 [,] 1 ) ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 elicc01 
 |-  ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
3 2 simp1bi 
 |-  ( T e. ( 0 [,] 1 ) -> T e. RR )
4 3 ad2antrl 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. RR )
5 resubcl 
 |-  ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
6 1 4 5 sylancr 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
7 6 recnd 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
8 7 mul02d 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. ( 1 - T ) ) = 0 )
9 8 eqcomd 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 = ( 0 x. ( 1 - T ) ) )
10 elicc01 
 |-  ( S e. ( 0 [,] 1 ) <-> ( S e. RR /\ 0 <_ S /\ S <_ 1 ) )
11 10 simp1bi 
 |-  ( S e. ( 0 [,] 1 ) -> S e. RR )
12 11 ad2antll 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. RR )
13 resubcl 
 |-  ( ( 1 e. RR /\ S e. RR ) -> ( 1 - S ) e. RR )
14 1 12 13 sylancr 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. RR )
15 14 recnd 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. CC )
16 15 mulid2d 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. ( 1 - S ) ) = ( 1 - S ) )
17 oveq2 
 |-  ( S = 0 -> ( 1 - S ) = ( 1 - 0 ) )
18 17 adantr 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) = ( 1 - 0 ) )
19 1m0e1 
 |-  ( 1 - 0 ) = 1
20 18 19 eqtrdi 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) = 1 )
21 16 20 eqtr2d 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 1 = ( 1 x. ( 1 - S ) ) )
22 4 recnd 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. CC )
23 22 mul02d 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. T ) = 0 )
24 oveq2 
 |-  ( S = 0 -> ( 1 x. S ) = ( 1 x. 0 ) )
25 24 adantr 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. S ) = ( 1 x. 0 ) )
26 ax-1cn 
 |-  1 e. CC
27 26 mul01i 
 |-  ( 1 x. 0 ) = 0
28 25 27 eqtrdi 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. S ) = 0 )
29 23 28 eqtr4d 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. T ) = ( 1 x. S ) )
30 1elunit 
 |-  1 e. ( 0 [,] 1 )
31 0elunit 
 |-  0 e. ( 0 [,] 1 )
32 oveq2 
 |-  ( r = 1 -> ( 1 - r ) = ( 1 - 1 ) )
33 1m1e0 
 |-  ( 1 - 1 ) = 0
34 32 33 eqtrdi 
 |-  ( r = 1 -> ( 1 - r ) = 0 )
35 34 oveq1d 
 |-  ( r = 1 -> ( ( 1 - r ) x. ( 1 - T ) ) = ( 0 x. ( 1 - T ) ) )
36 35 eqeq2d 
 |-  ( r = 1 -> ( p = ( ( 1 - r ) x. ( 1 - T ) ) <-> p = ( 0 x. ( 1 - T ) ) ) )
37 eqeq1 
 |-  ( r = 1 -> ( r = ( ( 1 - p ) x. ( 1 - S ) ) <-> 1 = ( ( 1 - p ) x. ( 1 - S ) ) ) )
38 34 oveq1d 
 |-  ( r = 1 -> ( ( 1 - r ) x. T ) = ( 0 x. T ) )
39 38 eqeq1d 
 |-  ( r = 1 -> ( ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) <-> ( 0 x. T ) = ( ( 1 - p ) x. S ) ) )
40 36 37 39 3anbi123d 
 |-  ( r = 1 -> ( ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) <-> ( p = ( 0 x. ( 1 - T ) ) /\ 1 = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( 0 x. T ) = ( ( 1 - p ) x. S ) ) ) )
41 eqeq1 
 |-  ( p = 0 -> ( p = ( 0 x. ( 1 - T ) ) <-> 0 = ( 0 x. ( 1 - T ) ) ) )
42 oveq2 
 |-  ( p = 0 -> ( 1 - p ) = ( 1 - 0 ) )
43 42 19 eqtrdi 
 |-  ( p = 0 -> ( 1 - p ) = 1 )
44 43 oveq1d 
 |-  ( p = 0 -> ( ( 1 - p ) x. ( 1 - S ) ) = ( 1 x. ( 1 - S ) ) )
45 44 eqeq2d 
 |-  ( p = 0 -> ( 1 = ( ( 1 - p ) x. ( 1 - S ) ) <-> 1 = ( 1 x. ( 1 - S ) ) ) )
46 43 oveq1d 
 |-  ( p = 0 -> ( ( 1 - p ) x. S ) = ( 1 x. S ) )
47 46 eqeq2d 
 |-  ( p = 0 -> ( ( 0 x. T ) = ( ( 1 - p ) x. S ) <-> ( 0 x. T ) = ( 1 x. S ) ) )
48 41 45 47 3anbi123d 
 |-  ( p = 0 -> ( ( p = ( 0 x. ( 1 - T ) ) /\ 1 = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( 0 x. T ) = ( ( 1 - p ) x. S ) ) <-> ( 0 = ( 0 x. ( 1 - T ) ) /\ 1 = ( 1 x. ( 1 - S ) ) /\ ( 0 x. T ) = ( 1 x. S ) ) ) )
49 40 48 rspc2ev 
 |-  ( ( 1 e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) /\ ( 0 = ( 0 x. ( 1 - T ) ) /\ 1 = ( 1 x. ( 1 - S ) ) /\ ( 0 x. T ) = ( 1 x. S ) ) ) -> E. r e. ( 0 [,] 1 ) E. p e. ( 0 [,] 1 ) ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) )
50 30 31 49 mp3an12 
 |-  ( ( 0 = ( 0 x. ( 1 - T ) ) /\ 1 = ( 1 x. ( 1 - S ) ) /\ ( 0 x. T ) = ( 1 x. S ) ) -> E. r e. ( 0 [,] 1 ) E. p e. ( 0 [,] 1 ) ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) )
51 9 21 29 50 syl3anc 
 |-  ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> E. r e. ( 0 [,] 1 ) E. p e. ( 0 [,] 1 ) ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) )
52 51 ex 
 |-  ( S = 0 -> ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) -> E. r e. ( 0 [,] 1 ) E. p e. ( 0 [,] 1 ) ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) ) )
53 3 ad2antrl 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. RR )
54 11 ad2antll 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. RR )
55 54 53 remulcld 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) e. RR )
56 53 55 resubcld 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) e. RR )
57 54 53 readdcld 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S + T ) e. RR )
58 57 55 resubcld 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) e. RR )
59 1red 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 1 e. RR )
60 2 simp2bi 
 |-  ( T e. ( 0 [,] 1 ) -> 0 <_ T )
61 60 ad2antrl 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ T )
62 10 simp3bi 
 |-  ( S e. ( 0 [,] 1 ) -> S <_ 1 )
63 62 ad2antll 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S <_ 1 )
64 54 59 53 61 63 lemul1ad 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ ( 1 x. T ) )
65 53 recnd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. CC )
66 65 mulid2d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. T ) = T )
67 64 66 breqtrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ T )
68 10 simp2bi 
 |-  ( S e. ( 0 [,] 1 ) -> 0 <_ S )
69 68 ad2antll 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ S )
70 simpl 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S =/= 0 )
71 54 69 70 ne0gt0d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 < S )
72 54 53 ltaddpos2d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 < S <-> T < ( S + T ) ) )
73 71 72 mpbid 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T < ( S + T ) )
74 55 53 57 67 73 lelttrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) < ( S + T ) )
75 55 57 posdifd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S x. T ) < ( S + T ) <-> 0 < ( ( S + T ) - ( S x. T ) ) ) )
76 74 75 mpbid 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 < ( ( S + T ) - ( S x. T ) ) )
77 76 gt0ne0d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) =/= 0 )
78 56 58 77 redivcld 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. RR )
79 53 55 subge0d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ ( T - ( S x. T ) ) <-> ( S x. T ) <_ T ) )
80 67 79 mpbird 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( T - ( S x. T ) ) )
81 divge0 
 |-  ( ( ( ( T - ( S x. T ) ) e. RR /\ 0 <_ ( T - ( S x. T ) ) ) /\ ( ( ( S + T ) - ( S x. T ) ) e. RR /\ 0 < ( ( S + T ) - ( S x. T ) ) ) ) -> 0 <_ ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) )
82 56 80 58 76 81 syl22anc 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) )
83 53 57 73 ltled 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T <_ ( S + T ) )
84 53 57 55 83 lesub1dd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) <_ ( ( S + T ) - ( S x. T ) ) )
85 58 recnd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) e. CC )
86 85 mulid2d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. ( ( S + T ) - ( S x. T ) ) ) = ( ( S + T ) - ( S x. T ) ) )
87 84 86 breqtrrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) )
88 ledivmul2 
 |-  ( ( ( T - ( S x. T ) ) e. RR /\ 1 e. RR /\ ( ( ( S + T ) - ( S x. T ) ) e. RR /\ 0 < ( ( S + T ) - ( S x. T ) ) ) ) -> ( ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) <_ 1 <-> ( T - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) ) )
89 56 59 58 76 88 syl112anc 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) <_ 1 <-> ( T - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) ) )
90 87 89 mpbird 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) <_ 1 )
91 elicc01 
 |-  ( ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. ( 0 [,] 1 ) <-> ( ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. RR /\ 0 <_ ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) /\ ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) <_ 1 ) )
92 78 82 90 91 syl3anbrc 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. ( 0 [,] 1 ) )
93 54 55 resubcld 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) e. RR )
94 93 58 77 redivcld 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. RR )
95 2 simp3bi 
 |-  ( T e. ( 0 [,] 1 ) -> T <_ 1 )
96 95 ad2antrl 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T <_ 1 )
97 53 59 54 69 96 lemul2ad 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ ( S x. 1 ) )
98 54 recnd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. CC )
99 98 mulid1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. 1 ) = S )
100 97 99 breqtrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ S )
101 54 55 subge0d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ ( S - ( S x. T ) ) <-> ( S x. T ) <_ S ) )
102 100 101 mpbird 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( S - ( S x. T ) ) )
103 divge0 
 |-  ( ( ( ( S - ( S x. T ) ) e. RR /\ 0 <_ ( S - ( S x. T ) ) ) /\ ( ( ( S + T ) - ( S x. T ) ) e. RR /\ 0 < ( ( S + T ) - ( S x. T ) ) ) ) -> 0 <_ ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) )
104 93 102 58 76 103 syl22anc 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) )
105 54 53 addge01d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ T <-> S <_ ( S + T ) ) )
106 61 105 mpbid 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S <_ ( S + T ) )
107 54 57 55 106 lesub1dd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) <_ ( ( S + T ) - ( S x. T ) ) )
108 107 86 breqtrrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) )
109 ledivmul2 
 |-  ( ( ( S - ( S x. T ) ) e. RR /\ 1 e. RR /\ ( ( ( S + T ) - ( S x. T ) ) e. RR /\ 0 < ( ( S + T ) - ( S x. T ) ) ) ) -> ( ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) <_ 1 <-> ( S - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) ) )
110 93 59 58 76 109 syl112anc 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) <_ 1 <-> ( S - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) ) )
111 108 110 mpbird 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) <_ 1 )
112 elicc01 
 |-  ( ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. ( 0 [,] 1 ) <-> ( ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. RR /\ 0 <_ ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) /\ ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) <_ 1 ) )
113 94 104 111 112 syl3anbrc 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. ( 0 [,] 1 ) )
114 1 53 5 sylancr 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
115 114 recnd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
116 98 115 85 77 div23d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S x. ( 1 - T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( S / ( ( S + T ) - ( S x. T ) ) ) x. ( 1 - T ) ) )
117 subdi 
 |-  ( ( S e. CC /\ 1 e. CC /\ T e. CC ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
118 26 117 mp3an2 
 |-  ( ( S e. CC /\ T e. CC ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
119 98 65 118 syl2anc 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
120 99 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S x. 1 ) - ( S x. T ) ) = ( S - ( S x. T ) ) )
121 119 120 eqtrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. ( 1 - T ) ) = ( S - ( S x. T ) ) )
122 121 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S x. ( 1 - T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) )
123 56 recnd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) e. CC )
124 85 123 85 77 divsubdird 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( ( S + T ) - ( S x. T ) ) - ( T - ( S x. T ) ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( ( ( S + T ) - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) )
125 57 recnd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S + T ) e. CC )
126 55 recnd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) e. CC )
127 125 65 126 nnncan2d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( T - ( S x. T ) ) ) = ( ( S + T ) - T ) )
128 98 65 pncand 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - T ) = S )
129 127 128 eqtrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( T - ( S x. T ) ) ) = S )
130 129 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( ( S + T ) - ( S x. T ) ) - ( T - ( S x. T ) ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( S / ( ( S + T ) - ( S x. T ) ) ) )
131 85 77 dividd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = 1 )
132 131 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( ( S + T ) - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) = ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) )
133 124 130 132 3eqtr3d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S / ( ( S + T ) - ( S x. T ) ) ) = ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) )
134 133 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S / ( ( S + T ) - ( S x. T ) ) ) x. ( 1 - T ) ) = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - T ) ) )
135 116 122 134 3eqtr3d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - T ) ) )
136 1 54 13 sylancr 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. RR )
137 136 recnd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. CC )
138 65 137 85 77 div23d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T x. ( 1 - S ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( T / ( ( S + T ) - ( S x. T ) ) ) x. ( 1 - S ) ) )
139 subdi 
 |-  ( ( T e. CC /\ 1 e. CC /\ S e. CC ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
140 26 139 mp3an2 
 |-  ( ( T e. CC /\ S e. CC ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
141 65 98 140 syl2anc 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
142 65 mulid1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. 1 ) = T )
143 65 98 mulcomd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. S ) = ( S x. T ) )
144 142 143 oveq12d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T x. 1 ) - ( T x. S ) ) = ( T - ( S x. T ) ) )
145 141 144 eqtrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. ( 1 - S ) ) = ( T - ( S x. T ) ) )
146 145 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T x. ( 1 - S ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) )
147 93 recnd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) e. CC )
148 85 147 85 77 divsubdird 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( ( S + T ) - ( S x. T ) ) - ( S - ( S x. T ) ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( ( ( S + T ) - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) )
149 125 98 126 nnncan2d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( S - ( S x. T ) ) ) = ( ( S + T ) - S ) )
150 98 65 pncan2d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - S ) = T )
151 149 150 eqtrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( S - ( S x. T ) ) ) = T )
152 151 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( ( S + T ) - ( S x. T ) ) - ( S - ( S x. T ) ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( T / ( ( S + T ) - ( S x. T ) ) ) )
153 131 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( ( S + T ) - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) = ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) )
154 148 152 153 3eqtr3d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T / ( ( S + T ) - ( S x. T ) ) ) = ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) )
155 154 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T / ( ( S + T ) - ( S x. T ) ) ) x. ( 1 - S ) ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - S ) ) )
156 138 146 155 3eqtr3d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - S ) ) )
157 98 65 mulcomd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) = ( T x. S ) )
158 157 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S x. T ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( T x. S ) / ( ( S + T ) - ( S x. T ) ) ) )
159 98 65 85 77 div23d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S x. T ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( S / ( ( S + T ) - ( S x. T ) ) ) x. T ) )
160 133 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S / ( ( S + T ) - ( S x. T ) ) ) x. T ) = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) )
161 159 160 eqtrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S x. T ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) )
162 65 98 85 77 div23d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T x. S ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( T / ( ( S + T ) - ( S x. T ) ) ) x. S ) )
163 154 oveq1d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T / ( ( S + T ) - ( S x. T ) ) ) x. S ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. S ) )
164 162 163 eqtrd 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T x. S ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. S ) )
165 158 161 164 3eqtr3d 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. S ) )
166 oveq2 
 |-  ( r = ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( 1 - r ) = ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) )
167 166 oveq1d 
 |-  ( r = ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( ( 1 - r ) x. ( 1 - T ) ) = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - T ) ) )
168 167 eqeq2d 
 |-  ( r = ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( p = ( ( 1 - r ) x. ( 1 - T ) ) <-> p = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - T ) ) ) )
169 eqeq1 
 |-  ( r = ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( r = ( ( 1 - p ) x. ( 1 - S ) ) <-> ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - p ) x. ( 1 - S ) ) ) )
170 166 oveq1d 
 |-  ( r = ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( ( 1 - r ) x. T ) = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) )
171 170 eqeq1d 
 |-  ( r = ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) <-> ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) = ( ( 1 - p ) x. S ) ) )
172 168 169 171 3anbi123d 
 |-  ( r = ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) <-> ( p = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - T ) ) /\ ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) = ( ( 1 - p ) x. S ) ) ) )
173 eqeq1 
 |-  ( p = ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( p = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - T ) ) <-> ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - T ) ) ) )
174 oveq2 
 |-  ( p = ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( 1 - p ) = ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) )
175 174 oveq1d 
 |-  ( p = ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( ( 1 - p ) x. ( 1 - S ) ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - S ) ) )
176 175 eqeq2d 
 |-  ( p = ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - p ) x. ( 1 - S ) ) <-> ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - S ) ) ) )
177 174 oveq1d 
 |-  ( p = ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( ( 1 - p ) x. S ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. S ) )
178 177 eqeq2d 
 |-  ( p = ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) = ( ( 1 - p ) x. S ) <-> ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. S ) ) )
179 173 176 178 3anbi123d 
 |-  ( p = ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( ( p = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - T ) ) /\ ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) = ( ( 1 - p ) x. S ) ) <-> ( ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - T ) ) /\ ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - S ) ) /\ ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. S ) ) ) )
180 172 179 rspc2ev 
 |-  ( ( ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. ( 0 [,] 1 ) /\ ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. ( 0 [,] 1 ) /\ ( ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - T ) ) /\ ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. ( 1 - S ) ) /\ ( ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. T ) = ( ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) x. S ) ) ) -> E. r e. ( 0 [,] 1 ) E. p e. ( 0 [,] 1 ) ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) )
181 92 113 135 156 165 180 syl113anc 
 |-  ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> E. r e. ( 0 [,] 1 ) E. p e. ( 0 [,] 1 ) ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) )
182 181 ex 
 |-  ( S =/= 0 -> ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) -> E. r e. ( 0 [,] 1 ) E. p e. ( 0 [,] 1 ) ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) ) )
183 52 182 pm2.61ine 
 |-  ( ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) -> E. r e. ( 0 [,] 1 ) E. p e. ( 0 [,] 1 ) ( p = ( ( 1 - r ) x. ( 1 - T ) ) /\ r = ( ( 1 - p ) x. ( 1 - S ) ) /\ ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) ) )