prmdvdsprmop

Description: The primorial of a number plus an integer greater than 1 and less then or equal to the number is divisible by a prime less then or equal to the number. (Contributed by AV, 15-Aug-2020) (Revised by AV, 28-Aug-2020)

		Ref	Expression
	Assertion	prmdvdsprmop	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \exists p \in ℙ (p \leq N \land p ∥ I \land p ∥ (#_{p} (N) + I))$

Proof

Step	Hyp	Ref	Expression
1		prmdvdsfz	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \exists p \in ℙ (p \leq N \land p ∥ I)$
2		simprl	$⊢ (((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \land (p \leq N \land p ∥ I)) \to p \leq N$
3		simprr	$⊢ (((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \land (p \leq N \land p ∥ I)) \to p ∥ I$
4		prmz	$⊢ p \in ℙ \to p \in ℤ$
5	4	ad2antlr	$⊢ (((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \land (p \leq N \land p ∥ I)) \to p \in ℤ$
6		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
7		prmocl	$⊢ N \in ℕ_{0} \to #_{p} (N) \in ℕ$
8	6 7	syl	$⊢ N \in ℕ \to #_{p} (N) \in ℕ$
9	8	nnzd	$⊢ N \in ℕ \to #_{p} (N) \in ℤ$
10	9	adantr	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to #_{p} (N) \in ℤ$
11	10	adantr	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to #_{p} (N) \in ℤ$
12	11	adantr	$⊢ (((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \land (p \leq N \land p ∥ I)) \to #_{p} (N) \in ℤ$
13		elfzelz	$⊢ I \in (2 \dots N) \to I \in ℤ$
14	13	ad2antlr	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to I \in ℤ$
15	14	adantr	$⊢ (((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \land (p \leq N \land p ∥ I)) \to I \in ℤ$
16		prmdvdsprmo	$⊢ N \in ℕ \to \forall q \in ℙ (q \leq N \to q ∥ #_{p} (N))$
17		breq1	$⊢ q = p \to (q \leq N \leftrightarrow p \leq N)$
18		breq1	$⊢ q = p \to (q ∥ #_{p} (N) \leftrightarrow p ∥ #_{p} (N))$
19	17 18	imbi12d	$⊢ q = p \to ((q \leq N \to q ∥ #_{p} (N)) \leftrightarrow (p \leq N \to p ∥ #_{p} (N)))$
20	19	rspcv	$⊢ p \in ℙ \to (\forall q \in ℙ (q \leq N \to q ∥ #_{p} (N)) \to (p \leq N \to p ∥ #_{p} (N)))$
21	16 20	syl5com	$⊢ N \in ℕ \to (p \in ℙ \to (p \leq N \to p ∥ #_{p} (N)))$
22	21	adantr	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to (p \in ℙ \to (p \leq N \to p ∥ #_{p} (N)))$
23	22	imp	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to (p \leq N \to p ∥ #_{p} (N))$
24	23	adantrd	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to ((p \leq N \land p ∥ I) \to p ∥ #_{p} (N))$
25	24	imp	$⊢ (((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \land (p \leq N \land p ∥ I)) \to p ∥ #_{p} (N)$
26	5 12 15 25 3	dvds2addd	$⊢ (((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \land (p \leq N \land p ∥ I)) \to p ∥ (#_{p} (N) + I)$
27	2 3 26	3jca	$⊢ (((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \land (p \leq N \land p ∥ I)) \to (p \leq N \land p ∥ I \land p ∥ (#_{p} (N) + I))$
28	27	ex	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land p \in ℙ) \to ((p \leq N \land p ∥ I) \to (p \leq N \land p ∥ I \land p ∥ (#_{p} (N) + I)))$
29	28	reximdva	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to (\exists p \in ℙ (p \leq N \land p ∥ I) \to \exists p \in ℙ (p \leq N \land p ∥ I \land p ∥ (#_{p} (N) + I)))$
30	1 29	mpd	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \exists p \in ℙ (p \leq N \land p ∥ I \land p ∥ (#_{p} (N) + I))$

Metamath Proof Explorer

Theorem prmdvdsprmop

Proof