:: Fundamental Theorem of Algebra
:: by Robert Milewski
::
:: Received August 21, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: POLYNOM5:1
theorem Th2: :: POLYNOM5:2
theorem Th3: :: POLYNOM5:3
Lm1:
for x, y being Real st ( for c being Real st c > 0 & c < 1 holds
c * x >= y ) holds
y <= 0
theorem Th4: :: POLYNOM5:4
theorem Th5: :: POLYNOM5:5
theorem Th6: :: POLYNOM5:6
theorem :: POLYNOM5:7
canceled;
theorem Th8: :: POLYNOM5:8
:: deftheorem Def1 defines |. POLYNOM5:def 1 :
theorem Th9: :: POLYNOM5:9
theorem Th10: :: POLYNOM5:10
theorem :: POLYNOM5:11
theorem :: POLYNOM5:12
theorem Th13: :: POLYNOM5:13
theorem :: POLYNOM5:14
theorem Th15: :: POLYNOM5:15
:: deftheorem defines `^ POLYNOM5:def 2 :
theorem Th16: :: POLYNOM5:16
theorem :: POLYNOM5:17
theorem :: POLYNOM5:18
theorem :: POLYNOM5:19
theorem Th20: :: POLYNOM5:20
theorem Th21: :: POLYNOM5:21
theorem :: POLYNOM5:22
theorem Th23: :: POLYNOM5:23
Lm2:
for L being non empty ZeroStr
for p being AlgSequence of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
theorem Th24: :: POLYNOM5:24
:: deftheorem Def3 defines * POLYNOM5:def 3 :
theorem Th25: :: POLYNOM5:25
theorem Th26: :: POLYNOM5:26
theorem Th27: :: POLYNOM5:27
theorem Th28: :: POLYNOM5:28
theorem Th29: :: POLYNOM5:29
theorem Th30: :: POLYNOM5:30
theorem Th31: :: POLYNOM5:31
theorem Th32: :: POLYNOM5:32
:: deftheorem defines <% POLYNOM5:def 4 :
theorem Th33: :: POLYNOM5:33
theorem Th34: :: POLYNOM5:34
theorem Th35: :: POLYNOM5:35
theorem Th36: :: POLYNOM5:36
theorem Th37: :: POLYNOM5:37
theorem :: POLYNOM5:38
theorem Th39: :: POLYNOM5:39
theorem Th40: :: POLYNOM5:40
theorem Th41: :: POLYNOM5:41
theorem Th42: :: POLYNOM5:42
theorem Th43: :: POLYNOM5:43
theorem :: POLYNOM5:44
theorem Th45: :: POLYNOM5:45
theorem :: POLYNOM5:46
theorem :: POLYNOM5:47
theorem Th48: :: POLYNOM5:48
theorem :: POLYNOM5:49
:: deftheorem Def5 defines Subst POLYNOM5:def 5 :
theorem Th50: :: POLYNOM5:50
theorem :: POLYNOM5:51
theorem :: POLYNOM5:52
theorem Th53: :: POLYNOM5:53
theorem Th54: :: POLYNOM5:54
:: deftheorem Def6 defines is_a_root_of POLYNOM5:def 6 :
:: deftheorem Def7 defines with_roots POLYNOM5:def 7 :
theorem Th55: :: POLYNOM5:55
theorem :: POLYNOM5:56
:: deftheorem Def8 defines algebraic-closed POLYNOM5:def 8 :
:: deftheorem Def9 defines Roots POLYNOM5:def 9 :
:: deftheorem Def10 defines NormPolynomial POLYNOM5:def 10 :
theorem Th57: :: POLYNOM5:57
theorem Th58: :: POLYNOM5:58
theorem Th59: :: POLYNOM5:59
theorem Th60: :: POLYNOM5:60
theorem Th61: :: POLYNOM5:61
theorem :: POLYNOM5:62
theorem Th63: :: POLYNOM5:63
theorem Th64: :: POLYNOM5:64
:: deftheorem Def11 defines FPower POLYNOM5:def 11 :
theorem :: POLYNOM5:65
theorem :: POLYNOM5:66
theorem Th67: :: POLYNOM5:67
theorem :: POLYNOM5:68
theorem :: POLYNOM5:69
theorem Th70: :: POLYNOM5:70
theorem Th71: :: POLYNOM5:71
:: deftheorem Def12 defines Polynomial-Function POLYNOM5:def 12 :
theorem Th72: :: POLYNOM5:72
theorem Th73: :: POLYNOM5:73
theorem Th74: :: POLYNOM5:74
theorem Th75: :: POLYNOM5:75