exprmfct

Description: Every integer greater than or equal to 2 has a prime factor. (Contributed by Paul Chapman, 26-Oct-2012) (Proof shortened by Mario Carneiro, 20-Jun-2015)

		Ref	Expression
	Assertion	exprmfct	$⊢ N \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ N$

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
2		eleq1	$⊢ x = 1 \to (x \in ℤ_{\geq 2} \leftrightarrow 1 \in ℤ_{\geq 2})$
3	2	imbi1d	$⊢ x = 1 \to ((x \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ x) \leftrightarrow (1 \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ x))$
4		eleq1	$⊢ x = y \to (x \in ℤ_{\geq 2} \leftrightarrow y \in ℤ_{\geq 2})$
5		breq2	$⊢ x = y \to (p ∥ x \leftrightarrow p ∥ y)$
6	5	rexbidv	$⊢ x = y \to (\exists p \in ℙ p ∥ x \leftrightarrow \exists p \in ℙ p ∥ y)$
7	4 6	imbi12d	$⊢ x = y \to ((x \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ x) \leftrightarrow (y \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ y))$
8		eleq1	$⊢ x = z \to (x \in ℤ_{\geq 2} \leftrightarrow z \in ℤ_{\geq 2})$
9		breq2	$⊢ x = z \to (p ∥ x \leftrightarrow p ∥ z)$
10	9	rexbidv	$⊢ x = z \to (\exists p \in ℙ p ∥ x \leftrightarrow \exists p \in ℙ p ∥ z)$
11	8 10	imbi12d	$⊢ x = z \to ((x \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ x) \leftrightarrow (z \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ z))$
12		eleq1	$⊢ x = y z \to (x \in ℤ_{\geq 2} \leftrightarrow y z \in ℤ_{\geq 2})$
13		breq2	$⊢ x = y z \to (p ∥ x \leftrightarrow p ∥ y z)$
14	13	rexbidv	$⊢ x = y z \to (\exists p \in ℙ p ∥ x \leftrightarrow \exists p \in ℙ p ∥ y z)$
15	12 14	imbi12d	$⊢ x = y z \to ((x \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ x) \leftrightarrow (y z \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ y z))$
16		eleq1	$⊢ x = N \to (x \in ℤ_{\geq 2} \leftrightarrow N \in ℤ_{\geq 2})$
17		breq2	$⊢ x = N \to (p ∥ x \leftrightarrow p ∥ N)$
18	17	rexbidv	$⊢ x = N \to (\exists p \in ℙ p ∥ x \leftrightarrow \exists p \in ℙ p ∥ N)$
19	16 18	imbi12d	$⊢ x = N \to ((x \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ x) \leftrightarrow (N \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ N))$
20		1m1e0	$⊢ 1 - 1 = 0$
21		uz2m1nn	$⊢ 1 \in ℤ_{\geq 2} \to 1 - 1 \in ℕ$
22	20 21	eqeltrrid	$⊢ 1 \in ℤ_{\geq 2} \to 0 \in ℕ$
23		0nnn	$⊢ \neg 0 \in ℕ$
24	23	pm2.21i	$⊢ 0 \in ℕ \to \exists p \in ℙ p ∥ x$
25	22 24	syl	$⊢ 1 \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ x$
26		prmz	$⊢ x \in ℙ \to x \in ℤ$
27		iddvds	$⊢ x \in ℤ \to x ∥ x$
28	26 27	syl	$⊢ x \in ℙ \to x ∥ x$
29		breq1	$⊢ p = x \to (p ∥ x \leftrightarrow x ∥ x)$
30	29	rspcev	$⊢ (x \in ℙ \land x ∥ x) \to \exists p \in ℙ p ∥ x$
31	28 30	mpdan	$⊢ x \in ℙ \to \exists p \in ℙ p ∥ x$
32	31	a1d	$⊢ x \in ℙ \to (x \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ x)$
33		simpl	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to y \in ℤ_{\geq 2}$
34		eluzelz	$⊢ y \in ℤ_{\geq 2} \to y \in ℤ$
35	34	ad2antrr	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to y \in ℤ$
36		eluzelz	$⊢ z \in ℤ_{\geq 2} \to z \in ℤ$
37	36	ad2antlr	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to z \in ℤ$
38		dvdsmul1	$⊢ (y \in ℤ \land z \in ℤ) \to y ∥ y z$
39	35 37 38	syl2anc	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to y ∥ y z$
40		prmz	$⊢ p \in ℙ \to p \in ℤ$
41	40	adantl	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to p \in ℤ$
42	35 37	zmulcld	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to y z \in ℤ$
43		dvdstr	$⊢ (p \in ℤ \land y \in ℤ \land y z \in ℤ) \to ((p ∥ y \land y ∥ y z) \to p ∥ y z)$
44	41 35 42 43	syl3anc	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to ((p ∥ y \land y ∥ y z) \to p ∥ y z)$
45	39 44	mpan2d	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to (p ∥ y \to p ∥ y z)$
46	45	reximdva	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to (\exists p \in ℙ p ∥ y \to \exists p \in ℙ p ∥ y z)$
47	33 46	embantd	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to ((y \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ y) \to \exists p \in ℙ p ∥ y z)$
48	47	a1dd	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to ((y \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ y) \to (y z \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ y z))$
49	48	adantrd	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to (((y \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ y) \land (z \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ z)) \to (y z \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ y z))$
50	3 7 11 15 19 25 32 49	prmind	$⊢ N \in ℕ \to (N \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ N)$
51	1 50	mpcom	$⊢ N \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ N$

Metamath Proof Explorer

Theorem exprmfct

Proof