Proof of Theorem infpnlem1
Step | Hyp | Ref
| Expression |
1 | | nnz 9231 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
2 | 1 | ad2antrr 485 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 1 <
𝑀) → 𝑁 ∈ ℤ) |
3 | | nnz 9231 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
4 | 3 | ad2antlr 486 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 1 <
𝑀) → 𝑀 ∈ ℤ) |
5 | | zdclt 9289 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
DECID 𝑁 <
𝑀) |
6 | 2, 4, 5 | syl2anc 409 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 1 <
𝑀) →
DECID 𝑁 <
𝑀) |
7 | | nnre 8885 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
8 | | nnre 8885 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
9 | | lenlt 7995 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀)) |
10 | 7, 8, 9 | syl2anr 288 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀)) |
11 | 10 | adantr 274 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 1 <
𝑀) → (𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀)) |
12 | | nnnn0 9142 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
13 | | facndiv 10673 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ (1 < 𝑀 ∧ 𝑀 ≤ 𝑁)) → ¬ (((!‘𝑁) + 1) / 𝑀) ∈ ℤ) |
14 | | infpnlem.1 |
. . . . . . . . . . 11
⊢ 𝐾 = ((!‘𝑁) + 1) |
15 | 14 | oveq1i 5863 |
. . . . . . . . . 10
⊢ (𝐾 / 𝑀) = (((!‘𝑁) + 1) / 𝑀) |
16 | | nnz 9231 |
. . . . . . . . . 10
⊢ ((𝐾 / 𝑀) ∈ ℕ → (𝐾 / 𝑀) ∈ ℤ) |
17 | 15, 16 | eqeltrrid 2258 |
. . . . . . . . 9
⊢ ((𝐾 / 𝑀) ∈ ℕ → (((!‘𝑁) + 1) / 𝑀) ∈ ℤ) |
18 | 13, 17 | nsyl 623 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ (1 < 𝑀 ∧ 𝑀 ≤ 𝑁)) → ¬ (𝐾 / 𝑀) ∈ ℕ) |
19 | 12, 18 | sylanl1 400 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (1 <
𝑀 ∧ 𝑀 ≤ 𝑁)) → ¬ (𝐾 / 𝑀) ∈ ℕ) |
20 | 19 | expr 373 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 1 <
𝑀) → (𝑀 ≤ 𝑁 → ¬ (𝐾 / 𝑀) ∈ ℕ)) |
21 | 11, 20 | sylbird 169 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 1 <
𝑀) → (¬ 𝑁 < 𝑀 → ¬ (𝐾 / 𝑀) ∈ ℕ)) |
22 | | condc 848 |
. . . . 5
⊢
(DECID 𝑁 < 𝑀 → ((¬ 𝑁 < 𝑀 → ¬ (𝐾 / 𝑀) ∈ ℕ) → ((𝐾 / 𝑀) ∈ ℕ → 𝑁 < 𝑀))) |
23 | 6, 21, 22 | sylc 62 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 1 <
𝑀) → ((𝐾 / 𝑀) ∈ ℕ → 𝑁 < 𝑀)) |
24 | 23 | expimpd 361 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → ((1 <
𝑀 ∧ (𝐾 / 𝑀) ∈ ℕ) → 𝑁 < 𝑀)) |
25 | 24 | adantrd 277 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (((1
< 𝑀 ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗)) → 𝑁 < 𝑀)) |
26 | 12 | faccld 10670 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℕ) |
27 | 26 | peano2nnd 8893 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) + 1) ∈
ℕ) |
28 | 14, 27 | eqeltrid 2257 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝐾 ∈
ℕ) |
29 | 28 | nncnd 8892 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝐾 ∈
ℂ) |
30 | | nndivtr 8920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑗 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝐾 ∈ ℂ) ∧ ((𝑀 / 𝑗) ∈ ℕ ∧ (𝐾 / 𝑀) ∈ ℕ)) → (𝐾 / 𝑗) ∈ ℕ) |
31 | 30 | ex 114 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝐾 ∈ ℂ) → (((𝑀 / 𝑗) ∈ ℕ ∧ (𝐾 / 𝑀) ∈ ℕ) → (𝐾 / 𝑗) ∈ ℕ)) |
32 | 31 | 3com13 1203 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℂ ∧ 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (((𝑀 / 𝑗) ∈ ℕ ∧ (𝐾 / 𝑀) ∈ ℕ) → (𝐾 / 𝑗) ∈ ℕ)) |
33 | 32 | 3expa 1198 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℂ ∧ 𝑀 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((𝑀 / 𝑗) ∈ ℕ ∧ (𝐾 / 𝑀) ∈ ℕ) → (𝐾 / 𝑗) ∈ ℕ)) |
34 | 29, 33 | sylanl1 400 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((𝑀 / 𝑗) ∈ ℕ ∧ (𝐾 / 𝑀) ∈ ℕ) → (𝐾 / 𝑗) ∈ ℕ)) |
35 | 34 | adantrl 475 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ)) → (((𝑀 / 𝑗) ∈ ℕ ∧ (𝐾 / 𝑀) ∈ ℕ) → (𝐾 / 𝑗) ∈ ℕ)) |
36 | | nnre 8885 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
37 | | letri3 8000 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑗 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑗 = 𝑀 ↔ (𝑗 ≤ 𝑀 ∧ 𝑀 ≤ 𝑗))) |
38 | 36, 7, 37 | syl2an 287 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑗 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑗 = 𝑀 ↔ (𝑗 ≤ 𝑀 ∧ 𝑀 ≤ 𝑗))) |
39 | 38 | biimprd 157 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ ℕ ∧ 𝑀 ∈ ℕ) → ((𝑗 ≤ 𝑀 ∧ 𝑀 ≤ 𝑗) → 𝑗 = 𝑀)) |
40 | 39 | exp4b 365 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → (𝑀 ∈ ℕ → (𝑗 ≤ 𝑀 → (𝑀 ≤ 𝑗 → 𝑗 = 𝑀)))) |
41 | 40 | com3l 81 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ → (𝑗 ≤ 𝑀 → (𝑗 ∈ ℕ → (𝑀 ≤ 𝑗 → 𝑗 = 𝑀)))) |
42 | 41 | imp32 255 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℕ ∧ (𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ)) → (𝑀 ≤ 𝑗 → 𝑗 = 𝑀)) |
43 | 42 | adantll 473 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ)) → (𝑀 ≤ 𝑗 → 𝑗 = 𝑀)) |
44 | 43 | imim2d 54 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ)) → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑗 = 𝑀))) |
45 | 44 | com23 78 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ)) → ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → 𝑗 = 𝑀))) |
46 | 35, 45 | sylan2d 292 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ)) → ((1 < 𝑗 ∧ ((𝑀 / 𝑗) ∈ ℕ ∧ (𝐾 / 𝑀) ∈ ℕ)) → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → 𝑗 = 𝑀))) |
47 | 46 | exp4d 367 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ)) → (1 < 𝑗 → ((𝑀 / 𝑗) ∈ ℕ → ((𝐾 / 𝑀) ∈ ℕ → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → 𝑗 = 𝑀))))) |
48 | 47 | com24 87 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝑗 ≤ 𝑀 ∧ 𝑗 ∈ ℕ)) → ((𝐾 / 𝑀) ∈ ℕ → ((𝑀 / 𝑗) ∈ ℕ → (1 < 𝑗 → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → 𝑗 = 𝑀))))) |
49 | 48 | exp32 363 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑗 ≤ 𝑀 → (𝑗 ∈ ℕ → ((𝐾 / 𝑀) ∈ ℕ → ((𝑀 / 𝑗) ∈ ℕ → (1 < 𝑗 → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → 𝑗 = 𝑀))))))) |
50 | 49 | com24 87 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → ((𝐾 / 𝑀) ∈ ℕ → (𝑗 ∈ ℕ → (𝑗 ≤ 𝑀 → ((𝑀 / 𝑗) ∈ ℕ → (1 < 𝑗 → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → 𝑗 = 𝑀))))))) |
51 | 50 | imp31 254 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝑗 ≤ 𝑀 → ((𝑀 / 𝑗) ∈ ℕ → (1 < 𝑗 → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → 𝑗 = 𝑀))))) |
52 | 51 | com14 88 |
. . . . . . . . 9
⊢ (1 <
𝑗 → (𝑗 ≤ 𝑀 → ((𝑀 / 𝑗) ∈ ℕ → ((((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → 𝑗 = 𝑀))))) |
53 | 52 | 3imp 1188 |
. . . . . . . 8
⊢ ((1 <
𝑗 ∧ 𝑗 ≤ 𝑀 ∧ (𝑀 / 𝑗) ∈ ℕ) → ((((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → 𝑗 = 𝑀))) |
54 | 53 | com3l 81 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → ((1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ (𝑀 / 𝑗) ∈ ℕ) → 𝑗 = 𝑀))) |
55 | 54 | ralimdva 2537 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ (𝐾 / 𝑀) ∈ ℕ) → (∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ (𝑀 / 𝑗) ∈ ℕ) → 𝑗 = 𝑀))) |
56 | 55 | ex 114 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → ((𝐾 / 𝑀) ∈ ℕ → (∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ (𝑀 / 𝑗) ∈ ℕ) → 𝑗 = 𝑀)))) |
57 | 56 | adantld 276 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → ((1 <
𝑀 ∧ (𝐾 / 𝑀) ∈ ℕ) → (∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗) → ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ (𝑀 / 𝑗) ∈ ℕ) → 𝑗 = 𝑀)))) |
58 | 57 | impd 252 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (((1
< 𝑀 ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗)) → ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ (𝑀 / 𝑗) ∈ ℕ) → 𝑗 = 𝑀))) |
59 | | prime 9311 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(∀𝑗 ∈ ℕ
((𝑀 / 𝑗) ∈ ℕ → (𝑗 = 1 ∨ 𝑗 = 𝑀)) ↔ ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ (𝑀 / 𝑗) ∈ ℕ) → 𝑗 = 𝑀))) |
60 | 59 | adantl 275 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) →
(∀𝑗 ∈ ℕ
((𝑀 / 𝑗) ∈ ℕ → (𝑗 = 1 ∨ 𝑗 = 𝑀)) ↔ ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ 𝑗 ≤ 𝑀 ∧ (𝑀 / 𝑗) ∈ ℕ) → 𝑗 = 𝑀))) |
61 | 58, 60 | sylibrd 168 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (((1
< 𝑀 ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗)) → ∀𝑗 ∈ ℕ ((𝑀 / 𝑗) ∈ ℕ → (𝑗 = 1 ∨ 𝑗 = 𝑀)))) |
62 | 25, 61 | jcad 305 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (((1
< 𝑀 ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗)) → (𝑁 < 𝑀 ∧ ∀𝑗 ∈ ℕ ((𝑀 / 𝑗) ∈ ℕ → (𝑗 = 1 ∨ 𝑗 = 𝑀))))) |