Theorem zaddsubg 8062

Description: The integers under addition comprise a subgroup of the complex numbers under addition. (Contributed by Paul Chapman, 25-Apr-2008.)

Assertion

Ref	Expression
zaddsubg	⊢ ( + ↾ (ℤ × ℤ)) ∈ (SubGrp ‘ + )

Proof of Theorem zaddsubg

Step	Hyp	Ref	Expression
1		cnaddabl 8058	. . 3 ⊢ + ∈ Abel
2		ablgrp 8033	. . 3 ⊢ ( + ∈ Abel → + ∈ Grp)
3	1, 2	ax-mp 7	. 2 ⊢ + ∈ Grp
4		axaddopr 5232	. . . 4 ⊢ + :(ℂ × ℂ)–→ℂ
5		fdm 3612	. . . 4 ⊢ ( + :(ℂ × ℂ)–→ℂ → dom + = (ℂ × ℂ))
6	4, 5	ax-mp 7	. . 3 ⊢ dom + = (ℂ × ℂ)
7	3, 6	grprn 7985	. 2 ⊢ ℂ = ran +
8		cnid 8059	. 2 ⊢ 0 = (Id ‘ + )
9		eqid 1467	. 2 ⊢ (inv ‘ + ) = (inv ‘ + )
10		zsscn 6085	. 2 ⊢ ℤ ⊆ ℂ
11		eqid 1467	. 2 ⊢ ( + ↾ (ℤ × ℤ)) = ( + ↾ (ℤ × ℤ))
12		zaddclt 6107	. 2 ⊢ ((x ∈ ℤ ⋀ y ∈ ℤ) → (x + y) ∈ ℤ)
13		0z 6088	. 2 ⊢ 0 ∈ ℤ
14		zcnt 6082	. . . 4 ⊢ (x ∈ ℤ → x ∈ ℂ)
15		addinv 8060	. . . 4 ⊢ (x ∈ ℂ → ((inv ‘ + ) ‘x) = -x)
16	14, 15	syl 10	. . 3 ⊢ (x ∈ ℤ → ((inv ‘ + ) ‘x) = -x)
17		znegclt 6105	. . 3 ⊢ (x ∈ ℤ → -x ∈ ℤ)
18	16, 17	eqeltrd 1539	. 2 ⊢ (x ∈ ℤ → ((inv ‘ + ) ‘x) ∈ ℤ)
19	3, 7, 8, 9, 10, 11, 12, 13, 18	issubgi 8054	1 ⊢ ( + ↾ (ℤ × ℤ)) ∈ (SubGrp ‘ + )

Syntax hints:   = wceq 953   ∈ wcel 955   × cxp 3155  dom cdm 3157   ↾ cres 3159  –→wf 3165   ‘cfv 3169  ℂcc 5199  0cc0 5201   + caddc 5204  -cneg 5260  ℤcz 5265  Grpcgr 7962  invcgn 7964  Abelcabl 8030  SubGrpcsubg 8046

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1451  ax-rep 2682  ax-sep 2692  ax-nul 2699  ax-pow 2731  ax-pr 2768  ax-un 2854  ax-inf2 4592

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1374  df-mo 1375  df-clab 1456  df-cleq 1461  df-clel 1464  df-ne 1578  df-nel 1579  df-ral 1640  df-rex 1641  df-reu 1642  df-rab 1643  df-v 1802  df-sbc 1931  df-csb 1991  df-dif 2038  df-un 2039  df-in 2040  df-ss 2042  df-pss 2044  df-nul 2270  df-if 2351  df-pw 2391  df-sn 2401  df-pr 2402  df-tp 2404  df-op 2405  df-uni 2493  df-int 2523  df-iun 2557  df-br 2609  df-opab 2656  df-tr 2670  df-eprel 2818  df-id 2821  df-po 2828  df-so 2838  df-fr 2904  df-we 2921  df-ord 2938  df-on 2939  df-lim 2940  df-suc 2941  df-om 3119  df-xp 3171  df-rel 3172  df-cnv 3173  df-co 3174  df-dm 3175  df-rn 3176  df-res 3177  df-ima 3178  df-fun 3179  df-fn 3180  df-f 3181  df-f1 3182  df-fo 3183  df-f1o 3184  df-fv 3185  df-rdg 3912  df-opr 3945  df-oprab 3946  df-1st 4058  df-2nd 4059  df-1o 4112  df-oadd 4114  df-omul 4115  df-er 4240  df-ec 4242  df-qs 4245  df-en 4346  df-dom 4347  df-sdom 4348  df-ni 4967  df-pli 4968  df-mi 4969  df-lti 4970  df-plpq 5002  df-mpq 5003  df-enq 5004  df-nq 5005  df-plq 5006  df-mq 5007  df-rq 5008  df-ltq 5009  df-1q 5010  df-np 5053  df-1p 5054  df-plp 5055  df-mp 5056  df-ltp 5057  df-plpr 5131  df-mpr 5132  df-enr 5133  df-nr 5134  df-plr 5135  df-mr 5136  df-ltr 5137  df-0r 5138  df-1r 5139  df-m1r 5140  df-c 5207  df-0 5208  df-1 5209  df-i 5210  df-r 5211  df-plus 5212  df-mul 5213  df-lt 5214  df-sub 5323  df-neg 5325  df-pnf 5454  df-mnf 5455  df-xr 5456  df-ltxr 5457  df-le 5458  df-n 5868  df-n0 6042  df-z 6078  df-grp 7966  df-gid 7967  df-ginv 7968  df-abl 8031  df-subg 8047

Copyright terms: Public domain