Proof of Theorem etransclem15
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | etransclem15.t | . . 3
⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) | 
| 2 | 1 | a1i 11 | . 2
⊢ (𝜑 → 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))))) | 
| 3 |  | iftrue 4530 | . . . . . . 7
⊢ ((𝑃 − 1) < (𝐶‘0) → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) = 0) | 
| 4 | 3 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ (𝑃 − 1) < (𝐶‘0)) → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) = 0) | 
| 5 |  | iffalse 4533 | . . . . . . . 8
⊢ (¬
(𝑃 − 1) < (𝐶‘0) → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) | 
| 6 | 5 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) | 
| 7 |  | etransclem15.j | . . . . . . . . . . 11
⊢ (𝜑 → 𝐽 = 0) | 
| 8 | 7 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝜑 → (𝐽↑((𝑃 − 1) − (𝐶‘0))) = (0↑((𝑃 − 1) − (𝐶‘0)))) | 
| 9 | 8 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝐽↑((𝑃 − 1) − (𝐶‘0))) = (0↑((𝑃 − 1) − (𝐶‘0)))) | 
| 10 |  | etransclem15.p | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 11 | 10 | nnzd 12642 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 12 |  | 1zzd 12650 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℤ) | 
| 13 | 11, 12 | zsubcld 12729 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 − 1) ∈ ℤ) | 
| 14 |  | etransclem15.c | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) | 
| 15 |  | etransclem15.m | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 16 |  | nn0uz 12921 | . . . . . . . . . . . . . . . . 17
⊢
ℕ0 = (ℤ≥‘0) | 
| 17 | 15, 16 | eleqtrdi 2850 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) | 
| 18 |  | eluzfz1 13572 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈ (0...𝑀)) | 
| 20 | 14, 19 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶‘0) ∈ (0...𝑁)) | 
| 21 | 20 | elfzelzd 13566 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶‘0) ∈ ℤ) | 
| 22 | 13, 21 | zsubcld 12729 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 − 1) − (𝐶‘0)) ∈ ℤ) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((𝑃 − 1) − (𝐶‘0)) ∈ ℤ) | 
| 24 | 21 | zred 12724 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶‘0) ∈ ℝ) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝐶‘0) ∈ ℝ) | 
| 26 | 13 | zred 12724 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) | 
| 27 | 26 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝑃 − 1) ∈ ℝ) | 
| 28 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ¬ (𝑃 − 1) < (𝐶‘0)) | 
| 29 | 25, 27, 28 | nltled 11412 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝐶‘0) ≤ (𝑃 − 1)) | 
| 30 |  | etransclem15.cpm1 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶‘0) ≠ (𝑃 − 1)) | 
| 31 | 30 | necomd 2995 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 − 1) ≠ (𝐶‘0)) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝑃 − 1) ≠ (𝐶‘0)) | 
| 33 | 25, 27, 29, 32 | leneltd 11416 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝐶‘0) < (𝑃 − 1)) | 
| 34 | 25, 27 | posdifd 11851 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((𝐶‘0) < (𝑃 − 1) ↔ 0 < ((𝑃 − 1) − (𝐶‘0)))) | 
| 35 | 33, 34 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → 0 < ((𝑃 − 1) − (𝐶‘0))) | 
| 36 |  | elnnz 12625 | . . . . . . . . . . 11
⊢ (((𝑃 − 1) − (𝐶‘0)) ∈ ℕ ↔
(((𝑃 − 1) −
(𝐶‘0)) ∈ ℤ
∧ 0 < ((𝑃 − 1)
− (𝐶‘0)))) | 
| 37 | 23, 35, 36 | sylanbrc 583 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((𝑃 − 1) − (𝐶‘0)) ∈ ℕ) | 
| 38 | 37 | 0expd 14180 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (0↑((𝑃 − 1) − (𝐶‘0))) =
0) | 
| 39 | 9, 38 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (𝐽↑((𝑃 − 1) − (𝐶‘0))) = 0) | 
| 40 | 39 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · 0)) | 
| 41 |  | nnm1nn0 12569 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) | 
| 42 | 10, 41 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) | 
| 43 | 42 | faccld 14324 | . . . . . . . . . . 11
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℕ) | 
| 44 | 43 | nncnd 12283 | . . . . . . . . . 10
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℂ) | 
| 45 | 44 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (!‘(𝑃 − 1)) ∈
ℂ) | 
| 46 | 37 | nnnn0d 12589 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((𝑃 − 1) − (𝐶‘0)) ∈
ℕ0) | 
| 47 | 46 | faccld 14324 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (!‘((𝑃 − 1) − (𝐶‘0))) ∈
ℕ) | 
| 48 | 47 | nncnd 12283 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (!‘((𝑃 − 1) − (𝐶‘0))) ∈
ℂ) | 
| 49 | 47 | nnne0d 12317 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (!‘((𝑃 − 1) − (𝐶‘0))) ≠
0) | 
| 50 | 45, 48, 49 | divcld 12044 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) ∈
ℂ) | 
| 51 | 50 | mul01d 11461 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · 0) =
0) | 
| 52 | 6, 40, 51 | 3eqtrd 2780 | . . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑃 − 1) < (𝐶‘0)) → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) = 0) | 
| 53 | 4, 52 | pm2.61dan 812 | . . . . 5
⊢ (𝜑 → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) = 0) | 
| 54 | 53 | oveq1d 7447 | . . . 4
⊢ (𝜑 → (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))) = (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) | 
| 55 | 7, 19 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) | 
| 56 | 10, 14, 55 | etransclem7 46261 | . . . . . 6
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) | 
| 57 | 56 | zcnd 12725 | . . . . 5
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℂ) | 
| 58 | 57 | mul02d 11460 | . . . 4
⊢ (𝜑 → (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))) = 0) | 
| 59 | 54, 58 | eqtrd 2776 | . . 3
⊢ (𝜑 → (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))) = 0) | 
| 60 | 59 | oveq2d 7448 | . 2
⊢ (𝜑 → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · 0)) | 
| 61 |  | etransclem15.n | . . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 62 | 61 | faccld 14324 | . . . . 5
⊢ (𝜑 → (!‘𝑁) ∈ ℕ) | 
| 63 | 62 | nncnd 12283 | . . . 4
⊢ (𝜑 → (!‘𝑁) ∈ ℂ) | 
| 64 |  | fzfid 14015 | . . . . 5
⊢ (𝜑 → (0...𝑀) ∈ Fin) | 
| 65 |  | fzssnn0 45334 | . . . . . . . 8
⊢
(0...𝑁) ⊆
ℕ0 | 
| 66 | 14 | ffvelcdmda 7103 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐶‘𝑗) ∈ (0...𝑁)) | 
| 67 | 65, 66 | sselid 3980 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐶‘𝑗) ∈
ℕ0) | 
| 68 | 67 | faccld 14324 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐶‘𝑗)) ∈ ℕ) | 
| 69 | 68 | nncnd 12283 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐶‘𝑗)) ∈ ℂ) | 
| 70 | 64, 69 | fprodcl 15989 | . . . 4
⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗)) ∈ ℂ) | 
| 71 | 68 | nnne0d 12317 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐶‘𝑗)) ≠ 0) | 
| 72 | 64, 69, 71 | fprodn0 16016 | . . . 4
⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗)) ≠ 0) | 
| 73 | 63, 70, 72 | divcld 12044 | . . 3
⊢ (𝜑 → ((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) ∈ ℂ) | 
| 74 | 73 | mul01d 11461 | . 2
⊢ (𝜑 → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · 0) = 0) | 
| 75 | 2, 60, 74 | 3eqtrd 2780 | 1
⊢ (𝜑 → 𝑇 = 0) |