axpaschlem

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

		Ref	Expression
	Assertion	axpaschlem	$⊢ (T \in [0, 1] \land S \in [0, 1]) \to \exists r \in [0, 1] \exists p \in [0, 1] (p = (1 - r) (1 - T) \land r = (1 - p) (1 - S) \land (1 - r) T = (1 - p) S)$

Proof

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

Metamath Proof Explorer

Theorem axpaschlem

Proof