MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axpaschlem Structured version   Visualization version   GIF version

Theorem axpaschlem 27889
Description: Lemma for axpasch 27890. 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
StepHypRef Expression
1 1re 11155 . . . . . . . 8 1 ∈ ℝ
2 elicc01 13383 . . . . . . . . . 10 (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇𝑇 ≤ 1))
32simp1bi 1145 . . . . . . . . 9 (𝑇 ∈ (0[,]1) → 𝑇 ∈ ℝ)
43ad2antrl 726 . . . . . . . 8 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5 resubcl 11465 . . . . . . . 8 ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
61, 4, 5sylancr 587 . . . . . . 7 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
76recnd 11183 . . . . . 6 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
87mul02d 11353 . . . . 5 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · (1 − 𝑇)) = 0)
98eqcomd 2742 . . . 4 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 = (0 · (1 − 𝑇)))
10 elicc01 13383 . . . . . . . . . 10 (𝑆 ∈ (0[,]1) ↔ (𝑆 ∈ ℝ ∧ 0 ≤ 𝑆𝑆 ≤ 1))
1110simp1bi 1145 . . . . . . . . 9 (𝑆 ∈ (0[,]1) → 𝑆 ∈ ℝ)
1211ad2antll 727 . . . . . . . 8 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℝ)
13 resubcl 11465 . . . . . . . 8 ((1 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (1 − 𝑆) ∈ ℝ)
141, 12, 13sylancr 587 . . . . . . 7 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℝ)
1514recnd 11183 . . . . . 6 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℂ)
1615mulid2d 11173 . . . . 5 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · (1 − 𝑆)) = (1 − 𝑆))
17 oveq2 7365 . . . . . . 7 (𝑆 = 0 → (1 − 𝑆) = (1 − 0))
1817adantr 481 . . . . . 6 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) = (1 − 0))
19 1m0e1 12274 . . . . . 6 (1 − 0) = 1
2018, 19eqtrdi 2792 . . . . 5 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) = 1)
2116, 20eqtr2d 2777 . . . 4 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 1 = (1 · (1 − 𝑆)))
224recnd 11183 . . . . . 6 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
2322mul02d 11353 . . . . 5 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · 𝑇) = 0)
24 oveq2 7365 . . . . . . 7 (𝑆 = 0 → (1 · 𝑆) = (1 · 0))
2524adantr 481 . . . . . 6 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑆) = (1 · 0))
26 ax-1cn 11109 . . . . . . 7 1 ∈ ℂ
2726mul01i 11345 . . . . . 6 (1 · 0) = 0
2825, 27eqtrdi 2792 . . . . 5 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑆) = 0)
2923, 28eqtr4d 2779 . . . 4 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 · 𝑇) = (1 · 𝑆))
30 1elunit 13387 . . . . 5 1 ∈ (0[,]1)
31 0elunit 13386 . . . . 5 0 ∈ (0[,]1)
32 oveq2 7365 . . . . . . . . . 10 (𝑟 = 1 → (1 − 𝑟) = (1 − 1))
33 1m1e0 12225 . . . . . . . . . 10 (1 − 1) = 0
3432, 33eqtrdi 2792 . . . . . . . . 9 (𝑟 = 1 → (1 − 𝑟) = 0)
3534oveq1d 7372 . . . . . . . 8 (𝑟 = 1 → ((1 − 𝑟) · (1 − 𝑇)) = (0 · (1 − 𝑇)))
3635eqeq2d 2747 . . . . . . 7 (𝑟 = 1 → (𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ↔ 𝑝 = (0 · (1 − 𝑇))))
37 eqeq1 2740 . . . . . . 7 (𝑟 = 1 → (𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ↔ 1 = ((1 − 𝑝) · (1 − 𝑆))))
3834oveq1d 7372 . . . . . . . 8 (𝑟 = 1 → ((1 − 𝑟) · 𝑇) = (0 · 𝑇))
3938eqeq1d 2738 . . . . . . 7 (𝑟 = 1 → (((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ (0 · 𝑇) = ((1 − 𝑝) · 𝑆)))
4036, 37, 393anbi123d 1436 . . . . . 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 7365 . . . . . . . . . 10 (𝑝 = 0 → (1 − 𝑝) = (1 − 0))
4342, 19eqtrdi 2792 . . . . . . . . 9 (𝑝 = 0 → (1 − 𝑝) = 1)
4443oveq1d 7372 . . . . . . . 8 (𝑝 = 0 → ((1 − 𝑝) · (1 − 𝑆)) = (1 · (1 − 𝑆)))
4544eqeq2d 2747 . . . . . . 7 (𝑝 = 0 → (1 = ((1 − 𝑝) · (1 − 𝑆)) ↔ 1 = (1 · (1 − 𝑆))))
4643oveq1d 7372 . . . . . . . 8 (𝑝 = 0 → ((1 − 𝑝) · 𝑆) = (1 · 𝑆))
4746eqeq2d 2747 . . . . . . 7 (𝑝 = 0 → ((0 · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ (0 · 𝑇) = (1 · 𝑆)))
4841, 45, 473anbi123d 1436 . . . . . 6 (𝑝 = 0 → ((𝑝 = (0 · (1 − 𝑇)) ∧ 1 = ((1 − 𝑝) · (1 − 𝑆)) ∧ (0 · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (0 = (0 · (1 − 𝑇)) ∧ 1 = (1 · (1 − 𝑆)) ∧ (0 · 𝑇) = (1 · 𝑆))))
4940, 48rspc2ev 3592 . . . . 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 − 𝑝) · 𝑆)))
5030, 31, 49mp3an12 1451 . . . 4 ((0 = (0 · (1 − 𝑇)) ∧ 1 = (1 · (1 − 𝑆)) ∧ (0 · 𝑇) = (1 · 𝑆)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
519, 21, 29, 50syl3anc 1371 . . 3 ((𝑆 = 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
5251ex 413 . 2 (𝑆 = 0 → ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆))))
533ad2antrl 726 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5411ad2antll 727 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℝ)
5554, 53remulcld 11185 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ∈ ℝ)
5653, 55resubcld 11583 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ∈ ℝ)
5754, 53readdcld 11184 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 + 𝑇) ∈ ℝ)
5857, 55resubcld 11583 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ)
59 1red 11156 . . . . . . . . . . 11 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 1 ∈ ℝ)
602simp2bi 1146 . . . . . . . . . . . 12 (𝑇 ∈ (0[,]1) → 0 ≤ 𝑇)
6160ad2antrl 726 . . . . . . . . . . 11 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ 𝑇)
6210simp3bi 1147 . . . . . . . . . . . 12 (𝑆 ∈ (0[,]1) → 𝑆 ≤ 1)
6362ad2antll 727 . . . . . . . . . . 11 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≤ 1)
6454, 59, 53, 61, 63lemul1ad 12094 . . . . . . . . . 10 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ (1 · 𝑇))
6553recnd 11183 . . . . . . . . . . 11 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
6665mulid2d 11173 . . . . . . . . . 10 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · 𝑇) = 𝑇)
6764, 66breqtrd 5131 . . . . . . . . 9 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ 𝑇)
6810simp2bi 1146 . . . . . . . . . . . 12 (𝑆 ∈ (0[,]1) → 0 ≤ 𝑆)
6968ad2antll 727 . . . . . . . . . . 11 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ 𝑆)
70 simpl 483 . . . . . . . . . . 11 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≠ 0)
7154, 69, 70ne0gt0d 11292 . . . . . . . . . 10 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 < 𝑆)
7254, 53ltaddpos2d 11740 . . . . . . . . . 10 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 < 𝑆𝑇 < (𝑆 + 𝑇)))
7371, 72mpbid 231 . . . . . . . . 9 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 < (𝑆 + 𝑇))
7455, 53, 57, 67, 73lelttrd 11313 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) < (𝑆 + 𝑇))
7555, 57posdifd 11742 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) < (𝑆 + 𝑇) ↔ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
7674, 75mpbid 231 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
7776gt0ne0d 11719 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ≠ 0)
7856, 58, 77redivcld 11983 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ)
7953, 55subge0d 11745 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ (𝑇 − (𝑆 · 𝑇)) ↔ (𝑆 · 𝑇) ≤ 𝑇))
8067, 79mpbird 256 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ (𝑇 − (𝑆 · 𝑇)))
81 divge0 12024 . . . . . 6 ((((𝑇 − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 ≤ (𝑇 − (𝑆 · 𝑇))) ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
8256, 80, 58, 76, 81syl22anc 837 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
8353, 57, 73ltled 11303 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ≤ (𝑆 + 𝑇))
8453, 57, 55, 83lesub1dd 11771 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ≤ ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
8558recnd 11183 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℂ)
8685mulid2d 11173 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
8784, 86breqtrrd 5133 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
88 ledivmul2 12034 . . . . . . 7 (((𝑇 − (𝑆 · 𝑇)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
8956, 59, 58, 76, 88syl112anc 1374 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑇 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
9087, 89mpbird 256 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1)
91 elicc01 13383 . . . . 5 (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ↔ (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ ∧ 0 ≤ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1))
9278, 82, 90, 91syl3anbrc 1343 . . . 4 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1))
9354, 55resubcld 11583 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ∈ ℝ)
9493, 58, 77redivcld 11983 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ)
952simp3bi 1147 . . . . . . . . . 10 (𝑇 ∈ (0[,]1) → 𝑇 ≤ 1)
9695ad2antrl 726 . . . . . . . . 9 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑇 ≤ 1)
9753, 59, 54, 69, 96lemul2ad 12095 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ (𝑆 · 1))
9854recnd 11183 . . . . . . . . 9 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ∈ ℂ)
9998mulid1d 11172 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 1) = 𝑆)
10097, 99breqtrd 5131 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ≤ 𝑆)
10154, 55subge0d 11745 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ (𝑆 − (𝑆 · 𝑇)) ↔ (𝑆 · 𝑇) ≤ 𝑆))
102100, 101mpbird 256 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ (𝑆 − (𝑆 · 𝑇)))
103 divge0 12024 . . . . . 6 ((((𝑆 − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 ≤ (𝑆 − (𝑆 · 𝑇))) ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
10493, 102, 58, 76, 103syl22anc 837 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
10554, 53addge01d 11743 . . . . . . . . 9 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (0 ≤ 𝑇𝑆 ≤ (𝑆 + 𝑇)))
10661, 105mpbid 231 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → 𝑆 ≤ (𝑆 + 𝑇))
10754, 57, 55, 106lesub1dd 11771 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ≤ ((𝑆 + 𝑇) − (𝑆 · 𝑇)))
108107, 86breqtrrd 5133 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
109 ledivmul2 12034 . . . . . . 7 (((𝑆 − (𝑆 · 𝑇)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((𝑆 + 𝑇) − (𝑆 · 𝑇)) ∈ ℝ ∧ 0 < ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) → (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
11093, 59, 58, 76, 109syl112anc 1374 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1 ↔ (𝑆 − (𝑆 · 𝑇)) ≤ (1 · ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
111108, 110mpbird 256 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1)
112 elicc01 13383 . . . . 5 (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ↔ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ ℝ ∧ 0 ≤ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∧ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ≤ 1))
11394, 104, 111, 112syl3anbrc 1343 . . . 4 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1))
1141, 53, 5sylancr 587 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
115114recnd 11183 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
11698, 115, 85, 77div23d 11968 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · (1 − 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑇)))
117 subdi 11588 . . . . . . . . 9 ((𝑆 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
11826, 117mp3an2 1449 . . . . . . . 8 ((𝑆 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
11998, 65, 118syl2anc 584 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · (1 − 𝑇)) = ((𝑆 · 1) − (𝑆 · 𝑇)))
12099oveq1d 7372 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 1) − (𝑆 · 𝑇)) = (𝑆 − (𝑆 · 𝑇)))
121119, 120eqtrd 2776 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · (1 − 𝑇)) = (𝑆 − (𝑆 · 𝑇)))
122121oveq1d 7372 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · (1 − 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
12356recnd 11183 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 − (𝑆 · 𝑇)) ∈ ℂ)
12485, 123, 85, 77divsubdird 11970 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
12557recnd 11183 . . . . . . . . . 10 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 + 𝑇) ∈ ℂ)
12655recnd 11183 . . . . . . . . . 10 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) ∈ ℂ)
127125, 65, 126nnncan2d 11547 . . . . . . . . 9 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − 𝑇))
12898, 65pncand 11513 . . . . . . . . 9 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − 𝑇) = 𝑆)
129127, 128eqtrd 2776 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) = 𝑆)
130129oveq1d 7372 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑇 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
13185, 77dividd 11929 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = 1)
132131oveq1d 7372 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
133124, 130, 1323eqtr3d 2784 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
134133oveq1d 7372 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑇)) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
135116, 122, 1343eqtr3d 2784 . . . 4 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
1361, 54, 13sylancr 587 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℝ)
137136recnd 11183 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (1 − 𝑆) ∈ ℂ)
13865, 137, 85, 77div23d 11968 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · (1 − 𝑆)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑆)))
139 subdi 11588 . . . . . . . . 9 ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
14026, 139mp3an2 1449 . . . . . . . 8 ((𝑇 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
14165, 98, 140syl2anc 584 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · (1 − 𝑆)) = ((𝑇 · 1) − (𝑇 · 𝑆)))
14265mulid1d 11172 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · 1) = 𝑇)
14365, 98mulcomd 11176 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · 𝑆) = (𝑆 · 𝑇))
144142, 143oveq12d 7375 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 1) − (𝑇 · 𝑆)) = (𝑇 − (𝑆 · 𝑇)))
145141, 144eqtrd 2776 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 · (1 − 𝑆)) = (𝑇 − (𝑆 · 𝑇)))
146145oveq1d 7372 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · (1 − 𝑆)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
14793recnd 11183 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 − (𝑆 · 𝑇)) ∈ ℂ)
14885, 147, 85, 77divsubdird 11970 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
149125, 98, 126nnncan2d 11547 . . . . . . . . 9 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) = ((𝑆 + 𝑇) − 𝑆))
15098, 65pncan2d 11514 . . . . . . . . 9 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 + 𝑇) − 𝑆) = 𝑇)
151149, 150eqtrd 2776 . . . . . . . 8 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) = 𝑇)
152151oveq1d 7372 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) − (𝑆 − (𝑆 · 𝑇))) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
153131oveq1d 7372 . . . . . . 7 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((((𝑆 + 𝑇) − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
154148, 152, 1533eqtr3d 2784 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
155154oveq1d 7372 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · (1 − 𝑆)) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
156138, 146, 1553eqtr3d 2784 . . . 4 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
15798, 65mulcomd 11176 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → (𝑆 · 𝑇) = (𝑇 · 𝑆))
158157oveq1d 7372 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))))
15998, 65, 85, 77div23d 11968 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑇))
160133oveq1d 7372 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑇) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
161159, 160eqtrd 2776 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑆 · 𝑇) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
16265, 98, 85, 77div23d 11968 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑆))
163154oveq1d 7372 . . . . . 6 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) · 𝑆) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
164162, 163eqtrd 2776 . . . . 5 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((𝑇 · 𝑆) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
165158, 161, 1643eqtr3d 2784 . . . 4 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
166 oveq2 7365 . . . . . . . 8 (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (1 − 𝑟) = (1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
167166oveq1d 7372 . . . . . . 7 (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑟) · (1 − 𝑇)) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)))
168167eqeq2d 2747 . . . . . 6 (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ↔ 𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇))))
169 eqeq1 2740 . . . . . 6 (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ↔ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆))))
170166oveq1d 7372 . . . . . . 7 (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑟) · 𝑇) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇))
171170eqeq1d 2738 . . . . . 6 (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆)))
172168, 169, 1713anbi123d 1436 . . . . 5 (𝑟 = ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆))))
173 eqeq1 2740 . . . . . 6 (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ↔ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇))))
174 oveq2 7365 . . . . . . . 8 (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (1 − 𝑝) = (1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))))
175174oveq1d 7372 . . . . . . 7 (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑝) · (1 − 𝑆)) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)))
176175eqeq2d 2747 . . . . . 6 (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ↔ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆))))
177174oveq1d 7372 . . . . . . 7 (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((1 − 𝑝) · 𝑆) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))
178177eqeq2d 2747 . . . . . 6 (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → (((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆) ↔ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆)))
179173, 176, 1783anbi123d 1436 . . . . 5 (𝑝 = ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) → ((𝑝 = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − 𝑝) · 𝑆)) ↔ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))))
180172, 179rspc2ev 3592 . . . 4 ((((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ∧ ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) ∈ (0[,]1) ∧ (((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑇)) ∧ ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇))) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · (1 − 𝑆)) ∧ ((1 − ((𝑇 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑇) = ((1 − ((𝑆 − (𝑆 · 𝑇)) / ((𝑆 + 𝑇) − (𝑆 · 𝑇)))) · 𝑆))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
18192, 113, 135, 156, 165, 180syl113anc 1382 . . 3 ((𝑆 ≠ 0 ∧ (𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
182181ex 413 . 2 (𝑆 ≠ 0 → ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆))))
18352, 182pm2.61ine 3028 1 ((𝑇 ∈ (0[,]1) ∧ 𝑆 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑝 ∈ (0[,]1)(𝑝 = ((1 − 𝑟) · (1 − 𝑇)) ∧ 𝑟 = ((1 − 𝑝) · (1 − 𝑆)) ∧ ((1 − 𝑟) · 𝑇) = ((1 − 𝑝) · 𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wrex 3073   class class class wbr 5105  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  [,]cicc 13267
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-icc 13271
This theorem is referenced by:  axpasch  27890
  Copyright terms: Public domain W3C validator