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

Theorem axcontlem7 28492
Description: Lemma for axcont 28498. Given two points in ๐ท, one preceeds the other iff its scaling constant is less than the other point's. (Contributed by Scott Fenton, 18-Jun-2013.)
Hypotheses
Ref Expression
axcontlem7.1 ๐ท = {๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆฃ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)}
axcontlem7.2 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
Assertion
Ref Expression
axcontlem7 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ (๐‘ƒ Btwn โŸจ๐‘, ๐‘„โŸฉ โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
Distinct variable groups:   ๐‘ก,๐ท,๐‘ฅ   ๐‘–,๐น,๐‘ก   ๐‘–,๐‘,๐‘ฅ,๐‘,๐‘ก   ๐‘ƒ,๐‘–,๐‘ก,๐‘ฅ   ๐‘„,๐‘–,๐‘ก,๐‘ฅ   ๐‘ˆ,๐‘–,๐‘,๐‘ก,๐‘ฅ   ๐‘–,๐‘,๐‘,๐‘ก,๐‘ฅ
Allowed substitution hints:   ๐ท(๐‘–,๐‘)   ๐‘ƒ(๐‘)   ๐‘„(๐‘)   ๐น(๐‘ฅ,๐‘)

Proof of Theorem axcontlem7
StepHypRef Expression
1 axcontlem7.1 . . . . . 6 ๐ท = {๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆฃ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)}
21ssrab3 4081 . . . . 5 ๐ท โŠ† (๐”ผโ€˜๐‘)
32sseli 3979 . . . 4 (๐‘ƒ โˆˆ ๐ท โ†’ ๐‘ƒ โˆˆ (๐”ผโ€˜๐‘))
43ad2antrl 725 . . 3 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ ๐‘ƒ โˆˆ (๐”ผโ€˜๐‘))
5 simpll2 1212 . . 3 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
62sseli 3979 . . . 4 (๐‘„ โˆˆ ๐ท โ†’ ๐‘„ โˆˆ (๐”ผโ€˜๐‘))
76ad2antll 726 . . 3 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ ๐‘„ โˆˆ (๐”ผโ€˜๐‘))
8 brbtwn 28421 . . 3 ((๐‘ƒ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘„ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ƒ Btwn โŸจ๐‘, ๐‘„โŸฉ โ†” โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–)))))
94, 5, 7, 8syl3anc 1370 . 2 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ (๐‘ƒ Btwn โŸจ๐‘, ๐‘„โŸฉ โ†” โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–)))))
10 axcontlem7.2 . . . . 5 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
111, 10axcontlem6 28491 . . . 4 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ƒ โˆˆ ๐ท) โ†’ ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)))))
121, 10axcontlem6 28491 . . . 4 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘„ โˆˆ ๐ท) โ†’ ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
1311, 12anim12dan 618 . . 3 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)))) โˆง ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
14 an4 653 . . . . 5 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)))) โˆง ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
15 r19.26 3110 . . . . . 6 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
1615anbi2i 622 . . . . 5 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
1714, 16bitr4i 277 . . . 4 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)))) โˆง ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
18 id 22 . . . . . . . . . 10 ((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โ†’ (๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))))
19 oveq2 7420 . . . . . . . . . . 11 ((๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))) โ†’ (๐‘ก ยท (๐‘„โ€˜๐‘–)) = (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
2019oveq2d 7428 . . . . . . . . . 10 ((๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
2118, 20eqeqan12d 2745 . . . . . . . . 9 (((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))))
2221ralimi 3082 . . . . . . . 8 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))))
23 ralbi 3102 . . . . . . . 8 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))))
2422, 23syl 17 . . . . . . 7 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))))
2524rexbidv 3177 . . . . . 6 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))))
26 simpll2 1212 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
27 fveecn 28424 . . . . . . . . . . . . 13 ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
2826, 27sylan 579 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
29 simpll3 1213 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
30 fveecn 28424 . . . . . . . . . . . . 13 ((๐‘ˆ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
3129, 30sylan 579 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
32 elicc01 13448 . . . . . . . . . . . . . . . 16 (๐‘ก โˆˆ (0[,]1) โ†” (๐‘ก โˆˆ โ„ โˆง 0 โ‰ค ๐‘ก โˆง ๐‘ก โ‰ค 1))
3332simp1bi 1144 . . . . . . . . . . . . . . 15 (๐‘ก โˆˆ (0[,]1) โ†’ ๐‘ก โˆˆ โ„)
3433recnd 11247 . . . . . . . . . . . . . 14 (๐‘ก โˆˆ (0[,]1) โ†’ ๐‘ก โˆˆ โ„‚)
3534ad2antll 726 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ๐‘ก โˆˆ โ„‚)
3635adantr 480 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ก โˆˆ โ„‚)
37 elrege0 13436 . . . . . . . . . . . . . . . . 17 ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โ†” ((๐นโ€˜๐‘ƒ) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘ƒ)))
3837simplbi 497 . . . . . . . . . . . . . . . 16 ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„)
3938recnd 11247 . . . . . . . . . . . . . . 15 ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
4039adantr 480 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
4140ad2antrl 725 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
4241adantr 480 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
43 elrege0 13436 . . . . . . . . . . . . . . . . 17 ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โ†” ((๐นโ€˜๐‘„) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘„)))
4443simplbi 497 . . . . . . . . . . . . . . . 16 ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„)
4544recnd 11247 . . . . . . . . . . . . . . 15 ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
4645adantl 481 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
4746ad2antrl 725 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
4847adantr 480 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
49 ax-1cn 11171 . . . . . . . . . . . . . . . . 17 1 โˆˆ โ„‚
50 simpr1 1193 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ๐‘ก โˆˆ โ„‚)
51 simpr3 1195 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
5250, 51mulcld 11239 . . . . . . . . . . . . . . . . 17 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚)
53 subcl 11464 . . . . . . . . . . . . . . . . 17 ((1 โˆˆ โ„‚ โˆง (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚) โ†’ (1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆˆ โ„‚)
5449, 52, 53sylancr 586 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆˆ โ„‚)
55 subcl 11464 . . . . . . . . . . . . . . . . . . 19 ((1 โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚) โ†’ (1 โˆ’ (๐นโ€˜๐‘ƒ)) โˆˆ โ„‚)
5649, 55mpan 687 . . . . . . . . . . . . . . . . . 18 ((๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โ†’ (1 โˆ’ (๐นโ€˜๐‘ƒ)) โˆˆ โ„‚)
57563ad2ant2 1133 . . . . . . . . . . . . . . . . 17 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (1 โˆ’ (๐นโ€˜๐‘ƒ)) โˆˆ โ„‚)
5857adantl 481 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (1 โˆ’ (๐นโ€˜๐‘ƒ)) โˆˆ โ„‚)
59 simpll 764 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
6054, 58, 59subdird 11676 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆ’ (1 โˆ’ (๐นโ€˜๐‘ƒ))) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))))
61 simpr2 1194 . . . . . . . . . . . . . . . . 17 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
62 nnncan1 11501 . . . . . . . . . . . . . . . . 17 ((1 โˆˆ โ„‚ โˆง (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚) โ†’ ((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆ’ (1 โˆ’ (๐นโ€˜๐‘ƒ))) = ((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
6349, 52, 61, 62mp3an2i 1465 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆ’ (1 โˆ’ (๐นโ€˜๐‘ƒ))) = ((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
6463oveq1d 7427 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆ’ (1 โˆ’ (๐นโ€˜๐‘ƒ))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)))
65 subdi 11652 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ก โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) = ((๐‘ก ยท 1) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
6649, 65mp3an2 1448 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) = ((๐‘ก ยท 1) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
67 mulrid 11217 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ก โˆˆ โ„‚ โ†’ (๐‘ก ยท 1) = ๐‘ก)
6867adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (๐‘ก ยท 1) = ๐‘ก)
6968oveq1d 7427 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ ((๐‘ก ยท 1) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
7066, 69eqtrd 2771 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) = (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
7150, 51, 70syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) = (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
7271oveq2d 7428 . . . . . . . . . . . . . . . . . . 19 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ ๐‘ก) + (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„)))) = ((1 โˆ’ ๐‘ก) + (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„)))))
73 npncan 11486 . . . . . . . . . . . . . . . . . . . 20 ((1 โˆˆ โ„‚ โˆง ๐‘ก โˆˆ โ„‚ โˆง (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚) โ†’ ((1 โˆ’ ๐‘ก) + (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„)))) = (1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
7449, 50, 52, 73mp3an2i 1465 . . . . . . . . . . . . . . . . . . 19 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ ๐‘ก) + (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„)))) = (1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
7572, 74eqtr2d 2772 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = ((1 โˆ’ ๐‘ก) + (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„)))))
7675oveq1d 7427 . . . . . . . . . . . . . . . . 17 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ ๐‘ก) + (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„)))) ยท (๐‘โ€˜๐‘–)))
77 subcl 11464 . . . . . . . . . . . . . . . . . . . . 21 ((1 โˆˆ โ„‚ โˆง ๐‘ก โˆˆ โ„‚) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
7849, 77mpan 687 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก โˆˆ โ„‚ โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
79783ad2ant1 1132 . . . . . . . . . . . . . . . . . . 19 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
8079adantl 481 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
81 subcl 11464 . . . . . . . . . . . . . . . . . . . . . 22 ((1 โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (1 โˆ’ (๐นโ€˜๐‘„)) โˆˆ โ„‚)
8249, 81mpan 687 . . . . . . . . . . . . . . . . . . . . 21 ((๐นโ€˜๐‘„) โˆˆ โ„‚ โ†’ (1 โˆ’ (๐นโ€˜๐‘„)) โˆˆ โ„‚)
83823ad2ant3 1134 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (1 โˆ’ (๐นโ€˜๐‘„)) โˆˆ โ„‚)
8483adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (1 โˆ’ (๐นโ€˜๐‘„)) โˆˆ โ„‚)
8550, 84mulcld 11239 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) โˆˆ โ„‚)
8680, 85, 59adddird 11244 . . . . . . . . . . . . . . . . 17 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ ๐‘ก) + (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„)))) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + ((๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–))))
8750, 84, 59mulassd 11242 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–))))
8887oveq2d 7428 . . . . . . . . . . . . . . . . 17 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + ((๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))))
8976, 86, 883eqtrd 2775 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))))
9089oveq1d 7427 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))) = ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))))
9160, 64, 903eqtr3d 2779 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))))
92 simplr 766 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
9361, 52, 92subdird 11676 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ ((๐‘ก ยท (๐นโ€˜๐‘„)) ยท (๐‘ˆโ€˜๐‘–))))
9450, 51, 92mulassd 11242 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((๐‘ก ยท (๐นโ€˜๐‘„)) ยท (๐‘ˆโ€˜๐‘–)) = (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))
9594oveq2d 7428 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ ((๐‘ก ยท (๐นโ€˜๐‘„)) ยท (๐‘ˆโ€˜๐‘–))) = (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
9693, 95eqtrd 2771 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
9791, 96eqeq12d 2747 . . . . . . . . . . . . 13 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) โ†” ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))) = (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
9858, 59mulcld 11239 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
9961, 92mulcld 11239 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆˆ โ„‚)
10080, 59mulcld 11239 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
10184, 59mulcld 11239 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
10250, 101mulcld 11239 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–))) โˆˆ โ„‚)
103100, 102addcld 11238 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) โˆˆ โ„‚)
10451, 92mulcld 11239 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)) โˆˆ โ„‚)
10550, 104mulcld 11239 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))) โˆˆ โ„‚)
10698, 99, 103, 105addsubeq4d 11627 . . . . . . . . . . . . 13 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†” ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))) = (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
107100, 102, 105addassd 11241 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + ((๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
10850, 101, 104adddid 11243 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) = ((๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
109108oveq2d 7428 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + ((๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
110107, 109eqtr4d 2774 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
111110eqeq2d 2742 . . . . . . . . . . . . 13 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†” (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))))
11297, 106, 1113bitr2rd 307 . . . . . . . . . . . 12 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–))))
11328, 31, 36, 42, 48, 112syl23anc 1376 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–))))
114113ralbidva 3174 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–))))
11536, 48mulcld 11239 . . . . . . . . . . . . 13 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚)
11642, 115subcld 11576 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆˆ โ„‚)
117 mulcan1g 11872 . . . . . . . . . . . 12 ((((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โ†’ ((((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
118116, 28, 31, 117syl3anc 1370 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
119118ralbidva 3174 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
120 r19.32v 3190 . . . . . . . . . . 11 (โˆ€๐‘– โˆˆ (1...๐‘)(((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
121 simplr 766 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ๐‘ โ‰  ๐‘ˆ)
122121neneqd 2944 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ยฌ ๐‘ = ๐‘ˆ)
123 biorf 934 . . . . . . . . . . . . . 14 (ยฌ ๐‘ = ๐‘ˆ โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โ†” (๐‘ = ๐‘ˆ โˆจ ((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0)))
124 orcom 867 . . . . . . . . . . . . . 14 ((๐‘ = ๐‘ˆ โˆจ ((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ ๐‘ = ๐‘ˆ))
125123, 124bitrdi 286 . . . . . . . . . . . . 13 (ยฌ ๐‘ = ๐‘ˆ โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ ๐‘ = ๐‘ˆ)))
126122, 125syl 17 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ ๐‘ = ๐‘ˆ)))
12735, 47mulcld 11239 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚)
12841, 127subeq0ad 11586 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โ†” (๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
129 eqeefv 28425 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
1301293adant1 1129 . . . . . . . . . . . . . . 15 ((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
131130adantr 480 . . . . . . . . . . . . . 14 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
132131adantr 480 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
133132orbi2d 913 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ((((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ ๐‘ = ๐‘ˆ) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
134126, 128, 1333bitr3rd 309 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ((((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)) โ†” (๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
135120, 134bitrid 282 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)) โ†” (๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
136114, 119, 1353bitrd 304 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
137136anassrs 467 . . . . . . . 8 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
138137rexbidva 3175 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
13933adantl 481 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ ๐‘ก โˆˆ โ„)
140 1red 11220 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ 1 โˆˆ โ„)
14143biimpi 215 . . . . . . . . . . . . . 14 ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โ†’ ((๐นโ€˜๐‘„) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘„)))
142141ad2antlr 724 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ ((๐นโ€˜๐‘„) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘„)))
14332simp3bi 1146 . . . . . . . . . . . . . 14 (๐‘ก โˆˆ (0[,]1) โ†’ ๐‘ก โ‰ค 1)
144143adantl 481 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ ๐‘ก โ‰ค 1)
145 lemul1a 12073 . . . . . . . . . . . . 13 (((๐‘ก โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง ((๐นโ€˜๐‘„) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘„))) โˆง ๐‘ก โ‰ค 1) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โ‰ค (1 ยท (๐นโ€˜๐‘„)))
146139, 140, 142, 144, 145syl31anc 1372 . . . . . . . . . . . 12 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โ‰ค (1 ยท (๐นโ€˜๐‘„)))
14745ad2antlr 724 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
148147mullidd 11237 . . . . . . . . . . . 12 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ (1 ยท (๐นโ€˜๐‘„)) = (๐นโ€˜๐‘„))
149146, 148breqtrd 5175 . . . . . . . . . . 11 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โ‰ค (๐นโ€˜๐‘„))
150 breq1 5152 . . . . . . . . . . 11 ((๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)) โ†’ ((๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„) โ†” (๐‘ก ยท (๐นโ€˜๐‘„)) โ‰ค (๐นโ€˜๐‘„)))
151149, 150syl5ibrcom 246 . . . . . . . . . 10 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ ((๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
152151rexlimdva 3154 . . . . . . . . 9 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
153 0elunit 13451 . . . . . . . . . . . . . 14 0 โˆˆ (0[,]1)
154 simpl 482 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) = 0 โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘ƒ) = 0)
15545mul02d 11417 . . . . . . . . . . . . . . . 16 ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โ†’ (0 ยท (๐นโ€˜๐‘„)) = 0)
156155adantl 481 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) = 0 โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (0 ยท (๐นโ€˜๐‘„)) = 0)
157154, 156eqtr4d 2774 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) = 0 โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘ƒ) = (0 ยท (๐นโ€˜๐‘„)))
158 oveq1 7419 . . . . . . . . . . . . . . 15 (๐‘ก = 0 โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) = (0 ยท (๐นโ€˜๐‘„)))
159158rspceeqv 3634 . . . . . . . . . . . . . 14 ((0 โˆˆ (0[,]1) โˆง (๐นโ€˜๐‘ƒ) = (0 ยท (๐นโ€˜๐‘„))) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))
160153, 157, 159sylancr 586 . . . . . . . . . . . . 13 (((๐นโ€˜๐‘ƒ) = 0 โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))
161160adantrl 713 . . . . . . . . . . . 12 (((๐นโ€˜๐‘ƒ) = 0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))
162161a1d 25 . . . . . . . . . . 11 (((๐นโ€˜๐‘ƒ) = 0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โ†’ ((๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
163162ex 412 . . . . . . . . . 10 ((๐นโ€˜๐‘ƒ) = 0 โ†’ (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ ((๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))))
164 simp3 1137 . . . . . . . . . . . . 13 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„))
16538adantr 480 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„)
1661653ad2ant2 1133 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„)
16737simprbi 496 . . . . . . . . . . . . . . . 16 ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โ†’ 0 โ‰ค (๐นโ€˜๐‘ƒ))
168167adantr 480 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ 0 โ‰ค (๐นโ€˜๐‘ƒ))
1691683ad2ant2 1133 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ 0 โ‰ค (๐นโ€˜๐‘ƒ))
17044adantl 481 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„)
1711703ad2ant2 1133 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„)
172 0red 11222 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ 0 โˆˆ โ„)
173 simp1 1135 . . . . . . . . . . . . . . . 16 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โ‰  0)
174166, 169, 173ne0gt0d 11356 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ 0 < (๐นโ€˜๐‘ƒ))
175172, 166, 171, 174, 164ltletrd 11379 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ 0 < (๐นโ€˜๐‘„))
176 divelunit 13476 . . . . . . . . . . . . . 14 ((((๐นโ€˜๐‘ƒ) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘ƒ)) โˆง ((๐นโ€˜๐‘„) โˆˆ โ„ โˆง 0 < (๐นโ€˜๐‘„))) โ†’ (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) โˆˆ (0[,]1) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
177166, 169, 171, 175, 176syl22anc 836 . . . . . . . . . . . . 13 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) โˆˆ (0[,]1) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
178164, 177mpbird 256 . . . . . . . . . . . 12 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ ((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) โˆˆ (0[,]1))
179403ad2ant2 1133 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
180463ad2ant2 1133 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
181175gt0ne0d 11783 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘„) โ‰  0)
182179, 180, 181divcan1d 11996 . . . . . . . . . . . . 13 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) ยท (๐นโ€˜๐‘„)) = (๐นโ€˜๐‘ƒ))
183182eqcomd 2737 . . . . . . . . . . . 12 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) = (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) ยท (๐นโ€˜๐‘„)))
184 oveq1 7419 . . . . . . . . . . . . 13 (๐‘ก = ((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) = (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) ยท (๐นโ€˜๐‘„)))
185184rspceeqv 3634 . . . . . . . . . . . 12 ((((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) โˆˆ (0[,]1) โˆง (๐นโ€˜๐‘ƒ) = (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) ยท (๐นโ€˜๐‘„))) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))
186178, 183, 185syl2anc 583 . . . . . . . . . . 11 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))
1871863exp 1118 . . . . . . . . . 10 ((๐นโ€˜๐‘ƒ) โ‰  0 โ†’ (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ ((๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))))
188163, 187pm2.61ine 3024 . . . . . . . . 9 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ ((๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
189152, 188impbid 211 . . . . . . . 8 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
190189adantl 481 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
191138, 190bitrd 278 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
19225, 191sylan9bbr 510 . . . . 5 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
193192anasss 466 . . . 4 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
19417, 193sylan2b 593 . . 3 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)))) โˆง ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
19513, 194syldan 590 . 2 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
1969, 195bitrd 278 1 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ (๐‘ƒ Btwn โŸจ๐‘, ๐‘„โŸฉ โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆง w3a 1086   = wceq 1540   โˆˆ wcel 2105   โ‰  wne 2939  โˆ€wral 3060  โˆƒwrex 3069  {crab 3431  โŸจcop 4635   class class class wbr 5149  {copab 5211  โ€˜cfv 6544  (class class class)co 7412  โ„‚cc 11111  โ„cr 11112  0cc0 11113  1c1 11114   + caddc 11116   ยท cmul 11118  +โˆžcpnf 11250   < clt 11253   โ‰ค cle 11254   โˆ’ cmin 11449   / cdiv 11876  โ„•cn 12217  [,)cico 13331  [,]cicc 13332  ...cfz 13489  ๐”ผcee 28410   Btwn cbtwn 28411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-1st 7978  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-er 8706  df-map 8825  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-z 12564  df-uz 12828  df-ico 13335  df-icc 13336  df-fz 13490  df-ee 28413  df-btwn 28414
This theorem is referenced by:  axcontlem9  28494
  Copyright terms: Public domain W3C validator