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

Theorem axsegconlem10 27938
Description: Lemma for axsegcon 27939. Show that the scaling constant from axsegconlem7 27935 produces the betweenness condition for ๐ด, ๐ต and ๐น. (Contributed by Scott Fenton, 21-Sep-2013.)
Hypotheses
Ref Expression
axsegconlem2.1 ๐‘† = ฮฃ๐‘ โˆˆ (1...๐‘)(((๐ดโ€˜๐‘) โˆ’ (๐ตโ€˜๐‘))โ†‘2)
axsegconlem7.2 ๐‘‡ = ฮฃ๐‘ โˆˆ (1...๐‘)(((๐ถโ€˜๐‘) โˆ’ (๐ทโ€˜๐‘))โ†‘2)
axsegconlem8.3 ๐น = (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘˜)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘˜))) / (โˆšโ€˜๐‘†)))
Assertion
Ref Expression
axsegconlem10 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((1 โˆ’ ((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))) ยท (๐ดโ€˜๐‘–)) + (((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) ยท (๐นโ€˜๐‘–))))
Distinct variable groups:   ๐ด,๐‘   ๐ต,๐‘   ๐ถ,๐‘   ๐ท,๐‘   ๐‘,๐‘   ๐ด,๐‘–,๐‘˜   ๐ต,๐‘–,๐‘˜   ๐ถ,๐‘–,๐‘˜   ๐ท,๐‘–,๐‘˜   ๐‘–,๐‘,๐‘˜   ๐‘†,๐‘–,๐‘˜   ๐‘‡,๐‘–,๐‘˜   ๐‘–,๐‘
Allowed substitution hints:   ๐‘†(๐‘)   ๐‘‡(๐‘)   ๐น(๐‘–,๐‘˜,๐‘)

Proof of Theorem axsegconlem10
StepHypRef Expression
1 axsegconlem7.2 . . . . . . . 8 ๐‘‡ = ฮฃ๐‘ โˆˆ (1...๐‘)(((๐ถโ€˜๐‘) โˆ’ (๐ทโ€˜๐‘))โ†‘2)
21axsegconlem4 27932 . . . . . . 7 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆšโ€˜๐‘‡) โˆˆ โ„)
32ad2antlr 725 . . . . . 6 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (โˆšโ€˜๐‘‡) โˆˆ โ„)
4 simpl1 1191 . . . . . . 7 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ ๐ด โˆˆ (๐”ผโ€˜๐‘))
5 fveere 27913 . . . . . . 7 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„)
64, 5sylan 580 . . . . . 6 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„)
73, 6remulcld 11194 . . . . 5 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) โˆˆ โ„)
87recnd 11192 . . . 4 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) โˆˆ โ„‚)
9 axsegconlem2.1 . . . . . . . . 9 ๐‘† = ฮฃ๐‘ โˆˆ (1...๐‘)(((๐ดโ€˜๐‘) โˆ’ (๐ตโ€˜๐‘))โ†‘2)
109axsegconlem4 27932 . . . . . . . 8 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆšโ€˜๐‘†) โˆˆ โ„)
11103adant3 1132 . . . . . . 7 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โ†’ (โˆšโ€˜๐‘†) โˆˆ โ„)
1211ad2antrr 724 . . . . . 6 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (โˆšโ€˜๐‘†) โˆˆ โ„)
13 axsegconlem8.3 . . . . . . . 8 ๐น = (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘˜)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘˜))) / (โˆšโ€˜๐‘†)))
149, 1, 13axsegconlem8 27936 . . . . . . 7 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ ๐น โˆˆ (๐”ผโ€˜๐‘))
15 fveere 27913 . . . . . . 7 ((๐น โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐นโ€˜๐‘–) โˆˆ โ„)
1614, 15sylan 580 . . . . . 6 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐นโ€˜๐‘–) โˆˆ โ„)
1712, 16remulcld 11194 . . . . 5 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–)) โˆˆ โ„)
1817recnd 11192 . . . 4 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–)) โˆˆ โ„‚)
19 readdcl 11143 . . . . . . 7 (((โˆšโ€˜๐‘†) โˆˆ โ„ โˆง (โˆšโ€˜๐‘‡) โˆˆ โ„) โ†’ ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โˆˆ โ„)
2011, 2, 19syl2an 596 . . . . . 6 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โˆˆ โ„)
2120adantr 481 . . . . 5 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โˆˆ โ„)
2221recnd 11192 . . . 4 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โˆˆ โ„‚)
23 0red 11167 . . . . . . 7 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ 0 โˆˆ โ„)
2411adantr 481 . . . . . . 7 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ (โˆšโ€˜๐‘†) โˆˆ โ„)
259axsegconlem6 27934 . . . . . . . 8 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โ†’ 0 < (โˆšโ€˜๐‘†))
2625adantr 481 . . . . . . 7 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ 0 < (โˆšโ€˜๐‘†))
271axsegconlem5 27933 . . . . . . . . 9 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘)) โ†’ 0 โ‰ค (โˆšโ€˜๐‘‡))
2827adantl 482 . . . . . . . 8 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ 0 โ‰ค (โˆšโ€˜๐‘‡))
29 addge01 11674 . . . . . . . . 9 (((โˆšโ€˜๐‘†) โˆˆ โ„ โˆง (โˆšโ€˜๐‘‡) โˆˆ โ„) โ†’ (0 โ‰ค (โˆšโ€˜๐‘‡) โ†” (โˆšโ€˜๐‘†) โ‰ค ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))))
3011, 2, 29syl2an 596 . . . . . . . 8 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ (0 โ‰ค (โˆšโ€˜๐‘‡) โ†” (โˆšโ€˜๐‘†) โ‰ค ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))))
3128, 30mpbid 231 . . . . . . 7 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ (โˆšโ€˜๐‘†) โ‰ค ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))
3223, 24, 20, 26, 31ltletrd 11324 . . . . . 6 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ 0 < ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))
3332gt0ne0d 11728 . . . . 5 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โ‰  0)
3433adantr 481 . . . 4 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โ‰  0)
358, 18, 22, 34divdird 11978 . . 3 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) + ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–))) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) = ((((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) + (((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))))
36 fveq2 6847 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘– โ†’ (๐ตโ€˜๐‘˜) = (๐ตโ€˜๐‘–))
3736oveq2d 7378 . . . . . . . . . . . 12 (๐‘˜ = ๐‘– โ†’ (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘˜)) = (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)))
38 fveq2 6847 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘– โ†’ (๐ดโ€˜๐‘˜) = (๐ดโ€˜๐‘–))
3938oveq2d 7378 . . . . . . . . . . . 12 (๐‘˜ = ๐‘– โ†’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘˜)) = ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)))
4037, 39oveq12d 7380 . . . . . . . . . . 11 (๐‘˜ = ๐‘– โ†’ ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘˜)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘˜))) = ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))))
4140oveq1d 7377 . . . . . . . . . 10 (๐‘˜ = ๐‘– โ†’ (((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘˜)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘˜))) / (โˆšโ€˜๐‘†)) = (((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))) / (โˆšโ€˜๐‘†)))
42 ovex 7395 . . . . . . . . . 10 (((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))) / (โˆšโ€˜๐‘†)) โˆˆ V
4341, 13, 42fvmpt 6953 . . . . . . . . 9 (๐‘– โˆˆ (1...๐‘) โ†’ (๐นโ€˜๐‘–) = (((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))) / (โˆšโ€˜๐‘†)))
4443adantl 482 . . . . . . . 8 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐นโ€˜๐‘–) = (((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))) / (โˆšโ€˜๐‘†)))
4544oveq2d 7378 . . . . . . 7 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–)) = ((โˆšโ€˜๐‘†) ยท (((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))) / (โˆšโ€˜๐‘†))))
46 simpl2 1192 . . . . . . . . . . . 12 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ ๐ต โˆˆ (๐”ผโ€˜๐‘))
47 fveere 27913 . . . . . . . . . . . 12 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
4846, 47sylan 580 . . . . . . . . . . 11 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„)
4921, 48remulcld 11194 . . . . . . . . . 10 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆˆ โ„)
5049, 7resubcld 11592 . . . . . . . . 9 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))) โˆˆ โ„)
5150recnd 11192 . . . . . . . 8 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))) โˆˆ โ„‚)
5212recnd 11192 . . . . . . . 8 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (โˆšโ€˜๐‘†) โˆˆ โ„‚)
5325gt0ne0d 11728 . . . . . . . . 9 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โ†’ (โˆšโ€˜๐‘†) โ‰  0)
5453ad2antrr 724 . . . . . . . 8 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (โˆšโ€˜๐‘†) โ‰  0)
5551, 52, 54divcan2d 11942 . . . . . . 7 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘†) ยท (((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))) / (โˆšโ€˜๐‘†))) = ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))))
5645, 55eqtrd 2771 . . . . . 6 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–)) = ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–))))
5756oveq2d 7378 . . . . 5 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) + ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–))) = (((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) + ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)))))
5849recnd 11192 . . . . . 6 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆˆ โ„‚)
598, 58pncan3d 11524 . . . . 5 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) + ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)) โˆ’ ((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)))) = (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)))
6057, 59eqtrd 2771 . . . 4 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) + ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–))) = (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–)))
617, 17readdcld 11193 . . . . . 6 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) + ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–))) โˆˆ โ„)
6261recnd 11192 . . . . 5 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) + ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–))) โˆˆ โ„‚)
6348recnd 11192 . . . . 5 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
6462, 63, 22, 34divmul2d 11973 . . . 4 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) + ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–))) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) = (๐ตโ€˜๐‘–) โ†” (((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) + ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–))) = (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) ยท (๐ตโ€˜๐‘–))))
6560, 64mpbird 256 . . 3 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) + ((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–))) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) = (๐ตโ€˜๐‘–))
662recnd 11192 . . . . . . 7 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆšโ€˜๐‘‡) โˆˆ โ„‚)
6766ad2antlr 725 . . . . . 6 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (โˆšโ€˜๐‘‡) โˆˆ โ„‚)
686recnd 11192 . . . . . 6 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
6967, 68, 22, 34div23d 11977 . . . . 5 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) = (((โˆšโ€˜๐‘‡) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) ยท (๐ดโ€˜๐‘–)))
7022, 52, 22, 34divsubdird 11979 . . . . . . 7 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โˆ’ (โˆšโ€˜๐‘†)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) = ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) โˆ’ ((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))))
7111recnd 11192 . . . . . . . . . 10 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โ†’ (โˆšโ€˜๐‘†) โˆˆ โ„‚)
72 pncan2 11417 . . . . . . . . . 10 (((โˆšโ€˜๐‘†) โˆˆ โ„‚ โˆง (โˆšโ€˜๐‘‡) โˆˆ โ„‚) โ†’ (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โˆ’ (โˆšโ€˜๐‘†)) = (โˆšโ€˜๐‘‡))
7371, 66, 72syl2an 596 . . . . . . . . 9 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โˆ’ (โˆšโ€˜๐‘†)) = (โˆšโ€˜๐‘‡))
7473adantr 481 . . . . . . . 8 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โˆ’ (โˆšโ€˜๐‘†)) = (โˆšโ€˜๐‘‡))
7574oveq1d 7377 . . . . . . 7 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) โˆ’ (โˆšโ€˜๐‘†)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) = ((โˆšโ€˜๐‘‡) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))))
7622, 34dividd 11938 . . . . . . . 8 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) = 1)
7776oveq1d 7377 . . . . . . 7 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) โˆ’ ((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))) = (1 โˆ’ ((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))))
7870, 75, 773eqtr3d 2779 . . . . . 6 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((โˆšโ€˜๐‘‡) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) = (1 โˆ’ ((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))))
7978oveq1d 7377 . . . . 5 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘‡) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) ยท (๐ดโ€˜๐‘–)) = ((1 โˆ’ ((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))) ยท (๐ดโ€˜๐‘–)))
8069, 79eqtrd 2771 . . . 4 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) = ((1 โˆ’ ((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))) ยท (๐ดโ€˜๐‘–)))
8116recnd 11192 . . . . 5 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐นโ€˜๐‘–) โˆˆ โ„‚)
8252, 81, 22, 34div23d 11977 . . . 4 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) = (((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) ยท (๐นโ€˜๐‘–)))
8380, 82oveq12d 7380 . . 3 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((โˆšโ€˜๐‘‡) ยท (๐ดโ€˜๐‘–)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) + (((โˆšโ€˜๐‘†) ยท (๐นโ€˜๐‘–)) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))) = (((1 โˆ’ ((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))) ยท (๐ดโ€˜๐‘–)) + (((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) ยท (๐นโ€˜๐‘–))))
8435, 65, 833eqtr3d 2779 . 2 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) = (((1 โˆ’ ((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))) ยท (๐ดโ€˜๐‘–)) + (((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) ยท (๐นโ€˜๐‘–))))
8584ralrimiva 3139 1 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โ‰  ๐ต) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ท โˆˆ (๐”ผโ€˜๐‘))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((1 โˆ’ ((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡)))) ยท (๐ดโ€˜๐‘–)) + (((โˆšโ€˜๐‘†) / ((โˆšโ€˜๐‘†) + (โˆšโ€˜๐‘‡))) ยท (๐นโ€˜๐‘–))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2939  โˆ€wral 3060   class class class wbr 5110   โ†ฆ cmpt 5193  โ€˜cfv 6501  (class class class)co 7362  โ„‚cc 11058  โ„cr 11059  0cc0 11060  1c1 11061   + caddc 11063   ยท cmul 11065   < clt 11198   โ‰ค cle 11199   โˆ’ cmin 11394   / cdiv 11821  2c2 12217  ...cfz 13434  โ†‘cexp 13977  โˆšcsqrt 15130  ฮฃcsu 15582  ๐”ผcee 27900
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 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9586  ax-cnex 11116  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136  ax-pre-mulgt0 11137  ax-pre-sup 11138
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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9387  df-oi 9455  df-card 9884  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-sub 11396  df-neg 11397  df-div 11822  df-nn 12163  df-2 12225  df-3 12226  df-n0 12423  df-z 12509  df-uz 12773  df-rp 12925  df-ico 13280  df-fz 13435  df-fzo 13578  df-seq 13917  df-exp 13978  df-hash 14241  df-cj 14996  df-re 14997  df-im 14998  df-sqrt 15132  df-abs 15133  df-clim 15382  df-sum 15583  df-ee 27903
This theorem is referenced by:  axsegcon  27939
  Copyright terms: Public domain W3C validator