Theorem infpnlem1 9388

Description: Lemma for infpn 9390. 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		nnre 7445	. . . . . . . . 9 |- (M e. NN -> M e. RR)
2		nnre 7445	. . . . . . . . 9 |- (N e. NN -> N e. RR)
3		lenlt 6869	. . . . . . . . 9 |- ((M e. RR /\ N e. RR) -> (M <_ N <-> -. N < M))
4	1, 2, 3	syl2an 603	. . . . . . . 8 |- ((M e. NN /\ N e. NN) -> (M <_ N <-> -. N < M))
5	4	ancoms 416	. . . . . . 7 |- ((N e. NN /\ M e. NN) -> (M <_ N <-> -. N < M))
6	5	adantr 447	. . . . . 6 |- (((N e. NN /\ M e. NN) /\ 1 < M) -> (M <_ N <-> -. N < M))
7		nnnn0 7655	. . . . . . . 8 |- (N e. NN -> N e. NN0)
8		facndiv 8580	. . . . . . . . 9 |- (((N e. NN0 /\ M e. NN) /\ (1 < M /\ M <_ N)) -> -. (((!` N) + 1) / M) e. ZZ)
9		infpnlem.1	. . . . . . . . . . 11 |- K = ((!` N) + 1)
10	9	opreq1i 4989	. . . . . . . . . 10 |- (K / M) = (((!` N) + 1) / M)
11		nnz 7703	. . . . . . . . . 10 |- ((K / M) e. NN -> (K / M) e. ZZ)
12	10, 11	syl5eqelr 2224	. . . . . . . . 9 |- ((K / M) e. NN -> (((!` N) + 1) / M) e. ZZ)
13	8, 12	nsyl 165	. . . . . . . 8 |- (((N e. NN0 /\ M e. NN) /\ (1 < M /\ M <_ N)) -> -. (K / M) e. NN)
14	7, 13	sylanl1 641	. . . . . . 7 |- (((N e. NN /\ M e. NN) /\ (1 < M /\ M <_ N)) -> -. (K / M) e. NN)
15	14	expr 589	. . . . . 6 |- (((N e. NN /\ M e. NN) /\ 1 < M) -> (M <_ N -> -. (K / M) e. NN))
16	6, 15	sylbird 248	. . . . 5 |- (((N e. NN /\ M e. NN) /\ 1 < M) -> (-. N < M -> -. (K / M) e. NN))
17	16	con4d 122	. . . 4 |- (((N e. NN /\ M e. NN) /\ 1 < M) -> ((K / M) e. NN -> N < M))
18	17	expimpd 576	. . 3 |- ((N e. NN /\ M e. NN) -> ((1 < M /\ (K / M) e. NN) -> N < M))
19	18	adantrd 452	. 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))
20		faccl 8577	. . . . . . . . . . . . . . . . . . . . . 22 |- (N e. NN0 -> (!` N) e. NN)
21	7, 20	syl 13	. . . . . . . . . . . . . . . . . . . . 21 |- (N e. NN -> (!` N) e. NN)
22		peano2nn 7451	. . . . . . . . . . . . . . . . . . . . 21 |- ((!` N) e. NN -> ((!` N) + 1) e. NN)
23	21, 22	syl 13	. . . . . . . . . . . . . . . . . . . 20 |- (N e. NN -> ((!` N) + 1) e. NN)
24	9, 23	syl5eqel 2222	. . . . . . . . . . . . . . . . . . 19 |- (N e. NN -> K e. NN)
25		nncn 7446	. . . . . . . . . . . . . . . . . . 19 |- (K e. NN -> K e. CC)
26	24, 25	syl 13	. . . . . . . . . . . . . . . . . 18 |- (N e. NN -> K e. CC)
27		nndivtr 7477	. . . . . . . . . . . . . . . . . . . . 21 |- (((j e. NN /\ M e. NN /\ K e. CC) /\ ((M / j) e. NN /\ (K / M) e. NN)) -> (K / j) e. NN)
28	27	ex 398	. . . . . . . . . . . . . . . . . . . 20 |- ((j e. NN /\ M e. NN /\ K e. CC) -> (((M / j) e. NN /\ (K / M) e. NN) -> (K / j) e. NN))
29	28	3com13 1322	. . . . . . . . . . . . . . . . . . 19 |- ((K e. CC /\ M e. NN /\ j e. NN) -> (((M / j) e. NN /\ (K / M) e. NN) -> (K / j) e. NN))
30	29	3expa 1317	. . . . . . . . . . . . . . . . . 18 |- (((K e. CC /\ M e. NN) /\ j e. NN) -> (((M / j) e. NN /\ (K / M) e. NN) -> (K / j) e. NN))
31	26, 30	sylanl1 641	. . . . . . . . . . . . . . . . 17 |- (((N e. NN /\ M e. NN) /\ j e. NN) -> (((M / j) e. NN /\ (K / M) e. NN) -> (K / j) e. NN))
32	31	adantrl 779	. . . . . . . . . . . . . . . 16 |- (((N e. NN /\ M e. NN) /\ (j <_ M /\ j e. NN)) -> (((M / j) e. NN /\ (K / M) e. NN) -> (K / j) e. NN))
33		nnre 7445	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (j e. NN -> j e. RR)
34		letri3 6876	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((j e. RR /\ M e. RR) -> (j = M <-> (j <_ M /\ M <_ j)))
35	33, 1, 34	syl2an 603	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((j e. NN /\ M e. NN) -> (j = M <-> (j <_ M /\ M <_ j)))
36	35	biimprd 232	. . . . . . . . . . . . . . . . . . . . . 22 |- ((j e. NN /\ M e. NN) -> ((j <_ M /\ M <_ j) -> j = M))
37	36	exp4b 580	. . . . . . . . . . . . . . . . . . . . 21 |- (j e. NN -> (M e. NN -> (j <_ M -> (M <_ j -> j = M))))
38	37	com3l 68	. . . . . . . . . . . . . . . . . . . 20 |- (M e. NN -> (j <_ M -> (j e. NN -> (M <_ j -> j = M))))
39	38	imp32 397	. . . . . . . . . . . . . . . . . . 19 |- ((M e. NN /\ (j <_ M /\ j e. NN)) -> (M <_ j -> j = M))
40	39	adantll 775	. . . . . . . . . . . . . . . . . 18 |- (((N e. NN /\ M e. NN) /\ (j <_ M /\ j e. NN)) -> (M <_ j -> j = M))
41	40	imim2d 28	. . . . . . . . . . . . . . . . 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)))
42	41	com23 65	. . . . . . . . . . . . . . . 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)))
43	32, 42	sylan2d 637	. . . . . . . . . . . . . . 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)))
44	43	exp4d 583	. . . . . . . . . . . . . 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)))))
45	44	com24 79	. . . . . . . . . . . . 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)))))
46	45	exp32 578	. . . . . . . . . . . 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)))))))
47	46	com24 79	. . . . . . . . . . 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)))))))
48	47	imp31 396	. . . . . . . . . 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)))))
49	48	com14 80	. . . . . . . . 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)))))
50	49	3imp 1311	. . . . . . . 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)))
51	50	com3l 68	. . . . . . 7 |- ((((N e. NN /\ M e. NN) /\ (K / M) e. NN) /\ j e. NN) -> (((1 < j /\ (K / j) e. NN) -> M <_ j) -> ((1 < j /\ j <_ M /\ (M / j) e. NN) -> j = M)))
52	51	ralimdva 2421	. . . . . 6 |- (((N e. NN /\ M e. NN) /\ (K / M) e. NN) -> (A.j e. NN ((1 < j /\ (K / j) e. NN) -> M <_ j) -> A.j e. NN ((1 < j /\ j <_ M /\ (M / j) e. NN) -> j = M)))
53	52	ex 398	. . . . 5 |- ((N e. NN /\ M e. NN) -> ((K / M) e. NN -> (A.j e. NN ((1 < j /\ (K / j) e. NN) -> M <_ j) -> A.j e. NN ((1 < j /\ j <_ M /\ (M / j) e. NN) -> j = M))))
54	53	adantld 450	. . . 4 |- ((N e. NN /\ M e. NN) -> ((1 < M /\ (K / M) e. NN) -> (A.j e. NN ((1 < j /\ (K / j) e. NN) -> M <_ j) -> A.j e. NN ((1 < j /\ j <_ M /\ (M / j) e. NN) -> j = M))))
55	54	imp3a 395	. . 3 |- ((N e. NN /\ M e. NN) -> (((1 < M /\ (K / M) e. NN) /\ A.j e. NN ((1 < j /\ (K / j) e. NN) -> M <_ j)) -> A.j e. NN ((1 < j /\ j <_ M /\ (M / j) e. NN) -> j = M)))
56		prime 7750	. . . 4 |- (M e. NN -> (A.j e. NN ((M / j) e. NN -> (j = 1 \/ j = M)) <-> A.j e. NN ((1 < j /\ j <_ M /\ (M / j) e. NN) -> j = M)))
57	56	adantl 448	. . 3 |- ((N e. NN /\ M e. NN) -> (A.j e. NN ((M / j) e. NN -> (j = 1 \/ j = M)) <-> A.j e. NN ((1 < j /\ j <_ M /\ (M / j) e. NN) -> j = M)))
58	55, 57	sylibrd 247	. 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)) -> A.j e. NN ((M / j) e. NN -> (j = 1 \/ j = M))))
59	19, 58	jcad 496	1 |- ((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)))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   \/ wo 336   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  A.wral 2355   class class class wbr 3507  ` cfv 4131  (class class class)co 4981  CCcc 6750  RRcr 6751  1c1 6753   + caddc 6755   <_ cle 6841   < clt 6845   / cdiv 6991  NNcn 6992  NN0cn0 6993  ZZcz 6994  !cfa 8568

This theorem is referenced by:  infpnlem2 9389

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-div 7223  df-n 7441  df-n0 7649  df-z 7686  df-seq1 8094  df-fac 8569

Copyright terms: Public domain