infpnlem1

Description: Lemma for infpn . The smallest divisor (greater than 1) M of N ! + 1 is a prime greater than N . (Contributed by NM, 5-May-2005)

		Ref	Expression
	Hypothesis	infpnlem.1	$⊢ K = N! + 1$
	Assertion	infpnlem1	$⊢ (N \in ℕ \land M \in ℕ) \to (((1 < M \land \frac{K}{M} \in ℕ) \land \forall j \in ℕ ((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j)) \to (N < M \land \forall j \in ℕ (\frac{M}{j} \in ℕ \to (j = 1 \lor j = M))))$

Proof

Step	Hyp	Ref	Expression
1		infpnlem.1	$⊢ K = N! + 1$
2		nnre	$⊢ M \in ℕ \to M \in ℝ$
3		nnre	$⊢ N \in ℕ \to N \in ℝ$
4		lenlt	$⊢ (M \in ℝ \land N \in ℝ) \to (M \leq N \leftrightarrow \neg N < M)$
5	2 3 4	syl2anr	$⊢ (N \in ℕ \land M \in ℕ) \to (M \leq N \leftrightarrow \neg N < M)$
6	5	adantr	$⊢ ((N \in ℕ \land M \in ℕ) \land 1 < M) \to (M \leq N \leftrightarrow \neg N < M)$
7		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
8		facndiv	$⊢ ((N \in ℕ_{0} \land M \in ℕ) \land (1 < M \land M \leq N)) \to \neg \frac{N! + 1}{M} \in ℤ$
9	1	oveq1i	$⊢ \frac{K}{M} = \frac{N! + 1}{M}$
10		nnz	$⊢ \frac{K}{M} \in ℕ \to \frac{K}{M} \in ℤ$
11	9 10	eqeltrrid	$⊢ \frac{K}{M} \in ℕ \to \frac{N! + 1}{M} \in ℤ$
12	8 11	nsyl	$⊢ ((N \in ℕ_{0} \land M \in ℕ) \land (1 < M \land M \leq N)) \to \neg \frac{K}{M} \in ℕ$
13	7 12	sylanl1	$⊢ ((N \in ℕ \land M \in ℕ) \land (1 < M \land M \leq N)) \to \neg \frac{K}{M} \in ℕ$
14	13	expr	$⊢ ((N \in ℕ \land M \in ℕ) \land 1 < M) \to (M \leq N \to \neg \frac{K}{M} \in ℕ)$
15	6 14	sylbird	$⊢ ((N \in ℕ \land M \in ℕ) \land 1 < M) \to (\neg N < M \to \neg \frac{K}{M} \in ℕ)$
16	15	con4d	$⊢ ((N \in ℕ \land M \in ℕ) \land 1 < M) \to (\frac{K}{M} \in ℕ \to N < M)$
17	16	expimpd	$⊢ (N \in ℕ \land M \in ℕ) \to ((1 < M \land \frac{K}{M} \in ℕ) \to N < M)$
18	17	adantrd	$⊢ (N \in ℕ \land M \in ℕ) \to (((1 < M \land \frac{K}{M} \in ℕ) \land \forall j \in ℕ ((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j)) \to N < M)$
19	7	faccld	$⊢ N \in ℕ \to N! \in ℕ$
20	19	peano2nnd	$⊢ N \in ℕ \to N! + 1 \in ℕ$
21	1 20	eqeltrid	$⊢ N \in ℕ \to K \in ℕ$
22	21	nncnd	$⊢ N \in ℕ \to K \in ℂ$
23		nndivtr	$⊢ ((j \in ℕ \land M \in ℕ \land K \in ℂ) \land (\frac{M}{j} \in ℕ \land \frac{K}{M} \in ℕ)) \to \frac{K}{j} \in ℕ$
24	23	ex	$⊢ (j \in ℕ \land M \in ℕ \land K \in ℂ) \to ((\frac{M}{j} \in ℕ \land \frac{K}{M} \in ℕ) \to \frac{K}{j} \in ℕ)$
25	24	3com13	$⊢ (K \in ℂ \land M \in ℕ \land j \in ℕ) \to ((\frac{M}{j} \in ℕ \land \frac{K}{M} \in ℕ) \to \frac{K}{j} \in ℕ)$
26	25	3expa	$⊢ ((K \in ℂ \land M \in ℕ) \land j \in ℕ) \to ((\frac{M}{j} \in ℕ \land \frac{K}{M} \in ℕ) \to \frac{K}{j} \in ℕ)$
27	22 26	sylanl1	$⊢ ((N \in ℕ \land M \in ℕ) \land j \in ℕ) \to ((\frac{M}{j} \in ℕ \land \frac{K}{M} \in ℕ) \to \frac{K}{j} \in ℕ)$
28	27	adantrl	$⊢ ((N \in ℕ \land M \in ℕ) \land (j \leq M \land j \in ℕ)) \to ((\frac{M}{j} \in ℕ \land \frac{K}{M} \in ℕ) \to \frac{K}{j} \in ℕ)$
29		nnre	$⊢ j \in ℕ \to j \in ℝ$
30		letri3	$⊢ (j \in ℝ \land M \in ℝ) \to (j = M \leftrightarrow (j \leq M \land M \leq j))$
31	29 2 30	syl2an	$⊢ (j \in ℕ \land M \in ℕ) \to (j = M \leftrightarrow (j \leq M \land M \leq j))$
32	31	biimprd	$⊢ (j \in ℕ \land M \in ℕ) \to ((j \leq M \land M \leq j) \to j = M)$
33	32	exp4b	$⊢ j \in ℕ \to (M \in ℕ \to (j \leq M \to (M \leq j \to j = M)))$
34	33	com3l	$⊢ M \in ℕ \to (j \leq M \to (j \in ℕ \to (M \leq j \to j = M)))$
35	34	imp32	$⊢ (M \in ℕ \land (j \leq M \land j \in ℕ)) \to (M \leq j \to j = M)$
36	35	adantll	$⊢ ((N \in ℕ \land M \in ℕ) \land (j \leq M \land j \in ℕ)) \to (M \leq j \to j = M)$
37	36	imim2d	$⊢ ((N \in ℕ \land M \in ℕ) \land (j \leq M \land j \in ℕ)) \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to ((1 < j \land \frac{K}{j} \in ℕ) \to j = M))$
38	37	com23	$⊢ ((N \in ℕ \land M \in ℕ) \land (j \leq M \land j \in ℕ)) \to ((1 < j \land \frac{K}{j} \in ℕ) \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to j = M))$
39	28 38	sylan2d	$⊢ ((N \in ℕ \land M \in ℕ) \land (j \leq M \land j \in ℕ)) \to ((1 < j \land (\frac{M}{j} \in ℕ \land \frac{K}{M} \in ℕ)) \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to j = M))$
40	39	exp4d	$⊢ ((N \in ℕ \land M \in ℕ) \land (j \leq M \land j \in ℕ)) \to (1 < j \to (\frac{M}{j} \in ℕ \to (\frac{K}{M} \in ℕ \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to j = M))))$
41	40	com24	$⊢ ((N \in ℕ \land M \in ℕ) \land (j \leq M \land j \in ℕ)) \to (\frac{K}{M} \in ℕ \to (\frac{M}{j} \in ℕ \to (1 < j \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to j = M))))$
42	41	exp32	$⊢ (N \in ℕ \land M \in ℕ) \to (j \leq M \to (j \in ℕ \to (\frac{K}{M} \in ℕ \to (\frac{M}{j} \in ℕ \to (1 < j \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to j = M))))))$
43	42	com24	$⊢ (N \in ℕ \land M \in ℕ) \to (\frac{K}{M} \in ℕ \to (j \in ℕ \to (j \leq M \to (\frac{M}{j} \in ℕ \to (1 < j \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to j = M))))))$
44	43	imp31	$⊢ (((N \in ℕ \land M \in ℕ) \land \frac{K}{M} \in ℕ) \land j \in ℕ) \to (j \leq M \to (\frac{M}{j} \in ℕ \to (1 < j \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to j = M))))$
45	44	com14	$⊢ 1 < j \to (j \leq M \to (\frac{M}{j} \in ℕ \to ((((N \in ℕ \land M \in ℕ) \land \frac{K}{M} \in ℕ) \land j \in ℕ) \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to j = M))))$
46	45	3imp	$⊢ (1 < j \land j \leq M \land \frac{M}{j} \in ℕ) \to ((((N \in ℕ \land M \in ℕ) \land \frac{K}{M} \in ℕ) \land j \in ℕ) \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to j = M))$
47	46	com3l	$⊢ (((N \in ℕ \land M \in ℕ) \land \frac{K}{M} \in ℕ) \land j \in ℕ) \to (((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to ((1 < j \land j \leq M \land \frac{M}{j} \in ℕ) \to j = M))$
48	47	ralimdva	$⊢ ((N \in ℕ \land M \in ℕ) \land \frac{K}{M} \in ℕ) \to (\forall j \in ℕ ((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to \forall j \in ℕ ((1 < j \land j \leq M \land \frac{M}{j} \in ℕ) \to j = M))$
49	48	ex	$⊢ (N \in ℕ \land M \in ℕ) \to (\frac{K}{M} \in ℕ \to (\forall j \in ℕ ((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to \forall j \in ℕ ((1 < j \land j \leq M \land \frac{M}{j} \in ℕ) \to j = M)))$
50	49	adantld	$⊢ (N \in ℕ \land M \in ℕ) \to ((1 < M \land \frac{K}{M} \in ℕ) \to (\forall j \in ℕ ((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j) \to \forall j \in ℕ ((1 < j \land j \leq M \land \frac{M}{j} \in ℕ) \to j = M)))$
51	50	impd	$⊢ (N \in ℕ \land M \in ℕ) \to (((1 < M \land \frac{K}{M} \in ℕ) \land \forall j \in ℕ ((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j)) \to \forall j \in ℕ ((1 < j \land j \leq M \land \frac{M}{j} \in ℕ) \to j = M))$
52		prime	$⊢ M \in ℕ \to (\forall j \in ℕ (\frac{M}{j} \in ℕ \to (j = 1 \lor j = M)) \leftrightarrow \forall j \in ℕ ((1 < j \land j \leq M \land \frac{M}{j} \in ℕ) \to j = M))$
53	52	adantl	$⊢ (N \in ℕ \land M \in ℕ) \to (\forall j \in ℕ (\frac{M}{j} \in ℕ \to (j = 1 \lor j = M)) \leftrightarrow \forall j \in ℕ ((1 < j \land j \leq M \land \frac{M}{j} \in ℕ) \to j = M))$
54	51 53	sylibrd	$⊢ (N \in ℕ \land M \in ℕ) \to (((1 < M \land \frac{K}{M} \in ℕ) \land \forall j \in ℕ ((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j)) \to \forall j \in ℕ (\frac{M}{j} \in ℕ \to (j = 1 \lor j = M)))$
55	18 54	jcad	$⊢ (N \in ℕ \land M \in ℕ) \to (((1 < M \land \frac{K}{M} \in ℕ) \land \forall j \in ℕ ((1 < j \land \frac{K}{j} \in ℕ) \to M \leq j)) \to (N < M \land \forall j \in ℕ (\frac{M}{j} \in ℕ \to (j = 1 \lor j = M))))$

Metamath Proof Explorer

Theorem infpnlem1

Proof