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	ffvelcdmd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁 ) ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / 𝑥 ) ) ∈ ( Base ‘ 𝑌 ) )
67	65 45	ffvelcdmd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑌 ∈ 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 ↔ 𝑁 ∈ ℙ ) )