Theorem axpaschlem 28924

Description: Lemma for axpasch 28925. Set up coefficients 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 11240	. . . . . . . 8 ⊢ 1 ∈ ℝ
2		elicc01 13488	. . . . . . . . . 10 ⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
3	2	simp1bi 1145	. . . . . . . . 9 ⊢ (𝑇 ∈ (0[,]1) → 𝑇 ∈ ℝ)
4	3	ad2antrl 728	. . . . . . . 8 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5		resubcl 11552	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
6	1, 4, 5	sylancr 587	. . . . . . 7 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
7	6	recnd 11268	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
8	7	mul02d 11438	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · (1 − 𝑇)) = 0)
9	8	eqcomd 2742	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 = (0 · (1 − 𝑇)))
10		elicc01 13488	. . . . . . . . . 10 ⊢ (𝑆 ∈ (0[,]1) ↔ (𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ∧ 𝑆 ≤ 1))
11	10	simp1bi 1145	. . . . . . . . 9 ⊢ (𝑆 ∈ (0[,]1) → 𝑆 ∈ ℝ)
12	11	ad2antll 729	. . . . . . . 8 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℝ)
13		resubcl 11552	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (1 − 𝑆) ∈ ℝ)
14	1, 12, 13	sylancr 587	. . . . . . 7 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℝ)
15	14	recnd 11268	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℂ)
16	15	mullidd 11258	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · (1 − 𝑆)) = (1 − 𝑆))
17		oveq2 7418	. . . . . . 7 ⊢ (𝑆 = 0 → (1 − 𝑆) = (1 − 0))
18	17	adantr 480	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) = (1 − 0))
19		1m0e1 12366	. . . . . 6 ⊢ (1 − 0) = 1
20	18, 19	eqtrdi 2787	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) = 1)
21	16, 20	eqtr2d 2772	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 1 = (1 · (1 − 𝑆)))
22	4	recnd 11268	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
23	22	mul02d 11438	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · 𝑇) = 0)
24		oveq2 7418	. . . . . . 7 ⊢ (𝑆 = 0 → (1 · 𝑆) = (1 · 0))
25	24	adantr 480	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑆) = (1 · 0))
26		ax-1cn 11192	. . . . . . 7 ⊢ 1 ∈ ℂ
27	26	mul01i 11430	. . . . . 6 ⊢ (1 · 0) = 0
28	25, 27	eqtrdi 2787	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑆) = 0)
29	23, 28	eqtr4d 2774	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · 𝑇) = (1 · 𝑆))
30		1elunit 13492	. . . . 5 ⊢ 1 ∈ (0[,]1)
31		0elunit 13491	. . . . 5 ⊢ 0 ∈ (0[,]1)
32		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑟 = 1 → (1 − 𝑟) = (1 − 1))
33		1m1e0 12317	. . . . . . . . . 10 ⊢ (1 − 1) = 0
34	32, 33	eqtrdi 2787	. . . . . . . . 9 ⊢ (𝑟 = 1 → (1 − 𝑟) = 0)
35	34	oveq1d 7425	. . . . . . . 8 ⊢ (𝑟 = 1 → ((1 − 𝑟) · (1 − 𝑇)) = (0 · (1 − 𝑇)))
36	35	eqeq2d 2747	. . . . . . 7 ⊢ (𝑟 = 1 → (𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ↔ 𝑝 = (0 · (1 − 𝑇))))
37		eqeq1 2740	. . . . . . 7 ⊢ (𝑟 = 1 → (𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ↔ 1 = ((1 − 𝑝) · (1 − 𝑆))))
38	34	oveq1d 7425	. . . . . . . 8 ⊢ (𝑟 = 1 → ((1 − 𝑟) · 𝑇) = (0 · 𝑇))
39	38	eqeq1d 2738	. . . . . . 7 ⊢ (𝑟 = 1 → (((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ (0 · 𝑇) = ((1 − 𝑝) · 𝑆)))
40	36, 37, 39	3anbi123d 1438	. . . . . 6 ⊢ (𝑟 = 1 → ((𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (𝑝 = (0 · (1 − 𝑇)) ∧ 1 = ((1 − 𝑝) · (1 − 𝑆)) ∧ (0 · 𝑇) = ((1 − 𝑝) · 𝑆))))
41		eqeq1 2740	. . . . . . 7 ⊢ (𝑝 = 0 → (𝑝 = (0 · (1 − 𝑇)) ↔ 0 = (0 · (1 − 𝑇))))
42		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑝 = 0 → (1 − 𝑝) = (1 − 0))
43	42, 19	eqtrdi 2787	. . . . . . . . 9 ⊢ (𝑝 = 0 → (1 − 𝑝) = 1)
44	43	oveq1d 7425	. . . . . . . 8 ⊢ (𝑝 = 0 → ((1 − 𝑝) · (1 − 𝑆)) = (1 · (1 − 𝑆)))
45	44	eqeq2d 2747	. . . . . . 7 ⊢ (𝑝 = 0 → (1 = ((1 − 𝑝) · (1 − 𝑆)) ↔ 1 = (1 · (1 − 𝑆))))
46	43	oveq1d 7425	. . . . . . . 8 ⊢ (𝑝 = 0 → ((1 − 𝑝) · 𝑆) = (1 · 𝑆))
47	46	eqeq2d 2747	. . . . . . 7 ⊢ (𝑝 = 0 → ((0 · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ (0 · 𝑇) = (1 · 𝑆)))
48	41, 45, 47	3anbi123d 1438	. . . . . 6 ⊢ (𝑝 = 0 → ((𝑝 = (0 · (1 − 𝑇)) ∧ 1 = ((1 − 𝑝) · (1 − 𝑆)) ∧ (0 · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (0 = (0 · (1 − 𝑇)) ∧ 1 = (1 · (1 − 𝑆)) ∧ (0 · 𝑇) = (1 · 𝑆))))
49	40, 48	rspc2ev 3619	. . . . 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 1453	. . . 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 1373	. . 3 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
52	51	ex 412	. 2 ⊢ (𝑆 = 0 → ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆))))
53	3	ad2antrl 728	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
54	11	ad2antll 729	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℝ)
55	54, 53	remulcld 11270	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ∈ ℝ)
56	53, 55	resubcld 11670	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ∈ ℝ)
57	54, 53	readdcld 11269	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 + 𝑇) ∈ ℝ)
58	57, 55	resubcld 11670	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ)
59		1red 11241	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 1 ∈ ℝ)
60	2	simp2bi 1146	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0[,]1) → 0 ≤ 𝑇)
61	60	ad2antrl 728	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ 𝑇)
62	10	simp3bi 1147	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (0[,]1) → 𝑆 ≤ 1)
63	62	ad2antll 729	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≤ 1)
64	54, 59, 53, 61, 63	lemul1ad 12186	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ (1 · 𝑇))
65	53	recnd 11268	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
66	65	mullidd 11258	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑇) = 𝑇)
67	64, 66	breqtrd 5150	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ 𝑇)
68	10	simp2bi 1146	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (0[,]1) → 0 ≤ 𝑆)
69	68	ad2antll 729	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ 𝑆)
70		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≠ 0)
71	54, 69, 70	ne0gt0d 11377	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 < 𝑆)
72	54, 53	ltaddpos2d 11827	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 < 𝑆 ↔ 𝑇 < (𝑆 + 𝑇)))
73	71, 72	mpbid 232	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 < (𝑆 + 𝑇))
74	55, 53, 57, 67, 73	lelttrd 11398	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) < (𝑆 + 𝑇))
75	55, 57	posdifd 11829	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) < (𝑆 + 𝑇) ↔ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
76	74, 75	mpbid 232	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
77	76	gt0ne0d 11806	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ≠ 0)
78	56, 58, 77	redivcld 12074	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ)
79	53, 55	subge0d 11832	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ (𝑇 − (𝑆 · 𝑇)) ↔ (𝑆 · 𝑇) ≤ 𝑇))
80	67, 79	mpbird 257	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ (𝑇 − (𝑆 · 𝑇)))
81		divge0 12116	. . . . . 6 ⊢ ((((𝑇 − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 ≤ (𝑇 − (𝑆 · 𝑇))) ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
82	56, 80, 58, 76, 81	syl22anc 838	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
83	53, 57, 73	ltled 11388	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ≤ (𝑆 + 𝑇))
84	53, 57, 55, 83	lesub1dd 11858	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ≤ ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
85	58	recnd 11268	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℂ)
86	85	mullidd 11258	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
87	84, 86	breqtrrd 5152	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
88		ledivmul2 12126	. . . . . . 7 ⊢ (((𝑇 − (𝑆 · 𝑇)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
89	56, 59, 58, 76, 88	syl112anc 1376	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
90	87, 89	mpbird 257	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1)
91		elicc01 13488	. . . . 5 ⊢ (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ↔ (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ ∧ 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1))
92	78, 82, 90, 91	syl3anbrc 1344	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1))
93	54, 55	resubcld 11670	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ∈ ℝ)
94	93, 58, 77	redivcld 12074	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ)
95	2	simp3bi 1147	. . . . . . . . . 10 ⊢ (𝑇 ∈ (0[,]1) → 𝑇 ≤ 1)
96	95	ad2antrl 728	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ≤ 1)
97	53, 59, 54, 69, 96	lemul2ad 12187	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ (𝑆 · 1))
98	54	recnd 11268	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℂ)
99	98	mulridd 11257	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 1) = 𝑆)
100	97, 99	breqtrd 5150	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ 𝑆)
101	54, 55	subge0d 11832	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ (𝑆 − (𝑆 · 𝑇)) ↔ (𝑆 · 𝑇) ≤ 𝑆))
102	100, 101	mpbird 257	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ (𝑆 − (𝑆 · 𝑇)))
103		divge0 12116	. . . . . 6 ⊢ ((((𝑆 − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 ≤ (𝑆 − (𝑆 · 𝑇))) ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
104	93, 102, 58, 76, 103	syl22anc 838	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
105	54, 53	addge01d 11830	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ 𝑇 ↔ 𝑆 ≤ (𝑆 + 𝑇)))
106	61, 105	mpbid 232	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≤ (𝑆 + 𝑇))
107	54, 57, 55, 106	lesub1dd 11858	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ≤ ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
108	107, 86	breqtrrd 5152	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
109		ledivmul2 12126	. . . . . . 7 ⊢ (((𝑆 − (𝑆 · 𝑇)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
110	93, 59, 58, 76, 109	syl112anc 1376	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
111	108, 110	mpbird 257	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1)
112		elicc01 13488	. . . . 5 ⊢ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ↔ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ ∧ 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∧ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1))
113	94, 104, 111, 112	syl3anbrc 1344	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1))
114	1, 53, 5	sylancr 587	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
115	114	recnd 11268	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
116	98, 115, 85, 77	div23d 12059	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · (1 − 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑇)))
117		subdi 11675	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
118	26, 117	mp3an2 1451	. . . . . . . 8 ⊢ ((𝑆 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
119	98, 65, 118	syl2anc 584	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
120	99	oveq1d 7425	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 1) − (𝑆 · 𝑇)) = (𝑆 − (𝑆 · 𝑇)))
121	119, 120	eqtrd 2771	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · (1 − 𝑇)) = (𝑆 − (𝑆 · 𝑇)))
122	121	oveq1d 7425	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · (1 − 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
123	56	recnd 11268	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ∈ ℂ)
124	85, 123, 85, 77	divsubdird 12061	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
125	57	recnd 11268	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 + 𝑇) ∈ ℂ)
126	55	recnd 11268	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ∈ ℂ)
127	125, 65, 126	nnncan2d 11634	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − 𝑇))
128	98, 65	pncand 11600	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − 𝑇) = 𝑆)
129	127, 128	eqtrd 2771	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) = 𝑆)
130	129	oveq1d 7425	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
131	85, 77	dividd 12020	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = 1)
132	131	oveq1d 7425	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
133	124, 130, 132	3eqtr3d 2779	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
134	133	oveq1d 7425	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑇)) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
135	116, 122, 134	3eqtr3d 2779	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
136	1, 54, 13	sylancr 587	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℝ)
137	136	recnd 11268	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℂ)
138	65, 137, 85, 77	div23d 12059	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · (1 − 𝑆)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑆)))
139		subdi 11675	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
140	26, 139	mp3an2 1451	. . . . . . . 8 ⊢ ((𝑇 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
141	65, 98, 140	syl2anc 584	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
142	65	mulridd 11257	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · 1) = 𝑇)
143	65, 98	mulcomd 11261	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · 𝑆) = (𝑆 · 𝑇))
144	142, 143	oveq12d 7428	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 1) − (𝑇 · 𝑆)) = (𝑇 − (𝑆 · 𝑇)))
145	141, 144	eqtrd 2771	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · (1 − 𝑆)) = (𝑇 − (𝑆 · 𝑇)))
146	145	oveq1d 7425	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · (1 − 𝑆)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
147	93	recnd 11268	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ∈ ℂ)
148	85, 147, 85, 77	divsubdird 12061	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
149	125, 98, 126	nnncan2d 11634	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − 𝑆))
150	98, 65	pncan2d 11601	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − 𝑆) = 𝑇)
151	149, 150	eqtrd 2771	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) = 𝑇)
152	151	oveq1d 7425	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
153	131	oveq1d 7425	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
154	148, 152, 153	3eqtr3d 2779	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
155	154	oveq1d 7425	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑆)) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
156	138, 146, 155	3eqtr3d 2779	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
157	98, 65	mulcomd 11261	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) = (𝑇 · 𝑆))
158	157	oveq1d 7425	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
159	98, 65, 85, 77	div23d 12059	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑇))
160	133	oveq1d 7425	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑇) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
161	159, 160	eqtrd 2771	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
162	65, 98, 85, 77	div23d 12059	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑆))
163	154	oveq1d 7425	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑆) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
164	162, 163	eqtrd 2771	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
165	158, 161, 164	3eqtr3d 2779	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
166		oveq2 7418	. . . . . . . 8 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (1 − 𝑟) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
167	166	oveq1d 7425	. . . . . . 7 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑟) · (1 − 𝑇)) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
168	167	eqeq2d 2747	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ↔ 𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇))))
169		eqeq1 2740	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ↔ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆))))
170	166	oveq1d 7425	. . . . . . 7 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑟) · 𝑇) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
171	170	eqeq1d 2738	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆)))
172	168, 169, 171	3anbi123d 1438	. . . . 5 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆))))
173		eqeq1 2740	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ↔ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇))))
174		oveq2 7418	. . . . . . . 8 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (1 − 𝑝) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
175	174	oveq1d 7425	. . . . . . 7 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑝) · (1 − 𝑆)) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
176	175	eqeq2d 2747	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ↔ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆))))
177	174	oveq1d 7425	. . . . . . 7 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑝) · 𝑆) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
178	177	eqeq2d 2747	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆)))
179	173, 176, 178	3anbi123d 1438	. . . . 5 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))))
180	172, 179	rspc2ev 3619	. . . 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 1384	. . 3 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
182	181	ex 412	. 2 ⊢ (𝑆 ≠ 0 → ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆))))
183	52, 182	pm2.61ine 3016	1 ⊢ ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  ∃wrex 3061   class class class wbr 5124  (class class class)co 7410  ℂcc 11132  ℝcr 11133  0cc0 11134  1c1 11135   + caddc 11137   · cmul 11139   < clt 11274   ≤ cle 11275   − cmin 11471   / cdiv 11899  [,]cicc 13370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-div 11900  df-icc 13374

This theorem is referenced by:  axpasch  28925