Metamath Proof Explorer

Theorem axpaschlem

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

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

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 elicc01 ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) ↔ ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1 ) )
3 2 simp1bi ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 𝑇 ∈ ℝ )
4 3 ad2antrl ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℝ )
5 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑇 ∈ ℝ ) → ( 1 − 𝑇 ) ∈ ℝ )
6 1 4 5 sylancr ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑇 ) ∈ ℝ )
7 6 recnd ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑇 ) ∈ ℂ )
8 7 mul02d ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 0 · ( 1 − 𝑇 ) ) = 0 )
9 8 eqcomd ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 0 = ( 0 · ( 1 − 𝑇 ) ) )
10 elicc01 ⊢ ( 𝑆 ∈ ( 0 [,] 1 ) ↔ ( 𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ∧ 𝑆 ≤ 1 ) )
11 10 simp1bi ⊢ ( 𝑆 ∈ ( 0 [,] 1 ) → 𝑆 ∈ ℝ )
12 11 ad2antll ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑆 ∈ ℝ )
13 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( 1 − 𝑆 ) ∈ ℝ )
14 1 12 13 sylancr ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑆 ) ∈ ℝ )
15 14 recnd ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑆 ) ∈ ℂ )
16 15 mullidd ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 · ( 1 − 𝑆 ) ) = ( 1 − 𝑆 ) )
17 oveq2 ⊢ ( 𝑆 = 0 → ( 1 − 𝑆 ) = ( 1 − 0 ) )
18 17 adantr ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑆 ) = ( 1 − 0 ) )
19 1m0e1 ⊢ ( 1 − 0 ) = 1
20 18 19 eqtrdi ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑆 ) = 1 )
21 16 20 eqtr2d ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 1 = ( 1 · ( 1 − 𝑆 ) ) )
22 4 recnd ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℂ )
23 22 mul02d ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 0 · 𝑇 ) = 0 )
24 oveq2 ⊢ ( 𝑆 = 0 → ( 1 · 𝑆 ) = ( 1 · 0 ) )
25 24 adantr ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 · 𝑆 ) = ( 1 · 0 ) )
26 ax-1cn ⊢ 1 ∈ ℂ
27 26 mul01i ⊢ ( 1 · 0 ) = 0
28 25 27 eqtrdi ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 · 𝑆 ) = 0 )
29 23 28 eqtr4d ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 0 · 𝑇 ) = ( 1 · 𝑆 ) )
30 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
31 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
32 oveq2 ⊢ ( 𝑟 = 1 → ( 1 − 𝑟 ) = ( 1 − 1 ) )
33 1m1e0 ⊢ ( 1 − 1 ) = 0
34 32 33 eqtrdi ⊢ ( 𝑟 = 1 → ( 1 − 𝑟 ) = 0 )
35 34 oveq1d ⊢ ( 𝑟 = 1 → ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) = ( 0 · ( 1 − 𝑇 ) ) )
36 35 eqeq2d ⊢ ( 𝑟 = 1 → ( 𝑝 = ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) ↔ 𝑝 = ( 0 · ( 1 − 𝑇 ) ) ) )
37 eqeq1 ⊢ ( 𝑟 = 1 → ( 𝑟 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ↔ 1 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ) )
38 34 oveq1d ⊢ ( 𝑟 = 1 → ( ( 1 − 𝑟 ) · 𝑇 ) = ( 0 · 𝑇 ) )
39 38 eqeq1d ⊢ ( 𝑟 = 1 → ( ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ↔ ( 0 · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) )
40 36 37 39 3anbi123d ⊢ ( 𝑟 = 1 → ( ( 𝑝 = ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) ∧ 𝑟 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) ↔ ( 𝑝 = ( 0 · ( 1 − 𝑇 ) ) ∧ 1 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( 0 · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) ) )
41 eqeq1 ⊢ ( 𝑝 = 0 → ( 𝑝 = ( 0 · ( 1 − 𝑇 ) ) ↔ 0 = ( 0 · ( 1 − 𝑇 ) ) ) )
42 oveq2 ⊢ ( 𝑝 = 0 → ( 1 − 𝑝 ) = ( 1 − 0 ) )
43 42 19 eqtrdi ⊢ ( 𝑝 = 0 → ( 1 − 𝑝 ) = 1 )
44 43 oveq1d ⊢ ( 𝑝 = 0 → ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) = ( 1 · ( 1 − 𝑆 ) ) )
45 44 eqeq2d ⊢ ( 𝑝 = 0 → ( 1 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ↔ 1 = ( 1 · ( 1 − 𝑆 ) ) ) )
46 43 oveq1d ⊢ ( 𝑝 = 0 → ( ( 1 − 𝑝 ) · 𝑆 ) = ( 1 · 𝑆 ) )
47 46 eqeq2d ⊢ ( 𝑝 = 0 → ( ( 0 · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ↔ ( 0 · 𝑇 ) = ( 1 · 𝑆 ) ) )
48 41 45 47 3anbi123d ⊢ ( 𝑝 = 0 → ( ( 𝑝 = ( 0 · ( 1 − 𝑇 ) ) ∧ 1 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( 0 · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) ↔ ( 0 = ( 0 · ( 1 − 𝑇 ) ) ∧ 1 = ( 1 · ( 1 − 𝑆 ) ) ∧ ( 0 · 𝑇 ) = ( 1 · 𝑆 ) ) ) )
49 40 48 rspc2ev ⊢ ( ( 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 ⊢ ( ( 0 = ( 0 · ( 1 − 𝑇 ) ) ∧ 1 = ( 1 · ( 1 − 𝑆 ) ) ∧ ( 0 · 𝑇 ) = ( 1 · 𝑆 ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑝 ∈ ( 0 [,] 1 ) ( 𝑝 = ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) ∧ 𝑟 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) )
51 9 21 29 50 syl3anc ⊢ ( ( 𝑆 = 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑝 ∈ ( 0 [,] 1 ) ( 𝑝 = ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) ∧ 𝑟 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) )
52 51 ex ⊢ ( 𝑆 = 0 → ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑝 ∈ ( 0 [,] 1 ) ( 𝑝 = ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) ∧ 𝑟 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) ) )
53 3 ad2antrl ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℝ )
54 11 ad2antll ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑆 ∈ ℝ )
55 54 53 remulcld ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · 𝑇 ) ∈ ℝ )
56 53 55 resubcld ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 − ( 𝑆 · 𝑇 ) ) ∈ ℝ )
57 54 53 readdcld ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 + 𝑇 ) ∈ ℝ )
58 57 55 resubcld ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ∈ ℝ )
59 1red ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 1 ∈ ℝ )
60 2 simp2bi ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 0 ≤ 𝑇 )
61 60 ad2antrl ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 0 ≤ 𝑇 )
62 10 simp3bi ⊢ ( 𝑆 ∈ ( 0 [,] 1 ) → 𝑆 ≤ 1 )
63 62 ad2antll ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑆 ≤ 1 )
64 54 59 53 61 63 lemul1ad ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · 𝑇 ) ≤ ( 1 · 𝑇 ) )
65 53 recnd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℂ )
66 65 mullidd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 · 𝑇 ) = 𝑇 )
67 64 66 breqtrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · 𝑇 ) ≤ 𝑇 )
68 10 simp2bi ⊢ ( 𝑆 ∈ ( 0 [,] 1 ) → 0 ≤ 𝑆 )
69 68 ad2antll ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 0 ≤ 𝑆 )
70 simpl ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑆 ≠ 0 )
71 54 69 70 ne0gt0d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 0 < 𝑆 )
72 54 53 ltaddpos2d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 0 < 𝑆 ↔ 𝑇 < ( 𝑆 + 𝑇 ) ) )
73 71 72 mpbid ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑇 < ( 𝑆 + 𝑇 ) )
74 55 53 57 67 73 lelttrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · 𝑇 ) < ( 𝑆 + 𝑇 ) )
75 55 57 posdifd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 · 𝑇 ) < ( 𝑆 + 𝑇 ) ↔ 0 < ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
76 74 75 mpbid ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 0 < ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) )
77 76 gt0ne0d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ≠ 0 )
78 56 58 77 redivcld ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∈ ℝ )
79 53 55 subge0d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 0 ≤ ( 𝑇 − ( 𝑆 · 𝑇 ) ) ↔ ( 𝑆 · 𝑇 ) ≤ 𝑇 ) )
80 67 79 mpbird ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 0 ≤ ( 𝑇 − ( 𝑆 · 𝑇 ) ) )
81 divge0 ⊢ ( ( ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑇 − ( 𝑆 · 𝑇 ) ) ) ∧ ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ∈ ℝ ∧ 0 < ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) → 0 ≤ ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
82 56 80 58 76 81 syl22anc ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 0 ≤ ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
83 53 57 73 ltled ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ≤ ( 𝑆 + 𝑇 ) )
84 53 57 55 83 lesub1dd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 − ( 𝑆 · 𝑇 ) ) ≤ ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) )
85 58 recnd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ∈ ℂ )
86 85 mullidd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 · ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) )
87 84 86 breqtrrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 − ( 𝑆 · 𝑇 ) ) ≤ ( 1 · ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
88 ledivmul2 ⊢ ( ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ∈ ℝ ∧ 0 < ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) → ( ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ≤ 1 ↔ ( 𝑇 − ( 𝑆 · 𝑇 ) ) ≤ ( 1 · ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
89 56 59 58 76 88 syl112anc ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ≤ 1 ↔ ( 𝑇 − ( 𝑆 · 𝑇 ) ) ≤ ( 1 · ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
90 87 89 mpbird ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ≤ 1 )
91 elicc01 ⊢ ( ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∈ ( 0 [,] 1 ) ↔ ( ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∧ ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ≤ 1 ) )
92 78 82 90 91 syl3anbrc ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∈ ( 0 [,] 1 ) )
93 54 55 resubcld ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 − ( 𝑆 · 𝑇 ) ) ∈ ℝ )
94 93 58 77 redivcld ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∈ ℝ )
95 2 simp3bi ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 𝑇 ≤ 1 )
96 95 ad2antrl ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ≤ 1 )
97 53 59 54 69 96 lemul2ad ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · 𝑇 ) ≤ ( 𝑆 · 1 ) )
98 54 recnd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑆 ∈ ℂ )
99 98 mulridd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · 1 ) = 𝑆 )
100 97 99 breqtrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · 𝑇 ) ≤ 𝑆 )
101 54 55 subge0d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 0 ≤ ( 𝑆 − ( 𝑆 · 𝑇 ) ) ↔ ( 𝑆 · 𝑇 ) ≤ 𝑆 ) )
102 100 101 mpbird ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 0 ≤ ( 𝑆 − ( 𝑆 · 𝑇 ) ) )
103 divge0 ⊢ ( ( ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑆 − ( 𝑆 · 𝑇 ) ) ) ∧ ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ∈ ℝ ∧ 0 < ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) → 0 ≤ ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
104 93 102 58 76 103 syl22anc ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 0 ≤ ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
105 54 53 addge01d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 0 ≤ 𝑇 ↔ 𝑆 ≤ ( 𝑆 + 𝑇 ) ) )
106 61 105 mpbid ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → 𝑆 ≤ ( 𝑆 + 𝑇 ) )
107 54 57 55 106 lesub1dd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 − ( 𝑆 · 𝑇 ) ) ≤ ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) )
108 107 86 breqtrrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 − ( 𝑆 · 𝑇 ) ) ≤ ( 1 · ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
109 ledivmul2 ⊢ ( ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ∈ ℝ ∧ 0 < ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) → ( ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ≤ 1 ↔ ( 𝑆 − ( 𝑆 · 𝑇 ) ) ≤ ( 1 · ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
110 93 59 58 76 109 syl112anc ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ≤ 1 ↔ ( 𝑆 − ( 𝑆 · 𝑇 ) ) ≤ ( 1 · ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
111 108 110 mpbird ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ≤ 1 )
112 elicc01 ⊢ ( ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∈ ( 0 [,] 1 ) ↔ ( ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∧ ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ≤ 1 ) )
113 94 104 111 112 syl3anbrc ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∈ ( 0 [,] 1 ) )
114 1 53 5 sylancr ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑇 ) ∈ ℝ )
115 114 recnd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑇 ) ∈ ℂ )
116 98 115 85 77 div23d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 · ( 1 − 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 𝑆 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) · ( 1 − 𝑇 ) ) )
117 subdi ⊢ ( ( 𝑆 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 𝑆 · ( 1 − 𝑇 ) ) = ( ( 𝑆 · 1 ) − ( 𝑆 · 𝑇 ) ) )
118 26 117 mp3an2 ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 𝑆 · ( 1 − 𝑇 ) ) = ( ( 𝑆 · 1 ) − ( 𝑆 · 𝑇 ) ) )
119 98 65 118 syl2anc ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · ( 1 − 𝑇 ) ) = ( ( 𝑆 · 1 ) − ( 𝑆 · 𝑇 ) ) )
120 99 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 · 1 ) − ( 𝑆 · 𝑇 ) ) = ( 𝑆 − ( 𝑆 · 𝑇 ) ) )
121 119 120 eqtrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · ( 1 − 𝑇 ) ) = ( 𝑆 − ( 𝑆 · 𝑇 ) ) )
122 121 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 · ( 1 − 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
123 56 recnd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 − ( 𝑆 · 𝑇 ) ) ∈ ℂ )
124 85 123 85 77 divsubdird ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) − ( 𝑇 − ( 𝑆 · 𝑇 ) ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
125 57 recnd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 + 𝑇 ) ∈ ℂ )
126 55 recnd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · 𝑇 ) ∈ ℂ )
127 125 65 126 nnncan2d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) − ( 𝑇 − ( 𝑆 · 𝑇 ) ) ) = ( ( 𝑆 + 𝑇 ) − 𝑇 ) )
128 98 65 pncand ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 + 𝑇 ) − 𝑇 ) = 𝑆 )
129 127 128 eqtrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) − ( 𝑇 − ( 𝑆 · 𝑇 ) ) ) = 𝑆 )
130 129 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) − ( 𝑇 − ( 𝑆 · 𝑇 ) ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( 𝑆 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
131 85 77 dividd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = 1 )
132 131 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) = ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
133 124 130 132 3eqtr3d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
134 133 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) · ( 1 − 𝑇 ) ) = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑇 ) ) )
135 116 122 134 3eqtr3d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑇 ) ) )
136 1 54 13 sylancr ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑆 ) ∈ ℝ )
137 136 recnd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑆 ) ∈ ℂ )
138 65 137 85 77 div23d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · ( 1 − 𝑆 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 𝑇 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) · ( 1 − 𝑆 ) ) )
139 subdi ⊢ ( ( 𝑇 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( 𝑇 · ( 1 − 𝑆 ) ) = ( ( 𝑇 · 1 ) − ( 𝑇 · 𝑆 ) ) )
140 26 139 mp3an2 ⊢ ( ( 𝑇 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( 𝑇 · ( 1 − 𝑆 ) ) = ( ( 𝑇 · 1 ) − ( 𝑇 · 𝑆 ) ) )
141 65 98 140 syl2anc ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 · ( 1 − 𝑆 ) ) = ( ( 𝑇 · 1 ) − ( 𝑇 · 𝑆 ) ) )
142 65 mulridd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 · 1 ) = 𝑇 )
143 65 98 mulcomd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 · 𝑆 ) = ( 𝑆 · 𝑇 ) )
144 142 143 oveq12d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 1 ) − ( 𝑇 · 𝑆 ) ) = ( 𝑇 − ( 𝑆 · 𝑇 ) ) )
145 141 144 eqtrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 · ( 1 − 𝑆 ) ) = ( 𝑇 − ( 𝑆 · 𝑇 ) ) )
146 145 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · ( 1 − 𝑆 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
147 93 recnd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 − ( 𝑆 · 𝑇 ) ) ∈ ℂ )
148 85 147 85 77 divsubdird ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) − ( 𝑆 − ( 𝑆 · 𝑇 ) ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
149 125 98 126 nnncan2d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) − ( 𝑆 − ( 𝑆 · 𝑇 ) ) ) = ( ( 𝑆 + 𝑇 ) − 𝑆 ) )
150 98 65 pncan2d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 + 𝑇 ) − 𝑆 ) = 𝑇 )
151 149 150 eqtrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) − ( 𝑆 − ( 𝑆 · 𝑇 ) ) ) = 𝑇 )
152 151 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) − ( 𝑆 − ( 𝑆 · 𝑇 ) ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( 𝑇 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
153 131 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) = ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
154 148 152 153 3eqtr3d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
155 154 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) · ( 1 − 𝑆 ) ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑆 ) ) )
156 138 146 155 3eqtr3d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑆 ) ) )
157 98 65 mulcomd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( 𝑆 · 𝑇 ) = ( 𝑇 · 𝑆 ) )
158 157 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 · 𝑇 ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 𝑇 · 𝑆 ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) )
159 98 65 85 77 div23d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 · 𝑇 ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 𝑆 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) · 𝑇 ) )
160 133 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) · 𝑇 ) = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑇 ) )
161 159 160 eqtrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑆 · 𝑇 ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑇 ) )
162 65 98 85 77 div23d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑆 ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 𝑇 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) · 𝑆 ) )
163 154 oveq1d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) · 𝑆 ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑆 ) )
164 162 163 eqtrd ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑆 ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑆 ) )
165 158 161 164 3eqtr3d ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑇 ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑆 ) )
166 oveq2 ⊢ ( 𝑟 = ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( 1 − 𝑟 ) = ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
167 166 oveq1d ⊢ ( 𝑟 = ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑇 ) ) )
168 167 eqeq2d ⊢ ( 𝑟 = ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( 𝑝 = ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) ↔ 𝑝 = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑇 ) ) ) )
169 eqeq1 ⊢ ( 𝑟 = ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( 𝑟 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ↔ ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ) )
170 166 oveq1d ⊢ ( 𝑟 = ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑇 ) )
171 170 eqeq1d ⊢ ( 𝑟 = ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ↔ ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) )
172 168 169 171 3anbi123d ⊢ ( 𝑟 = ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( ( 𝑝 = ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) ∧ 𝑟 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) ↔ ( 𝑝 = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑇 ) ) ∧ ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) ) )
173 eqeq1 ⊢ ( 𝑝 = ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( 𝑝 = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑇 ) ) ↔ ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑇 ) ) ) )
174 oveq2 ⊢ ( 𝑝 = ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( 1 − 𝑝 ) = ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) )
175 174 oveq1d ⊢ ( 𝑝 = ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑆 ) ) )
176 175 eqeq2d ⊢ ( 𝑝 = ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ↔ ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑆 ) ) ) )
177 174 oveq1d ⊢ ( 𝑝 = ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( ( 1 − 𝑝 ) · 𝑆 ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑆 ) )
178 177 eqeq2d ⊢ ( 𝑝 = ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ↔ ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑇 ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑆 ) ) )
179 173 176 178 3anbi123d ⊢ ( 𝑝 = ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) → ( ( 𝑝 = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑇 ) ) ∧ ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) ↔ ( ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑇 ) ) ∧ ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑇 ) = ( ( 1 − ( ( 𝑆 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ) · 𝑆 ) ) ) )
180 172 179 rspc2ev ⊢ ( ( ( ( 𝑇 − ( 𝑆 · 𝑇 ) ) / ( ( 𝑆 + 𝑇 ) − ( 𝑆 · 𝑇 ) ) ) ∈ ( 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 ⊢ ( ( 𝑆 ≠ 0 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑝 ∈ ( 0 [,] 1 ) ( 𝑝 = ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) ∧ 𝑟 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) )
182 181 ex ⊢ ( 𝑆 ≠ 0 → ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑝 ∈ ( 0 [,] 1 ) ( 𝑝 = ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) ∧ 𝑟 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) ) )
183 52 182 pm2.61ine ⊢ ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑝 ∈ ( 0 [,] 1 ) ( 𝑝 = ( ( 1 − 𝑟 ) · ( 1 − 𝑇 ) ) ∧ 𝑟 = ( ( 1 − 𝑝 ) · ( 1 − 𝑆 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑇 ) = ( ( 1 − 𝑝 ) · 𝑆 ) ) )