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 ⊢ 𝐾 = ( ( ! ‘ 𝑁 ) + 1 )
Assertion infpnlem1 ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( ( 1 < 𝑀 ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ∧ ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) ) → ( 𝑁 < 𝑀 ∧ ∀ 𝑗 ∈ ℕ ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( 𝑗 = 1 ∨ 𝑗 = 𝑀 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 infpnlem.1 ⊢ 𝐾 = ( ( ! ‘ 𝑁 ) + 1 )
2 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
3 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
4 lenlt ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
5 2 3 4 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
6 5 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 1 < 𝑀 ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
7 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
8 facndiv ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ ( 1 < 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) → ¬ ( ( ( ! ‘ 𝑁 ) + 1 ) / 𝑀 ) ∈ ℤ )
9 1 oveq1i ⊢ ( 𝐾 / 𝑀 ) = ( ( ( ! ‘ 𝑁 ) + 1 ) / 𝑀 )
10 nnz ⊢ ( ( 𝐾 / 𝑀 ) ∈ ℕ → ( 𝐾 / 𝑀 ) ∈ ℤ )
11 9 10 eqeltrrid ⊢ ( ( 𝐾 / 𝑀 ) ∈ ℕ → ( ( ( ! ‘ 𝑁 ) + 1 ) / 𝑀 ) ∈ ℤ )
12 8 11 nsyl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) ∧ ( 1 < 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) → ¬ ( 𝐾 / 𝑀 ) ∈ ℕ )
13 7 12 sylanl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 1 < 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) → ¬ ( 𝐾 / 𝑀 ) ∈ ℕ )
14 13 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 1 < 𝑀 ) → ( 𝑀 ≤ 𝑁 → ¬ ( 𝐾 / 𝑀 ) ∈ ℕ ) )
15 6 14 sylbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 1 < 𝑀 ) → ( ¬ 𝑁 < 𝑀 → ¬ ( 𝐾 / 𝑀 ) ∈ ℕ ) )
16 15 con4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 1 < 𝑀 ) → ( ( 𝐾 / 𝑀 ) ∈ ℕ → 𝑁 < 𝑀 ) )
17 16 expimpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( 1 < 𝑀 ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) → 𝑁 < 𝑀 ) )
18 17 adantrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( ( 1 < 𝑀 ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ∧ ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) ) → 𝑁 < 𝑀 ) )
19 7 faccld ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℕ )
20 19 peano2nnd ⊢ ( 𝑁 ∈ ℕ → ( ( ! ‘ 𝑁 ) + 1 ) ∈ ℕ )
21 1 20 eqeltrid ⊢ ( 𝑁 ∈ ℕ → 𝐾 ∈ ℕ )
22 21 nncnd ⊢ ( 𝑁 ∈ ℕ → 𝐾 ∈ ℂ )
23 nndivtr ⊢ ( ( ( 𝑗 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝐾 ∈ ℂ ) ∧ ( ( 𝑀 / 𝑗 ) ∈ ℕ ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ) → ( 𝐾 / 𝑗 ) ∈ ℕ )
24 23 ex ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝐾 ∈ ℂ ) → ( ( ( 𝑀 / 𝑗 ) ∈ ℕ ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) → ( 𝐾 / 𝑗 ) ∈ ℕ ) )
25 24 3com13 ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝑀 / 𝑗 ) ∈ ℕ ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) → ( 𝐾 / 𝑗 ) ∈ ℕ ) )
26 25 3expa ⊢ ( ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝑀 / 𝑗 ) ∈ ℕ ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) → ( 𝐾 / 𝑗 ) ∈ ℕ ) )
27 22 26 sylanl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝑀 / 𝑗 ) ∈ ℕ ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) → ( 𝐾 / 𝑗 ) ∈ ℕ ) )
28 27 adantrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ ) ) → ( ( ( 𝑀 / 𝑗 ) ∈ ℕ ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) → ( 𝐾 / 𝑗 ) ∈ ℕ ) )
29 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
30 letri3 ⊢ ( ( 𝑗 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑗 = 𝑀 ↔ ( 𝑗 ≤ 𝑀 ∧ 𝑀 ≤ 𝑗 ) ) )
31 29 2 30 syl2an ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑗 = 𝑀 ↔ ( 𝑗 ≤ 𝑀 ∧ 𝑀 ≤ 𝑗 ) ) )
32 31 biimprd ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑗 ≤ 𝑀 ∧ 𝑀 ≤ 𝑗 ) → 𝑗 = 𝑀 ) )
33 32 exp4b ⊢ ( 𝑗 ∈ ℕ → ( 𝑀 ∈ ℕ → ( 𝑗 ≤ 𝑀 → ( 𝑀 ≤ 𝑗 → 𝑗 = 𝑀 ) ) ) )
34 33 com3l ⊢ ( 𝑀 ∈ ℕ → ( 𝑗 ≤ 𝑀 → ( 𝑗 ∈ ℕ → ( 𝑀 ≤ 𝑗 → 𝑗 = 𝑀 ) ) ) )
35 34 imp32 ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ ) ) → ( 𝑀 ≤ 𝑗 → 𝑗 = 𝑀 ) )
36 35 adantll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ ) ) → ( 𝑀 ≤ 𝑗 → 𝑗 = 𝑀 ) )
37 36 imim2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ ) ) → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑗 = 𝑀 ) ) )
38 37 com23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ ) ) → ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → 𝑗 = 𝑀 ) ) )
39 28 38 sylan2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ ) ) → ( ( 1 < 𝑗 ∧ ( ( 𝑀 / 𝑗 ) ∈ ℕ ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ) → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → 𝑗 = 𝑀 ) ) )
40 39 exp4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ ) ) → ( 1 < 𝑗 → ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( ( 𝐾 / 𝑀 ) ∈ ℕ → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → 𝑗 = 𝑀 ) ) ) ) )
41 40 com24 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝐾 / 𝑀 ) ∈ ℕ → ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( 1 < 𝑗 → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → 𝑗 = 𝑀 ) ) ) ) )
42 41 exp32 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑗 ≤ 𝑀 → ( 𝑗 ∈ ℕ → ( ( 𝐾 / 𝑀 ) ∈ ℕ → ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( 1 < 𝑗 → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → 𝑗 = 𝑀 ) ) ) ) ) ) )
43 42 com24 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( 𝐾 / 𝑀 ) ∈ ℕ → ( 𝑗 ∈ ℕ → ( 𝑗 ≤ 𝑀 → ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( 1 < 𝑗 → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → 𝑗 = 𝑀 ) ) ) ) ) ) )
44 43 imp31 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑗 ≤ 𝑀 → ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( 1 < 𝑗 → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → 𝑗 = 𝑀 ) ) ) ) )
45 44 com14 ⊢ ( 1 < 𝑗 → ( 𝑗 ≤ 𝑀 → ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → 𝑗 = 𝑀 ) ) ) ) )
46 45 3imp ⊢ ( ( 1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ ( 𝑀 / 𝑗 ) ∈ ℕ ) → ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → 𝑗 = 𝑀 ) ) )
47 46 com3l ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → ( ( 1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ ( 𝑀 / 𝑗 ) ∈ ℕ ) → 𝑗 = 𝑀 ) ) )
48 47 ralimdva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) → ( ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ ( 𝑀 / 𝑗 ) ∈ ℕ ) → 𝑗 = 𝑀 ) ) )
49 48 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( 𝐾 / 𝑀 ) ∈ ℕ → ( ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ ( 𝑀 / 𝑗 ) ∈ ℕ ) → 𝑗 = 𝑀 ) ) ) )
50 49 adantld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( 1 < 𝑀 ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) → ( ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) → ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ ( 𝑀 / 𝑗 ) ∈ ℕ ) → 𝑗 = 𝑀 ) ) ) )
51 50 impd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( ( 1 < 𝑀 ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ∧ ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) ) → ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ ( 𝑀 / 𝑗 ) ∈ ℕ ) → 𝑗 = 𝑀 ) ) )
52 prime ⊢ ( 𝑀 ∈ ℕ → ( ∀ 𝑗 ∈ ℕ ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( 𝑗 = 1 ∨ 𝑗 = 𝑀 ) ) ↔ ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ ( 𝑀 / 𝑗 ) ∈ ℕ ) → 𝑗 = 𝑀 ) ) )
53 52 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ∀ 𝑗 ∈ ℕ ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( 𝑗 = 1 ∨ 𝑗 = 𝑀 ) ) ↔ ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ ( 𝑀 / 𝑗 ) ∈ ℕ ) → 𝑗 = 𝑀 ) ) )
54 51 53 sylibrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( ( 1 < 𝑀 ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ∧ ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) ) → ∀ 𝑗 ∈ ℕ ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( 𝑗 = 1 ∨ 𝑗 = 𝑀 ) ) ) )
55 18 54 jcad ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( ( 1 < 𝑀 ∧ ( 𝐾 / 𝑀 ) ∈ ℕ ) ∧ ∀ 𝑗 ∈ ℕ ( ( 1 < 𝑗 ∧ ( 𝐾 / 𝑗 ) ∈ ℕ ) → 𝑀 ≤ 𝑗 ) ) → ( 𝑁 < 𝑀 ∧ ∀ 𝑗 ∈ ℕ ( ( 𝑀 / 𝑗 ) ∈ ℕ → ( 𝑗 = 1 ∨ 𝑗 = 𝑀 ) ) ) ) )