Theorem axpaschlem 26728

Description: Lemma for axpasch 26729. 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 10643	. . . . . . . 8 ⊢ 1 ∈ ℝ
2		elicc01 12857	. . . . . . . . . 10 ⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
3	2	simp1bi 1141	. . . . . . . . 9 ⊢ (𝑇 ∈ (0[,]1) → 𝑇 ∈ ℝ)
4	3	ad2antrl 726	. . . . . . . 8 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5		resubcl 10952	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
6	1, 4, 5	sylancr 589	. . . . . . 7 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
7	6	recnd 10671	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
8	7	mul02d 10840	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · (1 − 𝑇)) = 0)
9	8	eqcomd 2829	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 = (0 · (1 − 𝑇)))
10		elicc01 12857	. . . . . . . . . 10 ⊢ (𝑆 ∈ (0[,]1) ↔ (𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ∧ 𝑆 ≤ 1))
11	10	simp1bi 1141	. . . . . . . . 9 ⊢ (𝑆 ∈ (0[,]1) → 𝑆 ∈ ℝ)
12	11	ad2antll 727	. . . . . . . 8 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℝ)
13		resubcl 10952	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (1 − 𝑆) ∈ ℝ)
14	1, 12, 13	sylancr 589	. . . . . . 7 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℝ)
15	14	recnd 10671	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℂ)
16	15	mulid2d 10661	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · (1 − 𝑆)) = (1 − 𝑆))
17		oveq2 7166	. . . . . . 7 ⊢ (𝑆 = 0 → (1 − 𝑆) = (1 − 0))
18	17	adantr 483	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) = (1 − 0))
19		1m0e1 11761	. . . . . 6 ⊢ (1 − 0) = 1
20	18, 19	syl6eq 2874	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) = 1)
21	16, 20	eqtr2d 2859	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 1 = (1 · (1 − 𝑆)))
22	4	recnd 10671	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
23	22	mul02d 10840	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · 𝑇) = 0)
24		oveq2 7166	. . . . . . 7 ⊢ (𝑆 = 0 → (1 · 𝑆) = (1 · 0))
25	24	adantr 483	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑆) = (1 · 0))
26		ax-1cn 10597	. . . . . . 7 ⊢ 1 ∈ ℂ
27	26	mul01i 10832	. . . . . 6 ⊢ (1 · 0) = 0
28	25, 27	syl6eq 2874	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑆) = 0)
29	23, 28	eqtr4d 2861	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · 𝑇) = (1 · 𝑆))
30		1elunit 12859	. . . . 5 ⊢ 1 ∈ (0[,]1)
31		0elunit 12858	. . . . 5 ⊢ 0 ∈ (0[,]1)
32		oveq2 7166	. . . . . . . . . 10 ⊢ (𝑟 = 1 → (1 − 𝑟) = (1 − 1))
33		1m1e0 11712	. . . . . . . . . 10 ⊢ (1 − 1) = 0
34	32, 33	syl6eq 2874	. . . . . . . . 9 ⊢ (𝑟 = 1 → (1 − 𝑟) = 0)
35	34	oveq1d 7173	. . . . . . . 8 ⊢ (𝑟 = 1 → ((1 − 𝑟) · (1 − 𝑇)) = (0 · (1 − 𝑇)))
36	35	eqeq2d 2834	. . . . . . 7 ⊢ (𝑟 = 1 → (𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ↔ 𝑝 = (0 · (1 − 𝑇))))
37		eqeq1 2827	. . . . . . 7 ⊢ (𝑟 = 1 → (𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ↔ 1 = ((1 − 𝑝) · (1 − 𝑆))))
38	34	oveq1d 7173	. . . . . . . 8 ⊢ (𝑟 = 1 → ((1 − 𝑟) · 𝑇) = (0 · 𝑇))
39	38	eqeq1d 2825	. . . . . . 7 ⊢ (𝑟 = 1 → (((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ (0 · 𝑇) = ((1 − 𝑝) · 𝑆)))
40	36, 37, 39	3anbi123d 1432	. . . . . 6 ⊢ (𝑟 = 1 → ((𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (𝑝 = (0 · (1 − 𝑇)) ∧ 1 = ((1 − 𝑝) · (1 − 𝑆)) ∧ (0 · 𝑇) = ((1 − 𝑝) · 𝑆))))
41		eqeq1 2827	. . . . . . 7 ⊢ (𝑝 = 0 → (𝑝 = (0 · (1 − 𝑇)) ↔ 0 = (0 · (1 − 𝑇))))
42		oveq2 7166	. . . . . . . . . 10 ⊢ (𝑝 = 0 → (1 − 𝑝) = (1 − 0))
43	42, 19	syl6eq 2874	. . . . . . . . 9 ⊢ (𝑝 = 0 → (1 − 𝑝) = 1)
44	43	oveq1d 7173	. . . . . . . 8 ⊢ (𝑝 = 0 → ((1 − 𝑝) · (1 − 𝑆)) = (1 · (1 − 𝑆)))
45	44	eqeq2d 2834	. . . . . . 7 ⊢ (𝑝 = 0 → (1 = ((1 − 𝑝) · (1 − 𝑆)) ↔ 1 = (1 · (1 − 𝑆))))
46	43	oveq1d 7173	. . . . . . . 8 ⊢ (𝑝 = 0 → ((1 − 𝑝) · 𝑆) = (1 · 𝑆))
47	46	eqeq2d 2834	. . . . . . 7 ⊢ (𝑝 = 0 → ((0 · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ (0 · 𝑇) = (1 · 𝑆)))
48	41, 45, 47	3anbi123d 1432	. . . . . 6 ⊢ (𝑝 = 0 → ((𝑝 = (0 · (1 − 𝑇)) ∧ 1 = ((1 − 𝑝) · (1 − 𝑆)) ∧ (0 · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (0 = (0 · (1 − 𝑇)) ∧ 1 = (1 · (1 − 𝑆)) ∧ (0 · 𝑇) = (1 · 𝑆))))
49	40, 48	rspc2ev 3637	. . . . 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 1447	. . . 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 1367	. . 3 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
52	51	ex 415	. 2 ⊢ (𝑆 = 0 → ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆))))
53	3	ad2antrl 726	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
54	11	ad2antll 727	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℝ)
55	54, 53	remulcld 10673	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ∈ ℝ)
56	53, 55	resubcld 11070	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ∈ ℝ)
57	54, 53	readdcld 10672	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 + 𝑇) ∈ ℝ)
58	57, 55	resubcld 11070	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ)
59		1red 10644	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 1 ∈ ℝ)
60	2	simp2bi 1142	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0[,]1) → 0 ≤ 𝑇)
61	60	ad2antrl 726	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ 𝑇)
62	10	simp3bi 1143	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (0[,]1) → 𝑆 ≤ 1)
63	62	ad2antll 727	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≤ 1)
64	54, 59, 53, 61, 63	lemul1ad 11581	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ (1 · 𝑇))
65	53	recnd 10671	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
66	65	mulid2d 10661	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑇) = 𝑇)
67	64, 66	breqtrd 5094	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ 𝑇)
68	10	simp2bi 1142	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (0[,]1) → 0 ≤ 𝑆)
69	68	ad2antll 727	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ 𝑆)
70		simpl 485	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≠ 0)
71	54, 69, 70	ne0gt0d 10779	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 < 𝑆)
72	54, 53	ltaddpos2d 11227	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 < 𝑆 ↔ 𝑇 < (𝑆 + 𝑇)))
73	71, 72	mpbid 234	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 < (𝑆 + 𝑇))
74	55, 53, 57, 67, 73	lelttrd 10800	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) < (𝑆 + 𝑇))
75	55, 57	posdifd 11229	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) < (𝑆 + 𝑇) ↔ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
76	74, 75	mpbid 234	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
77	76	gt0ne0d 11206	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ≠ 0)
78	56, 58, 77	redivcld 11470	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ)
79	53, 55	subge0d 11232	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ (𝑇 − (𝑆 · 𝑇)) ↔ (𝑆 · 𝑇) ≤ 𝑇))
80	67, 79	mpbird 259	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ (𝑇 − (𝑆 · 𝑇)))
81		divge0 11511	. . . . . 6 ⊢ ((((𝑇 − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 ≤ (𝑇 − (𝑆 · 𝑇))) ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
82	56, 80, 58, 76, 81	syl22anc 836	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
83	53, 57, 73	ltled 10790	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ≤ (𝑆 + 𝑇))
84	53, 57, 55, 83	lesub1dd 11258	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ≤ ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
85	58	recnd 10671	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℂ)
86	85	mulid2d 10661	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
87	84, 86	breqtrrd 5096	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
88		ledivmul2 11521	. . . . . . 7 ⊢ (((𝑇 − (𝑆 · 𝑇)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
89	56, 59, 58, 76, 88	syl112anc 1370	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
90	87, 89	mpbird 259	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1)
91		elicc01 12857	. . . . 5 ⊢ (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ↔ (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ ∧ 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1))
92	78, 82, 90, 91	syl3anbrc 1339	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1))
93	54, 55	resubcld 11070	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ∈ ℝ)
94	93, 58, 77	redivcld 11470	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ)
95	2	simp3bi 1143	. . . . . . . . . 10 ⊢ (𝑇 ∈ (0[,]1) → 𝑇 ≤ 1)
96	95	ad2antrl 726	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ≤ 1)
97	53, 59, 54, 69, 96	lemul2ad 11582	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ (𝑆 · 1))
98	54	recnd 10671	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℂ)
99	98	mulid1d 10660	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 1) = 𝑆)
100	97, 99	breqtrd 5094	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ 𝑆)
101	54, 55	subge0d 11232	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ (𝑆 − (𝑆 · 𝑇)) ↔ (𝑆 · 𝑇) ≤ 𝑆))
102	100, 101	mpbird 259	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ (𝑆 − (𝑆 · 𝑇)))
103		divge0 11511	. . . . . 6 ⊢ ((((𝑆 − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 ≤ (𝑆 − (𝑆 · 𝑇))) ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
104	93, 102, 58, 76, 103	syl22anc 836	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
105	54, 53	addge01d 11230	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ 𝑇 ↔ 𝑆 ≤ (𝑆 + 𝑇)))
106	61, 105	mpbid 234	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≤ (𝑆 + 𝑇))
107	54, 57, 55, 106	lesub1dd 11258	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ≤ ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
108	107, 86	breqtrrd 5096	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
109		ledivmul2 11521	. . . . . . 7 ⊢ (((𝑆 − (𝑆 · 𝑇)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
110	93, 59, 58, 76, 109	syl112anc 1370	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
111	108, 110	mpbird 259	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1)
112		elicc01 12857	. . . . 5 ⊢ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ↔ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ ∧ 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∧ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1))
113	94, 104, 111, 112	syl3anbrc 1339	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1))
114	1, 53, 5	sylancr 589	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
115	114	recnd 10671	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
116	98, 115, 85, 77	div23d 11455	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · (1 − 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑇)))
117		subdi 11075	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
118	26, 117	mp3an2 1445	. . . . . . . 8 ⊢ ((𝑆 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
119	98, 65, 118	syl2anc 586	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
120	99	oveq1d 7173	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 1) − (𝑆 · 𝑇)) = (𝑆 − (𝑆 · 𝑇)))
121	119, 120	eqtrd 2858	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · (1 − 𝑇)) = (𝑆 − (𝑆 · 𝑇)))
122	121	oveq1d 7173	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · (1 − 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
123	56	recnd 10671	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ∈ ℂ)
124	85, 123, 85, 77	divsubdird 11457	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
125	57	recnd 10671	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 + 𝑇) ∈ ℂ)
126	55	recnd 10671	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ∈ ℂ)
127	125, 65, 126	nnncan2d 11034	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − 𝑇))
128	98, 65	pncand 11000	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − 𝑇) = 𝑆)
129	127, 128	eqtrd 2858	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) = 𝑆)
130	129	oveq1d 7173	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
131	85, 77	dividd 11416	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = 1)
132	131	oveq1d 7173	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
133	124, 130, 132	3eqtr3d 2866	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
134	133	oveq1d 7173	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑇)) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
135	116, 122, 134	3eqtr3d 2866	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
136	1, 54, 13	sylancr 589	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℝ)
137	136	recnd 10671	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℂ)
138	65, 137, 85, 77	div23d 11455	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · (1 − 𝑆)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑆)))
139		subdi 11075	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
140	26, 139	mp3an2 1445	. . . . . . . 8 ⊢ ((𝑇 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
141	65, 98, 140	syl2anc 586	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
142	65	mulid1d 10660	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · 1) = 𝑇)
143	65, 98	mulcomd 10664	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · 𝑆) = (𝑆 · 𝑇))
144	142, 143	oveq12d 7176	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 1) − (𝑇 · 𝑆)) = (𝑇 − (𝑆 · 𝑇)))
145	141, 144	eqtrd 2858	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · (1 − 𝑆)) = (𝑇 − (𝑆 · 𝑇)))
146	145	oveq1d 7173	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · (1 − 𝑆)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
147	93	recnd 10671	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ∈ ℂ)
148	85, 147, 85, 77	divsubdird 11457	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
149	125, 98, 126	nnncan2d 11034	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − 𝑆))
150	98, 65	pncan2d 11001	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − 𝑆) = 𝑇)
151	149, 150	eqtrd 2858	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) = 𝑇)
152	151	oveq1d 7173	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
153	131	oveq1d 7173	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
154	148, 152, 153	3eqtr3d 2866	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
155	154	oveq1d 7173	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑆)) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
156	138, 146, 155	3eqtr3d 2866	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
157	98, 65	mulcomd 10664	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) = (𝑇 · 𝑆))
158	157	oveq1d 7173	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
159	98, 65, 85, 77	div23d 11455	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑇))
160	133	oveq1d 7173	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑇) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
161	159, 160	eqtrd 2858	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
162	65, 98, 85, 77	div23d 11455	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑆))
163	154	oveq1d 7173	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑆) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
164	162, 163	eqtrd 2858	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
165	158, 161, 164	3eqtr3d 2866	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
166		oveq2 7166	. . . . . . . 8 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (1 − 𝑟) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
167	166	oveq1d 7173	. . . . . . 7 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑟) · (1 − 𝑇)) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
168	167	eqeq2d 2834	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ↔ 𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇))))
169		eqeq1 2827	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ↔ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆))))
170	166	oveq1d 7173	. . . . . . 7 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑟) · 𝑇) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
171	170	eqeq1d 2825	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆)))
172	168, 169, 171	3anbi123d 1432	. . . . 5 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆))))
173		eqeq1 2827	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ↔ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇))))
174		oveq2 7166	. . . . . . . 8 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (1 − 𝑝) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
175	174	oveq1d 7173	. . . . . . 7 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑝) · (1 − 𝑆)) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
176	175	eqeq2d 2834	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ↔ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆))))
177	174	oveq1d 7173	. . . . . . 7 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑝) · 𝑆) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
178	177	eqeq2d 2834	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆)))
179	173, 176, 178	3anbi123d 1432	. . . . 5 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))))
180	172, 179	rspc2ev 3637	. . . 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 1378	. . 3 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
182	181	ex 415	. 2 ⊢ (𝑆 ≠ 0 → ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆))))
183	52, 182	pm2.61ine 3102	1 ⊢ ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  ∃wrex 3141   class class class wbr 5068  (class class class)co 7158  ℂcc 10537  ℝcr 10538  0cc0 10539  1c1 10540   + caddc 10542   · cmul 10544   < clt 10677   ≤ cle 10678   − cmin 10872   / cdiv 11299  [,]cicc 12744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-po 5476  df-so 5477  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-div 11300  df-icc 12748

This theorem is referenced by:  axpasch  26729