ztprmneprm

Description: A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019)

		Ref	Expression
	Assertion	ztprmneprm	$⊢ (Z \in ℤ \land A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B)$

Proof

Step	Hyp	Ref	Expression
1		elznn0nn	$⊢ Z \in ℤ \leftrightarrow (Z \in ℕ_{0} \lor (Z \in ℝ \land - Z \in ℕ))$
2		elnn0	$⊢ Z \in ℕ_{0} \leftrightarrow (Z \in ℕ \lor Z = 0)$
3		elnn1uz2	$⊢ Z \in ℕ \leftrightarrow (Z = 1 \lor Z \in ℤ_{\geq 2})$
4		oveq1	$⊢ Z = 1 \to Z A = 1 A$
5	4	adantr	$⊢ (Z = 1 \land (A \in ℙ \land B \in ℙ)) \to Z A = 1 A$
6	5	eqeq1d	$⊢ (Z = 1 \land (A \in ℙ \land B \in ℙ)) \to (Z A = B \leftrightarrow 1 A = B)$
7		prmz	$⊢ A \in ℙ \to A \in ℤ$
8	7	zcnd	$⊢ A \in ℙ \to A \in ℂ$
9	8	mullidd	$⊢ A \in ℙ \to 1 A = A$
10	9	adantr	$⊢ (A \in ℙ \land B \in ℙ) \to 1 A = A$
11	10	eqeq1d	$⊢ (A \in ℙ \land B \in ℙ) \to (1 A = B \leftrightarrow A = B)$
12	11	biimpd	$⊢ (A \in ℙ \land B \in ℙ) \to (1 A = B \to A = B)$
13	12	adantl	$⊢ (Z = 1 \land (A \in ℙ \land B \in ℙ)) \to (1 A = B \to A = B)$
14	6 13	sylbid	$⊢ (Z = 1 \land (A \in ℙ \land B \in ℙ)) \to (Z A = B \to A = B)$
15	14	ex	$⊢ Z = 1 \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
16		prmuz2	$⊢ A \in ℙ \to A \in ℤ_{\geq 2}$
17	16	adantr	$⊢ (A \in ℙ \land B \in ℙ) \to A \in ℤ_{\geq 2}$
18		nprm	$⊢ (Z \in ℤ_{\geq 2} \land A \in ℤ_{\geq 2}) \to \neg Z A \in ℙ$
19	17 18	sylan2	$⊢ (Z \in ℤ_{\geq 2} \land (A \in ℙ \land B \in ℙ)) \to \neg Z A \in ℙ$
20		eleq1	$⊢ Z A = B \to (Z A \in ℙ \leftrightarrow B \in ℙ)$
21	20	notbid	$⊢ Z A = B \to (\neg Z A \in ℙ \leftrightarrow \neg B \in ℙ)$
22		pm2.24	$⊢ B \in ℙ \to (\neg B \in ℙ \to A = B)$
23	22	adantl	$⊢ (A \in ℙ \land B \in ℙ) \to (\neg B \in ℙ \to A = B)$
24	23	adantl	$⊢ (Z \in ℤ_{\geq 2} \land (A \in ℙ \land B \in ℙ)) \to (\neg B \in ℙ \to A = B)$
25	24	com12	$⊢ \neg B \in ℙ \to ((Z \in ℤ_{\geq 2} \land (A \in ℙ \land B \in ℙ)) \to A = B)$
26	21 25	biimtrdi	$⊢ Z A = B \to (\neg Z A \in ℙ \to ((Z \in ℤ_{\geq 2} \land (A \in ℙ \land B \in ℙ)) \to A = B))$
27	26	com3l	$⊢ \neg Z A \in ℙ \to ((Z \in ℤ_{\geq 2} \land (A \in ℙ \land B \in ℙ)) \to (Z A = B \to A = B))$
28	19 27	mpcom	$⊢ (Z \in ℤ_{\geq 2} \land (A \in ℙ \land B \in ℙ)) \to (Z A = B \to A = B)$
29	28	ex	$⊢ Z \in ℤ_{\geq 2} \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
30	15 29	jaoi	$⊢ (Z = 1 \lor Z \in ℤ_{\geq 2}) \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
31	3 30	sylbi	$⊢ Z \in ℕ \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
32		oveq1	$⊢ Z = 0 \to Z A = 0 \cdot A$
33	32	eqeq1d	$⊢ Z = 0 \to (Z A = B \leftrightarrow 0 \cdot A = B)$
34		prmnn	$⊢ A \in ℙ \to A \in ℕ$
35	34	nnred	$⊢ A \in ℙ \to A \in ℝ$
36		mul02lem2	$⊢ A \in ℝ \to 0 \cdot A = 0$
37	35 36	syl	$⊢ A \in ℙ \to 0 \cdot A = 0$
38	37	adantr	$⊢ (A \in ℙ \land B \in ℙ) \to 0 \cdot A = 0$
39	38	eqeq1d	$⊢ (A \in ℙ \land B \in ℙ) \to (0 \cdot A = B \leftrightarrow 0 = B)$
40		prmnn	$⊢ B \in ℙ \to B \in ℕ$
41		elnnne0	$⊢ B \in ℕ \leftrightarrow (B \in ℕ_{0} \land B \neq 0)$
42		eqneqall	$⊢ B = 0 \to (B \neq 0 \to A = B)$
43	42	eqcoms	$⊢ 0 = B \to (B \neq 0 \to A = B)$
44	43	com12	$⊢ B \neq 0 \to (0 = B \to A = B)$
45	44	adantl	$⊢ (B \in ℕ_{0} \land B \neq 0) \to (0 = B \to A = B)$
46	41 45	sylbi	$⊢ B \in ℕ \to (0 = B \to A = B)$
47	40 46	syl	$⊢ B \in ℙ \to (0 = B \to A = B)$
48	47	adantl	$⊢ (A \in ℙ \land B \in ℙ) \to (0 = B \to A = B)$
49	39 48	sylbid	$⊢ (A \in ℙ \land B \in ℙ) \to (0 \cdot A = B \to A = B)$
50	49	com12	$⊢ 0 \cdot A = B \to ((A \in ℙ \land B \in ℙ) \to A = B)$
51	33 50	biimtrdi	$⊢ Z = 0 \to (Z A = B \to ((A \in ℙ \land B \in ℙ) \to A = B))$
52	51	com23	$⊢ Z = 0 \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
53	31 52	jaoi	$⊢ (Z \in ℕ \lor Z = 0) \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
54	2 53	sylbi	$⊢ Z \in ℕ_{0} \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
55		elnnz	$⊢ - Z \in ℕ \leftrightarrow (- Z \in ℤ \land 0 < - Z)$
56		lt0neg1	$⊢ Z \in ℝ \to (Z < 0 \leftrightarrow 0 < - Z)$
57	34	nngt0d	$⊢ A \in ℙ \to 0 < A$
58	57	adantr	$⊢ (A \in ℙ \land B \in ℙ) \to 0 < A$
59		simpr	$⊢ (Z \in ℝ \land Z < 0) \to Z < 0$
60	58 59	anim12ci	$⊢ ((A \in ℙ \land B \in ℙ) \land (Z \in ℝ \land Z < 0)) \to (Z < 0 \land 0 < A)$
61	60	orcd	$⊢ ((A \in ℙ \land B \in ℙ) \land (Z \in ℝ \land Z < 0)) \to ((Z < 0 \land 0 < A) \lor (0 < Z \land A < 0))$
62		simprl	$⊢ ((A \in ℙ \land B \in ℙ) \land (Z \in ℝ \land Z < 0)) \to Z \in ℝ$
63	35	adantr	$⊢ (A \in ℙ \land B \in ℙ) \to A \in ℝ$
64	63	adantr	$⊢ ((A \in ℙ \land B \in ℙ) \land (Z \in ℝ \land Z < 0)) \to A \in ℝ$
65	62 64	mul2lt0bi	$⊢ ((A \in ℙ \land B \in ℙ) \land (Z \in ℝ \land Z < 0)) \to (Z A < 0 \leftrightarrow ((Z < 0 \land 0 < A) \lor (0 < Z \land A < 0)))$
66	61 65	mpbird	$⊢ ((A \in ℙ \land B \in ℙ) \land (Z \in ℝ \land Z < 0)) \to Z A < 0$
67	66	ex	$⊢ (A \in ℙ \land B \in ℙ) \to ((Z \in ℝ \land Z < 0) \to Z A < 0)$
68		breq1	$⊢ Z A = B \to (Z A < 0 \leftrightarrow B < 0)$
69	68	adantl	$⊢ ((A \in ℙ \land B \in ℙ) \land Z A = B) \to (Z A < 0 \leftrightarrow B < 0)$
70		nnnn0	$⊢ B \in ℕ \to B \in ℕ_{0}$
71		nn0nlt0	$⊢ B \in ℕ_{0} \to \neg B < 0$
72	71	pm2.21d	$⊢ B \in ℕ_{0} \to (B < 0 \to A = B)$
73	70 72	syl	$⊢ B \in ℕ \to (B < 0 \to A = B)$
74	40 73	syl	$⊢ B \in ℙ \to (B < 0 \to A = B)$
75	74	adantl	$⊢ (A \in ℙ \land B \in ℙ) \to (B < 0 \to A = B)$
76	75	adantr	$⊢ ((A \in ℙ \land B \in ℙ) \land Z A = B) \to (B < 0 \to A = B)$
77	69 76	sylbid	$⊢ ((A \in ℙ \land B \in ℙ) \land Z A = B) \to (Z A < 0 \to A = B)$
78	77	ex	$⊢ (A \in ℙ \land B \in ℙ) \to (Z A = B \to (Z A < 0 \to A = B))$
79	78	com23	$⊢ (A \in ℙ \land B \in ℙ) \to (Z A < 0 \to (Z A = B \to A = B))$
80	67 79	syldc	$⊢ (Z \in ℝ \land Z < 0) \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
81	80	ex	$⊢ Z \in ℝ \to (Z < 0 \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B)))$
82	56 81	sylbird	$⊢ Z \in ℝ \to (0 < - Z \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B)))$
83	82	adantld	$⊢ Z \in ℝ \to ((- Z \in ℤ \land 0 < - Z) \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B)))$
84	55 83	biimtrid	$⊢ Z \in ℝ \to (- Z \in ℕ \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B)))$
85	84	imp	$⊢ (Z \in ℝ \land - Z \in ℕ) \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
86	54 85	jaoi	$⊢ (Z \in ℕ_{0} \lor (Z \in ℝ \land - Z \in ℕ)) \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
87	1 86	sylbi	$⊢ Z \in ℤ \to ((A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B))$
88	87	3impib	$⊢ (Z \in ℤ \land A \in ℙ \land B \in ℙ) \to (Z A = B \to A = B)$

Metamath Proof Explorer

Theorem ztprmneprm

Proof