Theorem axpaschlem 26734

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

Assertion

Ref	Expression
axpaschlem	⊢ ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))

Distinct variable groups:   𝑇,𝑝,𝑟   𝑆,𝑝,𝑟

Proof of Theorem axpaschlem

Step	Hyp	Ref	Expression
1		1re 10630	. . . . . . . 8 ⊢ 1 ∈ ℝ
2		elicc01 12844	. . . . . . . . . 10 ⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
3	2	simp1bi 1142	. . . . . . . . 9 ⊢ (𝑇 ∈ (0[,]1) → 𝑇 ∈ ℝ)
4	3	ad2antrl 727	. . . . . . . 8 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5		resubcl 10939	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
6	1, 4, 5	sylancr 590	. . . . . . 7 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
7	6	recnd 10658	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
8	7	mul02d 10827	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · (1 − 𝑇)) = 0)
9	8	eqcomd 2804	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 = (0 · (1 − 𝑇)))
10		elicc01 12844	. . . . . . . . . 10 ⊢ (𝑆 ∈ (0[,]1) ↔ (𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ∧ 𝑆 ≤ 1))
11	10	simp1bi 1142	. . . . . . . . 9 ⊢ (𝑆 ∈ (0[,]1) → 𝑆 ∈ ℝ)
12	11	ad2antll 728	. . . . . . . 8 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℝ)
13		resubcl 10939	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (1 − 𝑆) ∈ ℝ)
14	1, 12, 13	sylancr 590	. . . . . . 7 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℝ)
15	14	recnd 10658	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℂ)
16	15	mulid2d 10648	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · (1 − 𝑆)) = (1 − 𝑆))
17		oveq2 7143	. . . . . . 7 ⊢ (𝑆 = 0 → (1 − 𝑆) = (1 − 0))
18	17	adantr 484	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) = (1 − 0))
19		1m0e1 11746	. . . . . 6 ⊢ (1 − 0) = 1
20	18, 19	eqtrdi 2849	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) = 1)
21	16, 20	eqtr2d 2834	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 1 = (1 · (1 − 𝑆)))
22	4	recnd 10658	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
23	22	mul02d 10827	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · 𝑇) = 0)
24		oveq2 7143	. . . . . . 7 ⊢ (𝑆 = 0 → (1 · 𝑆) = (1 · 0))
25	24	adantr 484	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑆) = (1 · 0))
26		ax-1cn 10584	. . . . . . 7 ⊢ 1 ∈ ℂ
27	26	mul01i 10819	. . . . . 6 ⊢ (1 · 0) = 0
28	25, 27	eqtrdi 2849	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑆) = 0)
29	23, 28	eqtr4d 2836	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · 𝑇) = (1 · 𝑆))
30		1elunit 12848	. . . . 5 ⊢ 1 ∈ (0[,]1)
31		0elunit 12847	. . . . 5 ⊢ 0 ∈ (0[,]1)
32		oveq2 7143	. . . . . . . . . 10 ⊢ (𝑟 = 1 → (1 − 𝑟) = (1 − 1))
33		1m1e0 11697	. . . . . . . . . 10 ⊢ (1 − 1) = 0
34	32, 33	eqtrdi 2849	. . . . . . . . 9 ⊢ (𝑟 = 1 → (1 − 𝑟) = 0)
35	34	oveq1d 7150	. . . . . . . 8 ⊢ (𝑟 = 1 → ((1 − 𝑟) · (1 − 𝑇)) = (0 · (1 − 𝑇)))
36	35	eqeq2d 2809	. . . . . . 7 ⊢ (𝑟 = 1 → (𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ↔ 𝑝 = (0 · (1 − 𝑇))))
37		eqeq1 2802	. . . . . . 7 ⊢ (𝑟 = 1 → (𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ↔ 1 = ((1 − 𝑝) · (1 − 𝑆))))
38	34	oveq1d 7150	. . . . . . . 8 ⊢ (𝑟 = 1 → ((1 − 𝑟) · 𝑇) = (0 · 𝑇))
39	38	eqeq1d 2800	. . . . . . 7 ⊢ (𝑟 = 1 → (((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ (0 · 𝑇) = ((1 − 𝑝) · 𝑆)))
40	36, 37, 39	3anbi123d 1433	. . . . . 6 ⊢ (𝑟 = 1 → ((𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (𝑝 = (0 · (1 − 𝑇)) ∧ 1 = ((1 − 𝑝) · (1 − 𝑆)) ∧ (0 · 𝑇) = ((1 − 𝑝) · 𝑆))))
41		eqeq1 2802	. . . . . . 7 ⊢ (𝑝 = 0 → (𝑝 = (0 · (1 − 𝑇)) ↔ 0 = (0 · (1 − 𝑇))))
42		oveq2 7143	. . . . . . . . . 10 ⊢ (𝑝 = 0 → (1 − 𝑝) = (1 − 0))
43	42, 19	eqtrdi 2849	. . . . . . . . 9 ⊢ (𝑝 = 0 → (1 − 𝑝) = 1)
44	43	oveq1d 7150	. . . . . . . 8 ⊢ (𝑝 = 0 → ((1 − 𝑝) · (1 − 𝑆)) = (1 · (1 − 𝑆)))
45	44	eqeq2d 2809	. . . . . . 7 ⊢ (𝑝 = 0 → (1 = ((1 − 𝑝) · (1 − 𝑆)) ↔ 1 = (1 · (1 − 𝑆))))
46	43	oveq1d 7150	. . . . . . . 8 ⊢ (𝑝 = 0 → ((1 − 𝑝) · 𝑆) = (1 · 𝑆))
47	46	eqeq2d 2809	. . . . . . 7 ⊢ (𝑝 = 0 → ((0 · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ (0 · 𝑇) = (1 · 𝑆)))
48	41, 45, 47	3anbi123d 1433	. . . . . 6 ⊢ (𝑝 = 0 → ((𝑝 = (0 · (1 − 𝑇)) ∧ 1 = ((1 − 𝑝) · (1 − 𝑆)) ∧ (0 · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (0 = (0 · (1 − 𝑇)) ∧ 1 = (1 · (1 − 𝑆)) ∧ (0 · 𝑇) = (1 · 𝑆))))
49	40, 48	rspc2ev 3583	. . . . 5 ⊢ ((1 ∈ (0[,]1) ∧ 0 ∈ (0[,]1) ∧ (0 = (0 · (1 − 𝑇)) ∧ 1 = (1 · (1 − 𝑆)) ∧ (0 · 𝑇) = (1 · 𝑆))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
50	30, 31, 49	mp3an12 1448	. . . 4 ⊢ ((0 = (0 · (1 − 𝑇)) ∧ 1 = (1 · (1 − 𝑆)) ∧ (0 · 𝑇) = (1 · 𝑆)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
51	9, 21, 29, 50	syl3anc 1368	. . 3 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
52	51	ex 416	. 2 ⊢ (𝑆 = 0 → ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆))))
53	3	ad2antrl 727	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
54	11	ad2antll 728	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℝ)
55	54, 53	remulcld 10660	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ∈ ℝ)
56	53, 55	resubcld 11057	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ∈ ℝ)
57	54, 53	readdcld 10659	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 + 𝑇) ∈ ℝ)
58	57, 55	resubcld 11057	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ)
59		1red 10631	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 1 ∈ ℝ)
60	2	simp2bi 1143	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0[,]1) → 0 ≤ 𝑇)
61	60	ad2antrl 727	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ 𝑇)
62	10	simp3bi 1144	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (0[,]1) → 𝑆 ≤ 1)
63	62	ad2antll 728	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≤ 1)
64	54, 59, 53, 61, 63	lemul1ad 11568	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ (1 · 𝑇))
65	53	recnd 10658	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
66	65	mulid2d 10648	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑇) = 𝑇)
67	64, 66	breqtrd 5056	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ 𝑇)
68	10	simp2bi 1143	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (0[,]1) → 0 ≤ 𝑆)
69	68	ad2antll 728	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ 𝑆)
70		simpl 486	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≠ 0)
71	54, 69, 70	ne0gt0d 10766	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 < 𝑆)
72	54, 53	ltaddpos2d 11214	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 < 𝑆 ↔ 𝑇 < (𝑆 + 𝑇)))
73	71, 72	mpbid 235	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 < (𝑆 + 𝑇))
74	55, 53, 57, 67, 73	lelttrd 10787	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) < (𝑆 + 𝑇))
75	55, 57	posdifd 11216	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) < (𝑆 + 𝑇) ↔ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
76	74, 75	mpbid 235	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
77	76	gt0ne0d 11193	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ≠ 0)
78	56, 58, 77	redivcld 11457	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ)
79	53, 55	subge0d 11219	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ (𝑇 − (𝑆 · 𝑇)) ↔ (𝑆 · 𝑇) ≤ 𝑇))
80	67, 79	mpbird 260	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ (𝑇 − (𝑆 · 𝑇)))
81		divge0 11498	. . . . . 6 ⊢ ((((𝑇 − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 ≤ (𝑇 − (𝑆 · 𝑇))) ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
82	56, 80, 58, 76, 81	syl22anc 837	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
83	53, 57, 73	ltled 10777	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ≤ (𝑆 + 𝑇))
84	53, 57, 55, 83	lesub1dd 11245	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ≤ ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
85	58	recnd 10658	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℂ)
86	85	mulid2d 10648	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
87	84, 86	breqtrrd 5058	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
88		ledivmul2 11508	. . . . . . 7 ⊢ (((𝑇 − (𝑆 · 𝑇)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
89	56, 59, 58, 76, 88	syl112anc 1371	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
90	87, 89	mpbird 260	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1)
91		elicc01 12844	. . . . 5 ⊢ (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ↔ (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ ∧ 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1))
92	78, 82, 90, 91	syl3anbrc 1340	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1))
93	54, 55	resubcld 11057	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ∈ ℝ)
94	93, 58, 77	redivcld 11457	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ)
95	2	simp3bi 1144	. . . . . . . . . 10 ⊢ (𝑇 ∈ (0[,]1) → 𝑇 ≤ 1)
96	95	ad2antrl 727	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ≤ 1)
97	53, 59, 54, 69, 96	lemul2ad 11569	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ (𝑆 · 1))
98	54	recnd 10658	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℂ)
99	98	mulid1d 10647	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 1) = 𝑆)
100	97, 99	breqtrd 5056	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ 𝑆)
101	54, 55	subge0d 11219	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ (𝑆 − (𝑆 · 𝑇)) ↔ (𝑆 · 𝑇) ≤ 𝑆))
102	100, 101	mpbird 260	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ (𝑆 − (𝑆 · 𝑇)))
103		divge0 11498	. . . . . 6 ⊢ ((((𝑆 − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 ≤ (𝑆 − (𝑆 · 𝑇))) ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
104	93, 102, 58, 76, 103	syl22anc 837	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
105	54, 53	addge01d 11217	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ 𝑇 ↔ 𝑆 ≤ (𝑆 + 𝑇)))
106	61, 105	mpbid 235	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≤ (𝑆 + 𝑇))
107	54, 57, 55, 106	lesub1dd 11245	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ≤ ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
108	107, 86	breqtrrd 5058	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
109		ledivmul2 11508	. . . . . . 7 ⊢ (((𝑆 − (𝑆 · 𝑇)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
110	93, 59, 58, 76, 109	syl112anc 1371	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
111	108, 110	mpbird 260	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1)
112		elicc01 12844	. . . . 5 ⊢ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ↔ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ ∧ 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∧ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1))
113	94, 104, 111, 112	syl3anbrc 1340	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1))
114	1, 53, 5	sylancr 590	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
115	114	recnd 10658	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
116	98, 115, 85, 77	div23d 11442	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · (1 − 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑇)))
117		subdi 11062	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
118	26, 117	mp3an2 1446	. . . . . . . 8 ⊢ ((𝑆 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
119	98, 65, 118	syl2anc 587	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
120	99	oveq1d 7150	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 1) − (𝑆 · 𝑇)) = (𝑆 − (𝑆 · 𝑇)))
121	119, 120	eqtrd 2833	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · (1 − 𝑇)) = (𝑆 − (𝑆 · 𝑇)))
122	121	oveq1d 7150	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · (1 − 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
123	56	recnd 10658	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ∈ ℂ)
124	85, 123, 85, 77	divsubdird 11444	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
125	57	recnd 10658	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 + 𝑇) ∈ ℂ)
126	55	recnd 10658	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ∈ ℂ)
127	125, 65, 126	nnncan2d 11021	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − 𝑇))
128	98, 65	pncand 10987	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − 𝑇) = 𝑆)
129	127, 128	eqtrd 2833	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) = 𝑆)
130	129	oveq1d 7150	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
131	85, 77	dividd 11403	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = 1)
132	131	oveq1d 7150	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
133	124, 130, 132	3eqtr3d 2841	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
134	133	oveq1d 7150	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑇)) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
135	116, 122, 134	3eqtr3d 2841	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
136	1, 54, 13	sylancr 590	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℝ)
137	136	recnd 10658	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℂ)
138	65, 137, 85, 77	div23d 11442	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · (1 − 𝑆)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑆)))
139		subdi 11062	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
140	26, 139	mp3an2 1446	. . . . . . . 8 ⊢ ((𝑇 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
141	65, 98, 140	syl2anc 587	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
142	65	mulid1d 10647	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · 1) = 𝑇)
143	65, 98	mulcomd 10651	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · 𝑆) = (𝑆 · 𝑇))
144	142, 143	oveq12d 7153	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 1) − (𝑇 · 𝑆)) = (𝑇 − (𝑆 · 𝑇)))
145	141, 144	eqtrd 2833	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · (1 − 𝑆)) = (𝑇 − (𝑆 · 𝑇)))
146	145	oveq1d 7150	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · (1 − 𝑆)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
147	93	recnd 10658	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ∈ ℂ)
148	85, 147, 85, 77	divsubdird 11444	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
149	125, 98, 126	nnncan2d 11021	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − 𝑆))
150	98, 65	pncan2d 10988	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − 𝑆) = 𝑇)
151	149, 150	eqtrd 2833	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) = 𝑇)
152	151	oveq1d 7150	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
153	131	oveq1d 7150	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
154	148, 152, 153	3eqtr3d 2841	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
155	154	oveq1d 7150	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑆)) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
156	138, 146, 155	3eqtr3d 2841	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
157	98, 65	mulcomd 10651	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) = (𝑇 · 𝑆))
158	157	oveq1d 7150	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
159	98, 65, 85, 77	div23d 11442	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑇))
160	133	oveq1d 7150	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑇) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
161	159, 160	eqtrd 2833	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
162	65, 98, 85, 77	div23d 11442	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑆))
163	154	oveq1d 7150	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑆) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
164	162, 163	eqtrd 2833	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
165	158, 161, 164	3eqtr3d 2841	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
166		oveq2 7143	. . . . . . . 8 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (1 − 𝑟) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
167	166	oveq1d 7150	. . . . . . 7 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑟) · (1 − 𝑇)) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
168	167	eqeq2d 2809	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ↔ 𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇))))
169		eqeq1 2802	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ↔ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆))))
170	166	oveq1d 7150	. . . . . . 7 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑟) · 𝑇) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
171	170	eqeq1d 2800	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆)))
172	168, 169, 171	3anbi123d 1433	. . . . 5 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆))))
173		eqeq1 2802	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ↔ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇))))
174		oveq2 7143	. . . . . . . 8 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (1 − 𝑝) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
175	174	oveq1d 7150	. . . . . . 7 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑝) · (1 − 𝑆)) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
176	175	eqeq2d 2809	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ↔ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆))))
177	174	oveq1d 7150	. . . . . . 7 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑝) · 𝑆) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
178	177	eqeq2d 2809	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆)))
179	173, 176, 178	3anbi123d 1433	. . . . 5 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))))
180	172, 179	rspc2ev 3583	. . . 4 ⊢ ((((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ∧ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ∧ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
181	92, 113, 135, 156, 165, 180	syl113anc 1379	. . 3 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
182	181	ex 416	. 2 ⊢ (𝑆 ≠ 0 → ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆))))
183	52, 182	pm2.61ine 3070	1 ⊢ ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∃wrex 3107   class class class wbr 5030  (class class class)co 7135  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531   < clt 10664   ≤ cle 10665   − cmin 10859   / cdiv 11286  [,]cicc 12729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-icc 12733

This theorem is referenced by:  axpasch  26735