Theorem axpaschlem 24963

Description: Lemma for axpasch 24964. 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 9639	. . . . . . . 8 |- 1 e. RR
2		0re 9640	. . . . . . . . . . 11 |- 0 e. RR
3	2, 1	elicc2i 11697	. . . . . . . . . 10 |- ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
4	3	simp1bi 1022	. . . . . . . . 9 |- ( T e. ( 0 [,] 1 ) -> T e. RR )
5	4	ad2antrl 733	. . . . . . . 8 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. RR )
6		resubcl 9935	. . . . . . . 8 |- ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
7	1, 5, 6	sylancr 668	. . . . . . 7 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
8	7	recnd 9666	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
9	8	mul02d 9828	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. ( 1 - T ) ) = 0 )
10	9	eqcomd 2456	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 = ( 0 x. ( 1 - T ) ) )
11	2, 1	elicc2i 11697	. . . . . . . . . 10 |- ( S e. ( 0 [,] 1 ) <-> ( S e. RR /\ 0 <_ S /\ S <_ 1 ) )
12	11	simp1bi 1022	. . . . . . . . 9 |- ( S e. ( 0 [,] 1 ) -> S e. RR )
13	12	ad2antll 734	. . . . . . . 8 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. RR )
14		resubcl 9935	. . . . . . . 8 |- ( ( 1 e. RR /\ S e. RR ) -> ( 1 - S ) e. RR )
15	1, 13, 14	sylancr 668	. . . . . . 7 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. RR )
16	15	recnd 9666	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. CC )
17	16	mulid2d 9658	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. ( 1 - S ) ) = ( 1 - S ) )
18		oveq2 6296	. . . . . . 7 |- ( S = 0 -> ( 1 - S ) = ( 1 - 0 ) )
19	18	adantr 467	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) = ( 1 - 0 ) )
20		1m0e1 10717	. . . . . 6 |- ( 1 - 0 ) = 1
21	19, 20	syl6eq 2500	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) = 1 )
22	17, 21	eqtr2d 2485	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 1 = ( 1 x. ( 1 - S ) ) )
23	5	recnd 9666	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. CC )
24	23	mul02d 9828	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. T ) = 0 )
25		oveq2 6296	. . . . . . 7 |- ( S = 0 -> ( 1 x. S ) = ( 1 x. 0 ) )
26	25	adantr 467	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. S ) = ( 1 x. 0 ) )
27		ax-1cn 9594	. . . . . . 7 |- 1 e. CC
28	27	mul01i 9820	. . . . . 6 |- ( 1 x. 0 ) = 0
29	26, 28	syl6eq 2500	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. S ) = 0 )
30	24, 29	eqtr4d 2487	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. T ) = ( 1 x. S ) )
31		1elunit 11748	. . . . 5 |- 1 e. ( 0 [,] 1 )
32		0elunit 11747	. . . . 5 |- 0 e. ( 0 [,] 1 )
33		oveq2 6296	. . . . . . . . . 10 |- ( r = 1 -> ( 1 - r ) = ( 1 - 1 ) )
34		1m1e0 10675	. . . . . . . . . 10 |- ( 1 - 1 ) = 0
35	33, 34	syl6eq 2500	. . . . . . . . 9 |- ( r = 1 -> ( 1 - r ) = 0 )
36	35	oveq1d 6303	. . . . . . . 8 |- ( r = 1 -> ( ( 1 - r ) x. ( 1 - T ) ) = ( 0 x. ( 1 - T ) ) )
37	36	eqeq2d 2460	. . . . . . 7 |- ( r = 1 -> ( p = ( ( 1 - r ) x. ( 1 - T ) ) <-> p = ( 0 x. ( 1 - T ) ) ) )
38		eqeq1 2454	. . . . . . 7 |- ( r = 1 -> ( r = ( ( 1 - p ) x. ( 1 - S ) ) <-> 1 = ( ( 1 - p ) x. ( 1 - S ) ) ) )
39	35	oveq1d 6303	. . . . . . . 8 |- ( r = 1 -> ( ( 1 - r ) x. T ) = ( 0 x. T ) )
40	39	eqeq1d 2452	. . . . . . 7 |- ( r = 1 -> ( ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) <-> ( 0 x. T ) = ( ( 1 - p ) x. S ) ) )
41	37, 38, 40	3anbi123d 1338	. . . . . 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 2454	. . . . . . 7 |- ( p = 0 -> ( p = ( 0 x. ( 1 - T ) ) <-> 0 = ( 0 x. ( 1 - T ) ) ) )
43		oveq2 6296	. . . . . . . . . 10 |- ( p = 0 -> ( 1 - p ) = ( 1 - 0 ) )
44	43, 20	syl6eq 2500	. . . . . . . . 9 |- ( p = 0 -> ( 1 - p ) = 1 )
45	44	oveq1d 6303	. . . . . . . 8 |- ( p = 0 -> ( ( 1 - p ) x. ( 1 - S ) ) = ( 1 x. ( 1 - S ) ) )
46	45	eqeq2d 2460	. . . . . . 7 |- ( p = 0 -> ( 1 = ( ( 1 - p ) x. ( 1 - S ) ) <-> 1 = ( 1 x. ( 1 - S ) ) ) )
47	44	oveq1d 6303	. . . . . . . 8 |- ( p = 0 -> ( ( 1 - p ) x. S ) = ( 1 x. S ) )
48	47	eqeq2d 2460	. . . . . . 7 |- ( p = 0 -> ( ( 0 x. T ) = ( ( 1 - p ) x. S ) <-> ( 0 x. T ) = ( 1 x. S ) ) )
49	42, 46, 48	3anbi123d 1338	. . . . . 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 3160	. . . . 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 1353	. . . 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 1267	. . 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 436	. 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 733	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. RR )
55	12	ad2antll 734	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. RR )
56	55, 54	remulcld 9668	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) e. RR )
57	54, 56	resubcld 10044	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) e. RR )
58	55, 54	readdcld 9667	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S + T ) e. RR )
59	58, 56	resubcld 10044	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) e. RR )
60		1red 9655	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 1 e. RR )
61	3	simp2bi 1023	. . . . . . . . . . . 12 |- ( T e. ( 0 [,] 1 ) -> 0 <_ T )
62	61	ad2antrl 733	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ T )
63	11	simp3bi 1024	. . . . . . . . . . . 12 |- ( S e. ( 0 [,] 1 ) -> S <_ 1 )
64	63	ad2antll 734	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S <_ 1 )
65	55, 60, 54, 62, 64	lemul1ad 10543	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ ( 1 x. T ) )
66	54	recnd 9666	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. CC )
67	66	mulid2d 9658	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. T ) = T )
68	65, 67	breqtrd 4426	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ T )
69	11	simp2bi 1023	. . . . . . . . . . . 12 |- ( S e. ( 0 [,] 1 ) -> 0 <_ S )
70	69	ad2antll 734	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ S )
71		simpl 459	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S =/= 0 )
72	55, 70, 71	ne0gt0d 9769	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 < S )
73	55, 54	ltaddpos2d 10195	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 < S <-> T < ( S + T ) ) )
74	72, 73	mpbid 214	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T < ( S + T ) )
75	56, 54, 58, 68, 74	lelttrd 9790	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) < ( S + T ) )
76	56, 58	posdifd 10197	. . . . . . . 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 214	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 < ( ( S + T ) - ( S x. T ) ) )
78	77	gt0ne0d 10175	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) =/= 0 )
79	57, 59, 78	redivcld 10432	. . . . 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 10200	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ ( T - ( S x. T ) ) <-> ( S x. T ) <_ T ) )
81	68, 80	mpbird 236	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( T - ( S x. T ) ) )
82		divge0 10471	. . . . . 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 1268	. . . . 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 9780	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T <_ ( S + T ) )
85	54, 58, 56, 84	lesub1dd 10226	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) <_ ( ( S + T ) - ( S x. T ) ) )
86	59	recnd 9666	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) e. CC )
87	86	mulid2d 9658	. . . . . . 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 4428	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) )
89		ledivmul2 10481	. . . . . . 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 1271	. . . . . 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 236	. . . . 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 11697	. . . . 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 1191	. . . 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 10044	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) e. RR )
95	94, 59, 78	redivcld 10432	. . . . 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 1024	. . . . . . . . . 10 |- ( T e. ( 0 [,] 1 ) -> T <_ 1 )
97	96	ad2antrl 733	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T <_ 1 )
98	54, 60, 55, 70, 97	lemul2ad 10544	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ ( S x. 1 ) )
99	55	recnd 9666	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. CC )
100	99	mulid1d 9657	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. 1 ) = S )
101	98, 100	breqtrd 4426	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ S )
102	55, 56	subge0d 10200	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ ( S - ( S x. T ) ) <-> ( S x. T ) <_ S ) )
103	101, 102	mpbird 236	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ ( S - ( S x. T ) ) )
104		divge0 10471	. . . . . 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 1268	. . . . 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 10198	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 <_ T <-> S <_ ( S + T ) ) )
107	62, 106	mpbid 214	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S <_ ( S + T ) )
108	55, 58, 56, 107	lesub1dd 10226	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) <_ ( ( S + T ) - ( S x. T ) ) )
109	108, 87	breqtrrd 4428	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) )
110		ledivmul2 10481	. . . . . . 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 1271	. . . . . 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 236	. . . . 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 11697	. . . . 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 1191	. . . 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 668	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
116	115	recnd 9666	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
117	99, 116, 86, 78	div23d 10417	. . . . 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 10049	. . . . . . . . 9 |- ( ( S e. CC /\ 1 e. CC /\ T e. CC ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
119	27, 118	mp3an2 1351	. . . . . . . 8 |- ( ( S e. CC /\ T e. CC ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
120	99, 66, 119	syl2anc 666	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
121	100	oveq1d 6303	. . . . . . 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 2484	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. ( 1 - T ) ) = ( S - ( S x. T ) ) )
123	122	oveq1d 6303	. . . . 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 9666	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) e. CC )
125	86, 124, 86, 78	divsubdird 10419	. . . . . . 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 9666	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S + T ) e. CC )
127	56	recnd 9666	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) e. CC )
128	126, 66, 127	nnncan2d 10018	. . . . . . . . 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 9984	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - T ) = S )
130	128, 129	eqtrd 2484	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( T - ( S x. T ) ) ) = S )
131	130	oveq1d 6303	. . . . . . 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 10378	. . . . . . . 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 6303	. . . . . . 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 2492	. . . . . 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 6303	. . . . 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 2492	. . . 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 668	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. RR )
138	137	recnd 9666	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. CC )
139	66, 138, 86, 78	div23d 10417	. . . . 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 10049	. . . . . . . . 9 |- ( ( T e. CC /\ 1 e. CC /\ S e. CC ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
141	27, 140	mp3an2 1351	. . . . . . . 8 |- ( ( T e. CC /\ S e. CC ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
142	66, 99, 141	syl2anc 666	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
143	66	mulid1d 9657	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. 1 ) = T )
144	66, 99	mulcomd 9661	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. S ) = ( S x. T ) )
145	143, 144	oveq12d 6306	. . . . . . 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 2484	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. ( 1 - S ) ) = ( T - ( S x. T ) ) )
147	146	oveq1d 6303	. . . . 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 9666	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) e. CC )
149	86, 148, 86, 78	divsubdird 10419	. . . . . . 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 10018	. . . . . . . . 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 9985	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - S ) = T )
152	150, 151	eqtrd 2484	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( S - ( S x. T ) ) ) = T )
153	152	oveq1d 6303	. . . . . . 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 6303	. . . . . . 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 2492	. . . . . 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 6303	. . . . 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 2492	. . . 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 9661	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) = ( T x. S ) )
159	158	oveq1d 6303	. . . . 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 10417	. . . . . 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 6303	. . . . . 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 2484	. . . . 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 10417	. . . . . 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 6303	. . . . . 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 2484	. . . . 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 2492	. . . 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 6296	. . . . . . . 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 6303	. . . . . . 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 2460	. . . . . 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 2454	. . . . . 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 6303	. . . . . . 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 2452	. . . . . 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 1338	. . . . 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 2454	. . . . . 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 6296	. . . . . . . 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 6303	. . . . . . 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 2460	. . . . . 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 6303	. . . . . . 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 2460	. . . . . 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 1338	. . . . 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 3160	. . . 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 1279	. . 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 436	. 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 2706	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 188   /\ wa 371   /\ w3a 984   = wceq 1443   e. wcel 1886   =/= wne 2621   E.wrex 2737   class class class wbr 4401  (class class class)co 6288   CCcc 9534   RRcr 9535   0cc0 9536   1c1 9537   + caddc 9539   x. cmul 9541   < clt 9672   <_ cle 9673   - cmin 9857   / cdiv 10266   [,]cicc 11635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-po 4754  df-so 4755  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-icc 11639

This theorem is referenced by:  axpasch  24964