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

Theorem znidomb 20033
Description: The ℤ/n structure is a domain (and hence a field) precisely when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.)
Hypothesis
Ref Expression
zntos.y 𝑌 = (ℤ/nℤ‘𝑁)
Assertion
Ref Expression
znidomb (𝑁 ∈ ℕ → (𝑌 ∈ IDomn ↔ 𝑁 ∈ ℙ))

Proof of Theorem znidomb
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 2z 11522 . . . . . 6 2 ∈ ℤ
21a1i 11 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 2 ∈ ℤ)
3 nnz 11512 . . . . . 6 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
43adantr 472 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 𝑁 ∈ ℤ)
5 hash2 13306 . . . . . . 7 (♯‘2𝑜) = 2
6 isidom 19427 . . . . . . . . . . . 12 (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn))
76simprbi 483 . . . . . . . . . . 11 (𝑌 ∈ IDomn → 𝑌 ∈ Domn)
8 domnnzr 19418 . . . . . . . . . . 11 (𝑌 ∈ Domn → 𝑌 ∈ NzRing)
97, 8syl 17 . . . . . . . . . 10 (𝑌 ∈ IDomn → 𝑌 ∈ NzRing)
10 eqid 2724 . . . . . . . . . . . 12 (Base‘𝑌) = (Base‘𝑌)
1110isnzr2 19386 . . . . . . . . . . 11 (𝑌 ∈ NzRing ↔ (𝑌 ∈ Ring ∧ 2𝑜 ≼ (Base‘𝑌)))
1211simprbi 483 . . . . . . . . . 10 (𝑌 ∈ NzRing → 2𝑜 ≼ (Base‘𝑌))
139, 12syl 17 . . . . . . . . 9 (𝑌 ∈ IDomn → 2𝑜 ≼ (Base‘𝑌))
1413adantl 473 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 2𝑜 ≼ (Base‘𝑌))
15 df2o2 7694 . . . . . . . . . 10 2𝑜 = {∅, {∅}}
16 prfi 8351 . . . . . . . . . 10 {∅, {∅}} ∈ Fin
1715, 16eqeltri 2799 . . . . . . . . 9 2𝑜 ∈ Fin
18 fvex 6314 . . . . . . . . 9 (Base‘𝑌) ∈ V
19 hashdom 13281 . . . . . . . . 9 ((2𝑜 ∈ Fin ∧ (Base‘𝑌) ∈ V) → ((♯‘2𝑜) ≤ (♯‘(Base‘𝑌)) ↔ 2𝑜 ≼ (Base‘𝑌)))
2017, 18, 19mp2an 710 . . . . . . . 8 ((♯‘2𝑜) ≤ (♯‘(Base‘𝑌)) ↔ 2𝑜 ≼ (Base‘𝑌))
2114, 20sylibr 224 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → (♯‘2𝑜) ≤ (♯‘(Base‘𝑌)))
225, 21syl5eqbrr 4796 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 2 ≤ (♯‘(Base‘𝑌)))
23 zntos.y . . . . . . . 8 𝑌 = (ℤ/nℤ‘𝑁)
2423, 10znhash 20030 . . . . . . 7 (𝑁 ∈ ℕ → (♯‘(Base‘𝑌)) = 𝑁)
2524adantr 472 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → (♯‘(Base‘𝑌)) = 𝑁)
2622, 25breqtrd 4786 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 2 ≤ 𝑁)
27 eluz2 11806 . . . . 5 (𝑁 ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁))
282, 4, 26, 27syl3anbrc 1383 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 𝑁 ∈ (ℤ‘2))
29 nncn 11141 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
3029ad2antrr 764 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑁 ∈ ℂ)
31 nncn 11141 . . . . . . . . . . . 12 (𝑥 ∈ ℕ → 𝑥 ∈ ℂ)
3231ad2antrl 766 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑥 ∈ ℂ)
33 nnne0 11166 . . . . . . . . . . . 12 (𝑥 ∈ ℕ → 𝑥 ≠ 0)
3433ad2antrl 766 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑥 ≠ 0)
3530, 32, 34divcan1d 10915 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → ((𝑁 / 𝑥) · 𝑥) = 𝑁)
3635fveq2d 6308 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → ((ℤRHom‘𝑌)‘((𝑁 / 𝑥) · 𝑥)) = ((ℤRHom‘𝑌)‘𝑁))
377ad2antlr 765 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑌 ∈ Domn)
38 domnring 19419 . . . . . . . . . . . 12 (𝑌 ∈ Domn → 𝑌 ∈ Ring)
3937, 38syl 17 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑌 ∈ Ring)
40 eqid 2724 . . . . . . . . . . . 12 (ℤRHom‘𝑌) = (ℤRHom‘𝑌)
4140zrhrhm 19983 . . . . . . . . . . 11 (𝑌 ∈ Ring → (ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌))
4239, 41syl 17 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌))
43 simprr 813 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑥𝑁)
44 nnz 11512 . . . . . . . . . . . . 13 (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
4544ad2antrl 766 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑥 ∈ ℤ)
463ad2antrr 764 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑁 ∈ ℤ)
47 dvdsval2 15106 . . . . . . . . . . . 12 ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑥𝑁 ↔ (𝑁 / 𝑥) ∈ ℤ))
4845, 34, 46, 47syl3anc 1439 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑥𝑁 ↔ (𝑁 / 𝑥) ∈ ℤ))
4943, 48mpbid 222 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑁 / 𝑥) ∈ ℤ)
50 zringbas 19947 . . . . . . . . . . 11 ℤ = (Base‘ℤring)
51 zringmulr 19950 . . . . . . . . . . 11 · = (.r‘ℤring)
52 eqid 2724 . . . . . . . . . . 11 (.r𝑌) = (.r𝑌)
5350, 51, 52rhmmul 18850 . . . . . . . . . 10 (((ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌) ∧ (𝑁 / 𝑥) ∈ ℤ ∧ 𝑥 ∈ ℤ) → ((ℤRHom‘𝑌)‘((𝑁 / 𝑥) · 𝑥)) = (((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r𝑌)((ℤRHom‘𝑌)‘𝑥)))
5442, 49, 45, 53syl3anc 1439 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → ((ℤRHom‘𝑌)‘((𝑁 / 𝑥) · 𝑥)) = (((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r𝑌)((ℤRHom‘𝑌)‘𝑥)))
55 iddvds 15118 . . . . . . . . . . 11 (𝑁 ∈ ℤ → 𝑁𝑁)
5646, 55syl 17 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑁𝑁)
57 nnnn0 11412 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
5857ad2antrr 764 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑁 ∈ ℕ0)
59 eqid 2724 . . . . . . . . . . . 12 (0g𝑌) = (0g𝑌)
6023, 40, 59zndvds0 20022 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝑁 ∈ ℤ) → (((ℤRHom‘𝑌)‘𝑁) = (0g𝑌) ↔ 𝑁𝑁))
6158, 46, 60syl2anc 696 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (((ℤRHom‘𝑌)‘𝑁) = (0g𝑌) ↔ 𝑁𝑁))
6256, 61mpbird 247 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → ((ℤRHom‘𝑌)‘𝑁) = (0g𝑌))
6336, 54, 623eqtr3d 2766 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r𝑌)((ℤRHom‘𝑌)‘𝑥)) = (0g𝑌))
6450, 10rhmf 18849 . . . . . . . . . . 11 ((ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌))
6542, 64syl 17 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌))
6665, 49ffvelrnd 6475 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → ((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) ∈ (Base‘𝑌))
6765, 45ffvelrnd 6475 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → ((ℤRHom‘𝑌)‘𝑥) ∈ (Base‘𝑌))
6810, 52, 59domneq0 19420 . . . . . . . . 9 ((𝑌 ∈ Domn ∧ ((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) ∈ (Base‘𝑌) ∧ ((ℤRHom‘𝑌)‘𝑥) ∈ (Base‘𝑌)) → ((((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r𝑌)((ℤRHom‘𝑌)‘𝑥)) = (0g𝑌) ↔ (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g𝑌))))
6937, 66, 67, 68syl3anc 1439 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → ((((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r𝑌)((ℤRHom‘𝑌)‘𝑥)) = (0g𝑌) ↔ (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g𝑌))))
7063, 69mpbid 222 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g𝑌)))
7123, 40, 59zndvds0 20022 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑁 / 𝑥) ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g𝑌) ↔ 𝑁 ∥ (𝑁 / 𝑥)))
7258, 49, 71syl2anc 696 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g𝑌) ↔ 𝑁 ∥ (𝑁 / 𝑥)))
73 nnre 11140 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
7473ad2antrr 764 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑁 ∈ ℝ)
75 nnre 11140 . . . . . . . . . . . . . 14 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
7675ad2antrl 766 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑥 ∈ ℝ)
77 nngt0 11162 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 0 < 𝑁)
7877ad2antrr 764 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 0 < 𝑁)
79 nngt0 11162 . . . . . . . . . . . . . 14 (𝑥 ∈ ℕ → 0 < 𝑥)
8079ad2antrl 766 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 0 < 𝑥)
8174, 76, 78, 80divgt0d 11072 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 0 < (𝑁 / 𝑥))
82 elnnz 11500 . . . . . . . . . . . 12 ((𝑁 / 𝑥) ∈ ℕ ↔ ((𝑁 / 𝑥) ∈ ℤ ∧ 0 < (𝑁 / 𝑥)))
8349, 81, 82sylanbrc 701 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑁 / 𝑥) ∈ ℕ)
84 dvdsle 15155 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ (𝑁 / 𝑥) ∈ ℕ) → (𝑁 ∥ (𝑁 / 𝑥) → 𝑁 ≤ (𝑁 / 𝑥)))
8546, 83, 84syl2anc 696 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑁 ∥ (𝑁 / 𝑥) → 𝑁 ≤ (𝑁 / 𝑥)))
86 1red 10168 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 1 ∈ ℝ)
87 0lt1 10663 . . . . . . . . . . . . 13 0 < 1
8887a1i 11 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 0 < 1)
89 lediv2 11026 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ ∧ 0 < 𝑥) ∧ (1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑥 ≤ 1 ↔ (𝑁 / 1) ≤ (𝑁 / 𝑥)))
9076, 80, 86, 88, 74, 78, 89syl222anc 1455 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑥 ≤ 1 ↔ (𝑁 / 1) ≤ (𝑁 / 𝑥)))
91 nnle1eq1 11161 . . . . . . . . . . . 12 (𝑥 ∈ ℕ → (𝑥 ≤ 1 ↔ 𝑥 = 1))
9291ad2antrl 766 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑥 ≤ 1 ↔ 𝑥 = 1))
9330div1d 10906 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑁 / 1) = 𝑁)
9493breq1d 4770 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → ((𝑁 / 1) ≤ (𝑁 / 𝑥) ↔ 𝑁 ≤ (𝑁 / 𝑥)))
9590, 92, 943bitr3rd 299 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑁 ≤ (𝑁 / 𝑥) ↔ 𝑥 = 1))
9685, 95sylibd 229 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑁 ∥ (𝑁 / 𝑥) → 𝑥 = 1))
9772, 96sylbid 230 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g𝑌) → 𝑥 = 1))
9823, 40, 59zndvds0 20022 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑥 ∈ ℤ) → (((ℤRHom‘𝑌)‘𝑥) = (0g𝑌) ↔ 𝑁𝑥))
9958, 45, 98syl2anc 696 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (((ℤRHom‘𝑌)‘𝑥) = (0g𝑌) ↔ 𝑁𝑥))
100 nnnn0 11412 . . . . . . . . . . 11 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ0)
101100ad2antrl 766 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → 𝑥 ∈ ℕ0)
102 dvdseq 15159 . . . . . . . . . . 11 (((𝑥 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝑥𝑁𝑁𝑥)) → 𝑥 = 𝑁)
103102expr 644 . . . . . . . . . 10 (((𝑥 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑥𝑁) → (𝑁𝑥𝑥 = 𝑁))
104101, 58, 43, 103syl21anc 1438 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑁𝑥𝑥 = 𝑁))
10599, 104sylbid 230 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (((ℤRHom‘𝑌)‘𝑥) = (0g𝑌) → 𝑥 = 𝑁))
10697, 105orim12d 919 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → ((((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g𝑌)) → (𝑥 = 1 ∨ 𝑥 = 𝑁)))
10770, 106mpd 15 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥𝑁)) → (𝑥 = 1 ∨ 𝑥 = 𝑁))
108107expr 644 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ 𝑥 ∈ ℕ) → (𝑥𝑁 → (𝑥 = 1 ∨ 𝑥 = 𝑁)))
109108ralrimiva 3068 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → ∀𝑥 ∈ ℕ (𝑥𝑁 → (𝑥 = 1 ∨ 𝑥 = 𝑁)))
110 isprm2 15518 . . . 4 (𝑁 ∈ ℙ ↔ (𝑁 ∈ (ℤ‘2) ∧ ∀𝑥 ∈ ℕ (𝑥𝑁 → (𝑥 = 1 ∨ 𝑥 = 𝑁))))
11128, 109, 110sylanbrc 701 . . 3 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 𝑁 ∈ ℙ)
112111ex 449 . 2 (𝑁 ∈ ℕ → (𝑌 ∈ IDomn → 𝑁 ∈ ℙ))
11323znfld 20032 . . 3 (𝑁 ∈ ℙ → 𝑌 ∈ Field)
114 fldidom 19428 . . 3 (𝑌 ∈ Field → 𝑌 ∈ IDomn)
115113, 114syl 17 . 2 (𝑁 ∈ ℙ → 𝑌 ∈ IDomn)
116112, 115impbid1 215 1 (𝑁 ∈ ℕ → (𝑌 ∈ IDomn ↔ 𝑁 ∈ ℙ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383   = wceq 1596  wcel 2103  wne 2896  wral 3014  Vcvv 3304  c0 4023  {csn 4285  {cpr 4287   class class class wbr 4760  wf 5997  cfv 6001  (class class class)co 6765  2𝑜c2o 7674  cdom 8070  Fincfn 8072  cc 10047  cr 10048  0cc0 10049  1c1 10050   · cmul 10054   < clt 10187  cle 10188   / cdiv 10797  cn 11133  2c2 11183  0cn0 11405  cz 11490  cuz 11800  chash 13232  cdvds 15103  cprime 15508  Basecbs 15980  .rcmulr 16065  0gc0g 16223  Ringcrg 18668  CRingccrg 18669   RingHom crh 18835  Fieldcfield 18871  NzRingcnzr 19380  Domncdomn 19403  IDomncidom 19404  ringzring 19941  ℤRHomczrh 19971  ℤ/nczn 19974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-inf2 8651  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127  ax-addf 10128  ax-mulf 10129
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-tpos 7472  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-2o 7681  df-oadd 7684  df-er 7862  df-ec 7864  df-qs 7868  df-map 7976  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-sup 8464  df-inf 8465  df-card 8878  df-cda 9103  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-5 11195  df-6 11196  df-7 11197  df-8 11198  df-9 11199  df-n0 11406  df-xnn0 11477  df-z 11491  df-dec 11607  df-uz 11801  df-rp 11947  df-fz 12441  df-fzo 12581  df-fl 12708  df-mod 12784  df-seq 12917  df-exp 12976  df-hash 13233  df-cj 13959  df-re 13960  df-im 13961  df-sqrt 14095  df-abs 14096  df-dvds 15104  df-gcd 15340  df-prm 15509  df-struct 15982  df-ndx 15983  df-slot 15984  df-base 15986  df-sets 15987  df-ress 15988  df-plusg 16077  df-mulr 16078  df-starv 16079  df-sca 16080  df-vsca 16081  df-ip 16082  df-tset 16083  df-ple 16084  df-ds 16087  df-unif 16088  df-0g 16225  df-imas 16291  df-qus 16292  df-mgm 17364  df-sgrp 17406  df-mnd 17417  df-mhm 17457  df-grp 17547  df-minusg 17548  df-sbg 17549  df-mulg 17663  df-subg 17713  df-nsg 17714  df-eqg 17715  df-ghm 17780  df-cmn 18316  df-abl 18317  df-mgp 18611  df-ur 18623  df-ring 18670  df-cring 18671  df-oppr 18744  df-dvdsr 18762  df-unit 18763  df-invr 18793  df-rnghom 18838  df-drng 18872  df-field 18873  df-subrg 18901  df-lmod 18988  df-lss 19056  df-lsp 19095  df-sra 19295  df-rgmod 19296  df-lidl 19297  df-rsp 19298  df-2idl 19355  df-nzr 19381  df-rlreg 19406  df-domn 19407  df-idom 19408  df-cnfld 19870  df-zring 19942  df-zrh 19975  df-zn 19978
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator