:: Gauss Lemma and Law of Quadratic Reciprocity
:: by Li Yan , Xiquan Liang and Junjie Zhao
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: INT_5:1
theorem Th2: :: INT_5:2
Lm1:
for x, y being Integer holds
( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) )
:: deftheorem Def1 defines Poly-INT INT_5:def 1 :
theorem Th3: :: INT_5:3
theorem :: INT_5:4
theorem Th5: :: INT_5:5
theorem Th6: :: INT_5:6
theorem Th7: :: INT_5:7
theorem Th8: :: INT_5:8
:: deftheorem Def2 defines is_quadratic_residue_mod INT_5:def 2 :
theorem Th9: :: INT_5:9
theorem :: INT_5:10
theorem Th11: :: INT_5:11
Lm2:
for i being Integer
for p being Prime holds
( i,p are_relative_prime or p divides i )
theorem Th12: :: INT_5:12
theorem Th13: :: INT_5:13
theorem Th14: :: INT_5:14
theorem :: INT_5:15
theorem Th16: :: INT_5:16
theorem Th17: :: INT_5:17
theorem Th18: :: INT_5:18
theorem Th19: :: INT_5:19
theorem Th20: :: INT_5:20
theorem Th21: :: INT_5:21
theorem :: INT_5:22
theorem :: INT_5:23
theorem :: INT_5:24
:: deftheorem Def3 defines Lege INT_5:def 3 :
theorem Th25: :: INT_5:25
theorem Th26: :: INT_5:26
theorem :: INT_5:27
theorem Th28: :: INT_5:28
theorem :: INT_5:29
theorem :: INT_5:30
theorem Th31: :: INT_5:31
theorem Th32: :: INT_5:32
theorem Th33: :: INT_5:33
theorem Th34: :: INT_5:34
theorem :: INT_5:35
theorem Th36: :: INT_5:36
theorem :: INT_5:37
theorem :: INT_5:38
theorem Th39: :: INT_5:39
theorem Th40: :: INT_5:40
theorem Th41: :: INT_5:41
theorem Th42: :: INT_5:42
theorem :: INT_5:43
theorem :: INT_5:44
theorem Th45: :: INT_5:45
theorem Th46: :: INT_5:46
theorem Th47: :: INT_5:47
theorem Th48: :: INT_5:48
Lm3:
for fp being FinSequence of NAT holds Sum fp is Element of NAT
;
theorem Th49: :: INT_5:49
theorem :: INT_5:50
theorem :: INT_5:51