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

Theorem axcontlem7 28495
Description: Lemma for axcont 28501. 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 4079 . . . . 5 ๐ท โІ (๐”ผโ€˜๐‘)
32sseli 3977 . . . 4 (๐‘ƒ โˆˆ ๐ท โ†’ ๐‘ƒ โˆˆ (๐”ผโ€˜๐‘))
43ad2antrl 724 . . 3 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ ๐‘ƒ โˆˆ (๐”ผโ€˜๐‘))
5 simpll2 1211 . . 3 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
62sseli 3977 . . . 4 (๐‘„ โˆˆ ๐ท โ†’ ๐‘„ โˆˆ (๐”ผโ€˜๐‘))
76ad2antll 725 . . 3 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ ๐‘„ โˆˆ (๐”ผโ€˜๐‘))
8 brbtwn 28424 . . 3 ((๐‘ƒ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘„ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ƒ Btwn โŸจ๐‘, ๐‘„โŸฉ โ†” โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–)))))
94, 5, 7, 8syl3anc 1369 . 2 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ (๐‘ƒ Btwn โŸจ๐‘, ๐‘„โŸฉ โ†” โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–)))))
10 axcontlem7.2 . . . . 5 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
111, 10axcontlem6 28494 . . . 4 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘ƒ โˆˆ ๐ท) โ†’ ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)))))
121, 10axcontlem6 28494 . . . 4 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ๐‘„ โˆˆ ๐ท) โ†’ ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
1311, 12anim12dan 617 . . 3 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ƒ โˆˆ ๐ท โˆง ๐‘„ โˆˆ ๐ท)) โ†’ (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)))) โˆง ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
14 an4 652 . . . . 5 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)))) โˆง ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
15 r19.26 3109 . . . . . 6 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
1615anbi2i 621 . . . . 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 7419 . . . . . . . . . . 11 ((๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))) โ†’ (๐‘ก ยท (๐‘„โ€˜๐‘–)) = (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
2019oveq2d 7427 . . . . . . . . . 10 ((๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
2118, 20eqeqan12d 2744 . . . . . . . . 9 (((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†’ ((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))))
2221ralimi 3081 . . . . . . . 8 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))))
23 ralbi 3101 . . . . . . . 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 3176 . . . . . 6 (โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))))
26 simpll2 1211 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
27 fveecn 28427 . . . . . . . . . . . . 13 ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
2826, 27sylan 578 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
29 simpll3 1212 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
30 fveecn 28427 . . . . . . . . . . . . 13 ((๐‘ˆ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
3129, 30sylan 578 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
32 elicc01 13447 . . . . . . . . . . . . . . . 16 (๐‘ก โˆˆ (0[,]1) โ†” (๐‘ก โˆˆ โ„ โˆง 0 โ‰ค ๐‘ก โˆง ๐‘ก โ‰ค 1))
3332simp1bi 1143 . . . . . . . . . . . . . . 15 (๐‘ก โˆˆ (0[,]1) โ†’ ๐‘ก โˆˆ โ„)
3433recnd 11246 . . . . . . . . . . . . . 14 (๐‘ก โˆˆ (0[,]1) โ†’ ๐‘ก โˆˆ โ„‚)
3534ad2antll 725 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ๐‘ก โˆˆ โ„‚)
3635adantr 479 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ๐‘ก โˆˆ โ„‚)
37 elrege0 13435 . . . . . . . . . . . . . . . . 17 ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โ†” ((๐นโ€˜๐‘ƒ) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘ƒ)))
3837simplbi 496 . . . . . . . . . . . . . . . 16 ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„)
3938recnd 11246 . . . . . . . . . . . . . . 15 ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
4039adantr 479 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
4140ad2antrl 724 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
4241adantr 479 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
43 elrege0 13435 . . . . . . . . . . . . . . . . 17 ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โ†” ((๐นโ€˜๐‘„) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘„)))
4443simplbi 496 . . . . . . . . . . . . . . . 16 ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„)
4544recnd 11246 . . . . . . . . . . . . . . 15 ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
4645adantl 480 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
4746ad2antrl 724 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
4847adantr 479 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
49 ax-1cn 11170 . . . . . . . . . . . . . . . . 17 1 โˆˆ โ„‚
50 simpr1 1192 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ๐‘ก โˆˆ โ„‚)
51 simpr3 1194 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
5250, 51mulcld 11238 . . . . . . . . . . . . . . . . 17 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚)
53 subcl 11463 . . . . . . . . . . . . . . . . 17 ((1 โˆˆ โ„‚ โˆง (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚) โ†’ (1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆˆ โ„‚)
5449, 52, 53sylancr 585 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆˆ โ„‚)
55 subcl 11463 . . . . . . . . . . . . . . . . . . 19 ((1 โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚) โ†’ (1 โˆ’ (๐นโ€˜๐‘ƒ)) โˆˆ โ„‚)
5649, 55mpan 686 . . . . . . . . . . . . . . . . . 18 ((๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โ†’ (1 โˆ’ (๐นโ€˜๐‘ƒ)) โˆˆ โ„‚)
57563ad2ant2 1132 . . . . . . . . . . . . . . . . 17 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (1 โˆ’ (๐นโ€˜๐‘ƒ)) โˆˆ โ„‚)
5857adantl 480 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (1 โˆ’ (๐นโ€˜๐‘ƒ)) โˆˆ โ„‚)
59 simpll 763 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘โ€˜๐‘–) โˆˆ โ„‚)
6054, 58, 59subdird 11675 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆ’ (1 โˆ’ (๐นโ€˜๐‘ƒ))) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))))
61 simpr2 1193 . . . . . . . . . . . . . . . . 17 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
62 nnncan1 11500 . . . . . . . . . . . . . . . . 17 ((1 โˆˆ โ„‚ โˆง (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚) โ†’ ((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆ’ (1 โˆ’ (๐นโ€˜๐‘ƒ))) = ((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
6349, 52, 61, 62mp3an2i 1464 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆ’ (1 โˆ’ (๐นโ€˜๐‘ƒ))) = ((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
6463oveq1d 7426 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆ’ (1 โˆ’ (๐นโ€˜๐‘ƒ))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)))
65 subdi 11651 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ก โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) = ((๐‘ก ยท 1) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
6649, 65mp3an2 1447 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) = ((๐‘ก ยท 1) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
67 mulrid 11216 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ก โˆˆ โ„‚ โ†’ (๐‘ก ยท 1) = ๐‘ก)
6867adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (๐‘ก ยท 1) = ๐‘ก)
6968oveq1d 7426 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ ((๐‘ก ยท 1) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
7066, 69eqtrd 2770 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) = (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
7150, 51, 70syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) = (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
7271oveq2d 7427 . . . . . . . . . . . . . . . . . . 19 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ ๐‘ก) + (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„)))) = ((1 โˆ’ ๐‘ก) + (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„)))))
73 npncan 11485 . . . . . . . . . . . . . . . . . . . 20 ((1 โˆˆ โ„‚ โˆง ๐‘ก โˆˆ โ„‚ โˆง (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚) โ†’ ((1 โˆ’ ๐‘ก) + (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„)))) = (1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
7449, 50, 52, 73mp3an2i 1464 . . . . . . . . . . . . . . . . . . 19 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ ๐‘ก) + (๐‘ก โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„)))) = (1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))))
7572, 74eqtr2d 2771 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = ((1 โˆ’ ๐‘ก) + (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„)))))
7675oveq1d 7426 . . . . . . . . . . . . . . . . 17 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ ๐‘ก) + (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„)))) ยท (๐‘โ€˜๐‘–)))
77 subcl 11463 . . . . . . . . . . . . . . . . . . . . 21 ((1 โˆˆ โ„‚ โˆง ๐‘ก โˆˆ โ„‚) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
7849, 77mpan 686 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก โˆˆ โ„‚ โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
79783ad2ant1 1131 . . . . . . . . . . . . . . . . . . 19 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
8079adantl 480 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (1 โˆ’ ๐‘ก) โˆˆ โ„‚)
81 subcl 11463 . . . . . . . . . . . . . . . . . . . . . 22 ((1 โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (1 โˆ’ (๐นโ€˜๐‘„)) โˆˆ โ„‚)
8249, 81mpan 686 . . . . . . . . . . . . . . . . . . . . 21 ((๐นโ€˜๐‘„) โˆˆ โ„‚ โ†’ (1 โˆ’ (๐นโ€˜๐‘„)) โˆˆ โ„‚)
83823ad2ant3 1133 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚) โ†’ (1 โˆ’ (๐นโ€˜๐‘„)) โˆˆ โ„‚)
8483adantl 480 . . . . . . . . . . . . . . . . . . 19 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (1 โˆ’ (๐นโ€˜๐‘„)) โˆˆ โ„‚)
8550, 84mulcld 11238 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) โˆˆ โ„‚)
8680, 85, 59adddird 11243 . . . . . . . . . . . . . . . . 17 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ ๐‘ก) + (๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„)))) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + ((๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–))))
8750, 84, 59mulassd 11241 . . . . . . . . . . . . . . . . . 18 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–))))
8887oveq2d 7427 . . . . . . . . . . . . . . . . 17 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + ((๐‘ก ยท (1 โˆ’ (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))))
8976, 86, 883eqtrd 2774 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))))
9089oveq1d 7426 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))) = ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))))
9160, 64, 903eqtr3d 2778 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))))
92 simplr 765 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚)
9361, 52, 92subdird 11675 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ ((๐‘ก ยท (๐นโ€˜๐‘„)) ยท (๐‘ˆโ€˜๐‘–))))
9450, 51, 92mulassd 11241 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((๐‘ก ยท (๐นโ€˜๐‘„)) ยท (๐‘ˆโ€˜๐‘–)) = (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))
9594oveq2d 7427 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ ((๐‘ก ยท (๐นโ€˜๐‘„)) ยท (๐‘ˆโ€˜๐‘–))) = (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
9693, 95eqtrd 2770 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
9791, 96eqeq12d 2746 . . . . . . . . . . . . 13 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) โ†” ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))) = (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
9858, 59mulcld 11238 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
9961, 92mulcld 11238 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆˆ โ„‚)
10080, 59mulcld 11238 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
10184, 59mulcld 11238 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) โˆˆ โ„‚)
10250, 101mulcld 11238 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–))) โˆˆ โ„‚)
103100, 102addcld 11237 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) โˆˆ โ„‚)
10451, 92mulcld 11238 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)) โˆˆ โ„‚)
10550, 104mulcld 11238 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))) โˆˆ โ„‚)
10698, 99, 103, 105addsubeq4d 11626 . . . . . . . . . . . . 13 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†” ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) โˆ’ ((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–))) = (((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)) โˆ’ (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
107100, 102, 105addassd 11240 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + ((๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
10850, 101, 104adddid 11242 . . . . . . . . . . . . . . . 16 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) = ((๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))
109108oveq2d 7427 . . . . . . . . . . . . . . 15 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + ((๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
110107, 109eqtr4d 2773 . . . . . . . . . . . . . 14 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))))
111110eqeq2d 2741 . . . . . . . . . . . . 13 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = ((((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท ((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)))) + (๐‘ก ยท ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))) โ†” (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))))
11297, 106, 1113bitr2rd 307 . . . . . . . . . . . 12 ((((๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โˆง (๐‘ก โˆˆ โ„‚ โˆง (๐นโ€˜๐‘ƒ) โˆˆ โ„‚ โˆง (๐นโ€˜๐‘„) โˆˆ โ„‚)) โ†’ ((((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–))))
11328, 31, 36, 42, 48, 112syl23anc 1375 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–))))
114113ralbidva 3173 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–))))
11536, 48mulcld 11238 . . . . . . . . . . . . 13 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚)
11642, 115subcld 11575 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆˆ โ„‚)
117 mulcan1g 11871 . . . . . . . . . . . 12 ((((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) โˆˆ โ„‚ โˆง (๐‘โ€˜๐‘–) โˆˆ โ„‚ โˆง (๐‘ˆโ€˜๐‘–) โˆˆ โ„‚) โ†’ ((((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
118116, 28, 31, 117syl3anc 1369 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
119118ralbidva 3173 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘โ€˜๐‘–)) = (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) ยท (๐‘ˆโ€˜๐‘–)) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–))))
120 r19.32v 3189 . . . . . . . . . . 11 (โˆ€๐‘– โˆˆ (1...๐‘)(((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ (๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
121 simplr 765 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ๐‘ โ‰  ๐‘ˆ)
122121neneqd 2943 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ ยฌ ๐‘ = ๐‘ˆ)
123 biorf 933 . . . . . . . . . . . . . 14 (ยฌ ๐‘ = ๐‘ˆ โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โ†” (๐‘ = ๐‘ˆ โˆจ ((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0)))
124 orcom 866 . . . . . . . . . . . . . 14 ((๐‘ = ๐‘ˆ โˆจ ((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0) โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ ๐‘ = ๐‘ˆ))
125123, 124bitrdi 286 . . . . . . . . . . . . 13 (ยฌ ๐‘ = ๐‘ˆ โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ ๐‘ = ๐‘ˆ)))
126122, 125syl 17 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โ†” (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โˆจ ๐‘ = ๐‘ˆ)))
12735, 47mulcld 11238 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โˆˆ โ„‚)
12841, 127subeq0ad 11585 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (((๐นโ€˜๐‘ƒ) โˆ’ (๐‘ก ยท (๐นโ€˜๐‘„))) = 0 โ†” (๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
129 eqeefv 28428 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
1301293adant1 1128 . . . . . . . . . . . . . . 15 ((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
131130adantr 479 . . . . . . . . . . . . . 14 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
132131adantr 479 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1))) โ†’ (๐‘ = ๐‘ˆ โ†” โˆ€๐‘– โˆˆ (1...๐‘)(๐‘โ€˜๐‘–) = (๐‘ˆโ€˜๐‘–)))
133132orbi2d 912 . . . . . . . . . . . 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 466 . . . . . . . 8 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
138137rexbidva 3174 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
13933adantl 480 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ ๐‘ก โˆˆ โ„)
140 1red 11219 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ 1 โˆˆ โ„)
14143biimpi 215 . . . . . . . . . . . . . 14 ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โ†’ ((๐นโ€˜๐‘„) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘„)))
142141ad2antlr 723 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ ((๐นโ€˜๐‘„) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘„)))
14332simp3bi 1145 . . . . . . . . . . . . . 14 (๐‘ก โˆˆ (0[,]1) โ†’ ๐‘ก โ‰ค 1)
144143adantl 480 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ ๐‘ก โ‰ค 1)
145 lemul1a 12072 . . . . . . . . . . . . 13 (((๐‘ก โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง ((๐นโ€˜๐‘„) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘„))) โˆง ๐‘ก โ‰ค 1) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โ‰ค (1 ยท (๐นโ€˜๐‘„)))
146139, 140, 142, 144, 145syl31anc 1371 . . . . . . . . . . . 12 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โ‰ค (1 ยท (๐นโ€˜๐‘„)))
14745ad2antlr 723 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
148147mullidd 11236 . . . . . . . . . . . 12 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ (1 ยท (๐นโ€˜๐‘„)) = (๐นโ€˜๐‘„))
149146, 148breqtrd 5173 . . . . . . . . . . 11 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) โ‰ค (๐นโ€˜๐‘„))
150 breq1 5150 . . . . . . . . . . 11 ((๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)) โ†’ ((๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„) โ†” (๐‘ก ยท (๐นโ€˜๐‘„)) โ‰ค (๐นโ€˜๐‘„)))
151149, 150syl5ibrcom 246 . . . . . . . . . 10 ((((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง ๐‘ก โˆˆ (0[,]1)) โ†’ ((๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
152151rexlimdva 3153 . . . . . . . . 9 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
153 0elunit 13450 . . . . . . . . . . . . . 14 0 โˆˆ (0[,]1)
154 simpl 481 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) = 0 โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘ƒ) = 0)
15545mul02d 11416 . . . . . . . . . . . . . . . 16 ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โ†’ (0 ยท (๐นโ€˜๐‘„)) = 0)
156155adantl 480 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) = 0 โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (0 ยท (๐นโ€˜๐‘„)) = 0)
157154, 156eqtr4d 2773 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) = 0 โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘ƒ) = (0 ยท (๐นโ€˜๐‘„)))
158 oveq1 7418 . . . . . . . . . . . . . . 15 (๐‘ก = 0 โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) = (0 ยท (๐นโ€˜๐‘„)))
159158rspceeqv 3632 . . . . . . . . . . . . . 14 ((0 โˆˆ (0[,]1) โˆง (๐นโ€˜๐‘ƒ) = (0 ยท (๐นโ€˜๐‘„))) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))
160153, 157, 159sylancr 585 . . . . . . . . . . . . 13 (((๐นโ€˜๐‘ƒ) = 0 โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))
161160adantrl 712 . . . . . . . . . . . 12 (((๐นโ€˜๐‘ƒ) = 0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))
162161a1d 25 . . . . . . . . . . 11 (((๐นโ€˜๐‘ƒ) = 0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โ†’ ((๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
163162ex 411 . . . . . . . . . 10 ((๐นโ€˜๐‘ƒ) = 0 โ†’ (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ ((๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))))
164 simp3 1136 . . . . . . . . . . . . 13 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„))
16538adantr 479 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„)
1661653ad2ant2 1132 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„)
16737simprbi 495 . . . . . . . . . . . . . . . 16 ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โ†’ 0 โ‰ค (๐นโ€˜๐‘ƒ))
168167adantr 479 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ 0 โ‰ค (๐นโ€˜๐‘ƒ))
1691683ad2ant2 1132 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ 0 โ‰ค (๐นโ€˜๐‘ƒ))
17044adantl 480 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„)
1711703ad2ant2 1132 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„)
172 0red 11221 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ 0 โˆˆ โ„)
173 simp1 1134 . . . . . . . . . . . . . . . 16 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โ‰  0)
174166, 169, 173ne0gt0d 11355 . . . . . . . . . . . . . . 15 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ 0 < (๐นโ€˜๐‘ƒ))
175172, 166, 171, 174, 164ltletrd 11378 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ 0 < (๐นโ€˜๐‘„))
176 divelunit 13475 . . . . . . . . . . . . . 14 ((((๐นโ€˜๐‘ƒ) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘ƒ)) โˆง ((๐นโ€˜๐‘„) โˆˆ โ„ โˆง 0 < (๐นโ€˜๐‘„))) โ†’ (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) โˆˆ (0[,]1) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
177166, 169, 171, 175, 176syl22anc 835 . . . . . . . . . . . . 13 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) โˆˆ (0[,]1) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
178164, 177mpbird 256 . . . . . . . . . . . 12 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ ((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) โˆˆ (0[,]1))
179403ad2ant2 1132 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) โˆˆ โ„‚)
180463ad2ant2 1132 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘„) โˆˆ โ„‚)
181175gt0ne0d 11782 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘„) โ‰  0)
182179, 180, 181divcan1d 11995 . . . . . . . . . . . . 13 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) ยท (๐นโ€˜๐‘„)) = (๐นโ€˜๐‘ƒ))
183182eqcomd 2736 . . . . . . . . . . . 12 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ (๐นโ€˜๐‘ƒ) = (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) ยท (๐นโ€˜๐‘„)))
184 oveq1 7418 . . . . . . . . . . . . 13 (๐‘ก = ((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) โ†’ (๐‘ก ยท (๐นโ€˜๐‘„)) = (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) ยท (๐นโ€˜๐‘„)))
185184rspceeqv 3632 . . . . . . . . . . . 12 ((((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) โˆˆ (0[,]1) โˆง (๐นโ€˜๐‘ƒ) = (((๐นโ€˜๐‘ƒ) / (๐นโ€˜๐‘„)) ยท (๐นโ€˜๐‘„))) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))
186178, 183, 185syl2anc 582 . . . . . . . . . . 11 (((๐นโ€˜๐‘ƒ) โ‰  0 โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))
1871863exp 1117 . . . . . . . . . 10 ((๐นโ€˜๐‘ƒ) โ‰  0 โ†’ (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ ((๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)))))
188163, 187pm2.61ine 3023 . . . . . . . . 9 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ ((๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„) โ†’ โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„))))
189152, 188impbid 211 . . . . . . . 8 (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
190189adantl 480 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)(๐นโ€˜๐‘ƒ) = (๐‘ก ยท (๐นโ€˜๐‘„)) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
191138, 190bitrd 278 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
19225, 191sylan9bbr 509 . . . . 5 (((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง ((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž))) โˆง โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–))))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
193192anasss 465 . . . 4 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง (๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž)) โˆง โˆ€๐‘– โˆˆ (1...๐‘)((๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–))) โˆง (๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
19417, 193sylan2b 592 . . 3 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (((๐นโ€˜๐‘ƒ) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘ƒ)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘ƒ) ยท (๐‘ˆโ€˜๐‘–)))) โˆง ((๐นโ€˜๐‘„) โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘„โ€˜๐‘–) = (((1 โˆ’ (๐นโ€˜๐‘„)) ยท (๐‘โ€˜๐‘–)) + ((๐นโ€˜๐‘„) ยท (๐‘ˆโ€˜๐‘–)))))) โ†’ (โˆƒ๐‘ก โˆˆ (0[,]1)โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ƒโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘„โ€˜๐‘–))) โ†” (๐นโ€˜๐‘ƒ) โ‰ค (๐นโ€˜๐‘„)))
19513, 194syldan 589 . 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 394   โˆจ wo 843   โˆง w3a 1085   = wceq 1539   โˆˆ wcel 2104   โ‰  wne 2938  โˆ€wral 3059  โˆƒwrex 3068  {crab 3430  โŸจcop 4633   class class class wbr 5147  {copab 5209  โ€˜cfv 6542  (class class class)co 7411  โ„‚cc 11110  โ„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   ยท cmul 11117  +โˆžcpnf 11249   < clt 11252   โ‰ค cle 11253   โˆ’ cmin 11448   / cdiv 11875  โ„•cn 12216  [,)cico 13330  [,]cicc 13331  ...cfz 13488  ๐”ผcee 28413   Btwn cbtwn 28414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-z 12563  df-uz 12827  df-ico 13334  df-icc 13335  df-fz 13489  df-ee 28416  df-btwn 28417
This theorem is referenced by:  axcontlem9  28497
  Copyright terms: Public domain W3C validator