Theorem axpaschlem 29199

Description: Lemma for axpasch 29200. 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 11196	. . . . . . . 8 ⊢ 1 ∈ ℝ
2		elicc01 13484	. . . . . . . . . 10 ⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
3	2	simp1bi 1161	. . . . . . . . 9 ⊢ (𝑇 ∈ (0[,]1) → 𝑇 ∈ ℝ)
4	3	ad2antrl 740	. . . . . . . 8 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5		resubcl 11510	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
6	1, 4, 5	sylancr 598	. . . . . . 7 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
7	6	recnd 11225	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
8	7	mul02d 11396	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · (1 − 𝑇)) = 0)
9	8	eqcomd 2771	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 = (0 · (1 − 𝑇)))
10		elicc01 13484	. . . . . . . . . 10 ⊢ (𝑆 ∈ (0[,]1) ↔ (𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ∧ 𝑆 ≤ 1))
11	10	simp1bi 1161	. . . . . . . . 9 ⊢ (𝑆 ∈ (0[,]1) → 𝑆 ∈ ℝ)
12	11	ad2antll 741	. . . . . . . 8 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℝ)
13		resubcl 11510	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (1 − 𝑆) ∈ ℝ)
14	1, 12, 13	sylancr 598	. . . . . . 7 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℝ)
15	14	recnd 11225	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℂ)
16	15	mullidd 11215	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · (1 − 𝑆)) = (1 − 𝑆))
17		oveq2 7408	. . . . . . 7 ⊢ (𝑆 = 0 → (1 − 𝑆) = (1 − 0))
18	17	adantr 485	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) = (1 − 0))
19		1m0e1 12351	. . . . . 6 ⊢ (1 − 0) = 1
20	18, 19	eqtrdi 2816	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) = 1)
21	16, 20	eqtr2d 2801	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 1 = (1 · (1 − 𝑆)))
22	4	recnd 11225	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
23	22	mul02d 11396	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · 𝑇) = 0)
24		oveq2 7408	. . . . . . 7 ⊢ (𝑆 = 0 → (1 · 𝑆) = (1 · 0))
25	24	adantr 485	. . . . . 6 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑆) = (1 · 0))
26		ax-1cn 11146	. . . . . . 7 ⊢ 1 ∈ ℂ
27	26	mul01i 11388	. . . . . 6 ⊢ (1 · 0) = 0
28	25, 27	eqtrdi 2816	. . . . 5 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑆) = 0)
29	23, 28	eqtr4d 2803	. . . 4 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · 𝑇) = (1 · 𝑆))
30		1elunit 13488	. . . . 5 ⊢ 1 ∈ (0[,]1)
31		0elunit 13487	. . . . 5 ⊢ 0 ∈ (0[,]1)
32		oveq2 7408	. . . . . . . . . 10 ⊢ (𝑟 = 1 → (1 − 𝑟) = (1 − 1))
33		1m1e0 12304	. . . . . . . . . 10 ⊢ (1 − 1) = 0
34	32, 33	eqtrdi 2816	. . . . . . . . 9 ⊢ (𝑟 = 1 → (1 − 𝑟) = 0)
35	34	oveq1d 7415	. . . . . . . 8 ⊢ (𝑟 = 1 → ((1 − 𝑟) · (1 − 𝑇)) = (0 · (1 − 𝑇)))
36	35	eqeq2d 2776	. . . . . . 7 ⊢ (𝑟 = 1 → (𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ↔ 𝑝 = (0 · (1 − 𝑇))))
37		eqeq1 2769	. . . . . . 7 ⊢ (𝑟 = 1 → (𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ↔ 1 = ((1 − 𝑝) · (1 − 𝑆))))
38	34	oveq1d 7415	. . . . . . . 8 ⊢ (𝑟 = 1 → ((1 − 𝑟) · 𝑇) = (0 · 𝑇))
39	38	eqeq1d 2767	. . . . . . 7 ⊢ (𝑟 = 1 → (((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ (0 · 𝑇) = ((1 − 𝑝) · 𝑆)))
40	36, 37, 39	3anbi123d 1460	. . . . . 6 ⊢ (𝑟 = 1 → ((𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (𝑝 = (0 · (1 − 𝑇)) ∧ 1 = ((1 − 𝑝) · (1 − 𝑆)) ∧ (0 · 𝑇) = ((1 − 𝑝) · 𝑆))))
41		eqeq1 2769	. . . . . . 7 ⊢ (𝑝 = 0 → (𝑝 = (0 · (1 − 𝑇)) ↔ 0 = (0 · (1 − 𝑇))))
42		oveq2 7408	. . . . . . . . . 10 ⊢ (𝑝 = 0 → (1 − 𝑝) = (1 − 0))
43	42, 19	eqtrdi 2816	. . . . . . . . 9 ⊢ (𝑝 = 0 → (1 − 𝑝) = 1)
44	43	oveq1d 7415	. . . . . . . 8 ⊢ (𝑝 = 0 → ((1 − 𝑝) · (1 − 𝑆)) = (1 · (1 − 𝑆)))
45	44	eqeq2d 2776	. . . . . . 7 ⊢ (𝑝 = 0 → (1 = ((1 − 𝑝) · (1 − 𝑆)) ↔ 1 = (1 · (1 − 𝑆))))
46	43	oveq1d 7415	. . . . . . . 8 ⊢ (𝑝 = 0 → ((1 − 𝑝) · 𝑆) = (1 · 𝑆))
47	46	eqeq2d 2776	. . . . . . 7 ⊢ (𝑝 = 0 → ((0 · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ (0 · 𝑇) = (1 · 𝑆)))
48	41, 45, 47	3anbi123d 1460	. . . . . 6 ⊢ (𝑝 = 0 → ((𝑝 = (0 · (1 − 𝑇)) ∧ 1 = ((1 − 𝑝) · (1 − 𝑆)) ∧ (0 · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (0 = (0 · (1 − 𝑇)) ∧ 1 = (1 · (1 − 𝑆)) ∧ (0 · 𝑇) = (1 · 𝑆))))
49	40, 48	rspc2ev 3597	. . . . 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 1475	. . . 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 1394	. . 3 ⊢ ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
52	51	ex 417	. 2 ⊢ (𝑆 = 0 → ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆))))
53	3	ad2antrl 740	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
54	11	ad2antll 741	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℝ)
55	54, 53	remulcld 11227	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ∈ ℝ)
56	53, 55	resubcld 11630	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ∈ ℝ)
57	54, 53	readdcld 11226	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 + 𝑇) ∈ ℝ)
58	57, 55	resubcld 11630	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ)
59		1red 11197	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 1 ∈ ℝ)
60	2	simp2bi 1162	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0[,]1) → 0 ≤ 𝑇)
61	60	ad2antrl 740	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ 𝑇)
62	10	simp3bi 1163	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (0[,]1) → 𝑆 ≤ 1)
63	62	ad2antll 741	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≤ 1)
64	54, 59, 53, 61, 63	lemul1ad 12145	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ (1 · 𝑇))
65	53	recnd 11225	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
66	65	mullidd 11215	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑇) = 𝑇)
67	64, 66	breqtrd 5131	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ 𝑇)
68	10	simp2bi 1162	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (0[,]1) → 0 ≤ 𝑆)
69	68	ad2antll 741	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ 𝑆)
70		simpl 487	. . . . . . . . . . 11 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≠ 0)
71	54, 69, 70	ne0gt0d 11335	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 < 𝑆)
72	54, 53	ltaddpos2d 11787	. . . . . . . . . 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 11356	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) < (𝑆 + 𝑇))
75	55, 57	posdifd 11789	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) < (𝑆 + 𝑇) ↔ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
76	74, 75	mpbid 235	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
77	76	gt0ne0d 11766	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ≠ 0)
78	56, 58, 77	redivcld 12034	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ)
79	53, 55	subge0d 11792	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ (𝑇 − (𝑆 · 𝑇)) ↔ (𝑆 · 𝑇) ≤ 𝑇))
80	67, 79	mpbird 260	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ (𝑇 − (𝑆 · 𝑇)))
81		divge0 12075	. . . . . 6 ⊢ ((((𝑇 − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 ≤ (𝑇 − (𝑆 · 𝑇))) ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
82	56, 80, 58, 76, 81	syl22anc 851	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
83	53, 57, 73	ltled 11346	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ≤ (𝑆 + 𝑇))
84	53, 57, 55, 83	lesub1dd 11818	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ≤ ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
85	58	recnd 11225	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℂ)
86	85	mullidd 11215	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
87	84, 86	breqtrrd 5133	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
88		ledivmul2 12085	. . . . . . 7 ⊢ (((𝑇 − (𝑆 · 𝑇)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
89	56, 59, 58, 76, 88	syl112anc 1397	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
90	87, 89	mpbird 260	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1)
91		elicc01 13484	. . . . 5 ⊢ (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ↔ (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ ∧ 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1))
92	78, 82, 90, 91	syl3anbrc 1360	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1))
93	54, 55	resubcld 11630	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ∈ ℝ)
94	93, 58, 77	redivcld 12034	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ)
95	2	simp3bi 1163	. . . . . . . . . 10 ⊢ (𝑇 ∈ (0[,]1) → 𝑇 ≤ 1)
96	95	ad2antrl 740	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ≤ 1)
97	53, 59, 54, 69, 96	lemul2ad 12146	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ (𝑆 · 1))
98	54	recnd 11225	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℂ)
99	98	mulridd 11214	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 1) = 𝑆)
100	97, 99	breqtrd 5131	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ 𝑆)
101	54, 55	subge0d 11792	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ (𝑆 − (𝑆 · 𝑇)) ↔ (𝑆 · 𝑇) ≤ 𝑆))
102	100, 101	mpbird 260	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ (𝑆 − (𝑆 · 𝑇)))
103		divge0 12075	. . . . . 6 ⊢ ((((𝑆 − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 ≤ (𝑆 − (𝑆 · 𝑇))) ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
104	93, 102, 58, 76, 103	syl22anc 851	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
105	54, 53	addge01d 11790	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ 𝑇 ↔ 𝑆 ≤ (𝑆 + 𝑇)))
106	61, 105	mpbid 235	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≤ (𝑆 + 𝑇))
107	54, 57, 55, 106	lesub1dd 11818	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ≤ ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
108	107, 86	breqtrrd 5133	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
109		ledivmul2 12085	. . . . . . 7 ⊢ (((𝑆 − (𝑆 · 𝑇)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
110	93, 59, 58, 76, 109	syl112anc 1397	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
111	108, 110	mpbird 260	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1)
112		elicc01 13484	. . . . 5 ⊢ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ↔ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ ∧ 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∧ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1))
113	94, 104, 111, 112	syl3anbrc 1360	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1))
114	1, 53, 5	sylancr 598	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
115	114	recnd 11225	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
116	98, 115, 85, 77	div23d 12019	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · (1 − 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑇)))
117		subdi 11635	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
118	26, 117	mp3an2 1473	. . . . . . . 8 ⊢ ((𝑆 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
119	98, 65, 118	syl2anc 595	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
120	99	oveq1d 7415	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 1) − (𝑆 · 𝑇)) = (𝑆 − (𝑆 · 𝑇)))
121	119, 120	eqtrd 2800	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · (1 − 𝑇)) = (𝑆 − (𝑆 · 𝑇)))
122	121	oveq1d 7415	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · (1 − 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
123	56	recnd 11225	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ∈ ℂ)
124	85, 123, 85, 77	divsubdird 12021	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
125	57	recnd 11225	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 + 𝑇) ∈ ℂ)
126	55	recnd 11225	. . . . . . . . . 10 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ∈ ℂ)
127	125, 65, 126	nnncan2d 11592	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − 𝑇))
128	98, 65	pncand 11558	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − 𝑇) = 𝑆)
129	127, 128	eqtrd 2800	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) = 𝑆)
130	129	oveq1d 7415	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
131	85, 77	dividd 11980	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = 1)
132	131	oveq1d 7415	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
133	124, 130, 132	3eqtr3d 2808	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
134	133	oveq1d 7415	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑇)) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
135	116, 122, 134	3eqtr3d 2808	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
136	1, 54, 13	sylancr 598	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℝ)
137	136	recnd 11225	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℂ)
138	65, 137, 85, 77	div23d 12019	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · (1 − 𝑆)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑆)))
139		subdi 11635	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
140	26, 139	mp3an2 1473	. . . . . . . 8 ⊢ ((𝑇 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
141	65, 98, 140	syl2anc 595	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
142	65	mulridd 11214	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · 1) = 𝑇)
143	65, 98	mulcomd 11218	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · 𝑆) = (𝑆 · 𝑇))
144	142, 143	oveq12d 7418	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 1) − (𝑇 · 𝑆)) = (𝑇 − (𝑆 · 𝑇)))
145	141, 144	eqtrd 2800	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · (1 − 𝑆)) = (𝑇 − (𝑆 · 𝑇)))
146	145	oveq1d 7415	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · (1 − 𝑆)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
147	93	recnd 11225	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ∈ ℂ)
148	85, 147, 85, 77	divsubdird 12021	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
149	125, 98, 126	nnncan2d 11592	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − 𝑆))
150	98, 65	pncan2d 11559	. . . . . . . . 9 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − 𝑆) = 𝑇)
151	149, 150	eqtrd 2800	. . . . . . . 8 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) = 𝑇)
152	151	oveq1d 7415	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
153	131	oveq1d 7415	. . . . . . 7 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
154	148, 152, 153	3eqtr3d 2808	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
155	154	oveq1d 7415	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑆)) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
156	138, 146, 155	3eqtr3d 2808	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
157	98, 65	mulcomd 11218	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) = (𝑇 · 𝑆))
158	157	oveq1d 7415	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
159	98, 65, 85, 77	div23d 12019	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑇))
160	133	oveq1d 7415	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑇) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
161	159, 160	eqtrd 2800	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
162	65, 98, 85, 77	div23d 12019	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑆))
163	154	oveq1d 7415	. . . . . 6 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑆) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
164	162, 163	eqtrd 2800	. . . . 5 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
165	158, 161, 164	3eqtr3d 2808	. . . 4 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
166		oveq2 7408	. . . . . . . 8 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (1 − 𝑟) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
167	166	oveq1d 7415	. . . . . . 7 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑟) · (1 − 𝑇)) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
168	167	eqeq2d 2776	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ↔ 𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇))))
169		eqeq1 2769	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ↔ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆))))
170	166	oveq1d 7415	. . . . . . 7 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑟) · 𝑇) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
171	170	eqeq1d 2767	. . . . . 6 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆)))
172	168, 169, 171	3anbi123d 1460	. . . . 5 ⊢ (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆))))
173		eqeq1 2769	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ↔ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇))))
174		oveq2 7408	. . . . . . . 8 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (1 − 𝑝) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
175	174	oveq1d 7415	. . . . . . 7 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑝) · (1 − 𝑆)) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
176	175	eqeq2d 2776	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ↔ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆))))
177	174	oveq1d 7415	. . . . . . 7 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑝) · 𝑆) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
178	177	eqeq2d 2776	. . . . . 6 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆)))
179	173, 176, 178	3anbi123d 1460	. . . . 5 ⊢ (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))))
180	172, 179	rspc2ev 3597	. . . 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 1405	. . 3 ⊢ ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
182	181	ex 417	. 2 ⊢ (𝑆 ≠ 0 → ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆))))
183	52, 182	pm2.61ine 3043	1 ⊢ ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145   ≠ wne 2960  ∃wrex 3089   class class class wbr 5105  (class class class)co 7400  ℂcc 11086  ℝcr 11087  0cc0 11088  1c1 11089   + caddc 11091   · cmul 11093   < clt 11231   ≤ cle 11232   − cmin 11429   / cdiv 11859  [,]cicc 13366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-po 5560  df-so 5561  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-icc 13370

This theorem is referenced by:  axpasch  29200