Proof of Theorem etransclem7
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzfid 14015 | . 2
⊢ (𝜑 → (1...𝑀) ∈ Fin) | 
| 2 |  | 0zd 12627 | . . 3
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑃 < (𝐶‘𝑗)) → 0 ∈ ℤ) | 
| 3 |  | 0zd 12627 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → 0 ∈ ℤ) | 
| 4 |  | etransclem7.n | . . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 5 | 4 | nnzd 12642 | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 6 | 5 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → 𝑃 ∈ ℤ) | 
| 7 | 5 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℤ) | 
| 8 |  | etransclem7.c | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) | 
| 9 | 8 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐶:(0...𝑀)⟶(0...𝑁)) | 
| 10 |  | 0zd 12627 | . . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 0 ∈ ℤ) | 
| 11 |  | fzp1ss 13616 | . . . . . . . . . . . . . 14
⊢ (0 ∈
ℤ → ((0 + 1)...𝑀) ⊆ (0...𝑀)) | 
| 12 | 10, 11 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → ((0 + 1)...𝑀) ⊆ (0...𝑀)) | 
| 13 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (1...𝑀)) | 
| 14 |  | 1e0p1 12777 | . . . . . . . . . . . . . . 15
⊢ 1 = (0 +
1) | 
| 15 | 14 | oveq1i 7442 | . . . . . . . . . . . . . 14
⊢
(1...𝑀) = ((0 +
1)...𝑀) | 
| 16 | 13, 15 | eleqtrdi 2850 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ((0 + 1)...𝑀)) | 
| 17 | 12, 16 | sseldd 3983 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (0...𝑀)) | 
| 18 | 17 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀)) | 
| 19 | 9, 18 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶‘𝑗) ∈ (0...𝑁)) | 
| 20 | 19 | elfzelzd 13566 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶‘𝑗) ∈ ℤ) | 
| 21 | 7, 20 | zsubcld 12729 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐶‘𝑗)) ∈ ℤ) | 
| 22 | 21 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝑃 − (𝐶‘𝑗)) ∈ ℤ) | 
| 23 | 20 | zred 12724 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶‘𝑗) ∈ ℝ) | 
| 24 | 23 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝐶‘𝑗) ∈ ℝ) | 
| 25 | 6 | zred 12724 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → 𝑃 ∈ ℝ) | 
| 26 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → ¬ 𝑃 < (𝐶‘𝑗)) | 
| 27 | 24, 25, 26 | nltled 11412 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝐶‘𝑗) ≤ 𝑃) | 
| 28 | 25, 24 | subge0d 11854 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (0 ≤ (𝑃 − (𝐶‘𝑗)) ↔ (𝐶‘𝑗) ≤ 𝑃)) | 
| 29 | 27, 28 | mpbird 257 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → 0 ≤ (𝑃 − (𝐶‘𝑗))) | 
| 30 |  | elfzle1 13568 | . . . . . . . . . 10
⊢ ((𝐶‘𝑗) ∈ (0...𝑁) → 0 ≤ (𝐶‘𝑗)) | 
| 31 | 19, 30 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 0 ≤ (𝐶‘𝑗)) | 
| 32 | 31 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → 0 ≤ (𝐶‘𝑗)) | 
| 33 | 25, 24 | subge02d 11856 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (0 ≤ (𝐶‘𝑗) ↔ (𝑃 − (𝐶‘𝑗)) ≤ 𝑃)) | 
| 34 | 32, 33 | mpbid 232 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝑃 − (𝐶‘𝑗)) ≤ 𝑃) | 
| 35 | 3, 6, 22, 29, 34 | elfzd 13556 | . . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝑃 − (𝐶‘𝑗)) ∈ (0...𝑃)) | 
| 36 |  | permnn 14366 | . . . . . 6
⊢ ((𝑃 − (𝐶‘𝑗)) ∈ (0...𝑃) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) ∈ ℕ) | 
| 37 | 35, 36 | syl 17 | . . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) ∈ ℕ) | 
| 38 | 37 | nnzd 12642 | . . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) ∈ ℤ) | 
| 39 |  | etransclem7.j | . . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) | 
| 40 | 39 | elfzelzd 13566 | . . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 41 | 40 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐽 ∈ ℤ) | 
| 42 |  | elfzelz 13565 | . . . . . . . 8
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℤ) | 
| 43 | 42 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℤ) | 
| 44 | 41, 43 | zsubcld 12729 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐽 − 𝑗) ∈ ℤ) | 
| 45 | 44 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝐽 − 𝑗) ∈ ℤ) | 
| 46 |  | elnn0z 12628 | . . . . . 6
⊢ ((𝑃 − (𝐶‘𝑗)) ∈ ℕ0 ↔ ((𝑃 − (𝐶‘𝑗)) ∈ ℤ ∧ 0 ≤ (𝑃 − (𝐶‘𝑗)))) | 
| 47 | 22, 29, 46 | sylanbrc 583 | . . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (𝑃 − (𝐶‘𝑗)) ∈
ℕ0) | 
| 48 |  | zexpcl 14118 | . . . . 5
⊢ (((𝐽 − 𝑗) ∈ ℤ ∧ (𝑃 − (𝐶‘𝑗)) ∈ ℕ0) → ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))) ∈ ℤ) | 
| 49 | 45, 47, 48 | syl2anc 584 | . . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))) ∈ ℤ) | 
| 50 | 38, 49 | zmulcld 12730 | . . 3
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ 𝑃 < (𝐶‘𝑗)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))) ∈ ℤ) | 
| 51 | 2, 50 | ifclda 4560 | . 2
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) | 
| 52 | 1, 51 | fprodzcl 15991 | 1
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |