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

Theorem colinearalg 28695
Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 28690. (Contributed by Scott Fenton, 24-Jun-2013.)
Assertion
Ref Expression
colinearalg ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ((๐ด Btwn โŸจ๐ต, ๐ถโŸฉ โˆจ ๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โˆจ ๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
Distinct variable groups:   ๐‘–,๐‘,๐‘—   ๐ด,๐‘–,๐‘—   ๐ต,๐‘–,๐‘—   ๐ถ,๐‘–,๐‘—

Proof of Theorem colinearalg
Dummy variable ๐‘ is distinct from all other variables.
StepHypRef Expression
1 brbtwn2 28690 . . 3 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ด Btwn โŸจ๐ต, ๐ถโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
2 brbtwn2 28690 . . . . 5 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))))))
323comr 1123 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))))))
4 colinearalglem3 28693 . . . . . 6 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
543comr 1123 . . . . 5 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
65anbi2d 628 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))) โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
73, 6bitrd 279 . . 3 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
8 brbtwn2 28690 . . . . 5 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—))) = (((๐ดโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))))))
9 colinearalglem2 28692 . . . . . 6 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—))) = (((๐ดโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
109anbi2d 628 . . . . 5 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘)) โ†’ ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—))) = (((๐ดโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)))) โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
118, 10bitrd 279 . . . 4 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
12113coml 1125 . . 3 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
131, 7, 123orbi123d 1432 . 2 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ((๐ด Btwn โŸจ๐ต, ๐ถโŸฉ โˆจ ๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โˆจ ๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ) โ†” ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))))
14 fveecn 28687 . . . . . . . . . . . . 13 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
15 fveecn 28687 . . . . . . . . . . . . 13 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
16 subid 11495 . . . . . . . . . . . . . . . 16 ((๐ถโ€˜๐‘–) โˆˆ โ„‚ โ†’ ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) = 0)
1716oveq2d 7430 . . . . . . . . . . . . . . 15 ((๐ถโ€˜๐‘–) โˆˆ โ„‚ โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท 0))
1817adantl 481 . . . . . . . . . . . . . 14 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท 0))
19 subcl 11475 . . . . . . . . . . . . . . 15 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) โˆˆ โ„‚)
2019mul01d 11429 . . . . . . . . . . . . . 14 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท 0) = 0)
2118, 20eqtrd 2767 . . . . . . . . . . . . 13 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = 0)
2214, 15, 21syl2an 595 . . . . . . . . . . . 12 (((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘))) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = 0)
2322anandirs 678 . . . . . . . . . . 11 (((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = 0)
24 0le0 12329 . . . . . . . . . . 11 0 โ‰ค 0
2523, 24eqbrtrdi 5181 . . . . . . . . . 10 (((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)
2625ralrimiva 3141 . . . . . . . . 9 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)
27263adant1 1128 . . . . . . . 8 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)
28 fveq1 6890 . . . . . . . . . . . 12 (๐ถ = ๐ด โ†’ (๐ถโ€˜๐‘–) = (๐ดโ€˜๐‘–))
2928oveq2d 7430 . . . . . . . . . . 11 (๐ถ = ๐ด โ†’ ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) = ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))
3028oveq2d 7430 . . . . . . . . . . 11 (๐ถ = ๐ด โ†’ ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) = ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))
3129, 30oveq12d 7432 . . . . . . . . . 10 (๐ถ = ๐ด โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))
3231breq1d 5152 . . . . . . . . 9 (๐ถ = ๐ด โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
3332ralbidv 3172 . . . . . . . 8 (๐ถ = ๐ด โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
3427, 33syl5ibcom 244 . . . . . . 7 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ = ๐ด โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
35 3mix1 1328 . . . . . . 7 (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
3634, 35syl6 35 . . . . . 6 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ = ๐ด โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
3736a1dd 50 . . . . 5 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ = ๐ด โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))))
38 simp3 1136 . . . . . . . . 9 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ถ โˆˆ (๐”ผโ€˜๐‘))
39 simp1 1134 . . . . . . . . 9 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ด โˆˆ (๐”ผโ€˜๐‘))
40 eqeefv 28688 . . . . . . . . 9 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ = ๐ด โ†” โˆ€๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) = (๐ดโ€˜๐‘)))
4138, 39, 40syl2anc 583 . . . . . . . 8 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ = ๐ด โ†” โˆ€๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) = (๐ดโ€˜๐‘)))
4241necon3abid 2972 . . . . . . 7 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ โ‰  ๐ด โ†” ยฌ โˆ€๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) = (๐ดโ€˜๐‘)))
43 df-ne 2936 . . . . . . . . 9 ((๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘) โ†” ยฌ (๐ถโ€˜๐‘) = (๐ดโ€˜๐‘))
4443rexbii 3089 . . . . . . . 8 (โˆƒ๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘) โ†” โˆƒ๐‘ โˆˆ (1...๐‘) ยฌ (๐ถโ€˜๐‘) = (๐ดโ€˜๐‘))
45 rexnal 3095 . . . . . . . 8 (โˆƒ๐‘ โˆˆ (1...๐‘) ยฌ (๐ถโ€˜๐‘) = (๐ดโ€˜๐‘) โ†” ยฌ โˆ€๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) = (๐ดโ€˜๐‘))
4644, 45bitr2i 276 . . . . . . 7 (ยฌ โˆ€๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) = (๐ดโ€˜๐‘) โ†” โˆƒ๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))
4742, 46bitrdi 287 . . . . . 6 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ โ‰  ๐ด โ†” โˆƒ๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)))
48 ralcom 3281 . . . . . . . 8 (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” โˆ€๐‘— โˆˆ (1...๐‘)โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))
49 fveq2 6891 . . . . . . . . . . . . . . 15 (๐‘— = ๐‘ โ†’ (๐ถโ€˜๐‘—) = (๐ถโ€˜๐‘))
50 fveq2 6891 . . . . . . . . . . . . . . 15 (๐‘— = ๐‘ โ†’ (๐ดโ€˜๐‘—) = (๐ดโ€˜๐‘))
5149, 50oveq12d 7432 . . . . . . . . . . . . . 14 (๐‘— = ๐‘ โ†’ ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) = ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)))
5251oveq2d 7430 . . . . . . . . . . . . 13 (๐‘— = ๐‘ โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))))
53 fveq2 6891 . . . . . . . . . . . . . . 15 (๐‘— = ๐‘ โ†’ (๐ตโ€˜๐‘—) = (๐ตโ€˜๐‘))
5453, 50oveq12d 7432 . . . . . . . . . . . . . 14 (๐‘— = ๐‘ โ†’ ((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) = ((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)))
5554oveq1d 7429 . . . . . . . . . . . . 13 (๐‘— = ๐‘ โ†’ (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))
5652, 55eqeq12d 2743 . . . . . . . . . . . 12 (๐‘— = ๐‘ โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
5756ralbidv 3172 . . . . . . . . . . 11 (๐‘— = ๐‘ โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
5857rspcv 3603 . . . . . . . . . 10 (๐‘ โˆˆ (1...๐‘) โ†’ (โˆ€๐‘— โˆˆ (1...๐‘)โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
5958ad2antrl 727 . . . . . . . . 9 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘ โˆˆ (1...๐‘) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘— โˆˆ (1...๐‘)โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
60 fveere 28686 . . . . . . . . . . . . . 14 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„)
61603ad2antl1 1183 . . . . . . . . . . . . 13 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„)
62 fveere 28686 . . . . . . . . . . . . . 14 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘) โˆˆ โ„)
63623ad2antl2 1184 . . . . . . . . . . . . 13 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘) โˆˆ โ„)
64 fveere 28686 . . . . . . . . . . . . . 14 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„)
65643ad2antl3 1185 . . . . . . . . . . . . 13 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„)
6661, 63, 653jca 1126 . . . . . . . . . . . 12 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ ((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„))
6766anim1i 614 . . . . . . . . . . 11 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โˆˆ (1...๐‘)) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)))
6867anasss 466 . . . . . . . . . 10 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘ โˆˆ (1...๐‘) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)))
69 fveecn 28687 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
70693ad2antl1 1183 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
71143ad2antl2 1184 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
72153ad2antl3 1185 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
7370, 71, 723jca 1126 . . . . . . . . . . . . . 14 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚))
7473adantlr 714 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚))
75 recn 11214 . . . . . . . . . . . . . . . 16 ((๐ดโ€˜๐‘) โˆˆ โ„ โ†’ (๐ดโ€˜๐‘) โˆˆ โ„‚)
76 recn 11214 . . . . . . . . . . . . . . . 16 ((๐ตโ€˜๐‘) โˆˆ โ„ โ†’ (๐ตโ€˜๐‘) โˆˆ โ„‚)
77 recn 11214 . . . . . . . . . . . . . . . 16 ((๐ถโ€˜๐‘) โˆˆ โ„ โ†’ (๐ถโ€˜๐‘) โˆˆ โ„‚)
7875, 76, 773anim123i 1149 . . . . . . . . . . . . . . 15 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚))
7978adantr 480 . . . . . . . . . . . . . 14 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚))
8079ad2antlr 726 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚))
81 simplrr 777 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))
82 eqcom 2734 . . . . . . . . . . . . . 14 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†” (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) = (๐ตโ€˜๐‘–))
83 simp12 1202 . . . . . . . . . . . . . . . 16 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
84 simp11 1201 . . . . . . . . . . . . . . . 16 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
85 simp22 1205 . . . . . . . . . . . . . . . . . . 19 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ตโ€˜๐‘) โˆˆ โ„‚)
86 simp21 1204 . . . . . . . . . . . . . . . . . . 19 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„‚)
8785, 86subcld 11587 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โˆˆ โ„‚)
88 simp23 1206 . . . . . . . . . . . . . . . . . . 19 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„‚)
8988, 86subcld 11587 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โˆˆ โ„‚)
90 simpr3 1194 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚)) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„‚)
91 simpr1 1192 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚)) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„‚)
9290, 91subeq0ad 11597 . . . . . . . . . . . . . . . . . . . 20 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚)) โ†’ (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) = 0 โ†” (๐ถโ€˜๐‘) = (๐ดโ€˜๐‘)))
9392necon3bid 2980 . . . . . . . . . . . . . . . . . . 19 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚)) โ†’ (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โ‰  0 โ†” (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)))
9493biimp3ar 1467 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โ‰  0)
9587, 89, 94divcld 12006 . . . . . . . . . . . . . . . . 17 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โˆˆ โ„‚)
96 simp13 1203 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
9796, 84subcld 11587 . . . . . . . . . . . . . . . . 17 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) โˆˆ โ„‚)
9895, 97mulcld 11250 . . . . . . . . . . . . . . . 16 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โˆˆ โ„‚)
99 subadd2 11480 . . . . . . . . . . . . . . . . 17 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โˆˆ โ„‚) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) = (๐ตโ€˜๐‘–)))
10099bicomd 222 . . . . . . . . . . . . . . . 16 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โˆˆ โ„‚) โ†’ ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) = (๐ตโ€˜๐‘–) โ†” ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
10183, 84, 98, 100syl3anc 1369 . . . . . . . . . . . . . . 15 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) = (๐ตโ€˜๐‘–) โ†” ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
10287, 97, 89, 94div23d 12043 . . . . . . . . . . . . . . . 16 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))
103102eqeq2d 2738 . . . . . . . . . . . . . . 15 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โ†” ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
104 eqcom 2734 . . . . . . . . . . . . . . . 16 (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โ†” ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))
10587, 97mulcld 11250 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โˆˆ โ„‚)
10683, 84subcld 11587 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) โˆˆ โ„‚)
107105, 89, 106, 94divmuld 12028 . . . . . . . . . . . . . . . . 17 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) โ†” (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
10889, 106mulcomd 11251 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) = (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))))
109108eqeq1d 2729 . . . . . . . . . . . . . . . . 17 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
110107, 109bitrd 279 . . . . . . . . . . . . . . . 16 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
111104, 110bitrid 283 . . . . . . . . . . . . . . 15 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
112101, 103, 1113bitr2d 307 . . . . . . . . . . . . . 14 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) = (๐ตโ€˜๐‘–) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
11382, 112bitrid 283 . . . . . . . . . . . . 13 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
11474, 80, 81, 113syl3anc 1369 . . . . . . . . . . . 12 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
115114ralbidva 3170 . . . . . . . . . . 11 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
116 3simpb 1147 . . . . . . . . . . . 12 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)))
117 simpl2 1190 . . . . . . . . . . . . . 14 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ตโ€˜๐‘) โˆˆ โ„)
118 simpl1 1189 . . . . . . . . . . . . . 14 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„)
119117, 118resubcld 11658 . . . . . . . . . . . . 13 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โˆˆ โ„)
120 simpl3 1191 . . . . . . . . . . . . . 14 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„)
121120, 118resubcld 11658 . . . . . . . . . . . . 13 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โˆˆ โ„)
122 simp3 1136 . . . . . . . . . . . . . . . . 17 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„)
123122recnd 11258 . . . . . . . . . . . . . . . 16 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„‚)
124753ad2ant1 1131 . . . . . . . . . . . . . . . 16 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„‚)
125123, 124subeq0ad 11597 . . . . . . . . . . . . . . 15 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) = 0 โ†” (๐ถโ€˜๐‘) = (๐ดโ€˜๐‘)))
126125necon3bid 2980 . . . . . . . . . . . . . 14 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โ‰  0 โ†” (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)))
127126biimpar 477 . . . . . . . . . . . . 13 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โ‰  0)
128119, 121, 127redivcld 12058 . . . . . . . . . . . 12 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โˆˆ โ„)
129 colinearalglem4 28694 . . . . . . . . . . . . 13 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โˆˆ โ„) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
130 oveq1 7421 . . . . . . . . . . . . . . . . . 18 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)))
131130oveq1d 7429 . . . . . . . . . . . . . . . . 17 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) = (((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))
132131breq1d 5152 . . . . . . . . . . . . . . . 16 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†” (((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
133132ralimi 3078 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†” (((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
134 ralbi 3098 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†” (((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
135133, 134syl 17 . . . . . . . . . . . . . 14 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
136 oveq2 7422 . . . . . . . . . . . . . . . . . 18 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) = ((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))))
137 oveq2 7422 . . . . . . . . . . . . . . . . . 18 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) = ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))))
138136, 137oveq12d 7432 . . . . . . . . . . . . . . . . 17 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) = (((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))))
139138breq1d 5152 . . . . . . . . . . . . . . . 16 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0))
140139ralimi 3078 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0))
141 ralbi 3098 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0))
142140, 141syl 17 . . . . . . . . . . . . . 14 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0))
143 oveq1 7421 . . . . . . . . . . . . . . . . . 18 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) = ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–)))
144143oveq2d 7430 . . . . . . . . . . . . . . . . 17 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = (((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))))
145144breq1d 5152 . . . . . . . . . . . . . . . 16 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
146145ralimi 3078 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)((((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
147 ralbi 3098 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)((((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
148146, 147syl 17 . . . . . . . . . . . . . 14 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
149135, 142, 1483orbi123d 1432 . . . . . . . . . . . . 13 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
150129, 149syl5ibrcom 246 . . . . . . . . . . . 12 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โˆˆ โ„) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
151116, 128, 150syl2an 595 . . . . . . . . . . 11 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
152115, 151sylbird 260 . . . . . . . . . 10 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
15368, 152syldan 590 . . . . . . . . 9 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘ โˆˆ (1...๐‘) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
15459, 153syld 47 . . . . . . . 8 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘ โˆˆ (1...๐‘) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘— โˆˆ (1...๐‘)โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
15548, 154biimtrid 241 . . . . . . 7 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘ โˆˆ (1...๐‘) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
156155rexlimdvaa 3151 . . . . . 6 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆƒ๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))))
15747, 156sylbid 239 . . . . 5 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ โ‰  ๐ด โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))))
15837, 157pm2.61dne 3023 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
159158pm4.71rd 562 . . 3 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
160 andir 1007 . . . . 5 (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โ†” ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
161160orbi1i 912 . . . 4 ((((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))) โ†” (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
162 df-3or 1086 . . . . . 6 ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โ†” ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
163162anbi1i 623 . . . . 5 (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โ†” (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
164 andir 1007 . . . . 5 ((((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โ†” (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
165163, 164bitri 275 . . . 4 (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โ†” (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
166 df-3or 1086 . . . 4 (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))) โ†” (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
167161, 165, 1663bitr4i 303 . . 3 (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โ†” ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
168159, 167bitr2di 288 . 2 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
16913, 168bitrd 279 1 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ((๐ด Btwn โŸจ๐ต, ๐ถโŸฉ โˆจ ๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โˆจ ๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 846   โˆจ w3o 1084   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099   โ‰  wne 2935  โˆ€wral 3056  โˆƒwrex 3065  โŸจcop 4630   class class class wbr 5142  โ€˜cfv 6542  (class class class)co 7414  โ„‚cc 11122  โ„cr 11123  0cc0 11124  1c1 11125   + caddc 11127   ยท cmul 11129   โ‰ค cle 11265   โˆ’ cmin 11460   / cdiv 11887  ...cfz 13502  ๐”ผcee 28673   Btwn cbtwn 28674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  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 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7863  df-1st 7985  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8716  df-map 8836  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-sub 11462  df-neg 11463  df-div 11888  df-nn 12229  df-2 12291  df-n0 12489  df-z 12575  df-uz 12839  df-icc 13349  df-fz 13503  df-seq 13985  df-exp 14045  df-ee 28676  df-btwn 28677
This theorem is referenced by:  axlowdimlem6  28732
  Copyright terms: Public domain W3C validator