Theorem axpaschlem 23121

Description: Lemma for axpasch 23122. 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 9381	. . . . . . . 8 |- 1 e. RR
2		0re 9382	. . . . . . . . . . 11 |- 0 e. RR
3	2, 1	elicc2i 11357	. . . . . . . . . 10 |- ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
4	3	simp1bi 998	. . . . . . . . 9 |- ( T e. ( 0 [,] 1 ) -> T e. RR )
5	4	ad2antrl 722	. . . . . . . 8 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. RR )
6		resubcl 9669	. . . . . . . 8 |- ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
7	1, 5, 6	sylancr 658	. . . . . . 7 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
8	7	recnd 9408	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
9	8	mul02d 9563	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. ( 1 - T ) ) = 0 )
10	9	eqcomd 2446	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 = ( 0 x. ( 1 - T ) ) )
11	2, 1	elicc2i 11357	. . . . . . . . . 10 |- ( S e. ( 0 [,] 1 ) <-> ( S e. RR /\ 0 <_ S /\ S <_ 1 ) )
12	11	simp1bi 998	. . . . . . . . 9 |- ( S e. ( 0 [,] 1 ) -> S e. RR )
13	12	ad2antll 723	. . . . . . . 8 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. RR )
14		resubcl 9669	. . . . . . . 8 |- ( ( 1 e. RR /\ S e. RR ) -> ( 1 - S ) e. RR )
15	1, 13, 14	sylancr 658	. . . . . . 7 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. RR )
16	15	recnd 9408	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. CC )
17	16	mulid2d 9400	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. ( 1 - S ) ) = ( 1 - S ) )
18		oveq2 6098	. . . . . . 7 |- ( S = 0 -> ( 1 - S ) = ( 1 - 0 ) )
19	18	adantr 462	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) = ( 1 - 0 ) )
20		1m0e1 10428	. . . . . 6 |- ( 1 - 0 ) = 1
21	19, 20	syl6eq 2489	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) = 1 )
22	17, 21	eqtr2d 2474	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 1 = ( 1 x. ( 1 - S ) ) )
23	5	recnd 9408	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. CC )
24	23	mul02d 9563	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. T ) = 0 )
25		oveq2 6098	. . . . . . 7 |- ( S = 0 -> ( 1 x. S ) = ( 1 x. 0 ) )
26	25	adantr 462	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. S ) = ( 1 x. 0 ) )
27		ax-1cn 9336	. . . . . . 7 |- 1 e. CC
28	27	mul01i 9555	. . . . . 6 |- ( 1 x. 0 ) = 0
29	26, 28	syl6eq 2489	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. S ) = 0 )
30	24, 29	eqtr4d 2476	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. T ) = ( 1 x. S ) )
31		1elunit 11400	. . . . 5 |- 1 e. ( 0 [,] 1 )
32		0elunit 11399	. . . . 5 |- 0 e. ( 0 [,] 1 )
33		oveq2 6098	. . . . . . . . . 10 |- ( r = 1 -> ( 1 - r ) = ( 1 - 1 ) )
34		1m1e0 10386	. . . . . . . . . 10 |- ( 1 - 1 ) = 0
35	33, 34	syl6eq 2489	. . . . . . . . 9 |- ( r = 1 -> ( 1 - r ) = 0 )
36	35	oveq1d 6105	. . . . . . . 8 |- ( r = 1 -> ( ( 1 - r ) x. ( 1 - T ) ) = ( 0 x. ( 1 - T ) ) )
37	36	eqeq2d 2452	. . . . . . 7 |- ( r = 1 -> ( p = ( ( 1 - r ) x. ( 1 - T ) ) <-> p = ( 0 x. ( 1 - T ) ) ) )
38		eqeq1 2447	. . . . . . 7 |- ( r = 1 -> ( r = ( ( 1 - p ) x. ( 1 - S ) ) <-> 1 = ( ( 1 - p ) x. ( 1 - S ) ) ) )
39	35	oveq1d 6105	. . . . . . . 8 |- ( r = 1 -> ( ( 1 - r ) x. T ) = ( 0 x. T ) )
40	39	eqeq1d 2449	. . . . . . 7 |- ( r = 1 -> ( ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) <-> ( 0 x. T ) = ( ( 1 - p ) x. S ) ) )
41	37, 38, 40	3anbi123d 1284	. . . . . 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 2447	. . . . . . 7 |- ( p = 0 -> ( p = ( 0 x. ( 1 - T ) ) <-> 0 = ( 0 x. ( 1 - T ) ) ) )
43		oveq2 6098	. . . . . . . . . 10 |- ( p = 0 -> ( 1 - p ) = ( 1 - 0 ) )
44	43, 20	syl6eq 2489	. . . . . . . . 9 |- ( p = 0 -> ( 1 - p ) = 1 )
45	44	oveq1d 6105	. . . . . . . 8 |- ( p = 0 -> ( ( 1 - p ) x. ( 1 - S ) ) = ( 1 x. ( 1 - S ) ) )
46	45	eqeq2d 2452	. . . . . . 7 |- ( p = 0 -> ( 1 = ( ( 1 - p ) x. ( 1 - S ) ) <-> 1 = ( 1 x. ( 1 - S ) ) ) )
47	44	oveq1d 6105	. . . . . . . 8 |- ( p = 0 -> ( ( 1 - p ) x. S ) = ( 1 x. S ) )
48	47	eqeq2d 2452	. . . . . . 7 |- ( p = 0 -> ( ( 0 x. T ) = ( ( 1 - p ) x. S ) <-> ( 0 x. T ) = ( 1 x. S ) ) )
49	42, 46, 48	3anbi123d 1284	. . . . . 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 3078	. . . . 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 1299	. . . 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 1213	. . 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 434	. 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 722	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. RR )
55	12	ad2antll 723	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. RR )
56	55, 54	remulcld 9410	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) e. RR )
57	54, 56	resubcld 9772	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) e. RR )
58	55, 54	readdcld 9409	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S + T ) e. RR )
59	58, 56	resubcld 9772	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) e. RR )
60	1	a1i 11	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 1 e. RR )
61	3	simp2bi 999	. . . . . . . . . . . 12 |- ( T e. ( 0 [,] 1 ) -> 0 <_ T )
62	61	ad2antrl 722	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ T )
63	11	simp3bi 1000	. . . . . . . . . . . 12 |- ( S e. ( 0 [,] 1 ) -> S <_ 1 )
64	63	ad2antll 723	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S <_ 1 )
65	55, 60, 54, 62, 64	lemul1ad 10268	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ ( 1 x. T ) )
66	54	recnd 9408	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. CC )
67	66	mulid2d 9400	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. T ) = T )
68	65, 67	breqtrd 4313	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ T )
69	11	simp2bi 999	. . . . . . . . . . . 12 |- ( S e. ( 0 [,] 1 ) -> 0 <_ S )
70	69	ad2antll 723	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ S )
71		simpl 454	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S =/= 0 )
72	55, 70, 71	ne0gt0d 9507	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 < S )
73	55, 54	ltaddpos2d 9920	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 < S <-> T < ( S + T ) ) )
74	72, 73	mpbid 210	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T < ( S + T ) )
75	56, 54, 58, 68, 74	lelttrd 9525	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) < ( S + T ) )
76	56, 58	posdifd 9922	. . . . . . . 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 210	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 < ( ( S + T ) - ( S x. T ) ) )
78	77	gt0ne0d 9900	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) =/= 0 )
79	57, 59, 78	redivcld 10155	. . . . 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 9925	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ ( T - ( S x. T ) ) <-> ( S x. T ) <_ T ) )
81	68, 80	mpbird 232	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( T - ( S x. T ) ) )
82		divge0 10194	. . . . . 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 1214	. . . . 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 9518	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T <_ ( S + T ) )
85	54, 58, 56, 84	lesub1dd 9951	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) <_ ( ( S + T ) - ( S x. T ) ) )
86	59	recnd 9408	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) e. CC )
87	86	mulid2d 9400	. . . . . . 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 4315	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) )
89		ledivmul2 10205	. . . . . . 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 1217	. . . . . 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 232	. . . . 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 11357	. . . . 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 1167	. . . 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 9772	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) e. RR )
95	94, 59, 78	redivcld 10155	. . . . 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 1000	. . . . . . . . . 10 |- ( T e. ( 0 [,] 1 ) -> T <_ 1 )
97	96	ad2antrl 722	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T <_ 1 )
98	54, 60, 55, 70, 97	lemul2ad 10269	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ ( S x. 1 ) )
99	55	recnd 9408	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. CC )
100	99	mulid1d 9399	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. 1 ) = S )
101	98, 100	breqtrd 4313	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ S )
102	55, 56	subge0d 9925	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ ( S - ( S x. T ) ) <-> ( S x. T ) <_ S ) )
103	101, 102	mpbird 232	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( S - ( S x. T ) ) )
104		divge0 10194	. . . . . 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 1214	. . . . 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 9923	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ T <-> S <_ ( S + T ) ) )
107	62, 106	mpbid 210	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S <_ ( S + T ) )
108	55, 58, 56, 107	lesub1dd 9951	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) <_ ( ( S + T ) - ( S x. T ) ) )
109	108, 87	breqtrrd 4315	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) )
110		ledivmul2 10205	. . . . . . 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 1217	. . . . . 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 232	. . . . 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 11357	. . . . 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 1167	. . . 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 658	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
116	115	recnd 9408	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
117	99, 116, 86, 78	div23d 10140	. . . . 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 9774	. . . . . . . . 9 |- ( ( S e. CC /\ 1 e. CC /\ T e. CC ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
119	27, 118	mp3an2 1297	. . . . . . . 8 |- ( ( S e. CC /\ T e. CC ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
120	99, 66, 119	syl2anc 656	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
121	100	oveq1d 6105	. . . . . . 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 2473	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. ( 1 - T ) ) = ( S - ( S x. T ) ) )
123	122	oveq1d 6105	. . . . 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 9408	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) e. CC )
125	86, 124, 86, 78	divsubdird 10142	. . . . . . 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 9408	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S + T ) e. CC )
127	56	recnd 9408	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) e. CC )
128	126, 66, 127	nnncan2d 9750	. . . . . . . . 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 9716	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - T ) = S )
130	128, 129	eqtrd 2473	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( T - ( S x. T ) ) ) = S )
131	130	oveq1d 6105	. . . . . . 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 10101	. . . . . . . 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 6105	. . . . . . 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 2481	. . . . . 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 6105	. . . . 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 2481	. . . 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 658	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. RR )
138	137	recnd 9408	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. CC )
139	66, 138, 86, 78	div23d 10140	. . . . 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 9774	. . . . . . . . 9 |- ( ( T e. CC /\ 1 e. CC /\ S e. CC ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
141	27, 140	mp3an2 1297	. . . . . . . 8 |- ( ( T e. CC /\ S e. CC ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
142	66, 99, 141	syl2anc 656	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
143	66	mulid1d 9399	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. 1 ) = T )
144	66, 99	mulcomd 9403	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. S ) = ( S x. T ) )
145	143, 144	oveq12d 6108	. . . . . . 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 2473	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. ( 1 - S ) ) = ( T - ( S x. T ) ) )
147	146	oveq1d 6105	. . . . 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 9408	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) e. CC )
149	86, 148, 86, 78	divsubdird 10142	. . . . . . 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 9750	. . . . . . . . 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 9717	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - S ) = T )
152	150, 151	eqtrd 2473	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( S - ( S x. T ) ) ) = T )
153	152	oveq1d 6105	. . . . . . 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 6105	. . . . . . 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 2481	. . . . . 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 6105	. . . . 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 2481	. . . 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 9403	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) = ( T x. S ) )
159	158	oveq1d 6105	. . . . 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 10140	. . . . . 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 6105	. . . . . 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 2473	. . . . 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 10140	. . . . . 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 6105	. . . . . 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 2473	. . . . 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 2481	. . . 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 6098	. . . . . . . 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 6105	. . . . . . 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 2452	. . . . . 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 2447	. . . . . 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 6105	. . . . . . 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 2449	. . . . . 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 1284	. . . . 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 2447	. . . . . 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 6098	. . . . . . . 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 6105	. . . . . . 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 2452	. . . . . 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 6105	. . . . . . 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 2452	. . . . . 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 1284	. . . . 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 3078	. . . 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 1225	. . 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 434	. 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 2685	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 184   /\ wa 369   /\ w3a 960   = wceq 1364   e. wcel 1761   =/= wne 2604   E.wrex 2714   class class class wbr 4289  (class class class)co 6090   CCcc 9276   RRcr 9277   0cc0 9278   1c1 9279   + caddc 9281   x. cmul 9283   < clt 9414   <_ cle 9415   - cmin 9591   / cdiv 9989   [,]cicc 11299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-po 4637  df-so 4638  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-div 9990  df-icc 11303

This theorem is referenced by:  axpasch  23122