Theorem etransclem25

Description: P factorial divides the N -th derivative of F applied to J . (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		etransclem25.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2		etransclem25.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3		etransclem25.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		etransclem25.c	⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
5		etransclem25.sumc	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) = 𝑁 )
6		etransclem25.t	⊢ 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
7		etransclem25.j	⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑀 ) )
8	1	nnnn0d	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
9	8	faccld	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∈ ℕ )
10	9	nnzd	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∈ ℤ )
11	5	eqcomd	⊢ ( 𝜑 → 𝑁 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) )
12	11	fveq2d	⊢ ( 𝜑 → ( ! ‘ 𝑁 ) = ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) ) )
13	12	oveq1d	⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) )
14		nfcv	⊢ Ⅎ 𝑗 𝐶
15		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
16		nn0ex	⊢ ℕ0 ∈ V
17		fzssnn0	⊢ ( 0 ... 𝑁 ) ⊆ ℕ0
18		mapss	⊢ ( ( ℕ0 ∈ V ∧ ( 0 ... 𝑁 ) ⊆ ℕ0 ) → ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
19	16 17 18	mp2an	⊢ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0 ↑m ( 0 ... 𝑀 ) )
20		ovex	⊢ ( 0 ... 𝑁 ) ∈ V
21		ovexd	⊢ ( 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) → ( 0 ... 𝑀 ) ∈ V )
22		elmapg	⊢ ( ( ( 0 ... 𝑁 ) ∈ V ∧ ( 0 ... 𝑀 ) ∈ V ) → ( 𝐶 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ↔ 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) ) )
23	20 21 22	sylancr	⊢ ( 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) → ( 𝐶 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ↔ 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) ) )
24	23	ibir	⊢ ( 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) → 𝐶 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) )
25	19 24	sselid	⊢ ( 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) → 𝐶 ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
26	4 25	syl	⊢ ( 𝜑 → 𝐶 ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
27	14 15 26	mccl	⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℕ )
28	13 27	eqeltrd	⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℕ )
29	28	nnzd	⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℤ )
30	7	elfzelzd	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
31	1 2 4 30	etransclem10	⊢ ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ∈ ℤ )
32	29 31	zmulcld	⊢ ( 𝜑 → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) ∈ ℤ )
33		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
34	1	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
35	4	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
36		0z	⊢ 0 ∈ ℤ
37		fzp1ss	⊢ ( 0 ∈ ℤ → ( ( 0 + 1 ) ... 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
38	36 37	ax-mp	⊢ ( ( 0 + 1 ) ... 𝑀 ) ⊆ ( 0 ... 𝑀 )
39		id	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
40		1e0p1	⊢ 1 = ( 0 + 1 )
41	40	oveq1i	⊢ ( 1 ... 𝑀 ) = ( ( 0 + 1 ) ... 𝑀 )
42	39 41	eleqtrdi	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) )
43	38 42	sselid	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
44	43	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
45	30	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐽 ∈ ℤ )
46	34 35 44 45	etransclem3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
47	33 46	fprodzcl	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
48	10 32 47	3jca	⊢ ( 𝜑 → ( ( ! ‘ 𝑃 ) ∈ ℤ ∧ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) )
49	30	zcnd	⊢ ( 𝜑 → 𝐽 ∈ ℂ )
50	49	subidd	⊢ ( 𝜑 → ( 𝐽 − 𝐽 ) = 0 )
51	50	eqcomd	⊢ ( 𝜑 → 0 = ( 𝐽 − 𝐽 ) )
52	51	oveq1d	⊢ ( 𝜑 → ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = ( ( 𝐽 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
53	52	oveq2d	⊢ ( 𝜑 → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( ( 𝐽 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
54	53	ifeq2d	⊢ ( 𝜑 → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( ( 𝐽 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
55		id	⊢ ( 𝐽 ∈ ( 1 ... 𝑀 ) → 𝐽 ∈ ( 1 ... 𝑀 ) )
56	55 41	eleqtrdi	⊢ ( 𝐽 ∈ ( 1 ... 𝑀 ) → 𝐽 ∈ ( ( 0 + 1 ) ... 𝑀 ) )
57	38 56	sselid	⊢ ( 𝐽 ∈ ( 1 ... 𝑀 ) → 𝐽 ∈ ( 0 ... 𝑀 ) )
58	7 57	syl	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
59	1 4 58 30	etransclem3	⊢ ( 𝜑 → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( ( 𝐽 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) ∈ ℤ )
60	54 59	eqeltrd	⊢ ( 𝜑 → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) ∈ ℤ )
61		fzfi	⊢ ( 1 ... 𝑀 ) ∈ Fin
62		diffi	⊢ ( ( 1 ... 𝑀 ) ∈ Fin → ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ∈ Fin )
63	61 62	mp1i	⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ∈ Fin )
64	1	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ) → 𝑃 ∈ ℕ )
65	4	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ) → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
66		eldifi	⊢ ( 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
67	66 43	syl	⊢ ( 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
68	67	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
69	30	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ) → 𝐽 ∈ ℤ )
70	64 65 68 69	etransclem3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
71	63 70	fprodzcl	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
72		dvds0	⊢ ( ( ! ‘ 𝑃 ) ∈ ℤ → ( ! ‘ 𝑃 ) ∥ 0 )
73	10 72	syl	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ 0 )
74	73	adantr	⊢ ( ( 𝜑 ∧ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ 0 )
75		iftrue	⊢ ( 𝑃 < ( 𝐶 ‘ 𝐽 ) → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) = 0 )
76	75	eqcomd	⊢ ( 𝑃 < ( 𝐶 ‘ 𝐽 ) → 0 = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
77	76	adantl	⊢ ( ( 𝜑 ∧ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → 0 = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
78	74 77	breqtrd	⊢ ( ( 𝜑 ∧ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
79		iddvds	⊢ ( ( ! ‘ 𝑃 ) ∈ ℤ → ( ! ‘ 𝑃 ) ∥ ( ! ‘ 𝑃 ) )
80	10 79	syl	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ ( ! ‘ 𝑃 ) )
81	80	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ ( ! ‘ 𝑃 ) )
82		iffalse	⊢ ( ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
83	82	ad2antlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
84		oveq1	⊢ ( 𝑃 = ( 𝐶 ‘ 𝐽 ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) = ( ( 𝐶 ‘ 𝐽 ) − ( 𝐶 ‘ 𝐽 ) ) )
85	84	adantl	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) = ( ( 𝐶 ‘ 𝐽 ) − ( 𝐶 ‘ 𝐽 ) ) )
86	4 58	ffvelcdmd	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ( 0 ... 𝑁 ) )
87	86	elfzelzd	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ℤ )
88	87	zcnd	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ℂ )
89	88	adantr	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ∈ ℂ )
90	89	subidd	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( 𝐶 ‘ 𝐽 ) − ( 𝐶 ‘ 𝐽 ) ) = 0 )
91	85 90	eqtrd	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) = 0 )
92	91	fveq2d	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = ( ! ‘ 0 ) )
93		fac0	⊢ ( ! ‘ 0 ) = 1
94	92 93	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = 1 )
95	94	oveq2d	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ( ! ‘ 𝑃 ) / 1 ) )
96	9	nncnd	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∈ ℂ )
97	96	div1d	⊢ ( 𝜑 → ( ( ! ‘ 𝑃 ) / 1 ) = ( ! ‘ 𝑃 ) )
98	97	adantr	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ! ‘ 𝑃 ) / 1 ) = ( ! ‘ 𝑃 ) )
99	95 98	eqtrd	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ! ‘ 𝑃 ) )
100	91	oveq2d	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = ( 0 ↑ 0 ) )
101		0cnd	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → 0 ∈ ℂ )
102	101	exp0d	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 0 ↑ 0 ) = 1 )
103	100 102	eqtrd	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = 1 )
104	99 103	oveq12d	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ( ! ‘ 𝑃 ) · 1 ) )
105	96	mulridd	⊢ ( 𝜑 → ( ( ! ‘ 𝑃 ) · 1 ) = ( ! ‘ 𝑃 ) )
106	105	adantr	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ! ‘ 𝑃 ) · 1 ) = ( ! ‘ 𝑃 ) )
107	104 106	eqtrd	⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ! ‘ 𝑃 ) )
108	107	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ! ‘ 𝑃 ) )
109	83 108	eqtr2d	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
110	81 109	breqtrd	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
111	73	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ 0 )
112		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) )
113	112	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) )
114	113	iffalsed	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
115		simpll	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → 𝜑 )
116	87	zred	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ℝ )
117	116	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ∈ ℝ )
118	1	nnred	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
119	118	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → 𝑃 ∈ ℝ )
120	116	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ∈ ℝ )
121	118	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → 𝑃 ∈ ℝ )
122	120 121 112	nltled	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ≤ 𝑃 )
123	122	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ≤ 𝑃 )
124		neqne	⊢ ( ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) → 𝑃 ≠ ( 𝐶 ‘ 𝐽 ) )
125	124	adantl	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → 𝑃 ≠ ( 𝐶 ‘ 𝐽 ) )
126	117 119 123 125	leneltd	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) < 𝑃 )
127	1	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
128	127	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → 𝑃 ∈ ℤ )
129	87	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝐶 ‘ 𝐽 ) ∈ ℤ )
130	128 129	zsubcld	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℤ )
131		simpr	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝐶 ‘ 𝐽 ) < 𝑃 )
132	116	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝐶 ‘ 𝐽 ) ∈ ℝ )
133	118	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → 𝑃 ∈ ℝ )
134	132 133	posdifd	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ( 𝐶 ‘ 𝐽 ) < 𝑃 ↔ 0 < ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
135	131 134	mpbid	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → 0 < ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) )
136		elnnz	⊢ ( ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℕ ↔ ( ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℤ ∧ 0 < ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
137	130 135 136	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℕ )
138	137	0expd	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = 0 )
139	138	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · 0 ) )
140	96	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ! ‘ 𝑃 ) ∈ ℂ )
141	137	nnnn0d	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℕ0 )
142	141	faccld	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ∈ ℕ )
143	142	nncnd	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ∈ ℂ )
144	142	nnne0d	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ≠ 0 )
145	140 143 144	divcld	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ∈ ℂ )
146	145	mul01d	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · 0 ) = 0 )
147	139 146	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = 0 )
148	115 126 147	syl2anc	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = 0 )
149	114 148	eqtr2d	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → 0 = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
150	111 149	breqtrd	⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
151	110 150	pm2.61dan	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
152	78 151	pm2.61dan	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
153	10 60 71 152	dvdsmultr1d	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ ( if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) · ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
154	46	zcnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℂ )
155		fveq2	⊢ ( 𝑗 = 𝐽 → ( 𝐶 ‘ 𝑗 ) = ( 𝐶 ‘ 𝐽 ) )
156	155	breq2d	⊢ ( 𝑗 = 𝐽 → ( 𝑃 < ( 𝐶 ‘ 𝑗 ) ↔ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) )
157	156	adantl	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( 𝑃 < ( 𝐶 ‘ 𝑗 ) ↔ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) )
158	155	oveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) = ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) )
159	158	fveq2d	⊢ ( 𝑗 = 𝐽 → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) = ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
160	159	oveq2d	⊢ ( 𝑗 = 𝐽 → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) = ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
161	160	adantl	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) = ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
162		oveq2	⊢ ( 𝑗 = 𝐽 → ( 𝐽 − 𝑗 ) = ( 𝐽 − 𝐽 ) )
163	162 50	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( 𝐽 − 𝑗 ) = 0 )
164	158	adantl	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) = ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) )
165	163 164	oveq12d	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) = ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
166	161 165	oveq12d	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
167	157 166	ifbieq2d	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
168	33 154 7 167	fprodsplit1	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) = ( if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) · ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
169	153 168	breqtrrd	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) )
170		dvdsmultr2	⊢ ( ( ( ! ‘ 𝑃 ) ∈ ℤ ∧ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) → ( ( ! ‘ 𝑃 ) ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) → ( ! ‘ 𝑃 ) ∥ ( ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) ) )
171	48 169 170	sylc	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ ( ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
172	3	faccld	⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℕ )
173	172	nncnd	⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℂ )
174	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) )
175	17 174	sselid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℕ0 )
176	175	faccld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ∈ ℕ )
177	176	nncnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
178	15 177	fprodcl	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
179	176	nnne0d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ≠ 0 )
180	15 177 179	fprodn0	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ≠ 0 )
181	173 178 180	divcld	⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℂ )
182	31	zcnd	⊢ ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ∈ ℂ )
183	33 154	fprodcl	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℂ )
184	181 182 183	mulassd	⊢ ( 𝜑 → ( ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) ) )
185	184 6	eqtr4di	⊢ ( 𝜑 → ( ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) = 𝑇 )
186	171 185	breqtrd	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ 𝑇 )