nn0prpw

Description: Two nonnegative integers are the same if and only if they are divisible by the same prime powers. (Contributed by Jeff Hankins, 29-Sep-2013)

		Ref	Expression
	Assertion	nn0prpw	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A = B \leftrightarrow \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ A = B \to (p^{n} ∥ A \leftrightarrow p^{n} ∥ B)$
2	1	a1d	$⊢ A = B \to ((p \in ℙ \land n \in ℕ) \to (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
3	2	ralrimivv	$⊢ A = B \to \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B)$
4		elnn0	$⊢ A \in ℕ_{0} \leftrightarrow (A \in ℕ \lor A = 0)$
5		elnn0	$⊢ B \in ℕ_{0} \leftrightarrow (B \in ℕ \lor B = 0)$
6		nnre	$⊢ A \in ℕ \to A \in ℝ$
7		nnre	$⊢ B \in ℕ \to B \in ℝ$
8		lttri2	$⊢ (A \in ℝ \land B \in ℝ) \to (A \neq B \leftrightarrow (A < B \lor B < A))$
9	6 7 8	syl2an	$⊢ (A \in ℕ \land B \in ℕ) \to (A \neq B \leftrightarrow (A < B \lor B < A))$
10	9	ancoms	$⊢ (B \in ℕ \land A \in ℕ) \to (A \neq B \leftrightarrow (A < B \lor B < A))$
11		nn0prpwlem	$⊢ B \in ℕ \to \forall k \in ℕ (k < B \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ B))$
12		breq1	$⊢ k = A \to (k < B \leftrightarrow A < B)$
13		breq2	$⊢ k = A \to (p^{n} ∥ k \leftrightarrow p^{n} ∥ A)$
14	13	bibi1d	$⊢ k = A \to ((p^{n} ∥ k \leftrightarrow p^{n} ∥ B) \leftrightarrow (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
15	14	notbid	$⊢ k = A \to (\neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ B) \leftrightarrow \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
16	15	2rexbidv	$⊢ k = A \to (\exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ B) \leftrightarrow \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
17	12 16	imbi12d	$⊢ k = A \to ((k < B \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ B)) \leftrightarrow (A < B \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B)))$
18	17	rspcv	$⊢ A \in ℕ \to (\forall k \in ℕ (k < B \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ B)) \to (A < B \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B)))$
19	11 18	mpan9	$⊢ (B \in ℕ \land A \in ℕ) \to (A < B \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
20		breq1	$⊢ k = B \to (k < A \leftrightarrow B < A)$
21		breq2	$⊢ k = B \to (p^{n} ∥ k \leftrightarrow p^{n} ∥ B)$
22	21	bibi1d	$⊢ k = B \to ((p^{n} ∥ k \leftrightarrow p^{n} ∥ A) \leftrightarrow (p^{n} ∥ B \leftrightarrow p^{n} ∥ A))$
23		bicom	$⊢ (p^{n} ∥ B \leftrightarrow p^{n} ∥ A) \leftrightarrow (p^{n} ∥ A \leftrightarrow p^{n} ∥ B)$
24	22 23	bitrdi	$⊢ k = B \to ((p^{n} ∥ k \leftrightarrow p^{n} ∥ A) \leftrightarrow (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
25	24	notbid	$⊢ k = B \to (\neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A) \leftrightarrow \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
26	25	2rexbidv	$⊢ k = B \to (\exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A) \leftrightarrow \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
27	20 26	imbi12d	$⊢ k = B \to ((k < A \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A)) \leftrightarrow (B < A \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B)))$
28	27	rspcv	$⊢ B \in ℕ \to (\forall k \in ℕ (k < A \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A)) \to (B < A \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B)))$
29		nn0prpwlem	$⊢ A \in ℕ \to \forall k \in ℕ (k < A \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A))$
30	28 29	impel	$⊢ (B \in ℕ \land A \in ℕ) \to (B < A \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
31	19 30	jaod	$⊢ (B \in ℕ \land A \in ℕ) \to ((A < B \lor B < A) \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
32	10 31	sylbid	$⊢ (B \in ℕ \land A \in ℕ) \to (A \neq B \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
33		df-ne	$⊢ A \neq B \leftrightarrow \neg A = B$
34		rexnal2	$⊢ \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \leftrightarrow \neg \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B)$
35	32 33 34	3imtr3g	$⊢ (B \in ℕ \land A \in ℕ) \to (\neg A = B \to \neg \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$
36	35	con4d	$⊢ (B \in ℕ \land A \in ℕ) \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B)$
37	36	ex	$⊢ B \in ℕ \to (A \in ℕ \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B))$
38		prmunb	$⊢ A \in ℕ \to \exists p \in ℙ A < p$
39		1nn	$⊢ 1 \in ℕ$
40		prmz	$⊢ p \in ℙ \to p \in ℤ$
41		1nn0	$⊢ 1 \in ℕ_{0}$
42		zexpcl	$⊢ (p \in ℤ \land 1 \in ℕ_{0}) \to p^{1} \in ℤ$
43	40 41 42	sylancl	$⊢ p \in ℙ \to p^{1} \in ℤ$
44		dvds0	$⊢ p^{1} \in ℤ \to p^{1} ∥ 0$
45	43 44	syl	$⊢ p \in ℙ \to p^{1} ∥ 0$
46	45	3ad2ant2	$⊢ (A \in ℕ \land p \in ℙ \land A < p) \to p^{1} ∥ 0$
47		dvdsle	$⊢ (p^{1} \in ℤ \land A \in ℕ) \to (p^{1} ∥ A \to p^{1} \leq A)$
48	43 47	sylan	$⊢ (p \in ℙ \land A \in ℕ) \to (p^{1} ∥ A \to p^{1} \leq A)$
49		prmnn	$⊢ p \in ℙ \to p \in ℕ$
50		nnre	$⊢ p \in ℕ \to p \in ℝ$
51	49 50	syl	$⊢ p \in ℙ \to p \in ℝ$
52		reexpcl	$⊢ (p \in ℝ \land 1 \in ℕ_{0}) \to p^{1} \in ℝ$
53	51 41 52	sylancl	$⊢ p \in ℙ \to p^{1} \in ℝ$
54		lenlt	$⊢ (p^{1} \in ℝ \land A \in ℝ) \to (p^{1} \leq A \leftrightarrow \neg A < p^{1})$
55	53 6 54	syl2an	$⊢ (p \in ℙ \land A \in ℕ) \to (p^{1} \leq A \leftrightarrow \neg A < p^{1})$
56	49	nncnd	$⊢ p \in ℙ \to p \in ℂ$
57	56	exp1d	$⊢ p \in ℙ \to p^{1} = p$
58	57	adantr	$⊢ (p \in ℙ \land A \in ℕ) \to p^{1} = p$
59	58	breq2d	$⊢ (p \in ℙ \land A \in ℕ) \to (A < p^{1} \leftrightarrow A < p)$
60	59	notbid	$⊢ (p \in ℙ \land A \in ℕ) \to (\neg A < p^{1} \leftrightarrow \neg A < p)$
61	55 60	bitrd	$⊢ (p \in ℙ \land A \in ℕ) \to (p^{1} \leq A \leftrightarrow \neg A < p)$
62	48 61	sylibd	$⊢ (p \in ℙ \land A \in ℕ) \to (p^{1} ∥ A \to \neg A < p)$
63	62	ancoms	$⊢ (A \in ℕ \land p \in ℙ) \to (p^{1} ∥ A \to \neg A < p)$
64	63	con2d	$⊢ (A \in ℕ \land p \in ℙ) \to (A < p \to \neg p^{1} ∥ A)$
65	64	3impia	$⊢ (A \in ℕ \land p \in ℙ \land A < p) \to \neg p^{1} ∥ A$
66	46 65	jcnd	$⊢ (A \in ℕ \land p \in ℙ \land A < p) \to \neg (p^{1} ∥ 0 \to p^{1} ∥ A)$
67		biimpr	$⊢ (p^{1} ∥ A \leftrightarrow p^{1} ∥ 0) \to (p^{1} ∥ 0 \to p^{1} ∥ A)$
68	66 67	nsyl	$⊢ (A \in ℕ \land p \in ℙ \land A < p) \to \neg (p^{1} ∥ A \leftrightarrow p^{1} ∥ 0)$
69		oveq2	$⊢ n = 1 \to p^{n} = p^{1}$
70	69	breq1d	$⊢ n = 1 \to (p^{n} ∥ A \leftrightarrow p^{1} ∥ A)$
71	69	breq1d	$⊢ n = 1 \to (p^{n} ∥ 0 \leftrightarrow p^{1} ∥ 0)$
72	70 71	bibi12d	$⊢ n = 1 \to ((p^{n} ∥ A \leftrightarrow p^{n} ∥ 0) \leftrightarrow (p^{1} ∥ A \leftrightarrow p^{1} ∥ 0))$
73	72	notbid	$⊢ n = 1 \to (\neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0) \leftrightarrow \neg (p^{1} ∥ A \leftrightarrow p^{1} ∥ 0))$
74	73	rspcev	$⊢ (1 \in ℕ \land \neg (p^{1} ∥ A \leftrightarrow p^{1} ∥ 0)) \to \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0)$
75	39 68 74	sylancr	$⊢ (A \in ℕ \land p \in ℙ \land A < p) \to \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0)$
76	75	3expia	$⊢ (A \in ℕ \land p \in ℙ) \to (A < p \to \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0))$
77	76	reximdva	$⊢ A \in ℕ \to (\exists p \in ℙ A < p \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0))$
78	38 77	mpd	$⊢ A \in ℕ \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0)$
79		rexnal2	$⊢ \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0) \leftrightarrow \neg \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0)$
80	78 79	sylib	$⊢ A \in ℕ \to \neg \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0)$
81	80	pm2.21d	$⊢ A \in ℕ \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0) \to A = 0)$
82		breq2	$⊢ B = 0 \to (p^{n} ∥ B \leftrightarrow p^{n} ∥ 0)$
83	82	bibi2d	$⊢ B = 0 \to ((p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \leftrightarrow (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0))$
84	83	2ralbidv	$⊢ B = 0 \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \leftrightarrow \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0))$
85		eqeq2	$⊢ B = 0 \to (A = B \leftrightarrow A = 0)$
86	84 85	imbi12d	$⊢ B = 0 \to ((\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B) \leftrightarrow (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0) \to A = 0))$
87	81 86	imbitrrid	$⊢ B = 0 \to (A \in ℕ \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B))$
88	37 87	jaoi	$⊢ (B \in ℕ \lor B = 0) \to (A \in ℕ \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B))$
89	5 88	sylbi	$⊢ B \in ℕ_{0} \to (A \in ℕ \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B))$
90	89	com12	$⊢ A \in ℕ \to (B \in ℕ_{0} \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B))$
91		orcom	$⊢ (B \in ℕ \lor B = 0) \leftrightarrow (B = 0 \lor B \in ℕ)$
92		df-or	$⊢ (B = 0 \lor B \in ℕ) \leftrightarrow (\neg B = 0 \to B \in ℕ)$
93	5 91 92	3bitri	$⊢ B \in ℕ_{0} \leftrightarrow (\neg B = 0 \to B \in ℕ)$
94		prmunb	$⊢ B \in ℕ \to \exists p \in ℙ B < p$
95	45	3ad2ant2	$⊢ (B \in ℕ \land p \in ℙ \land B < p) \to p^{1} ∥ 0$
96		dvdsle	$⊢ (p^{1} \in ℤ \land B \in ℕ) \to (p^{1} ∥ B \to p^{1} \leq B)$
97	43 96	sylan	$⊢ (p \in ℙ \land B \in ℕ) \to (p^{1} ∥ B \to p^{1} \leq B)$
98		lenlt	$⊢ (p^{1} \in ℝ \land B \in ℝ) \to (p^{1} \leq B \leftrightarrow \neg B < p^{1})$
99	53 7 98	syl2an	$⊢ (p \in ℙ \land B \in ℕ) \to (p^{1} \leq B \leftrightarrow \neg B < p^{1})$
100	57	adantr	$⊢ (p \in ℙ \land B \in ℕ) \to p^{1} = p$
101	100	breq2d	$⊢ (p \in ℙ \land B \in ℕ) \to (B < p^{1} \leftrightarrow B < p)$
102	101	notbid	$⊢ (p \in ℙ \land B \in ℕ) \to (\neg B < p^{1} \leftrightarrow \neg B < p)$
103	99 102	bitrd	$⊢ (p \in ℙ \land B \in ℕ) \to (p^{1} \leq B \leftrightarrow \neg B < p)$
104	97 103	sylibd	$⊢ (p \in ℙ \land B \in ℕ) \to (p^{1} ∥ B \to \neg B < p)$
105	104	ancoms	$⊢ (B \in ℕ \land p \in ℙ) \to (p^{1} ∥ B \to \neg B < p)$
106	105	con2d	$⊢ (B \in ℕ \land p \in ℙ) \to (B < p \to \neg p^{1} ∥ B)$
107	106	3impia	$⊢ (B \in ℕ \land p \in ℙ \land B < p) \to \neg p^{1} ∥ B$
108	95 107	jcnd	$⊢ (B \in ℕ \land p \in ℙ \land B < p) \to \neg (p^{1} ∥ 0 \to p^{1} ∥ B)$
109		biimp	$⊢ (p^{1} ∥ 0 \leftrightarrow p^{1} ∥ B) \to (p^{1} ∥ 0 \to p^{1} ∥ B)$
110	108 109	nsyl	$⊢ (B \in ℕ \land p \in ℙ \land B < p) \to \neg (p^{1} ∥ 0 \leftrightarrow p^{1} ∥ B)$
111	69	breq1d	$⊢ n = 1 \to (p^{n} ∥ B \leftrightarrow p^{1} ∥ B)$
112	71 111	bibi12d	$⊢ n = 1 \to ((p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B) \leftrightarrow (p^{1} ∥ 0 \leftrightarrow p^{1} ∥ B))$
113	112	notbid	$⊢ n = 1 \to (\neg (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B) \leftrightarrow \neg (p^{1} ∥ 0 \leftrightarrow p^{1} ∥ B))$
114	113	rspcev	$⊢ (1 \in ℕ \land \neg (p^{1} ∥ 0 \leftrightarrow p^{1} ∥ B)) \to \exists n \in ℕ \neg (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B)$
115	39 110 114	sylancr	$⊢ (B \in ℕ \land p \in ℙ \land B < p) \to \exists n \in ℕ \neg (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B)$
116	115	3expia	$⊢ (B \in ℕ \land p \in ℙ) \to (B < p \to \exists n \in ℕ \neg (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B))$
117	116	reximdva	$⊢ B \in ℕ \to (\exists p \in ℙ B < p \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B))$
118	94 117	mpd	$⊢ B \in ℕ \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B)$
119		rexnal2	$⊢ \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B) \leftrightarrow \neg \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B)$
120	118 119	sylib	$⊢ B \in ℕ \to \neg \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B)$
121	120	imim2i	$⊢ (\neg B = 0 \to B \in ℕ) \to (\neg B = 0 \to \neg \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B))$
122	93 121	sylbi	$⊢ B \in ℕ_{0} \to (\neg B = 0 \to \neg \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B))$
123	122	con4d	$⊢ B \in ℕ_{0} \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B) \to B = 0)$
124		eqcom	$⊢ B = 0 \leftrightarrow 0 = B$
125	123 124	imbitrdi	$⊢ B \in ℕ_{0} \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B) \to 0 = B)$
126		breq2	$⊢ A = 0 \to (p^{n} ∥ A \leftrightarrow p^{n} ∥ 0)$
127	126	bibi1d	$⊢ A = 0 \to ((p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \leftrightarrow (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B))$
128	127	2ralbidv	$⊢ A = 0 \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \leftrightarrow \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B))$
129		eqeq1	$⊢ A = 0 \to (A = B \leftrightarrow 0 = B)$
130	128 129	imbi12d	$⊢ A = 0 \to ((\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B) \leftrightarrow (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ 0 \leftrightarrow p^{n} ∥ B) \to 0 = B))$
131	125 130	imbitrrid	$⊢ A = 0 \to (B \in ℕ_{0} \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B))$
132	90 131	jaoi	$⊢ (A \in ℕ \lor A = 0) \to (B \in ℕ_{0} \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B))$
133	132	imp	$⊢ ((A \in ℕ \lor A = 0) \land B \in ℕ_{0}) \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B)$
134	4 133	sylanb	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (\forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B) \to A = B)$
135	3 134	impbid2	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A = B \leftrightarrow \forall p \in ℙ \forall n \in ℕ (p^{n} ∥ A \leftrightarrow p^{n} ∥ B))$

Metamath Proof Explorer

Theorem nn0prpw

Proof