Proof of Theorem facndiv
| Step | Hyp | Ref
| Expression |
| 1 | | nnre 12273 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 2 | | recnz 12693 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 1 <
𝑁) → ¬ (1 / 𝑁) ∈
ℤ) |
| 3 | 1, 2 | sylan 580 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 1 <
𝑁) → ¬ (1 / 𝑁) ∈
ℤ) |
| 4 | 3 | ad2ant2lr 748 |
. 2
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ¬ (1 / 𝑁) ∈ ℤ) |
| 5 | | facdiv 14326 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℕ) |
| 6 | 5 | 3expa 1119 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℕ) |
| 7 | 6 | nnzd 12640 |
. . . . 5
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℤ) |
| 8 | 7 | adantrl 716 |
. . . 4
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ((!‘𝑀) / 𝑁) ∈ ℤ) |
| 9 | | zsubcl 12659 |
. . . . 5
⊢
(((((!‘𝑀) + 1)
/ 𝑁) ∈ ℤ ∧
((!‘𝑀) / 𝑁) ∈ ℤ) →
((((!‘𝑀) + 1) / 𝑁) − ((!‘𝑀) / 𝑁)) ∈ ℤ) |
| 10 | 9 | ex 412 |
. . . 4
⊢
((((!‘𝑀) + 1)
/ 𝑁) ∈ ℤ →
(((!‘𝑀) / 𝑁) ∈ ℤ →
((((!‘𝑀) + 1) / 𝑁) − ((!‘𝑀) / 𝑁)) ∈ ℤ)) |
| 11 | 8, 10 | syl5com 31 |
. . 3
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ((((!‘𝑀) + 1) / 𝑁) ∈ ℤ → ((((!‘𝑀) + 1) / 𝑁) − ((!‘𝑀) / 𝑁)) ∈ ℤ)) |
| 12 | | faccl 14322 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ (!‘𝑀) ∈
ℕ) |
| 13 | 12 | nncnd 12282 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (!‘𝑀) ∈
ℂ) |
| 14 | | peano2cn 11433 |
. . . . . . . 8
⊢
((!‘𝑀) ∈
ℂ → ((!‘𝑀)
+ 1) ∈ ℂ) |
| 15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ ((!‘𝑀) + 1)
∈ ℂ) |
| 16 | 15 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ((!‘𝑀) + 1) ∈ ℂ) |
| 17 | 13 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → (!‘𝑀) ∈ ℂ) |
| 18 | | nncn 12274 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 19 | | nnne0 12300 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
| 20 | 18, 19 | jca 511 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
| 21 | 20 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
| 22 | | divsubdir 11961 |
. . . . . 6
⊢
((((!‘𝑀) + 1)
∈ ℂ ∧ (!‘𝑀) ∈ ℂ ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → ((((!‘𝑀) + 1) − (!‘𝑀)) / 𝑁) = ((((!‘𝑀) + 1) / 𝑁) − ((!‘𝑀) / 𝑁))) |
| 23 | 16, 17, 21, 22 | syl3anc 1373 |
. . . . 5
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ((((!‘𝑀) + 1) − (!‘𝑀)) / 𝑁) = ((((!‘𝑀) + 1) / 𝑁) − ((!‘𝑀) / 𝑁))) |
| 24 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 25 | | pncan2 11515 |
. . . . . . . 8
⊢
(((!‘𝑀) ∈
ℂ ∧ 1 ∈ ℂ) → (((!‘𝑀) + 1) − (!‘𝑀)) = 1) |
| 26 | 13, 24, 25 | sylancl 586 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (((!‘𝑀) + 1)
− (!‘𝑀)) =
1) |
| 27 | 26 | oveq1d 7446 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ ((((!‘𝑀) + 1)
− (!‘𝑀)) /
𝑁) = (1 / 𝑁)) |
| 28 | 27 | ad2antrr 726 |
. . . . 5
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ((((!‘𝑀) + 1) − (!‘𝑀)) / 𝑁) = (1 / 𝑁)) |
| 29 | 23, 28 | eqtr3d 2779 |
. . . 4
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ((((!‘𝑀) + 1) / 𝑁) − ((!‘𝑀) / 𝑁)) = (1 / 𝑁)) |
| 30 | 29 | eleq1d 2826 |
. . 3
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → (((((!‘𝑀) + 1) / 𝑁) − ((!‘𝑀) / 𝑁)) ∈ ℤ ↔ (1 / 𝑁) ∈
ℤ)) |
| 31 | 11, 30 | sylibd 239 |
. 2
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ((((!‘𝑀) + 1) / 𝑁) ∈ ℤ → (1 / 𝑁) ∈
ℤ)) |
| 32 | 4, 31 | mtod 198 |
1
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ¬ (((!‘𝑀) + 1) / 𝑁) ∈ ℤ) |