prmirred - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > prmirred		Structured version Visualization version GIF version

Theorem prmirred 21523

Description: The irreducible elements of ℤ are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)

**Hypothesis**
Ref	Expression
prmirred.i	⊢ 𝐼 = (Irred‘ℤ_ring)

**Assertion**
Ref	Expression
prmirred	⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) ∈ ℙ))

**Proof of Theorem prmirred**
Step	Hyp	Ref	Expression
1		prmirred.i	. . 3 ⊢ 𝐼 = (Irred‘ℤ_ring)
2		zringbas 21502	. . 3 ⊢ ℤ = (Base‘ℤ_ring)
3	1, 2	irredcl 20469	. 2 ⊢ (𝐴 ∈ 𝐼 → 𝐴 ∈ ℤ)
4		elnn0 12483	. . . . . . 7 ⊢ (𝐴 ∈ ℕ₀ ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
5		zringring 21498	. . . . . . . . . . 11 ⊢ ℤ_ring ∈ Ring
6		zring0 21507	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘ℤ_ring)
7	1, 6	irredn0 20468	. . . . . . . . . . 11 ⊢ ((ℤ_ring ∈ Ring ∧ 𝐴 ∈ 𝐼) → 𝐴 ≠ 0)
8	5, 7	mpan 700	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐼 → 𝐴 ≠ 0)
9	8	necon2bi 2987	. . . . . . . . 9 ⊢ (𝐴 = 0 → ¬ 𝐴 ∈ 𝐼)
10	9	pm2.21d 121	. . . . . . . 8 ⊢ (𝐴 = 0 → (𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ))
11	10	jao1i 869	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 = 0) → (𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ))
12	4, 11	sylbi 219	. . . . . 6 ⊢ (𝐴 ∈ ℕ₀ → (𝐴 ∈ 𝐼 → 𝐴 ∈ ℕ))
13		prmnn 16708	. . . . . . 7 ⊢ (𝐴 ∈ ℙ → 𝐴 ∈ ℕ)
14	13	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ ℕ₀ → (𝐴 ∈ ℙ → 𝐴 ∈ ℕ))
15	1	prmirredlem 21521	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ))
16	15	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ ℕ₀ → (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ)))
17	12, 14, 16	pm5.21ndd 381	. . . . 5 ⊢ (𝐴 ∈ ℕ₀ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ))
18		nn0re 12490	. . . . . . 7 ⊢ (𝐴 ∈ ℕ₀ → 𝐴 ∈ ℝ)
19		nn0ge0 12506	. . . . . . 7 ⊢ (𝐴 ∈ ℕ₀ → 0 ≤ 𝐴)
20	18, 19	absidd 15450	. . . . . 6 ⊢ (𝐴 ∈ ℕ₀ → (abs‘𝐴) = 𝐴)
21	20	eleq1d 2847	. . . . 5 ⊢ (𝐴 ∈ ℕ₀ → ((abs‘𝐴) ∈ ℙ ↔ 𝐴 ∈ ℙ))
22	17, 21	bitr4d 284	. . . 4 ⊢ (𝐴 ∈ ℕ₀ → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ))
23	22	adantl 485	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ))
24	1	prmirredlem 21521	. . . . . 6 ⊢ (-𝐴 ∈ ℕ → (-𝐴 ∈ 𝐼 ↔ -𝐴 ∈ ℙ))
25	24	adantl 485	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (-𝐴 ∈ 𝐼 ↔ -𝐴 ∈ ℙ))
26		eqid 2762	. . . . . . . . 9 ⊢ (inv_g‘ℤ_ring) = (inv_g‘ℤ_ring)
27	1, 26, 2	irrednegb 20476	. . . . . . . 8 ⊢ ((ℤ_ring ∈ Ring ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ 𝐼 ↔ ((inv_g‘ℤ_ring)‘𝐴) ∈ 𝐼))
28	5, 27	mpan 700	. . . . . . 7 ⊢ (𝐴 ∈ ℤ → (𝐴 ∈ 𝐼 ↔ ((inv_g‘ℤ_ring)‘𝐴) ∈ 𝐼))
29		zsubrg 21469	. . . . . . . . . . 11 ⊢ ℤ ∈ (SubRing‘ℂ_fld)
30		subrgsubg 20623	. . . . . . . . . . 11 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubGrp‘ℂ_fld))
31	29, 30	ax-mp 5	. . . . . . . . . 10 ⊢ ℤ ∈ (SubGrp‘ℂ_fld)
32		df-zring 21496	. . . . . . . . . . 11 ⊢ ℤ_ring = (ℂ_fld ↾_s ℤ)
33		eqid 2762	. . . . . . . . . . 11 ⊢ (inv_g‘ℂ_fld) = (inv_g‘ℂ_fld)
34	32, 33, 26	subginv 19175	. . . . . . . . . 10 ⊢ ((ℤ ∈ (SubGrp‘ℂ_fld) ∧ 𝐴 ∈ ℤ) → ((inv_g‘ℂ_fld)‘𝐴) = ((inv_g‘ℤ_ring)‘𝐴))
35	31, 34	mpan 700	. . . . . . . . 9 ⊢ (𝐴 ∈ ℤ → ((inv_g‘ℂ_fld)‘𝐴) = ((inv_g‘ℤ_ring)‘𝐴))
36		zcn 12573	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
37		cnfldneg 21447	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((inv_g‘ℂ_fld)‘𝐴) = -𝐴)
38	36, 37	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ ℤ → ((inv_g‘ℂ_fld)‘𝐴) = -𝐴)
39	35, 38	eqtr3d 2799	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ → ((inv_g‘ℤ_ring)‘𝐴) = -𝐴)
40	39	eleq1d 2847	. . . . . . 7 ⊢ (𝐴 ∈ ℤ → (((inv_g‘ℤ_ring)‘𝐴) ∈ 𝐼 ↔ -𝐴 ∈ 𝐼))
41	28, 40	bitrd 281	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴 ∈ 𝐼 ↔ -𝐴 ∈ 𝐼))
42	41	adantr 484	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (𝐴 ∈ 𝐼 ↔ -𝐴 ∈ 𝐼))
43		zre 12572	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
44	43	adantr 484	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → 𝐴 ∈ ℝ)
45		nnnn0 12488	. . . . . . . . . 10 ⊢ (-𝐴 ∈ ℕ → -𝐴 ∈ ℕ₀)
46	45	nn0ge0d 12545	. . . . . . . . 9 ⊢ (-𝐴 ∈ ℕ → 0 ≤ -𝐴)
47	46	adantl 485	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → 0 ≤ -𝐴)
48	44	le0neg1d 11758	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴))
49	47, 48	mpbird 259	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → 𝐴 ≤ 0)
50	44, 49	absnidd 15441	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (abs‘𝐴) = -𝐴)
51	50	eleq1d 2847	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → ((abs‘𝐴) ∈ ℙ ↔ -𝐴 ∈ ℙ))
52	25, 42, 51	3bitr4d 313	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℕ) → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ))
53	52	adantrl 726	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ (𝐴 ∈ ℝ ∧ -𝐴 ∈ ℕ)) → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ))
54		elznn0nn 12582	. . . 4 ⊢ (𝐴 ∈ ℤ ↔ (𝐴 ∈ ℕ₀ ∨ (𝐴 ∈ ℝ ∧ -𝐴 ∈ ℕ)))
55	54	biimpi 218	. . 3 ⊢ (𝐴 ∈ ℤ → (𝐴 ∈ ℕ₀ ∨ (𝐴 ∈ ℝ ∧ -𝐴 ∈ ℕ)))
56	23, 53, 55	mpjaodan 971	. 2 ⊢ (𝐴 ∈ ℤ → (𝐴 ∈ 𝐼 ↔ (abs‘𝐴) ∈ ℙ))
57	3, 56	biadanii 831	1 ⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) ∈ ℙ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1560 ∈ wcel 2142 ≠ wne 2957 class class class wbr 5100 ‘cfv 6521 ℂcc 11071 ℝcr 11072 0cc0 11073 ≤ cle 11217 -cneg 11415 ℕcn 12210 ℕ₀cn0 12481 ℤcz 12568 abscabs 15261 ℙcprime 16705 inv_gcminusg 18976 SubGrpcsubg 19162 Ringcrg 20279 Irredcir 20401 SubRingcsubrg 20615 ℂ_fldccnfld 21421 ℤ_ringczring 21495

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151 ax-addf 11152 ax-mulf 11153

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-1st 7970 df-2nd 7971 df-tpos 8206 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-er 8678 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-sup 9388 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-z 12569 df-dec 12689 df-uz 12840 df-rp 12994 df-fz 13513 df-seq 14015 df-exp 14075 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-dvds 16287 df-prm 16706 df-gz 16966 df-struct 17183 df-sets 17200 df-slot 17218 df-ndx 17230 df-base 17246 df-ress 17267 df-plusg 17299 df-mulr 17300 df-starv 17301 df-tset 17305 df-ple 17306 df-ds 17308 df-unif 17309 df-0g 17470 df-mgm 18674 df-sgrp 18753 df-mnd 18769 df-grp 18978 df-minusg 18979 df-subg 19165 df-cmn 19822 df-abl 19823 df-mgp 20187 df-rng 20199 df-ur 20228 df-ring 20281 df-cring 20282 df-oppr 20382 df-dvdsr 20402 df-unit 20403 df-irred 20404 df-invr 20433 df-dvr 20446 df-subrng 20592 df-subrg 20616 df-drng 20777 df-cnfld 21422 df-zring 21496

This theorem is referenced by: (None)

W3C validator