Metamath Proof Explorer

Theorem axpaschlem

Description: Lemma for axpasch . Set up coefficents 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 โˆ’ ๐‘ ) ยท ๐‘† ) ) )