Theorem axpaschlem 25820

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

Assertion

Ref	Expression
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 ) ) )

Distinct variable groups:   T, p, r   S, p, r

Proof of Theorem axpaschlem

Step	Hyp	Ref	Expression
1		1re 10039	. . . . . . . 8 |- 1 e. RR
2		0re 10040	. . . . . . . . . . 11 |- 0 e. RR
3	2, 1	elicc2i 12239	. . . . . . . . . 10 |- ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
4	3	simp1bi 1076	. . . . . . . . 9 |- ( T e. ( 0 [,] 1 ) -> T e. RR )
5	4	ad2antrl 764	. . . . . . . 8 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. RR )
6		resubcl 10345	. . . . . . . 8 |- ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
7	1, 5, 6	sylancr 695	. . . . . . 7 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
8	7	recnd 10068	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
9	8	mul02d 10234	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. ( 1 - T ) ) = 0 )
10	9	eqcomd 2628	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 = ( 0 x. ( 1 - T ) ) )
11	2, 1	elicc2i 12239	. . . . . . . . . 10 |- ( S e. ( 0 [,] 1 ) <-> ( S e. RR /\ 0 <_ S /\ S <_ 1 ) )
12	11	simp1bi 1076	. . . . . . . . 9 |- ( S e. ( 0 [,] 1 ) -> S e. RR )
13	12	ad2antll 765	. . . . . . . 8 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. RR )
14		resubcl 10345	. . . . . . . 8 |- ( ( 1 e. RR /\ S e. RR ) -> ( 1 - S ) e. RR )
15	1, 13, 14	sylancr 695	. . . . . . 7 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. RR )
16	15	recnd 10068	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. CC )
17	16	mulid2d 10058	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. ( 1 - S ) ) = ( 1 - S ) )
18		oveq2 6658	. . . . . . 7 |- ( S = 0 -> ( 1 - S ) = ( 1 - 0 ) )
19	18	adantr 481	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) = ( 1 - 0 ) )
20		1m0e1 11131	. . . . . 6 |- ( 1 - 0 ) = 1
21	19, 20	syl6eq 2672	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) = 1 )
22	17, 21	eqtr2d 2657	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 1 = ( 1 x. ( 1 - S ) ) )
23	5	recnd 10068	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. CC )
24	23	mul02d 10234	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. T ) = 0 )
25		oveq2 6658	. . . . . . 7 |- ( S = 0 -> ( 1 x. S ) = ( 1 x. 0 ) )
26	25	adantr 481	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. S ) = ( 1 x. 0 ) )
27		ax-1cn 9994	. . . . . . 7 |- 1 e. CC
28	27	mul01i 10226	. . . . . 6 |- ( 1 x. 0 ) = 0
29	26, 28	syl6eq 2672	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. S ) = 0 )
30	24, 29	eqtr4d 2659	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. T ) = ( 1 x. S ) )
31		1elunit 12291	. . . . 5 |- 1 e. ( 0 [,] 1 )
32		0elunit 12290	. . . . 5 |- 0 e. ( 0 [,] 1 )
33		oveq2 6658	. . . . . . . . . 10 |- ( r = 1 -> ( 1 - r ) = ( 1 - 1 ) )
34		1m1e0 11089	. . . . . . . . . 10 |- ( 1 - 1 ) = 0
35	33, 34	syl6eq 2672	. . . . . . . . 9 |- ( r = 1 -> ( 1 - r ) = 0 )
36	35	oveq1d 6665	. . . . . . . 8 |- ( r = 1 -> ( ( 1 - r ) x. ( 1 - T ) ) = ( 0 x. ( 1 - T ) ) )
37	36	eqeq2d 2632	. . . . . . 7 |- ( r = 1 -> ( p = ( ( 1 - r ) x. ( 1 - T ) ) <-> p = ( 0 x. ( 1 - T ) ) ) )
38		eqeq1 2626	. . . . . . 7 |- ( r = 1 -> ( r = ( ( 1 - p ) x. ( 1 - S ) ) <-> 1 = ( ( 1 - p ) x. ( 1 - S ) ) ) )
39	35	oveq1d 6665	. . . . . . . 8 |- ( r = 1 -> ( ( 1 - r ) x. T ) = ( 0 x. T ) )
40	39	eqeq1d 2624	. . . . . . 7 |- ( r = 1 -> ( ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) <-> ( 0 x. T ) = ( ( 1 - p ) x. S ) ) )
41	37, 38, 40	3anbi123d 1399	. . . . . 6 |- ( 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 ) ) ) )
42		eqeq1 2626	. . . . . . 7 |- ( p = 0 -> ( p = ( 0 x. ( 1 - T ) ) <-> 0 = ( 0 x. ( 1 - T ) ) ) )
43		oveq2 6658	. . . . . . . . . 10 |- ( p = 0 -> ( 1 - p ) = ( 1 - 0 ) )
44	43, 20	syl6eq 2672	. . . . . . . . 9 |- ( p = 0 -> ( 1 - p ) = 1 )
45	44	oveq1d 6665	. . . . . . . 8 |- ( p = 0 -> ( ( 1 - p ) x. ( 1 - S ) ) = ( 1 x. ( 1 - S ) ) )
46	45	eqeq2d 2632	. . . . . . 7 |- ( p = 0 -> ( 1 = ( ( 1 - p ) x. ( 1 - S ) ) <-> 1 = ( 1 x. ( 1 - S ) ) ) )
47	44	oveq1d 6665	. . . . . . . 8 |- ( p = 0 -> ( ( 1 - p ) x. S ) = ( 1 x. S ) )
48	47	eqeq2d 2632	. . . . . . 7 |- ( p = 0 -> ( ( 0 x. T ) = ( ( 1 - p ) x. S ) <-> ( 0 x. T ) = ( 1 x. S ) ) )
49	42, 46, 48	3anbi123d 1399	. . . . . 6 |- ( 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 ) ) ) )
50	41, 49	rspc2ev 3324	. . . . 5 |- ( ( 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 ) ) )
51	31, 32, 50	mp3an12 1414	. . . 4 |- ( ( 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 ) ) )
52	10, 22, 30, 51	syl3anc 1326	. . 3 |- ( ( 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	52	ex 450	. 2 |- ( 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 ) ) ) )
54	4	ad2antrl 764	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. RR )
55	12	ad2antll 765	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. RR )
56	55, 54	remulcld 10070	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) e. RR )
57	54, 56	resubcld 10458	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) e. RR )
58	55, 54	readdcld 10069	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S + T ) e. RR )
59	58, 56	resubcld 10458	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) e. RR )
60		1red 10055	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 1 e. RR )
61	3	simp2bi 1077	. . . . . . . . . . . 12 |- ( T e. ( 0 [,] 1 ) -> 0 <_ T )
62	61	ad2antrl 764	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ T )
63	11	simp3bi 1078	. . . . . . . . . . . 12 |- ( S e. ( 0 [,] 1 ) -> S <_ 1 )
64	63	ad2antll 765	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S <_ 1 )
65	55, 60, 54, 62, 64	lemul1ad 10963	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ ( 1 x. T ) )
66	54	recnd 10068	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. CC )
67	66	mulid2d 10058	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. T ) = T )
68	65, 67	breqtrd 4679	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ T )
69	11	simp2bi 1077	. . . . . . . . . . . 12 |- ( S e. ( 0 [,] 1 ) -> 0 <_ S )
70	69	ad2antll 765	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ S )
71		simpl 473	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S =/= 0 )
72	55, 70, 71	ne0gt0d 10174	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 < S )
73	55, 54	ltaddpos2d 10612	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 < S <-> T < ( S + T ) ) )
74	72, 73	mpbid 222	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T < ( S + T ) )
75	56, 54, 58, 68, 74	lelttrd 10195	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) < ( S + T ) )
76	56, 58	posdifd 10614	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S x. T ) < ( S + T ) <-> 0 < ( ( S + T ) - ( S x. T ) ) ) )
77	75, 76	mpbid 222	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 < ( ( S + T ) - ( S x. T ) ) )
78	77	gt0ne0d 10592	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) =/= 0 )
79	57, 59, 78	redivcld 10853	. . . . 5 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. RR )
80	54, 56	subge0d 10617	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ ( T - ( S x. T ) ) <-> ( S x. T ) <_ T ) )
81	68, 80	mpbird 247	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( T - ( S x. T ) ) )
82		divge0 10892	. . . . . 6 |- ( ( ( ( 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 ) ) ) )
83	57, 81, 59, 77, 82	syl22anc 1327	. . . . 5 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) )
84	54, 58, 74	ltled 10185	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T <_ ( S + T ) )
85	54, 58, 56, 84	lesub1dd 10643	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) <_ ( ( S + T ) - ( S x. T ) ) )
86	59	recnd 10068	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) e. CC )
87	86	mulid2d 10058	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. ( ( S + T ) - ( S x. T ) ) ) = ( ( S + T ) - ( S x. T ) ) )
88	85, 87	breqtrrd 4681	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) )
89		ledivmul2 10902	. . . . . . 7 |- ( ( ( 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 ) ) ) ) )
90	57, 60, 59, 77, 89	syl112anc 1330	. . . . . 6 |- ( ( 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 ) ) ) ) )
91	88, 90	mpbird 247	. . . . 5 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) <_ 1 )
92	2, 1	elicc2i 12239	. . . . 5 |- ( ( ( 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 ) )
93	79, 83, 91, 92	syl3anbrc 1246	. . . 4 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. ( 0 [,] 1 ) )
94	55, 56	resubcld 10458	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) e. RR )
95	94, 59, 78	redivcld 10853	. . . . 5 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. RR )
96	3	simp3bi 1078	. . . . . . . . . 10 |- ( T e. ( 0 [,] 1 ) -> T <_ 1 )
97	96	ad2antrl 764	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T <_ 1 )
98	54, 60, 55, 70, 97	lemul2ad 10964	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ ( S x. 1 ) )
99	55	recnd 10068	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. CC )
100	99	mulid1d 10057	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. 1 ) = S )
101	98, 100	breqtrd 4679	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ S )
102	55, 56	subge0d 10617	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ ( S - ( S x. T ) ) <-> ( S x. T ) <_ S ) )
103	101, 102	mpbird 247	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( S - ( S x. T ) ) )
104		divge0 10892	. . . . . 6 |- ( ( ( ( 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 ) ) ) )
105	94, 103, 59, 77, 104	syl22anc 1327	. . . . 5 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) )
106	55, 54	addge01d 10615	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ T <-> S <_ ( S + T ) ) )
107	62, 106	mpbid 222	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S <_ ( S + T ) )
108	55, 58, 56, 107	lesub1dd 10643	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) <_ ( ( S + T ) - ( S x. T ) ) )
109	108, 87	breqtrrd 4681	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) )
110		ledivmul2 10902	. . . . . . 7 |- ( ( ( 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 ) ) ) ) )
111	94, 60, 59, 77, 110	syl112anc 1330	. . . . . 6 |- ( ( 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 ) ) ) ) )
112	109, 111	mpbird 247	. . . . 5 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) <_ 1 )
113	2, 1	elicc2i 12239	. . . . 5 |- ( ( ( 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 ) )
114	95, 105, 112, 113	syl3anbrc 1246	. . . 4 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) e. ( 0 [,] 1 ) )
115	1, 54, 6	sylancr 695	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
116	115	recnd 10068	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
117	99, 116, 86, 78	div23d 10838	. . . . 5 |- ( ( 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 ) ) )
118		subdi 10463	. . . . . . . . 9 |- ( ( S e. CC /\ 1 e. CC /\ T e. CC ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
119	27, 118	mp3an2 1412	. . . . . . . 8 |- ( ( S e. CC /\ T e. CC ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
120	99, 66, 119	syl2anc 693	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
121	100	oveq1d 6665	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S x. 1 ) - ( S x. T ) ) = ( S - ( S x. T ) ) )
122	120, 121	eqtrd 2656	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. ( 1 - T ) ) = ( S - ( S x. T ) ) )
123	122	oveq1d 6665	. . . . 5 |- ( ( 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 ) ) ) )
124	57	recnd 10068	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) e. CC )
125	86, 124, 86, 78	divsubdird 10840	. . . . . . 7 |- ( ( 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 ) ) ) ) )
126	58	recnd 10068	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S + T ) e. CC )
127	56	recnd 10068	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) e. CC )
128	126, 66, 127	nnncan2d 10427	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( T - ( S x. T ) ) ) = ( ( S + T ) - T ) )
129	99, 66	pncand 10393	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - T ) = S )
130	128, 129	eqtrd 2656	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( T - ( S x. T ) ) ) = S )
131	130	oveq1d 6665	. . . . . . 7 |- ( ( 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 ) ) ) )
132	86, 78	dividd 10799	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) = 1 )
133	132	oveq1d 6665	. . . . . . 7 |- ( ( 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 ) ) ) ) )
134	125, 131, 133	3eqtr3d 2664	. . . . . 6 |- ( ( 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 ) ) ) ) )
135	134	oveq1d 6665	. . . . 5 |- ( ( 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 ) ) )
136	117, 123, 135	3eqtr3d 2664	. . . 4 |- ( ( 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 ) ) )
137	1, 55, 14	sylancr 695	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. RR )
138	137	recnd 10068	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. CC )
139	66, 138, 86, 78	div23d 10838	. . . . 5 |- ( ( 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 ) ) )
140		subdi 10463	. . . . . . . . 9 |- ( ( T e. CC /\ 1 e. CC /\ S e. CC ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
141	27, 140	mp3an2 1412	. . . . . . . 8 |- ( ( T e. CC /\ S e. CC ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
142	66, 99, 141	syl2anc 693	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
143	66	mulid1d 10057	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. 1 ) = T )
144	66, 99	mulcomd 10061	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. S ) = ( S x. T ) )
145	143, 144	oveq12d 6668	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( T x. 1 ) - ( T x. S ) ) = ( T - ( S x. T ) ) )
146	142, 145	eqtrd 2656	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. ( 1 - S ) ) = ( T - ( S x. T ) ) )
147	146	oveq1d 6665	. . . . 5 |- ( ( 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 ) ) ) )
148	94	recnd 10068	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) e. CC )
149	86, 148, 86, 78	divsubdird 10840	. . . . . . 7 |- ( ( 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 ) ) ) ) )
150	126, 99, 127	nnncan2d 10427	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( S - ( S x. T ) ) ) = ( ( S + T ) - S ) )
151	99, 66	pncan2d 10394	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - S ) = T )
152	150, 151	eqtrd 2656	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( S - ( S x. T ) ) ) = T )
153	152	oveq1d 6665	. . . . . . 7 |- ( ( 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 ) ) ) )
154	132	oveq1d 6665	. . . . . . 7 |- ( ( 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 ) ) ) ) )
155	149, 153, 154	3eqtr3d 2664	. . . . . 6 |- ( ( 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 ) ) ) ) )
156	155	oveq1d 6665	. . . . 5 |- ( ( 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 ) ) )
157	139, 147, 156	3eqtr3d 2664	. . . 4 |- ( ( 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 ) ) )
158	99, 66	mulcomd 10061	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) = ( T x. S ) )
159	158	oveq1d 6665	. . . . 5 |- ( ( 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 ) ) ) )
160	99, 66, 86, 78	div23d 10838	. . . . . 6 |- ( ( 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 ) )
161	134	oveq1d 6665	. . . . . 6 |- ( ( 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 ) )
162	160, 161	eqtrd 2656	. . . . 5 |- ( ( 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 ) )
163	66, 99, 86, 78	div23d 10838	. . . . . 6 |- ( ( 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 ) )
164	155	oveq1d 6665	. . . . . 6 |- ( ( 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 ) )
165	163, 164	eqtrd 2656	. . . . 5 |- ( ( 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 ) )
166	159, 162, 165	3eqtr3d 2664	. . . 4 |- ( ( 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 ) )
167		oveq2 6658	. . . . . . . 8 |- ( r = ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( 1 - r ) = ( 1 - ( ( T - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) )
168	167	oveq1d 6665	. . . . . . 7 |- ( 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 ) ) )
169	168	eqeq2d 2632	. . . . . 6 |- ( 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 ) ) ) )
170		eqeq1 2626	. . . . . 6 |- ( 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 ) ) ) )
171	167	oveq1d 6665	. . . . . . 7 |- ( 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 ) )
172	171	eqeq1d 2624	. . . . . 6 |- ( 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 ) ) )
173	169, 170, 172	3anbi123d 1399	. . . . 5 |- ( 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 ) ) ) )
174		eqeq1 2626	. . . . . 6 |- ( 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 ) ) ) )
175		oveq2 6658	. . . . . . . 8 |- ( p = ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) -> ( 1 - p ) = ( 1 - ( ( S - ( S x. T ) ) / ( ( S + T ) - ( S x. T ) ) ) ) )
176	175	oveq1d 6665	. . . . . . 7 |- ( 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 ) ) )
177	176	eqeq2d 2632	. . . . . 6 |- ( 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 ) ) ) )
178	175	oveq1d 6665	. . . . . . 7 |- ( 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 ) )
179	178	eqeq2d 2632	. . . . . 6 |- ( 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 ) ) )
180	174, 177, 179	3anbi123d 1399	. . . . 5 |- ( 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 ) ) ) )
181	173, 180	rspc2ev 3324	. . . 4 |- ( ( ( ( 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 ) ) )
182	93, 114, 136, 157, 166, 181	syl113anc 1338	. . 3 |- ( ( 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	182	ex 450	. 2 |- ( 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 ) ) ) )
184	53, 183	pm2.61ine 2877	1 |- ( ( 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 ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   E.wrex 2913   class class class wbr 4653  (class class class)co 6650   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   [,]cicc 12178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-icc 12182

This theorem is referenced by:  axpasch  25821