:: Fundamental {T}heorem of {A}rithmetic
:: by Artur Korni{\l}owicz and Piotr Rudnicki
::
:: Received February 13, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: NAT_3:1
theorem Th2: :: NAT_3:2
theorem Th3: :: NAT_3:3
theorem Th4: :: NAT_3:4
theorem Th5: :: NAT_3:5
theorem Th6: :: NAT_3:6
theorem :: NAT_3:7
theorem :: NAT_3:8
:: deftheorem Def1 defines |^ NAT_3:def 1 :
theorem Th9: :: NAT_3:9
theorem :: NAT_3:10
theorem Th11: :: NAT_3:11
theorem Th12: :: NAT_3:12
theorem Th13: :: NAT_3:13
theorem Th14: :: NAT_3:14
theorem :: NAT_3:15
:: deftheorem Def2 defines * NAT_3:def 2 :
theorem Th16: :: NAT_3:16
:: deftheorem Def3 defines min NAT_3:def 3 :
theorem Th17: :: NAT_3:17
:: deftheorem Def4 defines max NAT_3:def 4 :
theorem Th18: :: NAT_3:18
:: deftheorem Def5 defines Product NAT_3:def 5 :
theorem Th19: :: NAT_3:19
:: deftheorem Def6 defines |^ NAT_3:def 6 :
theorem Th20: :: NAT_3:20
:: deftheorem Def7 defines |-count NAT_3:def 7 :
theorem Th21: :: NAT_3:21
theorem :: NAT_3:22
theorem Th23: :: NAT_3:23
theorem :: NAT_3:24
theorem Th25: :: NAT_3:25
theorem Th26: :: NAT_3:26
theorem Th27: :: NAT_3:27
theorem Th28: :: NAT_3:28
theorem Th29: :: NAT_3:29
theorem Th30: :: NAT_3:30
theorem Th31: :: NAT_3:31
theorem Th32: :: NAT_3:32
:: deftheorem Def8 defines prime_exponents NAT_3:def 8 :
theorem Th33: :: NAT_3:33
theorem Th34: :: NAT_3:34
theorem Th35: :: NAT_3:35
theorem :: NAT_3:36
theorem Th37: :: NAT_3:37
theorem Th38: :: NAT_3:38
theorem Th39: :: NAT_3:39
theorem Th40: :: NAT_3:40
theorem :: NAT_3:41
theorem Th42: :: NAT_3:42
theorem Th43: :: NAT_3:43
theorem Th44: :: NAT_3:44
theorem Th45: :: NAT_3:45
theorem Th46: :: NAT_3:46
theorem :: NAT_3:47
theorem :: NAT_3:48
theorem :: NAT_3:49
theorem :: NAT_3:50
theorem :: NAT_3:51
theorem Th52: :: NAT_3:52
theorem :: NAT_3:53
theorem :: NAT_3:54
:: deftheorem Def9 defines prime_factorization NAT_3:def 9 :
theorem Th55: :: NAT_3:55
theorem Th56: :: NAT_3:56
theorem :: NAT_3:57
theorem Th58: :: NAT_3:58
theorem Th59: :: NAT_3:59
theorem :: NAT_3:60
theorem :: NAT_3:61