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

Theorem colinearalg 28760
Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 28755. (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 28755 . . 3 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ด Btwn โŸจ๐ต, ๐ถโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
2 brbtwn2 28755 . . . . 5 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))))))
323comr 1122 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))))))
4 colinearalglem3 28758 . . . . . 6 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
543comr 1122 . . . . 5 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
65anbi2d 628 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))) โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
73, 6bitrd 278 . . 3 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
8 brbtwn2 28755 . . . . 5 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—))) = (((๐ดโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))))))
9 colinearalglem2 28757 . . . . . 6 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—))) = (((๐ดโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
109anbi2d 628 . . . . 5 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘)) โ†’ ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—))) = (((๐ดโ€˜๐‘—) โˆ’ (๐ถโ€˜๐‘—)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)))) โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
118, 10bitrd 278 . . . 4 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
12113coml 1124 . . 3 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ โ†” (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
131, 7, 123orbi123d 1431 . 2 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ((๐ด Btwn โŸจ๐ต, ๐ถโŸฉ โˆจ ๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โˆจ ๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ) โ†” ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))))
14 fveecn 28752 . . . . . . . . . . . . 13 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
15 fveecn 28752 . . . . . . . . . . . . 13 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
16 subid 11504 . . . . . . . . . . . . . . . 16 ((๐ถโ€˜๐‘–) โˆˆ โ„‚ โ†’ ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) = 0)
1716oveq2d 7429 . . . . . . . . . . . . . . 15 ((๐ถโ€˜๐‘–) โˆˆ โ„‚ โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท 0))
1817adantl 480 . . . . . . . . . . . . . 14 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท 0))
19 subcl 11484 . . . . . . . . . . . . . . 15 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) โˆˆ โ„‚)
2019mul01d 11438 . . . . . . . . . . . . . 14 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท 0) = 0)
2118, 20eqtrd 2765 . . . . . . . . . . . . 13 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = 0)
2214, 15, 21syl2an 594 . . . . . . . . . . . 12 (((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โˆง (๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘))) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = 0)
2322anandirs 677 . . . . . . . . . . 11 (((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = 0)
24 0le0 12338 . . . . . . . . . . 11 0 โ‰ค 0
2523, 24eqbrtrdi 5183 . . . . . . . . . 10 (((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)
2625ralrimiva 3136 . . . . . . . . 9 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)
27263adant1 1127 . . . . . . . 8 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)
28 fveq1 6889 . . . . . . . . . . . 12 (๐ถ = ๐ด โ†’ (๐ถโ€˜๐‘–) = (๐ดโ€˜๐‘–))
2928oveq2d 7429 . . . . . . . . . . 11 (๐ถ = ๐ด โ†’ ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) = ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))
3028oveq2d 7429 . . . . . . . . . . 11 (๐ถ = ๐ด โ†’ ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) = ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))
3129, 30oveq12d 7431 . . . . . . . . . 10 (๐ถ = ๐ด โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))
3231breq1d 5154 . . . . . . . . 9 (๐ถ = ๐ด โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
3332ralbidv 3168 . . . . . . . 8 (๐ถ = ๐ด โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
3427, 33syl5ibcom 244 . . . . . . 7 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ = ๐ด โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
35 3mix1 1327 . . . . . . 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 1135 . . . . . . . . 9 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ถ โˆˆ (๐”ผโ€˜๐‘))
39 simp1 1133 . . . . . . . . 9 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ด โˆˆ (๐”ผโ€˜๐‘))
40 eqeefv 28753 . . . . . . . . 9 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ด โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ = ๐ด โ†” โˆ€๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) = (๐ดโ€˜๐‘)))
4138, 39, 40syl2anc 582 . . . . . . . 8 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ = ๐ด โ†” โˆ€๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) = (๐ดโ€˜๐‘)))
4241necon3abid 2967 . . . . . . 7 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ โ‰  ๐ด โ†” ยฌ โˆ€๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) = (๐ดโ€˜๐‘)))
43 df-ne 2931 . . . . . . . . 9 ((๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘) โ†” ยฌ (๐ถโ€˜๐‘) = (๐ดโ€˜๐‘))
4443rexbii 3084 . . . . . . . 8 (โˆƒ๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘) โ†” โˆƒ๐‘ โˆˆ (1...๐‘) ยฌ (๐ถโ€˜๐‘) = (๐ดโ€˜๐‘))
45 rexnal 3090 . . . . . . . 8 (โˆƒ๐‘ โˆˆ (1...๐‘) ยฌ (๐ถโ€˜๐‘) = (๐ดโ€˜๐‘) โ†” ยฌ โˆ€๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) = (๐ดโ€˜๐‘))
4644, 45bitr2i 275 . . . . . . 7 (ยฌ โˆ€๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) = (๐ดโ€˜๐‘) โ†” โˆƒ๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))
4742, 46bitrdi 286 . . . . . 6 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ถ โ‰  ๐ด โ†” โˆƒ๐‘ โˆˆ (1...๐‘)(๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)))
48 ralcom 3277 . . . . . . . 8 (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” โˆ€๐‘— โˆˆ (1...๐‘)โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))
49 fveq2 6890 . . . . . . . . . . . . . . 15 (๐‘— = ๐‘ โ†’ (๐ถโ€˜๐‘—) = (๐ถโ€˜๐‘))
50 fveq2 6890 . . . . . . . . . . . . . . 15 (๐‘— = ๐‘ โ†’ (๐ดโ€˜๐‘—) = (๐ดโ€˜๐‘))
5149, 50oveq12d 7431 . . . . . . . . . . . . . 14 (๐‘— = ๐‘ โ†’ ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) = ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)))
5251oveq2d 7429 . . . . . . . . . . . . 13 (๐‘— = ๐‘ โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))))
53 fveq2 6890 . . . . . . . . . . . . . . 15 (๐‘— = ๐‘ โ†’ (๐ตโ€˜๐‘—) = (๐ตโ€˜๐‘))
5453, 50oveq12d 7431 . . . . . . . . . . . . . 14 (๐‘— = ๐‘ โ†’ ((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) = ((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)))
5554oveq1d 7428 . . . . . . . . . . . . 13 (๐‘— = ๐‘ โ†’ (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))
5652, 55eqeq12d 2741 . . . . . . . . . . . 12 (๐‘— = ๐‘ โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
5756ralbidv 3168 . . . . . . . . . . 11 (๐‘— = ๐‘ โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
5857rspcv 3599 . . . . . . . . . 10 (๐‘ โˆˆ (1...๐‘) โ†’ (โˆ€๐‘— โˆˆ (1...๐‘)โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
5958ad2antrl 726 . . . . . . . . 9 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘ โˆˆ (1...๐‘) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘— โˆˆ (1...๐‘)โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
60 fveere 28751 . . . . . . . . . . . . . 14 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„)
61603ad2antl1 1182 . . . . . . . . . . . . 13 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„)
62 fveere 28751 . . . . . . . . . . . . . 14 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘) โˆˆ โ„)
63623ad2antl2 1183 . . . . . . . . . . . . 13 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘) โˆˆ โ„)
64 fveere 28751 . . . . . . . . . . . . . 14 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„)
65643ad2antl3 1184 . . . . . . . . . . . . 13 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„)
6661, 63, 653jca 1125 . . . . . . . . . . . 12 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โˆˆ (1...๐‘)) โ†’ ((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„))
6766anim1i 613 . . . . . . . . . . 11 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โˆˆ (1...๐‘)) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)))
6867anasss 465 . . . . . . . . . 10 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘ โˆˆ (1...๐‘) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)))
69 fveecn 28752 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
70693ad2antl1 1182 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
71143ad2antl2 1183 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
72153ad2antl3 1184 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
7370, 71, 723jca 1125 . . . . . . . . . . . . . 14 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚))
7473adantlr 713 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚))
75 recn 11223 . . . . . . . . . . . . . . . 16 ((๐ดโ€˜๐‘) โˆˆ โ„ โ†’ (๐ดโ€˜๐‘) โˆˆ โ„‚)
76 recn 11223 . . . . . . . . . . . . . . . 16 ((๐ตโ€˜๐‘) โˆˆ โ„ โ†’ (๐ตโ€˜๐‘) โˆˆ โ„‚)
77 recn 11223 . . . . . . . . . . . . . . . 16 ((๐ถโ€˜๐‘) โˆˆ โ„ โ†’ (๐ถโ€˜๐‘) โˆˆ โ„‚)
7875, 76, 773anim123i 1148 . . . . . . . . . . . . . . 15 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚))
7978adantr 479 . . . . . . . . . . . . . 14 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚))
8079ad2antlr 725 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚))
81 simplrr 776 . . . . . . . . . . . . 13 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))
82 eqcom 2732 . . . . . . . . . . . . . 14 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†” (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) = (๐ตโ€˜๐‘–))
83 simp12 1201 . . . . . . . . . . . . . . . 16 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
84 simp11 1200 . . . . . . . . . . . . . . . 16 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
85 simp22 1204 . . . . . . . . . . . . . . . . . . 19 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ตโ€˜๐‘) โˆˆ โ„‚)
86 simp21 1203 . . . . . . . . . . . . . . . . . . 19 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„‚)
8785, 86subcld 11596 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โˆˆ โ„‚)
88 simp23 1205 . . . . . . . . . . . . . . . . . . 19 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„‚)
8988, 86subcld 11596 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โˆˆ โ„‚)
90 simpr3 1193 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚)) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„‚)
91 simpr1 1191 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚)) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„‚)
9290, 91subeq0ad 11606 . . . . . . . . . . . . . . . . . . . 20 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚)) โ†’ (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) = 0 โ†” (๐ถโ€˜๐‘) = (๐ดโ€˜๐‘)))
9392necon3bid 2975 . . . . . . . . . . . . . . . . . . 19 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚)) โ†’ (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โ‰  0 โ†” (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)))
9493biimp3ar 1466 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โ‰  0)
9587, 89, 94divcld 12015 . . . . . . . . . . . . . . . . 17 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โˆˆ โ„‚)
96 simp13 1202 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
9796, 84subcld 11596 . . . . . . . . . . . . . . . . 17 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) โˆˆ โ„‚)
9895, 97mulcld 11259 . . . . . . . . . . . . . . . 16 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โˆˆ โ„‚)
99 subadd2 11489 . . . . . . . . . . . . . . . . 17 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โˆˆ โ„‚) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) = (๐ตโ€˜๐‘–)))
10099bicomd 222 . . . . . . . . . . . . . . . 16 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โˆˆ โ„‚) โ†’ ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) = (๐ตโ€˜๐‘–) โ†” ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
10183, 84, 98, 100syl3anc 1368 . . . . . . . . . . . . . . 15 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) = (๐ตโ€˜๐‘–) โ†” ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
10287, 97, 89, 94div23d 12052 . . . . . . . . . . . . . . . 16 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))
103102eqeq2d 2736 . . . . . . . . . . . . . . 15 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โ†” ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
104 eqcom 2732 . . . . . . . . . . . . . . . 16 (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โ†” ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))
10587, 97mulcld 11259 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โˆˆ โ„‚)
10683, 84subcld 11596 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) โˆˆ โ„‚)
107105, 89, 106, 94divmuld 12037 . . . . . . . . . . . . . . . . 17 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) โ†” (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
10889, 106mulcomd 11260 . . . . . . . . . . . . . . . . . 18 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) = (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))))
109108eqeq1d 2727 . . . . . . . . . . . . . . . . 17 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
110107, 109bitrd 278 . . . . . . . . . . . . . . . 16 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
111104, 110bitrid 282 . . . . . . . . . . . . . . 15 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
112101, 103, 1113bitr2d 306 . . . . . . . . . . . . . 14 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) = (๐ตโ€˜๐‘–) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
11382, 112bitrid 282 . . . . . . . . . . . . 13 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘) โˆˆ โ„‚) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
11474, 80, 81, 113syl3anc 1368 . . . . . . . . . . . 12 ((((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†” (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
115114ralbidva 3166 . . . . . . . . . . 11 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
116 3simpb 1146 . . . . . . . . . . . 12 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)))
117 simpl2 1189 . . . . . . . . . . . . . 14 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ตโ€˜๐‘) โˆˆ โ„)
118 simpl1 1188 . . . . . . . . . . . . . 14 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„)
119117, 118resubcld 11667 . . . . . . . . . . . . 13 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โˆˆ โ„)
120 simpl3 1190 . . . . . . . . . . . . . 14 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„)
121120, 118resubcld 11667 . . . . . . . . . . . . 13 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โˆˆ โ„)
122 simp3 1135 . . . . . . . . . . . . . . . . 17 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„)
123122recnd 11267 . . . . . . . . . . . . . . . 16 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ (๐ถโ€˜๐‘) โˆˆ โ„‚)
124753ad2ant1 1130 . . . . . . . . . . . . . . . 16 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ (๐ดโ€˜๐‘) โˆˆ โ„‚)
125123, 124subeq0ad 11606 . . . . . . . . . . . . . . 15 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) = 0 โ†” (๐ถโ€˜๐‘) = (๐ดโ€˜๐‘)))
126125necon3bid 2975 . . . . . . . . . . . . . 14 (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โ†’ (((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โ‰  0 โ†” (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)))
127126biimpar 476 . . . . . . . . . . . . 13 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) โ‰  0)
128119, 121, 127redivcld 12067 . . . . . . . . . . . 12 ((((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘)) โ†’ (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โˆˆ โ„)
129 colinearalglem4 28759 . . . . . . . . . . . . 13 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) โˆˆ โ„) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
130 oveq1 7420 . . . . . . . . . . . . . . . . . 18 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) = ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)))
131130oveq1d 7428 . . . . . . . . . . . . . . . . 17 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) = (((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))
132131breq1d 5154 . . . . . . . . . . . . . . . 16 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†” (((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
133132ralimi 3073 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†” (((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
134 ralbi 3093 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†” (((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
135133, 134syl 17 . . . . . . . . . . . . . 14 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0))
136 oveq2 7421 . . . . . . . . . . . . . . . . . 18 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) = ((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))))
137 oveq2 7421 . . . . . . . . . . . . . . . . . 18 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) = ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))))
138136, 137oveq12d 7431 . . . . . . . . . . . . . . . . 17 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) = (((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))))
139138breq1d 5154 . . . . . . . . . . . . . . . 16 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0))
140139ralimi 3073 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0))
141 ralbi 3093 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0))
142140, 141syl 17 . . . . . . . . . . . . . 14 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–))) ยท ((๐ดโ€˜๐‘–) โˆ’ (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)))) โ‰ค 0))
143 oveq1 7420 . . . . . . . . . . . . . . . . . 18 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) = ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–)))
144143oveq2d 7429 . . . . . . . . . . . . . . . . 17 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) = (((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))))
145144breq1d 5154 . . . . . . . . . . . . . . . 16 ((๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ ((((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
146145ralimi 3073 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ โˆ€๐‘– โˆˆ (1...๐‘)((((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
147 ralbi 3093 . . . . . . . . . . . . . . 15 (โˆ€๐‘– โˆˆ (1...๐‘)((((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” (((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
148146, 147syl 17 . . . . . . . . . . . . . 14 (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โ†” โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
149135, 142, 1483orbi123d 1431 . . . . . . . . . . . . 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 594 . . . . . . . . . . 11 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(๐ตโ€˜๐‘–) = (((((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) / ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) + (๐ดโ€˜๐‘–)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
152115, 151sylbird 259 . . . . . . . . . 10 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (((๐ดโ€˜๐‘) โˆˆ โ„ โˆง (๐ตโ€˜๐‘) โˆˆ โ„ โˆง (๐ถโ€˜๐‘) โˆˆ โ„) โˆง (๐ถโ€˜๐‘) โ‰  (๐ดโ€˜๐‘))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘))) = (((๐ตโ€˜๐‘) โˆ’ (๐ดโ€˜๐‘)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
15368, 152syldan 589 . . . . . . . . 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 3146 . . . . . 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 3018 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0)))
159158pm4.71rd 561 . . 3 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
160 andir 1006 . . . . 5 (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โ†” ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
161160orbi1i 911 . . . 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 1085 . . . . . 6 ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โ†” ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0))
163162anbi1i 622 . . . . 5 (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โ†” (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
164 andir 1006 . . . . 5 ((((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โ†” (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
165163, 164bitri 274 . . . 4 (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โ†” (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
166 df-3or 1085 . . . 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 302 . . 3 (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆจ โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0) โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โ†” ((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))))
168159, 167bitr2di 287 . 2 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (((โˆ€๐‘– โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))) โˆจ (โˆ€๐‘– โˆˆ (1...๐‘)(((๐ดโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–)) ยท ((๐ตโ€˜๐‘–) โˆ’ (๐ถโ€˜๐‘–))) โ‰ค 0 โˆง โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
16913, 168bitrd 278 1 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ((๐ด Btwn โŸจ๐ต, ๐ถโŸฉ โˆจ ๐ต Btwn โŸจ๐ถ, ๐ดโŸฉ โˆจ ๐ถ Btwn โŸจ๐ด, ๐ตโŸฉ) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆจ wo 845   โˆจ w3o 1083   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2930  โˆ€wral 3051  โˆƒwrex 3060  โŸจcop 4631   class class class wbr 5144  โ€˜cfv 6543  (class class class)co 7413  โ„‚cc 11131  โ„cr 11132  0cc0 11133  1c1 11134   + caddc 11136   ยท cmul 11138   โ‰ค cle 11274   โˆ’ cmin 11469   / cdiv 11896  ...cfz 13511  ๐”ผcee 28738   Btwn cbtwn 28739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8718  df-map 8840  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-n0 12498  df-z 12584  df-uz 12848  df-icc 13358  df-fz 13512  df-seq 13994  df-exp 14054  df-ee 28741  df-btwn 28742
This theorem is referenced by:  axlowdimlem6  28797
  Copyright terms: Public domain W3C validator