Metamath Proof Explorer

Theorem 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 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 infpnlem.1 
 |-  K = ( ( ! ` N ) + 1 )
2 nnre 
 |-  ( M e. NN -> M e. RR )
3 nnre 
 |-  ( N e. NN -> N e. RR )
4 lenlt 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M <_ N <-> -. N < M ) )
5 2 3 4 syl2anr 
 |-  ( ( N e. NN /\ M e. NN ) -> ( M <_ N <-> -. N < M ) )
6 5 adantr 
 |-  ( ( ( N e. NN /\ M e. NN ) /\ 1 < M ) -> ( M <_ N <-> -. N < M ) )
7 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
8 facndiv 
 |-  ( ( ( N e. NN0 /\ M e. NN ) /\ ( 1 < M /\ M <_ N ) ) -> -. ( ( ( ! ` N ) + 1 ) / M ) e. ZZ )
9 1 oveq1i 
 |-  ( K / M ) = ( ( ( ! ` N ) + 1 ) / M )
10 nnz 
 |-  ( ( K / M ) e. NN -> ( K / M ) e. ZZ )
11 9 10 eqeltrrid 
 |-  ( ( K / M ) e. NN -> ( ( ( ! ` N ) + 1 ) / M ) e. ZZ )
12 8 11 nsyl 
 |-  ( ( ( N e. NN0 /\ M e. NN ) /\ ( 1 < M /\ M <_ N ) ) -> -. ( K / M ) e. NN )
13 7 12 sylanl1 
 |-  ( ( ( N e. NN /\ M e. NN ) /\ ( 1 < M /\ M <_ N ) ) -> -. ( K / M ) e. NN )
14 13 expr 
 |-  ( ( ( N e. NN /\ M e. NN ) /\ 1 < M ) -> ( M <_ N -> -. ( K / M ) e. NN ) )
15 6 14 sylbird 
 |-  ( ( ( N e. NN /\ M e. NN ) /\ 1 < M ) -> ( -. N < M -> -. ( K / M ) e. NN ) )
16 15 con4d 
 |-  ( ( ( N e. NN /\ M e. NN ) /\ 1 < M ) -> ( ( K / M ) e. NN -> N < M ) )
17 16 expimpd 
 |-  ( ( N e. NN /\ M e. NN ) -> ( ( 1 < M /\ ( K / M ) e. NN ) -> N < M ) )
18 17 adantrd 
 |-  ( ( 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 ) )
19 7 faccld 
 |-  ( N e. NN -> ( ! ` N ) e. NN )
20 19 peano2nnd 
 |-  ( N e. NN -> ( ( ! ` N ) + 1 ) e. NN )
21 1 20 eqeltrid 
 |-  ( N e. NN -> K e. NN )
22 21 nncnd 
 |-  ( N e. NN -> K e. CC )
23 nndivtr 
 |-  ( ( ( j e. NN /\ M e. NN /\ K e. CC ) /\ ( ( M / j ) e. NN /\ ( K / M ) e. NN ) ) -> ( K / j ) e. NN )
24 23 ex 
 |-  ( ( j e. NN /\ M e. NN /\ K e. CC ) -> ( ( ( M / j ) e. NN /\ ( K / M ) e. NN ) -> ( K / j ) e. NN ) )
25 24 3com13 
 |-  ( ( K e. CC /\ M e. NN /\ j e. NN ) -> ( ( ( M / j ) e. NN /\ ( K / M ) e. NN ) -> ( K / j ) e. NN ) )
26 25 3expa 
 |-  ( ( ( K e. CC /\ M e. NN ) /\ j e. NN ) -> ( ( ( M / j ) e. NN /\ ( K / M ) e. NN ) -> ( K / j ) e. NN ) )
27 22 26 sylanl1 
 |-  ( ( ( N e. NN /\ M e. NN ) /\ j e. NN ) -> ( ( ( M / j ) e. NN /\ ( K / M ) e. NN ) -> ( K / j ) e. NN ) )
28 27 adantrl 
 |-  ( ( ( N e. NN /\ M e. NN ) /\ ( j <_ M /\ j e. NN ) ) -> ( ( ( M / j ) e. NN /\ ( K / M ) e. NN ) -> ( K / j ) e. NN ) )
29 nnre 
 |-  ( j e. NN -> j e. RR )
30 letri3 
 |-  ( ( j e. RR /\ M e. RR ) -> ( j = M <-> ( j <_ M /\ M <_ j ) ) )
31 29 2 30 syl2an 
 |-  ( ( j e. NN /\ M e. NN ) -> ( j = M <-> ( j <_ M /\ M <_ j ) ) )
32 31 biimprd 
 |-  ( ( j e. NN /\ M e. NN ) -> ( ( j <_ M /\ M <_ j ) -> j = M ) )
33 32 exp4b 
 |-  ( j e. NN -> ( M e. NN -> ( j <_ M -> ( M <_ j -> j = M ) ) ) )
34 33 com3l 
 |-  ( M e. NN -> ( j <_ M -> ( j e. NN -> ( M <_ j -> j = M ) ) ) )
35 34 imp32 
 |-  ( ( M e. NN /\ ( j <_ M /\ j e. NN ) ) -> ( M <_ j -> j = M ) )
36 35 adantll 
 |-  ( ( ( N e. NN /\ M e. NN ) /\ ( j <_ M /\ j e. NN ) ) -> ( M <_ j -> j = M ) )
37 36 imim2d 
 |-  ( ( ( 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 ) ) )
38 37 com23 
 |-  ( ( ( 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 ) ) )
39 28 38 sylan2d 
 |-  ( ( ( 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 ) ) )
40 39 exp4d 
 |-  ( ( ( 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 ) ) ) ) )
41 40 com24 
 |-  ( ( ( 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 ) ) ) ) )
42 41 exp32 
 |-  ( ( 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 ) ) ) ) ) ) )
43 42 com24 
 |-  ( ( 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 ) ) ) ) ) ) )
44 43 imp31 
 |-  ( ( ( ( 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 ) ) ) ) )
45 44 com14 
 |-  ( 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 ) ) ) ) )
46 45 3imp 
 |-  ( ( 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 ) ) )
47 46 com3l 
 |-  ( ( ( ( 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 ) ) )
48 47 ralimdva 
 |-  ( ( ( 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 ) ) )
49 48 ex 
 |-  ( ( 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 ) ) ) )
50 49 adantld 
 |-  ( ( 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 ) ) ) )
51 50 impd 
 |-  ( ( 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 ) ) )
52 prime 
 |-  ( 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 ) ) )
53 52 adantl 
 |-  ( ( 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 ) ) )
54 51 53 sylibrd 
 |-  ( ( 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 ) ) ) )
55 18 54 jcad 
 |-  ( ( 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 ) ) ) ) )