Theorem axpaschlem 23201

Description: Lemma for axpasch 23202. 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 9400	. . . . . . . 8 |- 1 e. RR
2		0re 9401	. . . . . . . . . . 11 |- 0 e. RR
3	2, 1	elicc2i 11376	. . . . . . . . . 10 |- ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
4	3	simp1bi 1003	. . . . . . . . 9 |- ( T e. ( 0 [,] 1 ) -> T e. RR )
5	4	ad2antrl 727	. . . . . . . 8 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. RR )
6		resubcl 9688	. . . . . . . 8 |- ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
7	1, 5, 6	sylancr 663	. . . . . . 7 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
8	7	recnd 9427	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
9	8	mul02d 9582	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. ( 1 - T ) ) = 0 )
10	9	eqcomd 2448	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 = ( 0 x. ( 1 - T ) ) )
11	2, 1	elicc2i 11376	. . . . . . . . . 10 |- ( S e. ( 0 [,] 1 ) <-> ( S e. RR /\ 0 <_ S /\ S <_ 1 ) )
12	11	simp1bi 1003	. . . . . . . . 9 |- ( S e. ( 0 [,] 1 ) -> S e. RR )
13	12	ad2antll 728	. . . . . . . 8 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. RR )
14		resubcl 9688	. . . . . . . 8 |- ( ( 1 e. RR /\ S e. RR ) -> ( 1 - S ) e. RR )
15	1, 13, 14	sylancr 663	. . . . . . 7 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. RR )
16	15	recnd 9427	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. CC )
17	16	mulid2d 9419	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. ( 1 - S ) ) = ( 1 - S ) )
18		oveq2 6114	. . . . . . 7 |- ( S = 0 -> ( 1 - S ) = ( 1 - 0 ) )
19	18	adantr 465	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) = ( 1 - 0 ) )
20		1m0e1 10447	. . . . . 6 |- ( 1 - 0 ) = 1
21	19, 20	syl6eq 2491	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) = 1 )
22	17, 21	eqtr2d 2476	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 1 = ( 1 x. ( 1 - S ) ) )
23	5	recnd 9427	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. CC )
24	23	mul02d 9582	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. T ) = 0 )
25		oveq2 6114	. . . . . . 7 |- ( S = 0 -> ( 1 x. S ) = ( 1 x. 0 ) )
26	25	adantr 465	. . . . . 6 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. S ) = ( 1 x. 0 ) )
27		ax-1cn 9355	. . . . . . 7 |- 1 e. CC
28	27	mul01i 9574	. . . . . 6 |- ( 1 x. 0 ) = 0
29	26, 28	syl6eq 2491	. . . . 5 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. S ) = 0 )
30	24, 29	eqtr4d 2478	. . . 4 |- ( ( S = 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 0 x. T ) = ( 1 x. S ) )
31		1elunit 11419	. . . . 5 |- 1 e. ( 0 [,] 1 )
32		0elunit 11418	. . . . 5 |- 0 e. ( 0 [,] 1 )
33		oveq2 6114	. . . . . . . . . 10 |- ( r = 1 -> ( 1 - r ) = ( 1 - 1 ) )
34		1m1e0 10405	. . . . . . . . . 10 |- ( 1 - 1 ) = 0
35	33, 34	syl6eq 2491	. . . . . . . . 9 |- ( r = 1 -> ( 1 - r ) = 0 )
36	35	oveq1d 6121	. . . . . . . 8 |- ( r = 1 -> ( ( 1 - r ) x. ( 1 - T ) ) = ( 0 x. ( 1 - T ) ) )
37	36	eqeq2d 2454	. . . . . . 7 |- ( r = 1 -> ( p = ( ( 1 - r ) x. ( 1 - T ) ) <-> p = ( 0 x. ( 1 - T ) ) ) )
38		eqeq1 2449	. . . . . . 7 |- ( r = 1 -> ( r = ( ( 1 - p ) x. ( 1 - S ) ) <-> 1 = ( ( 1 - p ) x. ( 1 - S ) ) ) )
39	35	oveq1d 6121	. . . . . . . 8 |- ( r = 1 -> ( ( 1 - r ) x. T ) = ( 0 x. T ) )
40	39	eqeq1d 2451	. . . . . . 7 |- ( r = 1 -> ( ( ( 1 - r ) x. T ) = ( ( 1 - p ) x. S ) <-> ( 0 x. T ) = ( ( 1 - p ) x. S ) ) )
41	37, 38, 40	3anbi123d 1289	. . . . . 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 2449	. . . . . . 7 |- ( p = 0 -> ( p = ( 0 x. ( 1 - T ) ) <-> 0 = ( 0 x. ( 1 - T ) ) ) )
43		oveq2 6114	. . . . . . . . . 10 |- ( p = 0 -> ( 1 - p ) = ( 1 - 0 ) )
44	43, 20	syl6eq 2491	. . . . . . . . 9 |- ( p = 0 -> ( 1 - p ) = 1 )
45	44	oveq1d 6121	. . . . . . . 8 |- ( p = 0 -> ( ( 1 - p ) x. ( 1 - S ) ) = ( 1 x. ( 1 - S ) ) )
46	45	eqeq2d 2454	. . . . . . 7 |- ( p = 0 -> ( 1 = ( ( 1 - p ) x. ( 1 - S ) ) <-> 1 = ( 1 x. ( 1 - S ) ) ) )
47	44	oveq1d 6121	. . . . . . . 8 |- ( p = 0 -> ( ( 1 - p ) x. S ) = ( 1 x. S ) )
48	47	eqeq2d 2454	. . . . . . 7 |- ( p = 0 -> ( ( 0 x. T ) = ( ( 1 - p ) x. S ) <-> ( 0 x. T ) = ( 1 x. S ) ) )
49	42, 46, 48	3anbi123d 1289	. . . . . 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 3096	. . . . 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 1304	. . . 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 1218	. . 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 727	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. RR )
55	12	ad2antll 728	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. RR )
56	55, 54	remulcld 9429	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) e. RR )
57	54, 56	resubcld 9791	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) e. RR )
58	55, 54	readdcld 9428	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S + T ) e. RR )
59	58, 56	resubcld 9791	. . . . . 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 1004	. . . . . . . . . . . 12 |- ( T e. ( 0 [,] 1 ) -> 0 <_ T )
62	61	ad2antrl 727	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ T )
63	11	simp3bi 1005	. . . . . . . . . . . 12 |- ( S e. ( 0 [,] 1 ) -> S <_ 1 )
64	63	ad2antll 728	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S <_ 1 )
65	55, 60, 54, 62, 64	lemul1ad 10287	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ ( 1 x. T ) )
66	54	recnd 9427	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T e. CC )
67	66	mulid2d 9419	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 x. T ) = T )
68	65, 67	breqtrd 4331	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ T )
69	11	simp2bi 1004	. . . . . . . . . . . 12 |- ( S e. ( 0 [,] 1 ) -> 0 <_ S )
70	69	ad2antll 728	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 <_ S )
71		simpl 457	. . . . . . . . . . 11 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S =/= 0 )
72	55, 70, 71	ne0gt0d 9526	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> 0 < S )
73	55, 54	ltaddpos2d 9939	. . . . . . . . . 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 9544	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) < ( S + T ) )
76	56, 58	posdifd 9941	. . . . . . . 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 9919	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) =/= 0 )
79	57, 59, 78	redivcld 10174	. . . . 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 9944	. . . . . . 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 10213	. . . . . 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 1219	. . . . 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 9537	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T <_ ( S + T ) )
85	54, 58, 56, 84	lesub1dd 9970	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) <_ ( ( S + T ) - ( S x. T ) ) )
86	59	recnd 9427	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - ( S x. T ) ) e. CC )
87	86	mulid2d 9419	. . . . . . 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 4333	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) )
89		ledivmul2 10224	. . . . . . 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 1222	. . . . . 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 11376	. . . . 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 1172	. . . 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 9791	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) e. RR )
95	94, 59, 78	redivcld 10174	. . . . 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 1005	. . . . . . . . . 10 |- ( T e. ( 0 [,] 1 ) -> T <_ 1 )
97	96	ad2antrl 727	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> T <_ 1 )
98	54, 60, 55, 70, 97	lemul2ad 10288	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ ( S x. 1 ) )
99	55	recnd 9427	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> S e. CC )
100	99	mulid1d 9418	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. 1 ) = S )
101	98, 100	breqtrd 4331	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) <_ S )
102	55, 56	subge0d 9944	. . . . . . 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 10213	. . . . . 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 1219	. . . . 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 9942	. . . . . . . . 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 9970	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) <_ ( ( S + T ) - ( S x. T ) ) )
109	108, 87	breqtrrd 4333	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) <_ ( 1 x. ( ( S + T ) - ( S x. T ) ) ) )
110		ledivmul2 10224	. . . . . . 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 1222	. . . . . 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 11376	. . . . 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 1172	. . . 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 663	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
116	115	recnd 9427	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
117	99, 116, 86, 78	div23d 10159	. . . . 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 9793	. . . . . . . . 9 |- ( ( S e. CC /\ 1 e. CC /\ T e. CC ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
119	27, 118	mp3an2 1302	. . . . . . . 8 |- ( ( S e. CC /\ T e. CC ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
120	99, 66, 119	syl2anc 661	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. ( 1 - T ) ) = ( ( S x. 1 ) - ( S x. T ) ) )
121	100	oveq1d 6121	. . . . . . 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 2475	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. ( 1 - T ) ) = ( S - ( S x. T ) ) )
123	122	oveq1d 6121	. . . . 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 9427	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T - ( S x. T ) ) e. CC )
125	86, 124, 86, 78	divsubdird 10161	. . . . . . 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 9427	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S + T ) e. CC )
127	56	recnd 9427	. . . . . . . . . 10 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) e. CC )
128	126, 66, 127	nnncan2d 9769	. . . . . . . . 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 9735	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - T ) = S )
130	128, 129	eqtrd 2475	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( T - ( S x. T ) ) ) = S )
131	130	oveq1d 6121	. . . . . . 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 10120	. . . . . . . 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 6121	. . . . . . 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 2483	. . . . . 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 6121	. . . . 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 2483	. . . 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 663	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. RR )
138	137	recnd 9427	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( 1 - S ) e. CC )
139	66, 138, 86, 78	div23d 10159	. . . . 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 9793	. . . . . . . . 9 |- ( ( T e. CC /\ 1 e. CC /\ S e. CC ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
141	27, 140	mp3an2 1302	. . . . . . . 8 |- ( ( T e. CC /\ S e. CC ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
142	66, 99, 141	syl2anc 661	. . . . . . 7 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. ( 1 - S ) ) = ( ( T x. 1 ) - ( T x. S ) ) )
143	66	mulid1d 9418	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. 1 ) = T )
144	66, 99	mulcomd 9422	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. S ) = ( S x. T ) )
145	143, 144	oveq12d 6124	. . . . . . 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 2475	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( T x. ( 1 - S ) ) = ( T - ( S x. T ) ) )
147	146	oveq1d 6121	. . . . 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 9427	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S - ( S x. T ) ) e. CC )
149	86, 148, 86, 78	divsubdird 10161	. . . . . . 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 9769	. . . . . . . . 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 9736	. . . . . . . . 9 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( S + T ) - S ) = T )
152	150, 151	eqtrd 2475	. . . . . . . 8 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( ( ( S + T ) - ( S x. T ) ) - ( S - ( S x. T ) ) ) = T )
153	152	oveq1d 6121	. . . . . . 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 6121	. . . . . . 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 2483	. . . . . 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 6121	. . . . 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 2483	. . . 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 9422	. . . . . 6 |- ( ( S =/= 0 /\ ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) ) -> ( S x. T ) = ( T x. S ) )
159	158	oveq1d 6121	. . . . 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 10159	. . . . . 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 6121	. . . . . 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 2475	. . . . 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 10159	. . . . . 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 6121	. . . . . 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 2475	. . . . 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 2483	. . . 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 6114	. . . . . . . 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 6121	. . . . . . 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 2454	. . . . . 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 2449	. . . . . 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 6121	. . . . . . 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 2451	. . . . . 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 1289	. . . . 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 2449	. . . . . 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 6114	. . . . . . . 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 6121	. . . . . . 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 2454	. . . . . 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 6121	. . . . . . 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 2454	. . . . . 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 1289	. . . . 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 3096	. . . 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 1230	. . 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 2702	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 965   = wceq 1369   e. wcel 1756   =/= wne 2620   E.wrex 2731   class class class wbr 4307  (class class class)co 6106   CCcc 9295   RRcr 9296   0cc0 9297   1c1 9298   + caddc 9300   x. cmul 9302   < clt 9433   <_ cle 9434   - cmin 9610   / cdiv 10008   [,]cicc 11318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-br 4308  df-opab 4366  df-mpt 4367  df-id 4651  df-po 4656  df-so 4657  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-er 7116  df-en 7326  df-dom 7327  df-sdom 7328  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-div 10009  df-icc 11322

This theorem is referenced by:  axpasch  23202