Theorem infpnlem1 7466

Description: Lemma for infpn 7468. The smallest divisor (greater than 1) M of N! + 1 is a prime greater than N.

Hypothesis

Ref	Expression
infpnlem.1	|- K = ((!` N) + 1)

Assertion

Ref	Expression
infpnlem1	|- ((N e. NN /\ M e. NN) -> (((1 < M /\ (K / M) e. NN) /\ A.j e. NN ((1 < j /\ (K / j) e. NN) -> M <_ j)) -> (N < M /\ A.j e. NN ((M / j) e. NN -> (j = 1 \/ j = M)))))

Distinct variable groups:   j,N   j,M   j,K

Proof of Theorem infpnlem1

Step	Hyp	Ref	Expression
1		lenltt 5493	. . . . . . . . . 10 |- ((M e. RR /\ N e. RR) -> (M <_ N <-> -. N < M))
2		nnret 5887	. . . . . . . . . 10 |- (M e. NN -> M e. RR)
3		nnret 5887	. . . . . . . . . 10 |- (N e. NN -> N e. RR)
4	1, 2, 3	syl2an 454	. . . . . . . . 9 |- ((M e. NN /\ N e. NN) -> (M <_ N <-> -. N < M))
5	4	ancoms 436	. . . . . . . 8 |- ((N e. NN /\ M e. NN) -> (M <_ N <-> -. N < M))
6	5	adantr 389	. . . . . . 7 |- (((N e. NN /\ M e. NN) /\ 1 < M) -> (M <_ N <-> -. N < M))
7		facndivt 6895	. . . . . . . . . . 11 |- (((N e. NN0 /\ M e. NN) /\ (1 < M /\ M <_ N)) -> -. (((!` N) + 1) / M) e. ZZ)
8		nnzt 6110	. . . . . . . . . . . 12 |- ((K / M) e. NN -> (K / M) e. ZZ)
9		infpnlem.1	. . . . . . . . . . . . 13 |- K = ((!` N) + 1)
10	9	opreq1i 3966	. . . . . . . . . . . 12 |- (K / M) = (((!` N) + 1) / M)
11	8, 10	syl5eqelr 1551	. . . . . . . . . . 11 |- ((K / M) e. NN -> (((!` N) + 1) / M) e. ZZ)
12	7, 11	nsyl 116	. . . . . . . . . 10 |- (((N e. NN0 /\ M e. NN) /\ (1 < M /\ M <_ N)) -> -. (K / M) e. NN)
13		nnnn0t 6063	. . . . . . . . . 10 |- (N e. NN -> N e. NN0)
14	12, 13	sylanl1 460	. . . . . . . . 9 |- (((N e. NN /\ M e. NN) /\ (1 < M /\ M <_ N)) -> -. (K / M) e. NN)
15	14	exp32 377	. . . . . . . 8 |- ((N e. NN /\ M e. NN) -> (1 < M -> (M <_ N -> -. (K / M) e. NN)))
16	15	imp 350	. . . . . . 7 |- (((N e. NN /\ M e. NN) /\ 1 < M) -> (M <_ N -> -. (K / M) e. NN))
17	6, 16	sylbird 205	. . . . . 6 |- (((N e. NN /\ M e. NN) /\ 1 < M) -> (-. N < M -> -. (K / M) e. NN))
18	17	a3d 75	. . . . 5 |- (((N e. NN /\ M e. NN) /\ 1 < M) -> ((K / M) e. NN -> N < M))
19	18	ex 373	. . . 4 |- ((N e. NN /\ M e. NN) -> (1 < M -> ((K / M) e. NN -> N < M)))
20	19	imp3a 361	. . 3 |- ((N e. NN /\ M e. NN) -> ((1 < M /\ (K / M) e. NN) -> N < M))
21	20	adantrd 391	. 2 |- ((N e. NN /\ M e. NN) -> (((1 < M /\ (K / M) e. NN) /\ A.j e. NN ((1 < j /\ (K / j) e. NN) -> M <_ j)) -> N < M))
22		letri3t 5500	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((j e. RR /\ M e. RR) -> (j = M <-> (j <_ M /\ M <_ j)))
23		nnret 5887	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (j e. NN -> j e. RR)
24	22, 23, 2	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((j e. NN /\ M e. NN) -> (j = M <-> (j <_ M /\ M <_ j)))
25	24	biimprd 154	. . . . . . . . . . . . . . . . . . . . . 22 |- ((j e. NN /\ M e. NN) -> ((j <_ M /\ M <_ j) -> j = M))
26	25	exp4b 379	. . . . . . . . . . . . . . . . . . . . 21 |- (j e. NN -> (M e. NN -> (j <_ M -> (M <_ j -> j = M))))
27	26	com3l 34	. . . . . . . . . . . . . . . . . . . 20 |- (M e. NN -> (j <_ M -> (j e. NN -> (M <_ j -> j = M))))
28	27	imp32 363	. . . . . . . . . . . . . . . . . . 19 |- ((M e. NN /\ (j <_ M /\ j e. NN)) -> (M <_ j -> j = M))
29	28	adantll 392	. . . . . . . . . . . . . . . . . 18 |- (((N e. NN /\ M e. NN) /\ (j <_ M /\ j e. NN)) -> (M <_ j -> j = M))
30	29	imim2d 25	. . . . . . . . . . . . . . . . 17 |- (((N e. NN /\ M e. NN) /\ (j <_ M /\ j e. NN)) -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> ((1 < j /\ (K / j) e. NN) -> j = M)))
31	30	com23 32	. . . . . . . . . . . . . . . 16 |- (((N e. NN /\ M e. NN) /\ (j <_ M /\ j e. NN)) -> ((1 < j /\ (K / j) e. NN) -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> j = M)))
32		nndivtrt 5917	. . . . . . . . . . . . . . . . . . . . 21 |- (((j e. NN /\ M e. NN /\ K e. CC) /\ ((M / j) e. NN /\ (K / M) e. NN)) -> (K / j) e. NN)
33	32	ex 373	. . . . . . . . . . . . . . . . . . . 20 |- ((j e. NN /\ M e. NN /\ K e. CC) -> (((M / j) e. NN /\ (K / M) e. NN) -> (K / j) e. NN))
34	33	3com13 837	. . . . . . . . . . . . . . . . . . 19 |- ((K e. CC /\ M e. NN /\ j e. NN) -> (((M / j) e. NN /\ (K / M) e. NN) -> (K / j) e. NN))
35	34	3expa 832	. . . . . . . . . . . . . . . . . 18 |- (((K e. CC /\ M e. NN) /\ j e. NN) -> (((M / j) e. NN /\ (K / M) e. NN) -> (K / j) e. NN))
36		facclt 6892	. . . . . . . . . . . . . . . . . . . . . 22 |- (N e. NN0 -> (!` N) e. NN)
37	13, 36	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- (N e. NN -> (!` N) e. NN)
38		peano2nn 5893	. . . . . . . . . . . . . . . . . . . . 21 |- ((!` N) e. NN -> ((!` N) + 1) e. NN)
39	37, 38	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (N e. NN -> ((!` N) + 1) e. NN)
40	39, 9	syl5eqel 1550	. . . . . . . . . . . . . . . . . . 19 |- (N e. NN -> K e. NN)
41		nncnt 5888	. . . . . . . . . . . . . . . . . . 19 |- (K e. NN -> K e. CC)
42	40, 41	syl 10	. . . . . . . . . . . . . . . . . 18 |- (N e. NN -> K e. CC)
43	35, 42	sylanl1 460	. . . . . . . . . . . . . . . . 17 |- (((N e. NN /\ M e. NN) /\ j e. NN) -> (((M / j) e. NN /\ (K / M) e. NN) -> (K / j) e. NN))
44	43	adantrl 394	. . . . . . . . . . . . . . . 16 |- (((N e. NN /\ M e. NN) /\ (j <_ M /\ j e. NN)) -> (((M / j) e. NN /\ (K / M) e. NN) -> (K / j) e. NN))
45	31, 44	sylan2d 458	. . . . . . . . . . . . . . 15 |- (((N e. NN /\ M e. NN) /\ (j <_ M /\ j e. NN)) -> ((1 < j /\ ((M / j) e. NN /\ (K / M) e. NN)) -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> j = M)))
46	45	exp4d 381	. . . . . . . . . . . . . 14 |- (((N e. NN /\ M e. NN) /\ (j <_ M /\ j e. NN)) -> (1 < j -> ((M / j) e. NN -> ((K / M) e. NN -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> j = M)))))
47	46	com24 37	. . . . . . . . . . . . 13 |- (((N e. NN /\ M e. NN) /\ (j <_ M /\ j e. NN)) -> ((K / M) e. NN -> ((M / j) e. NN -> (1 < j -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> j = M)))))
48	47	exp32 377	. . . . . . . . . . . 12 |- ((N e. NN /\ M e. NN) -> (j <_ M -> (j e. NN -> ((K / M) e. NN -> ((M / j) e. NN -> (1 < j -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> j = M)))))))
49	48	com24 37	. . . . . . . . . . 11 |- ((N e. NN /\ M e. NN) -> ((K / M) e. NN -> (j e. NN -> (j <_ M -> ((M / j) e. NN -> (1 < j -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> j = M)))))))
50	49	imp31 362	. . . . . . . . . 10 |- ((((N e. NN /\ M e. NN) /\ (K / M) e. NN) /\ j e. NN) -> (j <_ M -> ((M / j) e. NN -> (1 < j -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> j = M)))))
51	50	com14 38	. . . . . . . . 9 |- (1 < j -> (j <_ M -> ((M / j) e. NN -> ((((N e. NN /\ M e. NN) /\ (K / M) e. NN) /\ j e. NN) -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> j = M)))))
52	51	3imp 826	. . . . . . . 8 |- ((1 < j /\ j <_ M /\ (M / j) e. NN) -> ((((N e. NN /\ M e. NN) /\ (K / M) e. NN) /\ j e. NN) -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> j = M)))
53	52	com3l 34	. . . . . . 7 |- ((((N e. NN /\ M e. NN) /\ (K / M) e. NN) /\ j e. NN) -> (((1 < j /\ (