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

Theorem axcontlem2 28658
Description: Lemma for axcont 28669. The idea here is to set up a mapping ๐น that will allow to transfer dedekind 11373 to two sets of points. Here, we set up ๐น and show its domain and codomain. (Contributed by Scott Fenton, 17-Jun-2013.)
Hypotheses
Ref Expression
axcontlem2.1 ๐ท = {๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆฃ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)}
axcontlem2.2 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
Assertion
Ref Expression
axcontlem2 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž))
Distinct variable groups:   ๐‘,๐‘,๐‘ฅ,๐‘ก,๐‘–   ๐‘ˆ,๐‘,๐‘ฅ,๐‘ก,๐‘–   ๐‘,๐‘,๐‘ฅ,๐‘ก,๐‘–   ๐‘ฅ,๐ท,๐‘ก
Allowed substitution hints:   ๐ท(๐‘–,๐‘)   ๐น(๐‘ฅ,๐‘ก,๐‘–,๐‘)

Proof of Theorem axcontlem2
Dummy variables ๐‘˜ ๐‘ฆ ๐‘  are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq2 4866 . . . . . . . . . 10 (๐‘ = ๐‘ฅ โ†’ โŸจ๐‘, ๐‘โŸฉ = โŸจ๐‘, ๐‘ฅโŸฉ)
21breq2d 5150 . . . . . . . . 9 (๐‘ = ๐‘ฅ โ†’ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โ†” ๐‘ˆ Btwn โŸจ๐‘, ๐‘ฅโŸฉ))
3 breq1 5141 . . . . . . . . 9 (๐‘ = ๐‘ฅ โ†’ (๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ โ†” ๐‘ฅ Btwn โŸจ๐‘, ๐‘ˆโŸฉ))
42, 3orbi12d 915 . . . . . . . 8 (๐‘ = ๐‘ฅ โ†’ ((๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ) โ†” (๐‘ˆ Btwn โŸจ๐‘, ๐‘ฅโŸฉ โˆจ ๐‘ฅ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)))
5 axcontlem2.1 . . . . . . . 8 ๐ท = {๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆฃ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)}
64, 5elrab2 3678 . . . . . . 7 (๐‘ฅ โˆˆ ๐ท โ†” (๐‘ฅ โˆˆ (๐”ผโ€˜๐‘) โˆง (๐‘ˆ Btwn โŸจ๐‘, ๐‘ฅโŸฉ โˆจ ๐‘ฅ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)))
7 simpll3 1211 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
8 simpll2 1210 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
9 simpr 484 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘))
10 brbtwn 28592 . . . . . . . . . . . 12 ((๐‘ˆ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ˆ Btwn โŸจ๐‘, ๐‘ฅโŸฉ โ†” โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))
117, 8, 9, 10syl3anc 1368 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ˆ Btwn โŸจ๐‘, ๐‘ฅโŸฉ โ†” โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))
1211biimpa 476 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ˆ Btwn โŸจ๐‘, ๐‘ฅโŸฉ) โ†’ โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))
13 simp-4r 781 . . . . . . . . . . . . 13 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) โ†’ ๐‘ โ‰  ๐‘ˆ)
14 oveq2 7409 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘  = 0 โ†’ (1 โˆ’ ๐‘ ) = (1 โˆ’ 0))
15 1m0e1 12329 . . . . . . . . . . . . . . . . . . . . . 22 (1 โˆ’ 0) = 1
1614, 15eqtrdi 2780 . . . . . . . . . . . . . . . . . . . . 21 (๐‘  = 0 โ†’ (1 โˆ’ ๐‘ ) = 1)
1716oveq1d 7416 . . . . . . . . . . . . . . . . . . . 20 (๐‘  = 0 โ†’ ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) = (1 ยท (๐‘โ€˜๐‘–)))
18 oveq1 7408 . . . . . . . . . . . . . . . . . . . 20 (๐‘  = 0 โ†’ (๐‘  ยท (๐‘ฅโ€˜๐‘–)) = (0 ยท (๐‘ฅโ€˜๐‘–)))
1917, 18oveq12d 7419 . . . . . . . . . . . . . . . . . . 19 (๐‘  = 0 โ†’ (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) = ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–))))
2019eqeq2d 2735 . . . . . . . . . . . . . . . . . 18 (๐‘  = 0 โ†’ ((๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โ†” (๐‘ˆโ€˜๐‘–) = ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–)))))
2120ralbidv 3169 . . . . . . . . . . . . . . . . 17 (๐‘  = 0 โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–)))))
2221biimpac 478 . . . . . . . . . . . . . . . 16 ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โˆง ๐‘  = 0) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–))))
23 eqcom 2731 . . . . . . . . . . . . . . . . 17 (๐‘ = ๐‘ˆ โ†” ๐‘ˆ = ๐‘)
247adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
258adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
26 eqeefv 28596 . . . . . . . . . . . . . . . . . . 19 ((๐‘ˆ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ˆ = ๐‘ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (๐‘โ€˜๐‘–)))
2724, 25, 26syl2anc 583 . . . . . . . . . . . . . . . . . 18 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โ†’ (๐‘ˆ = ๐‘ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (๐‘โ€˜๐‘–)))
288ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
29 fveecn 28595 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
3028, 29sylancom 587 . . . . . . . . . . . . . . . . . . . 20 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
31 fveecn 28595 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ฅโ€˜๐‘–) โˆˆ โ„‚)
3231ad4ant24 751 . . . . . . . . . . . . . . . . . . . 20 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ฅโ€˜๐‘–) โˆˆ โ„‚)
33 mullid 11209 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โ†’ (1 ยท (๐‘โ€˜๐‘–)) = (๐‘โ€˜๐‘–))
34 mul02 11388 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โ†’ (0 ยท (๐‘ฅโ€˜๐‘–)) = 0)
3533, 34oveqan12d 7420 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ฅโ€˜๐‘–) โˆˆ โ„‚) โ†’ ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–))) = ((๐‘โ€˜๐‘–) + 0))
36 addrid 11390 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โ†’ ((๐‘โ€˜๐‘–) + 0) = (๐‘โ€˜๐‘–))
3736adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ฅโ€˜๐‘–) โˆˆ โ„‚) โ†’ ((๐‘โ€˜๐‘–) + 0) = (๐‘โ€˜๐‘–))
3835, 37eqtrd 2764 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ฅโ€˜๐‘–) โˆˆ โ„‚) โ†’ ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–))) = (๐‘โ€˜๐‘–))
3938eqeq2d 2735 . . . . . . . . . . . . . . . . . . . 20 (((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ฅโ€˜๐‘–) โˆˆ โ„‚) โ†’ ((๐‘ˆโ€˜๐‘–) = ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–))) โ†” (๐‘ˆโ€˜๐‘–) = (๐‘โ€˜๐‘–)))
4030, 32, 39syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐‘ˆโ€˜๐‘–) = ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–))) โ†” (๐‘ˆโ€˜๐‘–) = (๐‘โ€˜๐‘–)))
4140ralbidva 3167 . . . . . . . . . . . . . . . . . 18 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (๐‘โ€˜๐‘–)))
4227, 41bitr4d 282 . . . . . . . . . . . . . . . . 17 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โ†’ (๐‘ˆ = ๐‘ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–)))))
4323, 42bitrid 283 . . . . . . . . . . . . . . . 16 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = ((1 ยท (๐‘โ€˜๐‘–)) + (0 ยท (๐‘ฅโ€˜๐‘–)))))
4422, 43imbitrrid 245 . . . . . . . . . . . . . . 15 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โ†’ ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โˆง ๐‘  = 0) โ†’ ๐‘ = ๐‘ˆ))
4544expdimp 452 . . . . . . . . . . . . . 14 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) โ†’ (๐‘  = 0 โ†’ ๐‘ = ๐‘ˆ))
4645necon3d 2953 . . . . . . . . . . . . 13 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) โ†’ (๐‘ โ‰  ๐‘ˆ โ†’ ๐‘  โ‰  0))
4713, 46mpd 15 . . . . . . . . . . . 12 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) โ†’ ๐‘  โ‰  0)
48 elicc01 13439 . . . . . . . . . . . . . . . . . . 19 (๐‘  โˆˆ (0[,]1) โ†” (๐‘  โˆˆ โ„ โˆง 0 โ‰ค ๐‘  โˆง ๐‘  โ‰ค 1))
4948simp1bi 1142 . . . . . . . . . . . . . . . . . 18 (๐‘  โˆˆ (0[,]1) โ†’ ๐‘  โˆˆ โ„)
50 rereccl 11928 . . . . . . . . . . . . . . . . . 18 ((๐‘  โˆˆ โ„ โˆง ๐‘  โ‰  0) โ†’ (1 / ๐‘ ) โˆˆ โ„)
5149, 50sylan 579 . . . . . . . . . . . . . . . . 17 ((๐‘  โˆˆ (0[,]1) โˆง ๐‘  โ‰  0) โ†’ (1 / ๐‘ ) โˆˆ โ„)
5249adantr 480 . . . . . . . . . . . . . . . . . 18 ((๐‘  โˆˆ (0[,]1) โˆง ๐‘  โ‰  0) โ†’ ๐‘  โˆˆ โ„)
5348simp2bi 1143 . . . . . . . . . . . . . . . . . . . 20 (๐‘  โˆˆ (0[,]1) โ†’ 0 โ‰ค ๐‘ )
5453adantr 480 . . . . . . . . . . . . . . . . . . 19 ((๐‘  โˆˆ (0[,]1) โˆง ๐‘  โ‰  0) โ†’ 0 โ‰ค ๐‘ )
55 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((๐‘  โˆˆ (0[,]1) โˆง ๐‘  โ‰  0) โ†’ ๐‘  โ‰  0)
5652, 54, 55ne0gt0d 11347 . . . . . . . . . . . . . . . . . 18 ((๐‘  โˆˆ (0[,]1) โˆง ๐‘  โ‰  0) โ†’ 0 < ๐‘ )
57 1re 11210 . . . . . . . . . . . . . . . . . . 19 1 โˆˆ โ„
58 0le1 11733 . . . . . . . . . . . . . . . . . . 19 0 โ‰ค 1
59 divge0 12079 . . . . . . . . . . . . . . . . . . 19 (((1 โˆˆ โ„ โˆง 0 โ‰ค 1) โˆง (๐‘  โˆˆ โ„ โˆง 0 < ๐‘ )) โ†’ 0 โ‰ค (1 / ๐‘ ))
6057, 58, 59mpanl12 699 . . . . . . . . . . . . . . . . . 18 ((๐‘  โˆˆ โ„ โˆง 0 < ๐‘ ) โ†’ 0 โ‰ค (1 / ๐‘ ))
6152, 56, 60syl2anc 583 . . . . . . . . . . . . . . . . 17 ((๐‘  โˆˆ (0[,]1) โˆง ๐‘  โ‰  0) โ†’ 0 โ‰ค (1 / ๐‘ ))
62 elrege0 13427 . . . . . . . . . . . . . . . . 17 ((1 / ๐‘ ) โˆˆ (0[,)+โˆž) โ†” ((1 / ๐‘ ) โˆˆ โ„ โˆง 0 โ‰ค (1 / ๐‘ )))
6351, 61, 62sylanbrc 582 . . . . . . . . . . . . . . . 16 ((๐‘  โˆˆ (0[,]1) โˆง ๐‘  โ‰  0) โ†’ (1 / ๐‘ ) โˆˆ (0[,)+โˆž))
6463adantll 711 . . . . . . . . . . . . . . 15 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โ†’ (1 / ๐‘ ) โˆˆ (0[,)+โˆž))
6549ad3antlr 728 . . . . . . . . . . . . . . . . . 18 (((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘  โˆˆ โ„)
6665recnd 11238 . . . . . . . . . . . . . . . . 17 (((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘  โˆˆ โ„‚)
67 simplr 766 . . . . . . . . . . . . . . . . 17 (((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘  โ‰  0)
6831ad5ant25 759 . . . . . . . . . . . . . . . . 17 (((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ฅโ€˜๐‘–) โˆˆ โ„‚)
698ad3antrrr 727 . . . . . . . . . . . . . . . . . 18 (((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
7069, 29sylancom 587 . . . . . . . . . . . . . . . . 17 (((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
71 ax-1cn 11163 . . . . . . . . . . . . . . . . . . . . . . . 24 1 โˆˆ โ„‚
72 reccl 11875 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ (1 / ๐‘ ) โˆˆ โ„‚)
73 subcl 11455 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 โˆˆ โ„‚ โˆง (1 / ๐‘ ) โˆˆ โ„‚) โ†’ (1 โˆ’ (1 / ๐‘ )) โˆˆ โ„‚)
7471, 72, 73sylancr 586 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ (1 โˆ’ (1 / ๐‘ )) โˆˆ โ„‚)
7574adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (1 โˆ’ (1 / ๐‘ )) โˆˆ โ„‚)
76 subcl 11455 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โ†’ (1 โˆ’ ๐‘ ) โˆˆ โ„‚)
7771, 76mpan 687 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘  โˆˆ โ„‚ โ†’ (1 โˆ’ ๐‘ ) โˆˆ โ„‚)
7877adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ (1 โˆ’ ๐‘ ) โˆˆ โ„‚)
7972, 78mulcld 11230 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ )) โˆˆ โ„‚)
8079adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ )) โˆˆ โ„‚)
81 simprr 770 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
8275, 80, 81adddird 11235 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ )) + ((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ ))) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + (((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ )) ยท (๐‘โ€˜๐‘–))))
83 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ๐‘  โˆˆ โ„‚)
84 subdi 11643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 / ๐‘ ) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โ†’ ((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ )) = (((1 / ๐‘ ) ยท 1) โˆ’ ((1 / ๐‘ ) ยท ๐‘ )))
8571, 84mp3an2 1445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 / ๐‘ ) โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โ†’ ((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ )) = (((1 / ๐‘ ) ยท 1) โˆ’ ((1 / ๐‘ ) ยท ๐‘ )))
8672, 83, 85syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ )) = (((1 / ๐‘ ) ยท 1) โˆ’ ((1 / ๐‘ ) ยท ๐‘ )))
8786oveq2d 7417 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ((1 โˆ’ (1 / ๐‘ )) + ((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ ))) = ((1 โˆ’ (1 / ๐‘ )) + (((1 / ๐‘ ) ยท 1) โˆ’ ((1 / ๐‘ ) ยท ๐‘ ))))
8872mulridd 11227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ((1 / ๐‘ ) ยท 1) = (1 / ๐‘ ))
89 recid2 11883 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ((1 / ๐‘ ) ยท ๐‘ ) = 1)
9088, 89oveq12d 7419 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ (((1 / ๐‘ ) ยท 1) โˆ’ ((1 / ๐‘ ) ยท ๐‘ )) = ((1 / ๐‘ ) โˆ’ 1))
9190oveq2d 7417 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ((1 โˆ’ (1 / ๐‘ )) + (((1 / ๐‘ ) ยท 1) โˆ’ ((1 / ๐‘ ) ยท ๐‘ ))) = ((1 โˆ’ (1 / ๐‘ )) + ((1 / ๐‘ ) โˆ’ 1)))
92 addsubass 11466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 โˆ’ (1 / ๐‘ )) โˆˆ โ„‚ โˆง (1 / ๐‘ ) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ (((1 โˆ’ (1 / ๐‘ )) + (1 / ๐‘ )) โˆ’ 1) = ((1 โˆ’ (1 / ๐‘ )) + ((1 / ๐‘ ) โˆ’ 1)))
9371, 92mp3an3 1446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 โˆ’ (1 / ๐‘ )) โˆˆ โ„‚ โˆง (1 / ๐‘ ) โˆˆ โ„‚) โ†’ (((1 โˆ’ (1 / ๐‘ )) + (1 / ๐‘ )) โˆ’ 1) = ((1 โˆ’ (1 / ๐‘ )) + ((1 / ๐‘ ) โˆ’ 1)))
9474, 72, 93syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ (((1 โˆ’ (1 / ๐‘ )) + (1 / ๐‘ )) โˆ’ 1) = ((1 โˆ’ (1 / ๐‘ )) + ((1 / ๐‘ ) โˆ’ 1)))
9574, 72addcld 11229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ((1 โˆ’ (1 / ๐‘ )) + (1 / ๐‘ )) โˆˆ โ„‚)
96 npcan 11465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 โˆˆ โ„‚ โˆง (1 / ๐‘ ) โˆˆ โ„‚) โ†’ ((1 โˆ’ (1 / ๐‘ )) + (1 / ๐‘ )) = 1)
9771, 72, 96sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ((1 โˆ’ (1 / ๐‘ )) + (1 / ๐‘ )) = 1)
9895, 97subeq0bd 11636 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ (((1 โˆ’ (1 / ๐‘ )) + (1 / ๐‘ )) โˆ’ 1) = 0)
9991, 94, 983eqtr2d 2770 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ((1 โˆ’ (1 / ๐‘ )) + (((1 / ๐‘ ) ยท 1) โˆ’ ((1 / ๐‘ ) ยท ๐‘ ))) = 0)
10087, 99eqtrd 2764 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ ((1 โˆ’ (1 / ๐‘ )) + ((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ ))) = 0)
101100adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (1 / ๐‘ )) + ((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ ))) = 0)
102101oveq1d 7416 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ )) + ((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ ))) ยท (๐‘โ€˜๐‘–)) = (0 ยท (๐‘โ€˜๐‘–)))
10372adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (1 / ๐‘ ) โˆˆ โ„‚)
10477ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (1 โˆ’ ๐‘ ) โˆˆ โ„‚)
105103, 104, 81mulassd 11233 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ )) ยท (๐‘โ€˜๐‘–)) = ((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–))))
106105oveq2d 7417 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + (((1 / ๐‘ ) ยท (1 โˆ’ ๐‘ )) ยท (๐‘โ€˜๐‘–))) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)))))
10782, 102, 1063eqtr3rd 2773 . . . . . . . . . . . . . . . . . . . 20 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)))) = (0 ยท (๐‘โ€˜๐‘–)))
108 mul02 11388 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โ†’ (0 ยท (๐‘โ€˜๐‘–)) = 0)
109108ad2antll 726 . . . . . . . . . . . . . . . . . . . 20 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (0 ยท (๐‘โ€˜๐‘–)) = 0)
110107, 109eqtrd 2764 . . . . . . . . . . . . . . . . . . 19 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)))) = 0)
111 simpll 764 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ๐‘  โˆˆ โ„‚)
112 simprl 768 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘ฅโ€˜๐‘–) โˆˆ โ„‚)
113103, 111, 112mulassd 11233 . . . . . . . . . . . . . . . . . . . 20 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 / ๐‘ ) ยท ๐‘ ) ยท (๐‘ฅโ€˜๐‘–)) = ((1 / ๐‘ ) ยท (๐‘  ยท (๐‘ฅโ€˜๐‘–))))
11489oveq1d 7416 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โ†’ (((1 / ๐‘ ) ยท ๐‘ ) ยท (๐‘ฅโ€˜๐‘–)) = (1 ยท (๐‘ฅโ€˜๐‘–)))
115 mullid 11209 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โ†’ (1 ยท (๐‘ฅโ€˜๐‘–)) = (๐‘ฅโ€˜๐‘–))
116115adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚) โ†’ (1 ยท (๐‘ฅโ€˜๐‘–)) = (๐‘ฅโ€˜๐‘–))
117114, 116sylan9eq 2784 . . . . . . . . . . . . . . . . . . . 20 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 / ๐‘ ) ยท ๐‘ ) ยท (๐‘ฅโ€˜๐‘–)) = (๐‘ฅโ€˜๐‘–))
118113, 117eqtr3d 2766 . . . . . . . . . . . . . . . . . . 19 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 / ๐‘ ) ยท (๐‘  ยท (๐‘ฅโ€˜๐‘–))) = (๐‘ฅโ€˜๐‘–))
119110, 118oveq12d 7419 . . . . . . . . . . . . . . . . . 18 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)))) + ((1 / ๐‘ ) ยท (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) = (0 + (๐‘ฅโ€˜๐‘–)))
12075, 81mulcld 11230 . . . . . . . . . . . . . . . . . . . 20 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
121 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
122 mulcl 11189 . . . . . . . . . . . . . . . . . . . . . 22 (((1 โˆ’ ๐‘ ) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚) โ†’ ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
12378, 121, 122syl2an 595 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
124103, 123mulcld 11230 . . . . . . . . . . . . . . . . . . . 20 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–))) โˆˆ โ„‚)
125 mulcl 11189 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘  โˆˆ โ„‚ โˆง (๐‘ฅโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐‘  ยท (๐‘ฅโ€˜๐‘–)) โˆˆ โ„‚)
126125ad2ant2r 744 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘  ยท (๐‘ฅโ€˜๐‘–)) โˆˆ โ„‚)
127103, 126mulcld 11230 . . . . . . . . . . . . . . . . . . . 20 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 / ๐‘ ) ยท (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โˆˆ โ„‚)
128120, 124, 127addassd 11232 . . . . . . . . . . . . . . . . . . 19 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)))) + ((1 / ๐‘ ) ยท (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + (((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–))) + ((1 / ๐‘ ) ยท (๐‘  ยท (๐‘ฅโ€˜๐‘–))))))
129103, 123, 126adddid 11234 . . . . . . . . . . . . . . . . . . . 20 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) = (((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–))) + ((1 / ๐‘ ) ยท (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))
130129oveq2d 7417 . . . . . . . . . . . . . . . . . . 19 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + (((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–))) + ((1 / ๐‘ ) ยท (๐‘  ยท (๐‘ฅโ€˜๐‘–))))))
131128, 130eqtr4d 2767 . . . . . . . . . . . . . . . . . 18 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)))) + ((1 / ๐‘ ) ยท (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))))
132 addlid 11393 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โ†’ (0 + (๐‘ฅโ€˜๐‘–)) = (๐‘ฅโ€˜๐‘–))
133132ad2antrl 725 . . . . . . . . . . . . . . . . . 18 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (0 + (๐‘ฅโ€˜๐‘–)) = (๐‘ฅโ€˜๐‘–))
134119, 131, 1333eqtr3rd 2773 . . . . . . . . . . . . . . . . 17 (((๐‘  โˆˆ โ„‚ โˆง ๐‘  โ‰  0) โˆง ((๐‘ฅโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘ฅโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))))
13566, 67, 68, 70, 134syl22anc 836 . . . . . . . . . . . . . . . 16 (((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ฅโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))))
136135ralrimiva 3138 . . . . . . . . . . . . . . 15 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))))
137 oveq2 7409 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (1 / ๐‘ ) โ†’ (1 โˆ’ ๐‘ก) = (1 โˆ’ (1 / ๐‘ )))
138137oveq1d 7416 . . . . . . . . . . . . . . . . . . 19 (๐‘ก = (1 / ๐‘ ) โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) = ((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)))
139 oveq1 7408 . . . . . . . . . . . . . . . . . . 19 (๐‘ก = (1 / ๐‘ ) โ†’ (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) = ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))
140138, 139oveq12d 7419 . . . . . . . . . . . . . . . . . 18 (๐‘ก = (1 / ๐‘ ) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))))
141140eqeq2d 2735 . . . . . . . . . . . . . . . . 17 (๐‘ก = (1 / ๐‘ ) โ†’ ((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))) โ†” (๐‘ฅโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))))
142141ralbidv 3169 . . . . . . . . . . . . . . . 16 (๐‘ก = (1 / ๐‘ ) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))))
143142rspcev 3604 . . . . . . . . . . . . . . 15 (((1 / ๐‘ ) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ )) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ ) ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))))
14464, 136, 143syl2anc 583 . . . . . . . . . . . . . 14 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))))
145 oveq2 7409 . . . . . . . . . . . . . . . . . . 19 ((๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โ†’ (๐‘ก ยท (๐‘ˆโ€˜๐‘–)) = (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))
146145oveq2d 7417 . . . . . . . . . . . . . . . . . 18 ((๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))))))
147146eqeq2d 2735 . . . . . . . . . . . . . . . . 17 ((๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โ†’ ((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” (๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))))
148147ralimi 3075 . . . . . . . . . . . . . . . 16 (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” (๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))))
149 ralbi 3095 . . . . . . . . . . . . . . . 16 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” (๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))))
150148, 149syl 17 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))))
151150rexbidv 3170 . . . . . . . . . . . . . 14 (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))))))
152144, 151syl5ibrcom 246 . . . . . . . . . . . . 13 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง ๐‘  โ‰  0) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–))) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
153152impancom 451 . . . . . . . . . . . 12 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) โ†’ (๐‘  โ‰  0 โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
15447, 153mpd 15 . . . . . . . . . . 11 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘  โˆˆ (0[,]1)) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
155154r19.29an 3150 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ฅโ€˜๐‘–)))) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
15612, 155syldan 590 . . . . . . . . 9 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ˆ Btwn โŸจ๐‘, ๐‘ฅโŸฉ) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
157 3simpa 1145 . . . . . . . . . . . 12 ((๐‘ฅ โˆˆ โ„ โˆง 0 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค 1) โ†’ (๐‘ฅ โˆˆ โ„ โˆง 0 โ‰ค ๐‘ฅ))
158 elicc01 13439 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ (0[,]1) โ†” (๐‘ฅ โˆˆ โ„ โˆง 0 โ‰ค ๐‘ฅ โˆง ๐‘ฅ โ‰ค 1))
159 elrege0 13427 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ (0[,)+โˆž) โ†” (๐‘ฅ โˆˆ โ„ โˆง 0 โ‰ค ๐‘ฅ))
160157, 158, 1593imtr4i 292 . . . . . . . . . . 11 (๐‘ฅ โˆˆ (0[,]1) โ†’ ๐‘ฅ โˆˆ (0[,)+โˆž))
161160ssriv 3978 . . . . . . . . . 10 (0[,]1) โІ (0[,)+โˆž)
162 brbtwn 28592 . . . . . . . . . . . 12 ((๐‘ฅ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ฅ Btwn โŸจ๐‘, ๐‘ˆโŸฉ โ†” โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
1639, 8, 7, 162syl3anc 1368 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ฅ Btwn โŸจ๐‘, ๐‘ˆโŸฉ โ†” โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
164163biimpa 476 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ฅ Btwn โŸจ๐‘, ๐‘ˆโŸฉ) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
165 ssrexv 4043 . . . . . . . . . 10 ((0[,]1) โІ (0[,)+โˆž) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
166161, 164, 165mpsyl 68 . . . . . . . . 9 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ฅ Btwn โŸจ๐‘, ๐‘ˆโŸฉ) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
167156, 166jaodan 954 . . . . . . . 8 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘ˆ Btwn โŸจ๐‘, ๐‘ฅโŸฉ โˆจ ๐‘ฅ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
168167anasss 466 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ฅ โˆˆ (๐”ผโ€˜๐‘) โˆง (๐‘ˆ Btwn โŸจ๐‘, ๐‘ฅโŸฉ โˆจ ๐‘ฅ Btwn โŸจ๐‘, ๐‘ˆโŸฉ))) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
1696, 168sylan2b 593 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ ๐ท) โ†’ โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
170 r19.26 3103 . . . . . . . . . 10 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))) โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))))
171 eqtr2 2748 . . . . . . . . . . 11 (((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))))
172171ralimi 3075 . . . . . . . . . 10 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))))
173170, 172sylbir 234 . . . . . . . . 9 ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))))
174 elrege0 13427 . . . . . . . . . . . . 13 (๐‘ก โˆˆ (0[,)+โˆž) โ†” (๐‘ก โˆˆ โ„ โˆง 0 โ‰ค ๐‘ก))
175174simplbi 497 . . . . . . . . . . . 12 (๐‘ก โˆˆ (0[,)+โˆž) โ†’ ๐‘ก โˆˆ โ„)
176175recnd 11238 . . . . . . . . . . 11 (๐‘ก โˆˆ (0[,)+โˆž) โ†’ ๐‘ก โˆˆ โ„‚)
177 elrege0 13427 . . . . . . . . . . . . 13 (๐‘  โˆˆ (0[,)+โˆž) โ†” (๐‘  โˆˆ โ„ โˆง 0 โ‰ค ๐‘ ))
178177simplbi 497 . . . . . . . . . . . 12 (๐‘  โˆˆ (0[,)+โˆž) โ†’ ๐‘  โˆˆ โ„)
179178recnd 11238 . . . . . . . . . . 11 (๐‘  โˆˆ (0[,)+โˆž) โ†’ ๐‘  โˆˆ โ„‚)
180176, 179anim12i 612 . . . . . . . . . 10 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง ๐‘  โˆˆ (0[,)+โˆž)) โ†’ (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚))
181 simplr 766 . . . . . . . . . . . . 13 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚))
182 simpl2 1189 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
183182ad2antrr 723 . . . . . . . . . . . . . 14 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
184183, 29sylancom 587 . . . . . . . . . . . . 13 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
185 simpl3 1190 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
186185ad2antrr 723 . . . . . . . . . . . . . 14 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
187 fveecn 28595 . . . . . . . . . . . . . 14 ((๐‘ˆ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
188186, 187sylancom 587 . . . . . . . . . . . . 13 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
189 subcl 11455 . . . . . . . . . . . . . . . . . 18 ((1 โˆˆ โ„‚ โˆง ๐‘ก โˆˆ โ„‚) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
19071, 189mpan 687 . . . . . . . . . . . . . . . . 17 (๐‘ก โˆˆ โ„‚ โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
191190adantr 480 . . . . . . . . . . . . . . . 16 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
192 simpl 482 . . . . . . . . . . . . . . . 16 (((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
193 mulcl 11189 . . . . . . . . . . . . . . . 16 (((1 โˆ’ ๐‘ก) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚) โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
194191, 192, 193syl2an 595 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
195 mulcl 11189 . . . . . . . . . . . . . . . 16 ((๐‘ก โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐‘ก ยท (๐‘ˆโ€˜๐‘–)) โˆˆ โ„‚)
196195ad2ant2rl 746 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘ก ยท (๐‘ˆโ€˜๐‘–)) โˆˆ โ„‚)
19777adantl 481 . . . . . . . . . . . . . . . 16 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โ†’ (1 โˆ’ ๐‘ ) โˆˆ โ„‚)
198197, 192, 122syl2an 595 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
199 mulcl 11189 . . . . . . . . . . . . . . . 16 ((๐‘  โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐‘  ยท (๐‘ˆโ€˜๐‘–)) โˆˆ โ„‚)
200199ad2ant2l 743 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘  ยท (๐‘ˆโ€˜๐‘–)) โˆˆ โ„‚)
201194, 196, 198, 200addsubeq4d 11618 . . . . . . . . . . . . . 14 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) โ†” (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) โˆ’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–))) = ((๐‘ก ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘  ยท (๐‘ˆโ€˜๐‘–)))))
202 nnncan1 11492 . . . . . . . . . . . . . . . . . . . 20 ((1 โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚ โˆง ๐‘ก โˆˆ โ„‚) โ†’ ((1 โˆ’ ๐‘ ) โˆ’ (1 โˆ’ ๐‘ก)) = (๐‘ก โˆ’ ๐‘ ))
20371, 202mp3an1 1444 . . . . . . . . . . . . . . . . . . 19 ((๐‘  โˆˆ โ„‚ โˆง ๐‘ก โˆˆ โ„‚) โ†’ ((1 โˆ’ ๐‘ ) โˆ’ (1 โˆ’ ๐‘ก)) = (๐‘ก โˆ’ ๐‘ ))
204203ancoms 458 . . . . . . . . . . . . . . . . . 18 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โ†’ ((1 โˆ’ ๐‘ ) โˆ’ (1 โˆ’ ๐‘ก)) = (๐‘ก โˆ’ ๐‘ ))
205204oveq1d 7416 . . . . . . . . . . . . . . . . 17 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โ†’ (((1 โˆ’ ๐‘ ) โˆ’ (1 โˆ’ ๐‘ก)) ยท (๐‘โ€˜๐‘–)) = ((๐‘ก โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)))
206205adantr 480 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ ๐‘ ) โˆ’ (1 โˆ’ ๐‘ก)) ยท (๐‘โ€˜๐‘–)) = ((๐‘ก โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)))
20777ad2antlr 724 . . . . . . . . . . . . . . . . 17 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (1 โˆ’ ๐‘ ) โˆˆ โ„‚)
208190ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
209 simprl 768 . . . . . . . . . . . . . . . . 17 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
210207, 208, 209subdird 11667 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ ๐‘ ) โˆ’ (1 โˆ’ ๐‘ก)) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) โˆ’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–))))
211206, 210eqtr3d 2766 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((๐‘ก โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) โˆ’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–))))
212 simpll 764 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ๐‘ก โˆˆ โ„‚)
213 simplr 766 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ๐‘  โˆˆ โ„‚)
214 simprr 770 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
215212, 213, 214subdird 11667 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((๐‘ก โˆ’ ๐‘ ) ยท (๐‘ˆโ€˜๐‘–)) = ((๐‘ก ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘  ยท (๐‘ˆโ€˜๐‘–))))
216211, 215eqeq12d 2740 . . . . . . . . . . . . . 14 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((๐‘ก โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) = ((๐‘ก โˆ’ ๐‘ ) ยท (๐‘ˆโ€˜๐‘–)) โ†” (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) โˆ’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–))) = ((๐‘ก ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘  ยท (๐‘ˆโ€˜๐‘–)))))
217 subcl 11455 . . . . . . . . . . . . . . . 16 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โ†’ (๐‘ก โˆ’ ๐‘ ) โˆˆ โ„‚)
218217adantr 480 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘ก โˆ’ ๐‘ ) โˆˆ โ„‚)
219 mulcan1g 11863 . . . . . . . . . . . . . . 15 (((๐‘ก โˆ’ ๐‘ ) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โ†’ (((๐‘ก โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) = ((๐‘ก โˆ’ ๐‘ ) ยท (๐‘ˆโ€˜๐‘–)) โ†” ((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
220218, 209, 214, 219syl3anc 1368 . . . . . . . . . . . . . 14 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((๐‘ก โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) = ((๐‘ก โˆ’ ๐‘ ) ยท (๐‘ˆโ€˜๐‘–)) โ†” ((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
221201, 216, 2203bitr2d 307 . . . . . . . . . . . . 13 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) โ†” ((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
222181, 184, 188, 221syl12anc 834 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) โ†” ((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
223222ralbidva 3167 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
224 r19.32v 3183 . . . . . . . . . . . 12 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)) โ†” ((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
225 simplr 766 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ ๐‘ โ‰  ๐‘ˆ)
226225neneqd 2937 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ ยฌ ๐‘ = ๐‘ˆ)
227 simpll2 1210 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
228 simpll3 1211 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
229 eqeefv 28596 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
230227, 228, 229syl2anc 583 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
231226, 230mtbid 324 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ ยฌ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))
232 orel2 887 . . . . . . . . . . . . . 14 (ยฌ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–) โ†’ (((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)) โ†’ (๐‘ก โˆ’ ๐‘ ) = 0))
233231, 232syl 17 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ (((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)) โ†’ (๐‘ก โˆ’ ๐‘ ) = 0))
234 subeq0 11482 . . . . . . . . . . . . . 14 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚) โ†’ ((๐‘ก โˆ’ ๐‘ ) = 0 โ†” ๐‘ก = ๐‘ ))
235234adantl 481 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ ((๐‘ก โˆ’ ๐‘ ) = 0 โ†” ๐‘ก = ๐‘ ))
236233, 235sylibd 238 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ (((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)) โ†’ ๐‘ก = ๐‘ ))
237224, 236biimtrid 241 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ก โˆ’ ๐‘ ) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)) โ†’ ๐‘ก = ๐‘ ))
238223, 237sylbid 239 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ โ„‚ โˆง ๐‘  โˆˆ โ„‚)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) โ†’ ๐‘ก = ๐‘ ))
239180, 238sylan2 592 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง ๐‘  โˆˆ (0[,)+โˆž))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) โ†’ ๐‘ก = ๐‘ ))
240173, 239syl5 34 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง ๐‘  โˆˆ (0[,)+โˆž))) โ†’ ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ๐‘ก = ๐‘ ))
241240ralrimivva 3192 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ โˆ€๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘  โˆˆ (0[,)+โˆž)((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ๐‘ก = ๐‘ ))
242241adantr 480 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ ๐ท) โ†’ โˆ€๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘  โˆˆ (0[,)+โˆž)((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ๐‘ก = ๐‘ ))
243 oveq2 7409 . . . . . . . . . . 11 (๐‘ก = ๐‘  โ†’ (1 โˆ’ ๐‘ก) = (1 โˆ’ ๐‘ ))
244243oveq1d 7416 . . . . . . . . . 10 (๐‘ก = ๐‘  โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) = ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)))
245 oveq1 7408 . . . . . . . . . 10 (๐‘ก = ๐‘  โ†’ (๐‘ก ยท (๐‘ˆโ€˜๐‘–)) = (๐‘  ยท (๐‘ˆโ€˜๐‘–)))
246244, 245oveq12d 7419 . . . . . . . . 9 (๐‘ก = ๐‘  โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))))
247246eqeq2d 2735 . . . . . . . 8 (๐‘ก = ๐‘  โ†’ ((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” (๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))))
248247ralbidv 3169 . . . . . . 7 (๐‘ก = ๐‘  โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))))
249248reu4 3719 . . . . . 6 (โˆƒ!๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” (โˆƒ๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘  โˆˆ (0[,)+โˆž)((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ๐‘ก = ๐‘ )))
250169, 242, 249sylanbrc 582 . . . . 5 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ ๐ท) โ†’ โˆƒ!๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
251 df-reu 3369 . . . . 5 (โˆƒ!๐‘ก โˆˆ (0[,)+โˆž)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆƒ!๐‘ก(๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
252250, 251sylib 217 . . . 4 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ฅ โˆˆ ๐ท) โ†’ โˆƒ!๐‘ก(๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
253252ralrimiva 3138 . . 3 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ โˆ€๐‘ฅ โˆˆ ๐ท โˆƒ!๐‘ก(๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
254 axcontlem2.2 . . . 4 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
255254fnopabg 6677 . . 3 (โˆ€๐‘ฅ โˆˆ ๐ท โˆƒ!๐‘ก(๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†” ๐น Fn ๐ท)
256253, 255sylib 217 . 2 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐น Fn ๐ท)
257175ad2antlr 724 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ ๐‘ก โˆˆ โ„)
258182ad2antrr 723 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
259 fveere 28594 . . . . . . . . . . 11 ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘˜) โˆˆ โ„)
260258, 259sylancom 587 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘˜) โˆˆ โ„)
261185ad2antrr 723 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
262 fveere 28594 . . . . . . . . . . 11 ((๐‘ˆ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐‘ˆโ€˜๐‘˜) โˆˆ โ„)
263261, 262sylancom 587 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (๐‘ˆโ€˜๐‘˜) โˆˆ โ„)
264 resubcl 11520 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ โˆง ๐‘ก โˆˆ โ„) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„)
26557, 264mpan 687 . . . . . . . . . . . . 13 (๐‘ก โˆˆ โ„ โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„)
266 remulcl 11190 . . . . . . . . . . . . 13 (((1 โˆ’ ๐‘ก) โˆˆ โ„ โˆง (๐‘โ€˜๐‘˜) โˆˆ โ„) โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) โˆˆ โ„)
267265, 266sylan 579 . . . . . . . . . . . 12 ((๐‘ก โˆˆ โ„ โˆง (๐‘โ€˜๐‘˜) โˆˆ โ„) โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) โˆˆ โ„)
2682673adant3 1129 . . . . . . . . . . 11 ((๐‘ก โˆˆ โ„ โˆง (๐‘โ€˜๐‘˜) โˆˆ โ„ โˆง (๐‘ˆโ€˜๐‘˜) โˆˆ โ„) โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) โˆˆ โ„)
269 remulcl 11190 . . . . . . . . . . . 12 ((๐‘ก โˆˆ โ„ โˆง (๐‘ˆโ€˜๐‘˜) โˆˆ โ„) โ†’ (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)) โˆˆ โ„)
2702693adant2 1128 . . . . . . . . . . 11 ((๐‘ก โˆˆ โ„ โˆง (๐‘โ€˜๐‘˜) โˆˆ โ„ โˆง (๐‘ˆโ€˜๐‘˜) โˆˆ โ„) โ†’ (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)) โˆˆ โ„)
271268, 270readdcld 11239 . . . . . . . . . 10 ((๐‘ก โˆˆ โ„ โˆง (๐‘โ€˜๐‘˜) โˆˆ โ„ โˆง (๐‘ˆโ€˜๐‘˜) โˆˆ โ„) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))) โˆˆ โ„)
272257, 260, 263, 271syl3anc 1368 . . . . . . . . 9 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘˜ โˆˆ (1...๐‘)) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))) โˆˆ โ„)
273272ralrimiva 3138 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ โˆ€๐‘˜ โˆˆ (1...๐‘)(((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))) โˆˆ โ„)
274 simpll1 1209 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ ๐‘ โˆˆ โ„•)
275 mptelee 28588 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ (๐”ผโ€˜๐‘) โ†” โˆ€๐‘˜ โˆˆ (1...๐‘)(((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))) โˆˆ โ„))
276274, 275syl 17 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ (๐”ผโ€˜๐‘) โ†” โˆ€๐‘˜ โˆˆ (1...๐‘)(((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))) โˆˆ โ„))
277273, 276mpbird 257 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ (๐”ผโ€˜๐‘))
278 letric 11310 . . . . . . . . . 10 ((1 โˆˆ โ„ โˆง ๐‘ก โˆˆ โ„) โ†’ (1 โ‰ค ๐‘ก โˆจ ๐‘ก โ‰ค 1))
27957, 175, 278sylancr 586 . . . . . . . . 9 (๐‘ก โˆˆ (0[,)+โˆž) โ†’ (1 โ‰ค ๐‘ก โˆจ ๐‘ก โ‰ค 1))
280279adantl 481 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ (1 โ‰ค ๐‘ก โˆจ ๐‘ก โ‰ค 1))
281 simpr 484 . . . . . . . . . . . . . 14 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง 1 โ‰ค ๐‘ก) โ†’ 1 โ‰ค ๐‘ก)
282175adantr 480 . . . . . . . . . . . . . . 15 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง 1 โ‰ค ๐‘ก) โ†’ ๐‘ก โˆˆ โ„)
283 0red 11213 . . . . . . . . . . . . . . . 16 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง 1 โ‰ค ๐‘ก) โ†’ 0 โˆˆ โ„)
284 1red 11211 . . . . . . . . . . . . . . . 16 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง 1 โ‰ค ๐‘ก) โ†’ 1 โˆˆ โ„)
285 0lt1 11732 . . . . . . . . . . . . . . . . 17 0 < 1
286285a1i 11 . . . . . . . . . . . . . . . 16 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง 1 โ‰ค ๐‘ก) โ†’ 0 < 1)
287283, 284, 282, 286, 281ltletrd 11370 . . . . . . . . . . . . . . 15 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง 1 โ‰ค ๐‘ก) โ†’ 0 < ๐‘ก)
288 divelunit 13467 . . . . . . . . . . . . . . . 16 (((1 โˆˆ โ„ โˆง 0 โ‰ค 1) โˆง (๐‘ก โˆˆ โ„ โˆง 0 < ๐‘ก)) โ†’ ((1 / ๐‘ก) โˆˆ (0[,]1) โ†” 1 โ‰ค ๐‘ก))
28957, 58, 288mpanl12 699 . . . . . . . . . . . . . . 15 ((๐‘ก โˆˆ โ„ โˆง 0 < ๐‘ก) โ†’ ((1 / ๐‘ก) โˆˆ (0[,]1) โ†” 1 โ‰ค ๐‘ก))
290282, 287, 289syl2anc 583 . . . . . . . . . . . . . 14 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง 1 โ‰ค ๐‘ก) โ†’ ((1 / ๐‘ก) โˆˆ (0[,]1) โ†” 1 โ‰ค ๐‘ก))
291281, 290mpbird 257 . . . . . . . . . . . . 13 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง 1 โ‰ค ๐‘ก) โ†’ (1 / ๐‘ก) โˆˆ (0[,]1))
292291adantll 711 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โ†’ (1 / ๐‘ก) โˆˆ (0[,]1))
293175ad3antlr 728 . . . . . . . . . . . . . . 15 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ก โˆˆ โ„)
294293recnd 11238 . . . . . . . . . . . . . 14 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ก โˆˆ โ„‚)
295287gt0ne0d 11774 . . . . . . . . . . . . . . . 16 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง 1 โ‰ค ๐‘ก) โ†’ ๐‘ก โ‰  0)
296295adantll 711 . . . . . . . . . . . . . . 15 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โ†’ ๐‘ก โ‰  0)
297296adantr 480 . . . . . . . . . . . . . 14 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ก โ‰  0)
298182ad3antrrr 727 . . . . . . . . . . . . . . 15 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
299298, 29sylancom 587 . . . . . . . . . . . . . 14 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
300185ad3antrrr 727 . . . . . . . . . . . . . . 15 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
301300, 187sylancom 587 . . . . . . . . . . . . . 14 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
302 reccl 11875 . . . . . . . . . . . . . . . . . 18 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ (1 / ๐‘ก) โˆˆ โ„‚)
303302adantr 480 . . . . . . . . . . . . . . . . 17 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (1 / ๐‘ก) โˆˆ โ„‚)
304190adantr 480 . . . . . . . . . . . . . . . . . 18 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
305304, 192, 193syl2an 595 . . . . . . . . . . . . . . . . 17 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
306195ad2ant2rl 746 . . . . . . . . . . . . . . . . 17 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘ก ยท (๐‘ˆโ€˜๐‘–)) โˆˆ โ„‚)
307303, 305, 306adddid 11234 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) = (((1 / ๐‘ก) ยท ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–))) + ((1 / ๐‘ก) ยท (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
308307oveq2d 7417 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + (((1 / ๐‘ก) ยท ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–))) + ((1 / ๐‘ก) ยท (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))))
309 subcl 11455 . . . . . . . . . . . . . . . . . 18 ((1 โˆˆ โ„‚ โˆง (1 / ๐‘ก) โˆˆ โ„‚) โ†’ (1 โˆ’ (1 / ๐‘ก)) โˆˆ โ„‚)
31071, 302, 309sylancr 586 . . . . . . . . . . . . . . . . 17 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ (1 โˆ’ (1 / ๐‘ก)) โˆˆ โ„‚)
311 mulcl 11189 . . . . . . . . . . . . . . . . 17 (((1 โˆ’ (1 / ๐‘ก)) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚) โ†’ ((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
312310, 192, 311syl2an 595 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
313303, 305mulcld 11230 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 / ๐‘ก) ยท ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–))) โˆˆ โ„‚)
314 recid2 11883 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ ((1 / ๐‘ก) ยท ๐‘ก) = 1)
315314oveq1d 7416 . . . . . . . . . . . . . . . . . . 19 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ (((1 / ๐‘ก) ยท ๐‘ก) ยท (๐‘ˆโ€˜๐‘–)) = (1 ยท (๐‘ˆโ€˜๐‘–)))
316315adantr 480 . . . . . . . . . . . . . . . . . 18 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 / ๐‘ก) ยท ๐‘ก) ยท (๐‘ˆโ€˜๐‘–)) = (1 ยท (๐‘ˆโ€˜๐‘–)))
317 simpll 764 . . . . . . . . . . . . . . . . . . 19 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ๐‘ก โˆˆ โ„‚)
318 simprr 770 . . . . . . . . . . . . . . . . . . 19 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
319303, 317, 318mulassd 11233 . . . . . . . . . . . . . . . . . 18 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 / ๐‘ก) ยท ๐‘ก) ยท (๐‘ˆโ€˜๐‘–)) = ((1 / ๐‘ก) ยท (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
320 mullid 11209 . . . . . . . . . . . . . . . . . . 19 ((๐‘ˆโ€˜๐‘–) โˆˆ โ„‚ โ†’ (1 ยท (๐‘ˆโ€˜๐‘–)) = (๐‘ˆโ€˜๐‘–))
321320ad2antll 726 . . . . . . . . . . . . . . . . . 18 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (1 ยท (๐‘ˆโ€˜๐‘–)) = (๐‘ˆโ€˜๐‘–))
322316, 319, 3213eqtr3d 2772 . . . . . . . . . . . . . . . . 17 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 / ๐‘ก) ยท (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) = (๐‘ˆโ€˜๐‘–))
323322, 318eqeltrd 2825 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 / ๐‘ก) ยท (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆˆ โ„‚)
324312, 313, 323addassd 11232 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)))) + ((1 / ๐‘ก) ยท (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + (((1 / ๐‘ก) ยท ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–))) + ((1 / ๐‘ก) ยท (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))))
325310adantr 480 . . . . . . . . . . . . . . . . . . 19 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (1 โˆ’ (1 / ๐‘ก)) โˆˆ โ„‚)
326302, 304mulcld 11230 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก)) โˆˆ โ„‚)
327326adantr 480 . . . . . . . . . . . . . . . . . . 19 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก)) โˆˆ โ„‚)
328 simprl 768 . . . . . . . . . . . . . . . . . . 19 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
329325, 327, 328adddird 11235 . . . . . . . . . . . . . . . . . 18 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ก)) + ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก))) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + (((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก)) ยท (๐‘โ€˜๐‘–))))
330 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ ๐‘ก โˆˆ โ„‚)
331 subdi 11643 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 / ๐‘ก) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง ๐‘ก โˆˆ โ„‚) โ†’ ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก)) = (((1 / ๐‘ก) ยท 1) โˆ’ ((1 / ๐‘ก) ยท ๐‘ก)))
33271, 331mp3an2 1445 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1 / ๐‘ก) โˆˆ โ„‚ โˆง ๐‘ก โˆˆ โ„‚) โ†’ ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก)) = (((1 / ๐‘ก) ยท 1) โˆ’ ((1 / ๐‘ก) ยท ๐‘ก)))
333302, 330, 332syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก)) = (((1 / ๐‘ก) ยท 1) โˆ’ ((1 / ๐‘ก) ยท ๐‘ก)))
334302mulridd 11227 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ ((1 / ๐‘ก) ยท 1) = (1 / ๐‘ก))
335334, 314oveq12d 7419 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ (((1 / ๐‘ก) ยท 1) โˆ’ ((1 / ๐‘ก) ยท ๐‘ก)) = ((1 / ๐‘ก) โˆ’ 1))
336333, 335eqtrd 2764 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก)) = ((1 / ๐‘ก) โˆ’ 1))
337336oveq2d 7417 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ ((1 โˆ’ (1 / ๐‘ก)) + ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก))) = ((1 โˆ’ (1 / ๐‘ก)) + ((1 / ๐‘ก) โˆ’ 1)))
338 npncan2 11483 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 โˆˆ โ„‚ โˆง (1 / ๐‘ก) โˆˆ โ„‚) โ†’ ((1 โˆ’ (1 / ๐‘ก)) + ((1 / ๐‘ก) โˆ’ 1)) = 0)
33971, 302, 338sylancr 586 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ ((1 โˆ’ (1 / ๐‘ก)) + ((1 / ๐‘ก) โˆ’ 1)) = 0)
340337, 339eqtrd 2764 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โ†’ ((1 โˆ’ (1 / ๐‘ก)) + ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก))) = 0)
341340adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (1 / ๐‘ก)) + ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก))) = 0)
342341oveq1d 7416 . . . . . . . . . . . . . . . . . . 19 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ก)) + ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก))) ยท (๐‘โ€˜๐‘–)) = (0 ยท (๐‘โ€˜๐‘–)))
343108ad2antrl 725 . . . . . . . . . . . . . . . . . . 19 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (0 ยท (๐‘โ€˜๐‘–)) = 0)
344342, 343eqtrd 2764 . . . . . . . . . . . . . . . . . 18 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ก)) + ((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก))) ยท (๐‘โ€˜๐‘–)) = 0)
345190ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
346303, 345, 328mulassd 11233 . . . . . . . . . . . . . . . . . . 19 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก)) ยท (๐‘โ€˜๐‘–)) = ((1 / ๐‘ก) ยท ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–))))
347346oveq2d 7417 . . . . . . . . . . . . . . . . . 18 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + (((1 / ๐‘ก) ยท (1 โˆ’ ๐‘ก)) ยท (๐‘โ€˜๐‘–))) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)))))
348329, 344, 3473eqtr3rd 2773 . . . . . . . . . . . . . . . . 17 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)))) = 0)
349348, 322oveq12d 7419 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)))) + ((1 / ๐‘ก) ยท (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) = (0 + (๐‘ˆโ€˜๐‘–)))
350 addlid 11393 . . . . . . . . . . . . . . . . 17 ((๐‘ˆโ€˜๐‘–) โˆˆ โ„‚ โ†’ (0 + (๐‘ˆโ€˜๐‘–)) = (๐‘ˆโ€˜๐‘–))
351350ad2antll 726 . . . . . . . . . . . . . . . 16 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (0 + (๐‘ˆโ€˜๐‘–)) = (๐‘ˆโ€˜๐‘–))
352349, 351eqtrd 2764 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)))) + ((1 / ๐‘ก) ยท (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) = (๐‘ˆโ€˜๐‘–))
353308, 324, 3523eqtr2rd 2771 . . . . . . . . . . . . . 14 (((๐‘ก โˆˆ โ„‚ โˆง ๐‘ก โ‰  0) โˆง ((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)) โ†’ (๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))))
354294, 297, 299, 301, 353syl22anc 836 . . . . . . . . . . . . 13 ((((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))))
355354ralrimiva 3138 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))))
356 oveq2 7409 . . . . . . . . . . . . . . . . . 18 (๐‘  = (1 / ๐‘ก) โ†’ (1 โˆ’ ๐‘ ) = (1 โˆ’ (1 / ๐‘ก)))
357356oveq1d 7416 . . . . . . . . . . . . . . . . 17 (๐‘  = (1 / ๐‘ก) โ†’ ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) = ((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)))
358 oveq1 7408 . . . . . . . . . . . . . . . . 17 (๐‘  = (1 / ๐‘ก) โ†’ (๐‘  ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–)) = ((1 / ๐‘ก) ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–)))
359357, 358oveq12d 7419 . . . . . . . . . . . . . . . 16 (๐‘  = (1 / ๐‘ก) โ†’ (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))))
360359eqeq2d 2735 . . . . . . . . . . . . . . 15 (๐‘  = (1 / ๐‘ก) โ†’ ((๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))) โ†” (๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–)))))
361360ralbidv 3169 . . . . . . . . . . . . . 14 (๐‘  = (1 / ๐‘ก) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–)))))
362 fveq2 6881 . . . . . . . . . . . . . . . . . . . . 21 (๐‘˜ = ๐‘– โ†’ (๐‘โ€˜๐‘˜) = (๐‘โ€˜๐‘–))
363362oveq2d 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘˜ = ๐‘– โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) = ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)))
364 fveq2 6881 . . . . . . . . . . . . . . . . . . . . 21 (๐‘˜ = ๐‘– โ†’ (๐‘ˆโ€˜๐‘˜) = (๐‘ˆโ€˜๐‘–))
365364oveq2d 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘˜ = ๐‘– โ†’ (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)) = (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))
366363, 365oveq12d 7419 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ = ๐‘– โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
367 eqid 2724 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) = (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))
368 ovex 7434 . . . . . . . . . . . . . . . . . . 19 (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆˆ V
369366, 367, 368fvmpt 6988 . . . . . . . . . . . . . . . . . 18 (๐‘– โˆˆ (1...๐‘) โ†’ ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
370369oveq2d 7417 . . . . . . . . . . . . . . . . 17 (๐‘– โˆˆ (1...๐‘) โ†’ ((1 / ๐‘ก) ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–)) = ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
371370oveq2d 7417 . . . . . . . . . . . . . . . 16 (๐‘– โˆˆ (1...๐‘) โ†’ (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))))
372371eqeq2d 2735 . . . . . . . . . . . . . . 15 (๐‘– โˆˆ (1...๐‘) โ†’ ((๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))) โ†” (๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))))
373372ralbiia 3083 . . . . . . . . . . . . . 14 (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))))
374361, 373bitrdi 287 . . . . . . . . . . . . 13 (๐‘  = (1 / ๐‘ก) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))))
375374rspcev 3604 . . . . . . . . . . . 12 (((1 / ๐‘ก) โˆˆ (0[,]1) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ (1 / ๐‘ก)) ยท (๐‘โ€˜๐‘–)) + ((1 / ๐‘ก) ยท (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))) โ†’ โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))))
376292, 355, 375syl2anc 583 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โ†’ โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))))
377185ad2antrr 723 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
378182ad2antrr 723 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
379277adantr 480 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โ†’ (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ (๐”ผโ€˜๐‘))
380 brbtwn 28592 . . . . . . . . . . . 12 ((๐‘ˆ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ˆ Btwn โŸจ๐‘, (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โŸฉ โ†” โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–)))))
381377, 378, 379, 380syl3anc 1368 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โ†’ (๐‘ˆ Btwn โŸจ๐‘, (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โŸฉ โ†” โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ˆโ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–)))))
382376, 381mpbird 257 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง 1 โ‰ค ๐‘ก) โ†’ ๐‘ˆ Btwn โŸจ๐‘, (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โŸฉ)
383382ex 412 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ (1 โ‰ค ๐‘ก โ†’ ๐‘ˆ Btwn โŸจ๐‘, (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โŸฉ))
384 simpll 764 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„ โˆง 0 โ‰ค ๐‘ก) โˆง ๐‘ก โ‰ค 1) โ†’ ๐‘ก โˆˆ โ„)
385 simplr 766 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„ โˆง 0 โ‰ค ๐‘ก) โˆง ๐‘ก โ‰ค 1) โ†’ 0 โ‰ค ๐‘ก)
386 simpr 484 . . . . . . . . . . . . . . 15 (((๐‘ก โˆˆ โ„ โˆง 0 โ‰ค ๐‘ก) โˆง ๐‘ก โ‰ค 1) โ†’ ๐‘ก โ‰ค 1)
387384, 385, 3863jca 1125 . . . . . . . . . . . . . 14 (((๐‘ก โˆˆ โ„ โˆง 0 โ‰ค ๐‘ก) โˆง ๐‘ก โ‰ค 1) โ†’ (๐‘ก โˆˆ โ„ โˆง 0 โ‰ค ๐‘ก โˆง ๐‘ก โ‰ค 1))
388174anbi1i 623 . . . . . . . . . . . . . 14 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง ๐‘ก โ‰ค 1) โ†” ((๐‘ก โˆˆ โ„ โˆง 0 โ‰ค ๐‘ก) โˆง ๐‘ก โ‰ค 1))
389 elicc01 13439 . . . . . . . . . . . . . 14 (๐‘ก โˆˆ (0[,]1) โ†” (๐‘ก โˆˆ โ„ โˆง 0 โ‰ค ๐‘ก โˆง ๐‘ก โ‰ค 1))
390387, 388, 3893imtr4i 292 . . . . . . . . . . . . 13 ((๐‘ก โˆˆ (0[,)+โˆž) โˆง ๐‘ก โ‰ค 1) โ†’ ๐‘ก โˆˆ (0[,]1))
391390adantll 711 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โ‰ค 1) โ†’ ๐‘ก โˆˆ (0[,]1))
392369rgen 3055 . . . . . . . . . . . 12 โˆ€๐‘– โˆˆ (1...๐‘)((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))
393 oveq2 7409 . . . . . . . . . . . . . . . . 17 (๐‘  = ๐‘ก โ†’ (1 โˆ’ ๐‘ ) = (1 โˆ’ ๐‘ก))
394393oveq1d 7416 . . . . . . . . . . . . . . . 16 (๐‘  = ๐‘ก โ†’ ((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) = ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)))
395 oveq1 7408 . . . . . . . . . . . . . . . 16 (๐‘  = ๐‘ก โ†’ (๐‘  ยท (๐‘ˆโ€˜๐‘–)) = (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))
396394, 395oveq12d 7419 . . . . . . . . . . . . . . 15 (๐‘  = ๐‘ก โ†’ (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
397396eqeq2d 2735 . . . . . . . . . . . . . 14 (๐‘  = ๐‘ก โ†’ (((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) โ†” ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
398397ralbidv 3169 . . . . . . . . . . . . 13 (๐‘  = ๐‘ก โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
399398rspcev 3604 . . . . . . . . . . . 12 ((๐‘ก โˆˆ (0[,]1) โˆง โˆ€๐‘– โˆˆ (1...๐‘)((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))))
400391, 392, 399sylancl 585 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โ‰ค 1) โ†’ โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–))))
401277adantr 480 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โ‰ค 1) โ†’ (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ (๐”ผโ€˜๐‘))
402182ad2antrr 723 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โ‰ค 1) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
403185ad2antrr 723 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โ‰ค 1) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
404 brbtwn 28592 . . . . . . . . . . . 12 (((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) Btwn โŸจ๐‘, ๐‘ˆโŸฉ โ†” โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))))
405401, 402, 403, 404syl3anc 1368 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โ‰ค 1) โ†’ ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) Btwn โŸจ๐‘, ๐‘ˆโŸฉ โ†” โˆƒ๐‘  โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ ) ยท (๐‘โ€˜๐‘–)) + (๐‘  ยท (๐‘ˆโ€˜๐‘–)))))
406400, 405mpbird 257 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โ‰ค 1) โ†’ (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) Btwn โŸจ๐‘, ๐‘ˆโŸฉ)
407406ex 412 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ (๐‘ก โ‰ค 1 โ†’ (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) Btwn โŸจ๐‘, ๐‘ˆโŸฉ))
408383, 407orim12d 961 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ ((1 โ‰ค ๐‘ก โˆจ ๐‘ก โ‰ค 1) โ†’ (๐‘ˆ Btwn โŸจ๐‘, (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โŸฉ โˆจ (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) Btwn โŸจ๐‘, ๐‘ˆโŸฉ)))
409280, 408mpd 15 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ (๐‘ˆ Btwn โŸจ๐‘, (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โŸฉ โˆจ (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) Btwn โŸจ๐‘, ๐‘ˆโŸฉ))
410 opeq2 4866 . . . . . . . . . 10 (๐‘ = (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โ†’ โŸจ๐‘, ๐‘โŸฉ = โŸจ๐‘, (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โŸฉ)
411410breq2d 5150 . . . . . . . . 9 (๐‘ = (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โ†’ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โ†” ๐‘ˆ Btwn โŸจ๐‘, (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โŸฉ))
412 breq1 5141 . . . . . . . . 9 (๐‘ = (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โ†’ (๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ โ†” (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) Btwn โŸจ๐‘, ๐‘ˆโŸฉ))
413411, 412orbi12d 915 . . . . . . . 8 (๐‘ = (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โ†’ ((๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ) โ†” (๐‘ˆ Btwn โŸจ๐‘, (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โŸฉ โˆจ (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) Btwn โŸจ๐‘, ๐‘ˆโŸฉ)))
414413, 5elrab2 3678 . . . . . . 7 ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ ๐ท โ†” ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ (๐”ผโ€˜๐‘) โˆง (๐‘ˆ Btwn โŸจ๐‘, (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โŸฉ โˆจ (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) Btwn โŸจ๐‘, ๐‘ˆโŸฉ)))
415277, 409, 414sylanbrc 582 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ ๐ท)
416 fveq1 6880 . . . . . . . . 9 (๐‘ฅ = (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โ†’ (๐‘ฅโ€˜๐‘–) = ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–))
417416eqeq1d 2726 . . . . . . . 8 (๐‘ฅ = (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โ†’ ((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” ((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
418417ralbidv 3169 . . . . . . 7 (๐‘ฅ = (๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
419418rspcev 3604 . . . . . 6 (((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜)))) โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)((๐‘˜ โˆˆ (1...๐‘) โ†ฆ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘˜)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘˜))))โ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ท โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
420415, 392, 419sylancl 585 . . . . 5 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ท โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))
4216simplbi 497 . . . . . . . . 9 (๐‘ฅ โˆˆ ๐ท โ†’ ๐‘ฅ โˆˆ (๐”ผโ€˜๐‘))
4225ssrab3 4072 . . . . . . . . . 10 ๐ท โІ (๐”ผโ€˜๐‘)
423422sseli 3970 . . . . . . . . 9 (๐‘ฆ โˆˆ ๐ท โ†’ ๐‘ฆ โˆˆ (๐”ผโ€˜๐‘))
424421, 423anim12i 612 . . . . . . . 8 ((๐‘ฅ โˆˆ ๐ท โˆง ๐‘ฆ โˆˆ ๐ท) โ†’ (๐‘ฅ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ฆ โˆˆ (๐”ผโ€˜๐‘)))
425 r19.26 3103 . . . . . . . . . 10 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
426 eqtr3 2750 . . . . . . . . . . 11 (((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ (๐‘ฅโ€˜๐‘–) = (๐‘ฆโ€˜๐‘–))
427426ralimi 3075 . . . . . . . . . 10 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (๐‘ฆโ€˜๐‘–))
428425, 427sylbir 234 . . . . . . . . 9 ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (๐‘ฆโ€˜๐‘–))
429 eqeefv 28596 . . . . . . . . . 10 ((๐‘ฅ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ฆ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ฅ = ๐‘ฆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (๐‘ฆโ€˜๐‘–)))
430429adantl 481 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ฅ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ฆ โˆˆ (๐”ผโ€˜๐‘))) โ†’ (๐‘ฅ = ๐‘ฆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (๐‘ฆโ€˜๐‘–)))
431428, 430imbitrrid 245 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ฅ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ฆ โˆˆ (๐”ผโ€˜๐‘))) โ†’ ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ๐‘ฅ = ๐‘ฆ))
432424, 431sylan2 592 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ฅ โˆˆ ๐ท โˆง ๐‘ฆ โˆˆ ๐ท)) โ†’ ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ๐‘ฅ = ๐‘ฆ))
433432ralrimivva 3192 . . . . . 6 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ โˆ€๐‘ฅ โˆˆ ๐ท โˆ€๐‘ฆ โˆˆ ๐ท ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ๐‘ฅ = ๐‘ฆ))
434433adantr 480 . . . . 5 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ โˆ€๐‘ฅ โˆˆ ๐ท โˆ€๐‘ฆ โˆˆ ๐ท ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ๐‘ฅ = ๐‘ฆ))
435 df-reu 3369 . . . . . 6 (โˆƒ!๐‘ฅ โˆˆ ๐ท โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆƒ!๐‘ฅ(๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
436 fveq1 6880 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅโ€˜๐‘–) = (๐‘ฆโ€˜๐‘–))
437436eqeq1d 2726 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” (๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
438437ralbidv 3169 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
439438reu4 3719 . . . . . 6 (โˆƒ!๐‘ฅ โˆˆ ๐ท โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โ†” (โˆƒ๐‘ฅ โˆˆ ๐ท โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘ฅ โˆˆ ๐ท โˆ€๐‘ฆ โˆˆ ๐ท ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ๐‘ฅ = ๐‘ฆ)))
440435, 439bitr3i 277 . . . . 5 (โˆƒ!๐‘ฅ(๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†” (โˆƒ๐‘ฅ โˆˆ ๐ท โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘ฅ โˆˆ ๐ท โˆ€๐‘ฆ โˆˆ ๐ท ((โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฆโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ๐‘ฅ = ๐‘ฆ)))
441420, 434, 440sylanbrc 582 . . . 4 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ก โˆˆ (0[,)+โˆž)) โ†’ โˆƒ!๐‘ฅ(๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
442441ralrimiva 3138 . . 3 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ โˆ€๐‘ก โˆˆ (0[,)+โˆž)โˆƒ!๐‘ฅ(๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))
443 an12 642 . . . . . . . 8 ((๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))) โ†” (๐‘ก โˆˆ (0[,)+โˆž) โˆง (๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–))))))
444443opabbii 5205 . . . . . . 7 {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))} = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ก โˆˆ (0[,)+โˆž) โˆง (๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
445254, 444eqtri 2752 . . . . . 6 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ก โˆˆ (0[,)+โˆž) โˆง (๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
446445cnveqi 5864 . . . . 5 โ—ก๐น = โ—ก{โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ก โˆˆ (0[,)+โˆž) โˆง (๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
447 cnvopab 6128 . . . . 5 โ—ก{โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ก โˆˆ (0[,)+โˆž) โˆง (๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))} = {โŸจ๐‘ก, ๐‘ฅโŸฉ โˆฃ (๐‘ก โˆˆ (0[,)+โˆž) โˆง (๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
448446, 447eqtri 2752 . . . 4 โ—ก๐น = {โŸจ๐‘ก, ๐‘ฅโŸฉ โˆฃ (๐‘ก โˆˆ (0[,)+โˆž) โˆง (๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
449448fnopabg 6677 . . 3 (โˆ€๐‘ก โˆˆ (0[,)+โˆž)โˆƒ!๐‘ฅ(๐‘ฅ โˆˆ ๐ท โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))) โ†” โ—ก๐น Fn (0[,)+โˆž))
450442, 449sylib 217 . 2 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ โ—ก๐น Fn (0[,)+โˆž))
451 dff1o4 6831 . 2 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†” (๐น Fn ๐ท โˆง โ—ก๐น Fn (0[,)+โˆž)))
452256, 450, 451sylanbrc 582 1 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  โˆƒ!weu 2554   โ‰  wne 2932  โˆ€wral 3053  โˆƒwrex 3062  โˆƒ!wreu 3366  {crab 3424   โІ wss 3940  โŸจcop 4626   class class class wbr 5138  {copab 5200   โ†ฆ cmpt 5221  โ—กccnv 5665   Fn wfn 6528  โ€“1-1-ontoโ†’wf1o 6532  โ€˜cfv 6533  (class class class)co 7401  โ„‚cc 11103  โ„cr 11104  0cc0 11105  1c1 11106   + caddc 11108   ยท cmul 11110  +โˆžcpnf 11241   < clt 11244   โ‰ค cle 11245   โˆ’ cmin 11440   / cdiv 11867  โ„•cn 12208  [,)cico 13322  [,]cicc 13323  ...cfz 13480  ๐”ผcee 28581   Btwn cbtwn 28582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-er 8698  df-map 8817  df-en 8935  df-dom 8936  df-sdom 8937  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-z 12555  df-uz 12819  df-ico 13326  df-icc 13327  df-fz 13481  df-ee 28584  df-btwn 28585
This theorem is referenced by:  axcontlem5  28661  axcontlem9  28665  axcontlem10  28666
  Copyright terms: Public domain W3C validator