Metamath Proof Explorer

Theorem znidomb

Description: The Z/nZ structure is a domain (and hence a field) precisely when n is prime. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis zntos.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
Assertion znidomb ( 𝑁 ∈ ℕ → ( 𝑌 ∈ IDomn ↔ 𝑁 ∈ ℙ ) )

Proof

Step Hyp Ref Expression
1 zntos.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 2z ⊢ 2 ∈ ℤ
3 2 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) → 2 ∈ ℤ )
4 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
5 4 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) → 𝑁 ∈ ℤ )
6 hash2 ⊢ ( ♯ ‘ 2o ) = 2
7 isidom ⊢ ( 𝑌 ∈ IDomn ↔ ( 𝑌 ∈ CRing ∧ 𝑌 ∈ Domn ) )
8 7 simprbi ⊢ ( 𝑌 ∈ IDomn → 𝑌 ∈ Domn )
9 domnnzr ⊢ ( 𝑌 ∈ Domn → 𝑌 ∈ NzRing )
10 8 9 syl ⊢ ( 𝑌 ∈ IDomn → 𝑌 ∈ NzRing )
11 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
12 11 isnzr2 ⊢ ( 𝑌 ∈ NzRing ↔ ( 𝑌 ∈ Ring ∧ 2o ≼ ( Base ‘ 𝑌 ) ) )
13 12 simprbi ⊢ ( 𝑌 ∈ NzRing → 2o ≼ ( Base ‘ 𝑌 ) )
14 10 13 syl ⊢ ( 𝑌 ∈ IDomn → 2o ≼ ( Base ‘ 𝑌 ) )
15 14 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) → 2o ≼ ( Base ‘ 𝑌 ) )
16 df2o2 ⊢ 2o = { ∅ , { ∅ } }
17 prfi ⊢ { ∅ , { ∅ } } ∈ Fin
18 16 17 eqeltri ⊢ 2o ∈ Fin
19 fvex ⊢ ( Base ‘ 𝑌 ) ∈ V
20 hashdom ⊢ ( ( 2o ∈ Fin ∧ ( Base ‘ 𝑌 ) ∈ V ) → ( ( ♯ ‘ 2o ) ≤ ( ♯ ‘ ( Base ‘ 𝑌 ) ) ↔ 2o ≼ ( Base ‘ 𝑌 ) ) )
21 18 19 20 mp2an ⊢ ( ( ♯ ‘ 2o ) ≤ ( ♯ ‘ ( Base ‘ 𝑌 ) ) ↔ 2o ≼ ( Base ‘ 𝑌 ) )
22 15 21 sylibr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) → ( ♯ ‘ 2o ) ≤ ( ♯ ‘ ( Base ‘ 𝑌 ) ) )
23 6 22 eqbrtrrid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) → 2 ≤ ( ♯ ‘ ( Base ‘ 𝑌 ) ) )
24 1 11 znhash ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( Base ‘ 𝑌 ) ) = 𝑁 )
25 24 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) → ( ♯ ‘ ( Base ‘ 𝑌 ) ) = 𝑁 )
26 23 25 breqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) → 2 ≤ 𝑁 )
27 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
28 3 5 26 27 syl3anbrc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
29 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
30 29 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑁 ∈ ℂ )
31 nncn ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℂ )
32 31 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑥 ∈ ℂ )
33 nnne0 ⊢ ( 𝑥 ∈ ℕ → 𝑥 ≠ 0 )
34 33 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑥 ≠ 0 )
35 30 32 34 divcan1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( 𝑁 / 𝑥 ) · 𝑥 ) = 𝑁 )
36 35 fveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( ( 𝑁 / 𝑥 ) · 𝑥 ) ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑁 ) )
37 8 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑌 ∈ Domn )
38 domnring ⊢ ( 𝑌 ∈ Domn → 𝑌 ∈ Ring )
39 37 38 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑌 ∈ Ring )
40 eqid ⊢ ( ℤRHom ‘ 𝑌 ) = ( ℤRHom ‘ 𝑌 )
41 40 zrhrhm ⊢ ( 𝑌 ∈ Ring → ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) )
42 39 41 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) )
43 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑥 ∥ 𝑁 )
44 nnz ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℤ )
45 44 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑥 ∈ ℤ )
46 4 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑁 ∈ ℤ )
47 dvdsval2 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝑥 ∥ 𝑁 ↔ ( 𝑁 / 𝑥 ) ∈ ℤ ) )
48 45 34 46 47 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑥 ∥ 𝑁 ↔ ( 𝑁 / 𝑥 ) ∈ ℤ ) )
49 43 48 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑁 / 𝑥 ) ∈ ℤ )
50 zringbas ⊢ ℤ = ( Base ‘ ℤring )
51 zringmulr ⊢ · = ( .r ‘ ℤring )
52 eqid ⊢ ( .r ‘ 𝑌 ) = ( .r ‘ 𝑌 )
53 50 51 52 rhmmul ⊢ ( ( ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) ∧ ( 𝑁 / 𝑥 ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( ( 𝑁 / 𝑥 ) · 𝑥 ) ) = ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ) )
54 42 49 45 53 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( ( 𝑁 / 𝑥 ) · 𝑥 ) ) = ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ) )
55 iddvds ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∥ 𝑁 )
56 46 55 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑁 ∥ 𝑁 )
57 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
58 57 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
59 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
60 1 40 59 zndvds0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑁 ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ 𝑁 ) )
61 58 46 60 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑁 ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ 𝑁 ) )
62 56 61 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑁 ) = ( 0g ‘ 𝑌 ) )
63 36 54 62 3eqtr3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ) = ( 0g ‘ 𝑌 ) )
64 50 11 rhmf ⊢ ( ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) → ( ℤRHom ‘ 𝑌 ) : ℤ ⟶ ( Base ‘ 𝑌 ) )
65 42 64 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ℤRHom ‘ 𝑌 ) : ℤ ⟶ ( Base ‘ 𝑌 ) )
66 65 49 ffvelrnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) ∈ ( Base ‘ 𝑌 ) )
67 65 45 ffvelrnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑌 ) )
68 11 52 59 domneq0 ⊢ ( ( 𝑌 ∈ Domn ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ) = ( 0g ‘ 𝑌 ) ↔ ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) = ( 0g ‘ 𝑌 ) ∨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ) ) )
69 37 66 67 68 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ) = ( 0g ‘ 𝑌 ) ↔ ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) = ( 0g ‘ 𝑌 ) ∨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ) ) )
70 63 69 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) = ( 0g ‘ 𝑌 ) ∨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ) )
71 1 40 59 zndvds0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 𝑥 ) ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ ( 𝑁 / 𝑥 ) ) )
72 58 49 71 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ ( 𝑁 / 𝑥 ) ) )
73 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
74 73 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑁 ∈ ℝ )
75 nnre ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ )
76 75 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑥 ∈ ℝ )
77 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
78 77 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 0 < 𝑁 )
79 nngt0 ⊢ ( 𝑥 ∈ ℕ → 0 < 𝑥 )
80 79 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 0 < 𝑥 )
81 74 76 78 80 divgt0d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 0 < ( 𝑁 / 𝑥 ) )
82 elnnz ⊢ ( ( 𝑁 / 𝑥 ) ∈ ℕ ↔ ( ( 𝑁 / 𝑥 ) ∈ ℤ ∧ 0 < ( 𝑁 / 𝑥 ) ) )
83 49 81 82 sylanbrc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑁 / 𝑥 ) ∈ ℕ )
84 dvdsle ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 / 𝑥 ) ∈ ℕ ) → ( 𝑁 ∥ ( 𝑁 / 𝑥 ) → 𝑁 ≤ ( 𝑁 / 𝑥 ) ) )
85 46 83 84 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑁 ∥ ( 𝑁 / 𝑥 ) → 𝑁 ≤ ( 𝑁 / 𝑥 ) ) )
86 1red ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 1 ∈ ℝ )
87 0lt1 ⊢ 0 < 1
88 87 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 0 < 1 )
89 lediv2 ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ∧ ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( 𝑥 ≤ 1 ↔ ( 𝑁 / 1 ) ≤ ( 𝑁 / 𝑥 ) ) )
90 76 80 86 88 74 78 89 syl222anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑥 ≤ 1 ↔ ( 𝑁 / 1 ) ≤ ( 𝑁 / 𝑥 ) ) )
91 nnle1eq1 ⊢ ( 𝑥 ∈ ℕ → ( 𝑥 ≤ 1 ↔ 𝑥 = 1 ) )
92 91 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑥 ≤ 1 ↔ 𝑥 = 1 ) )
93 30 div1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑁 / 1 ) = 𝑁 )
94 93 breq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( 𝑁 / 1 ) ≤ ( 𝑁 / 𝑥 ) ↔ 𝑁 ≤ ( 𝑁 / 𝑥 ) ) )
95 90 92 94 3bitr3rd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑁 ≤ ( 𝑁 / 𝑥 ) ↔ 𝑥 = 1 ) )
96 85 95 sylibd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑁 ∥ ( 𝑁 / 𝑥 ) → 𝑥 = 1 ) )
97 72 96 sylbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) = ( 0g ‘ 𝑌 ) → 𝑥 = 1 ) )
98 1 40 59 zndvds0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ 𝑥 ) )
99 58 45 98 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ 𝑥 ) )
100 nnnn0 ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ0 )
101 100 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → 𝑥 ∈ ℕ0 )
102 dvdseq ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑥 ∥ 𝑁 ∧ 𝑁 ∥ 𝑥 ) ) → 𝑥 = 𝑁 )
103 102 expr ⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∥ 𝑁 ) → ( 𝑁 ∥ 𝑥 → 𝑥 = 𝑁 ) )
104 101 58 43 103 syl21anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑁 ∥ 𝑥 → 𝑥 = 𝑁 ) )
105 99 104 sylbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) → 𝑥 = 𝑁 ) )
106 97 105 orim12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) = ( 0g ‘ 𝑌 ) ∨ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ) → ( 𝑥 = 1 ∨ 𝑥 = 𝑁 ) ) )
107 70 106 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( 𝑥 = 1 ∨ 𝑥 = 𝑁 ) )
108 107 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ∥ 𝑁 → ( 𝑥 = 1 ∨ 𝑥 = 𝑁 ) ) )
109 108 ralrimiva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) → ∀ 𝑥 ∈ ℕ ( 𝑥 ∥ 𝑁 → ( 𝑥 = 1 ∨ 𝑥 = 𝑁 ) ) )
110 isprm2 ⊢ ( 𝑁 ∈ ℙ ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℕ ( 𝑥 ∥ 𝑁 → ( 𝑥 = 1 ∨ 𝑥 = 𝑁 ) ) ) )
111 28 109 110 sylanbrc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) → 𝑁 ∈ ℙ )
112 111 ex ⊢ ( 𝑁 ∈ ℕ → ( 𝑌 ∈ IDomn → 𝑁 ∈ ℙ ) )
113 1 znfld ⊢ ( 𝑁 ∈ ℙ → 𝑌 ∈ Field )
114 fldidom ⊢ ( 𝑌 ∈ Field → 𝑌 ∈ IDomn )
115 113 114 syl ⊢ ( 𝑁 ∈ ℙ → 𝑌 ∈ IDomn )
116 112 115 impbid1 ⊢ ( 𝑁 ∈ ℕ → ( 𝑌 ∈ IDomn ↔ 𝑁 ∈ ℙ ) )