Metamath Proof Explorer

Theorem etransclem15

Description: Value of the term T , when J = 0 and ( C0 ) = P - 1 (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem15.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem15.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
etransclem15.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
etransclem15.c ⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
etransclem15.t ⊢ 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
etransclem15.j ⊢ ( 𝜑 → 𝐽 = 0 )
etransclem15.cpm1 ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ≠ ( 𝑃 − 1 ) )
Assertion etransclem15 ( 𝜑 → 𝑇 = 0 )

Proof

Step Hyp Ref Expression
1 etransclem15.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2 etransclem15.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3 etransclem15.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 etransclem15.c ⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
5 etransclem15.t ⊢ 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
6 etransclem15.j ⊢ ( 𝜑 → 𝐽 = 0 )
7 etransclem15.cpm1 ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ≠ ( 𝑃 − 1 ) )
8 5 a1i ⊢ ( 𝜑 → 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) ) )
9 iftrue ⊢ ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) = 0 )
10 9 adantl ⊢ ( ( 𝜑 ∧ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) = 0 )
11 iffalse ⊢ ( ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) )
12 11 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) )
13 6 oveq1d ⊢ ( 𝜑 → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) = ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) = ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) )
15 1 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
16 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
17 15 16 zsubcld ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℤ )
18 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
19 2 18 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
20 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
21 19 20 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
22 4 21 ffvelcdmd ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ( 0 ... 𝑁 ) )
23 22 elfzelzd ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ℤ )
24 17 23 zsubcld ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℤ )
25 24 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℤ )
26 23 zred ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ℝ )
27 26 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝐶 ‘ 0 ) ∈ ℝ )
28 17 zred ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ )
29 28 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝑃 − 1 ) ∈ ℝ )
30 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) )
31 27 29 30 nltled ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝐶 ‘ 0 ) ≤ ( 𝑃 − 1 ) )
32 7 necomd ⊢ ( 𝜑 → ( 𝑃 − 1 ) ≠ ( 𝐶 ‘ 0 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝑃 − 1 ) ≠ ( 𝐶 ‘ 0 ) )
34 27 29 31 33 leneltd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝐶 ‘ 0 ) < ( 𝑃 − 1 ) )
35 27 29 posdifd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( 𝐶 ‘ 0 ) < ( 𝑃 − 1 ) ↔ 0 < ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) )
36 34 35 mpbid ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → 0 < ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) )
37 elnnz ⊢ ( ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℕ ↔ ( ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℤ ∧ 0 < ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) )
38 25 36 37 sylanbrc ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℕ )
39 38 0expd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) = 0 )
40 14 39 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) = 0 )
41 40 oveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · 0 ) )
42 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
43 1 42 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
44 43 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
45 44 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
46 45 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
47 38 nnnn0d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℕ0 )
48 47 faccld ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ∈ ℕ )
49 48 nncnd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ∈ ℂ )
50 48 nnne0d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ≠ 0 )
51 46 49 50 divcld ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ∈ ℂ )
52 51 mul01d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · 0 ) = 0 )
53 12 41 52 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) = 0 )
54 10 53 pm2.61dan ⊢ ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) = 0 )
55 54 oveq1d ⊢ ( 𝜑 → ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) = ( 0 · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
56 6 21 eqeltrd ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
57 1 4 56 etransclem7 ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
58 57 zcnd ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℂ )
59 58 mul02d ⊢ ( 𝜑 → ( 0 · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) = 0 )
60 55 59 eqtrd ⊢ ( 𝜑 → ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) = 0 )
61 60 oveq2d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) ) = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · 0 ) )
62 3 faccld ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℕ )
63 62 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℂ )
64 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
65 fzssnn0 ⊢ ( 0 ... 𝑁 ) ⊆ ℕ0
66 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) )
67 65 66 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℕ0 )
68 67 faccld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ∈ ℕ )
69 68 nncnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
70 64 69 fprodcl ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
71 68 nnne0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ≠ 0 )
72 64 69 71 fprodn0 ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ≠ 0 )
73 63 70 72 divcld ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℂ )
74 73 mul01d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · 0 ) = 0 )
75 8 61 74 3eqtrd ⊢ ( 𝜑 → 𝑇 = 0 )