Theorem iddvds 16232

Description: An integer divides itself. Theorem 1.1(a) in [ApostolNT] p. 14 (reflexive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)

Assertion

Ref	Expression
iddvds	⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 𝑁)

Proof of Theorem iddvds

Step	Hyp	Ref	Expression
1		zcn 12523	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
2	1	mullidd 11157	. 2 ⊢ (𝑁 ∈ ℤ → (1 · 𝑁) = 𝑁)
3		1z 12551	. . . 4 ⊢ 1 ∈ ℤ
4		dvds0lem 16229	. . . 4 ⊢ (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 · 𝑁) = 𝑁) → 𝑁 ∥ 𝑁)
5	3, 4	mp3anl1 1459	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 · 𝑁) = 𝑁) → 𝑁 ∥ 𝑁)
6	5	anabsan 667	. 2 ⊢ ((𝑁 ∈ ℤ ∧ (1 · 𝑁) = 𝑁) → 𝑁 ∥ 𝑁)
7	2, 6	mpdan 689	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 𝑁)

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2115   class class class wbr 5075  (class class class)co 7359  1c1 11033   · cmul 11037  ℤcz 12518   ∥ cdvds 16215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1970  ax-7 2011  ax-8 2117  ax-9 2125  ax-10 2148  ax-11 2164  ax-12 2185  ax-ext 2708  ax-sep 5221  ax-nul 5231  ax-pr 5365  ax-un 7681  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 850  df-3or 1089  df-3an 1090  df-tru 1546  df-fal 1556  df-ex 1783  df-nf 1787  df-sb 2070  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2932  df-ral 3051  df-rex 3061  df-reu 3342  df-rab 3389  df-v 3430  df-sbc 3727  df-csb 3835  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-pss 3906  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7362  df-om 7810  df-2nd 7935  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-neg 11374  df-nn 12169  df-z 12519  df-dvds 16216

This theorem is referenced by:  dvdsadd  16265  dvds1  16282  dvdsext  16284  z2even  16333  divalglem0  16356  divalglem2  16358  sadadd3  16424  gcd0id  16482  gcdzeq  16515  mulgcddvds  16618  1idssfct  16643  isprm2lem  16644  dvdsprime  16650  dvdsprm  16667  exprmfct  16668  coprm  16675  isprm6  16678  pcidlem  16837  pcprmpw2  16847  pcprmpw  16848  prmgaplem1  17014  prmgaplem2  17015  prmgaplcmlem1  17016  prmgaplcmlem2  17017  odeq  19519  pgpfi  19574  znidomb  21539  sgmnncl  27131  muinv  27177  ppiublem2  27187  perfect1  27212  perfectlem2  27214  2sqlem6  27407  ex-ind-dvds  30552  2sqr3nconstr  33968  cos9thpinconstrlem2  33977  eulerpartlemt  34558  dfgcd3  37681  poimirlem25  38009  poimirlem27  38011  aks4d1p9  42570  unitscyglem2  42678  unitscyglem4  42680  jm2.18  43430  jm2.15nn0  43445  jm2.16nn0  43446  jm2.27c  43449  nzss  44758  etransclem25  46699  perfectALTVlem2  48210