etransclem24

Description: P divides the I -th derivative of F applied to J . when J = 0 and I is not equal to P - 1 . This is the second part of case 2 proven in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem24.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem24.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
	etransclem24.i	⊢ ( 𝜑 → 𝐼 ∈ ℕ₀ )
	etransclem24.ip	⊢ ( 𝜑 → 𝐼 ≠ ( 𝑃 − 1 ) )
	etransclem24.j	⊢ ( 𝜑 → 𝐽 = 0 )
	etransclem24.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ₀ ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
	etransclem24.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ‘ 𝐼 ) )
Assertion	etransclem24	⊢ ( 𝜑 → 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		etransclem24.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2		etransclem24.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
3		etransclem24.i	⊢ ( 𝜑 → 𝐼 ∈ ℕ₀ )
4		etransclem24.ip	⊢ ( 𝜑 → 𝐼 ≠ ( 𝑃 − 1 ) )
5		etransclem24.j	⊢ ( 𝜑 → 𝐽 = 0 )
6		etransclem24.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ₀ ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
7		etransclem24.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ‘ 𝐼 ) )
8	6 3	etransclem12	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐼 ) = { 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝐼 } )
9	7 8	eleqtrd	⊢ ( 𝜑 → 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝐼 } )
10		fveq1	⊢ ( 𝑐 = 𝐷 → ( 𝑐 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑗 ) )
11	10	sumeq2sdv	⊢ ( 𝑐 = 𝐷 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) )
12	11	eqeq1d	⊢ ( 𝑐 = 𝐷 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝐼 ↔ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝐼 ) )
13	12	elrab	⊢ ( 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝐼 } ↔ ( 𝐷 ∈ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝐼 ) )
14	9 13	sylib	⊢ ( 𝜑 → ( 𝐷 ∈ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝐼 ) )
15	14	simprd	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝐼 )
16	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ¬ ∃ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝐼 )
17		ralnex	⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ↔ ¬ ∃ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝐷 ‘ 𝑘 ) ∈ ℕ )
18		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
19	2 18	eleqtrdi	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ_≥ ‘ 0 ) )
20	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 𝑀 ∈ ( ℤ_≥ ‘ 0 ) )
21		fzsscn	⊢ ( 0 ... 𝐼 ) ⊆ ℂ
22		ssrab2	⊢ { 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝐼 } ⊆ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) )
23	8 22	eqsstrdi	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐼 ) ⊆ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) )
24	23 7	sseldd	⊢ ( 𝜑 → 𝐷 ∈ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) )
25		elmapi	⊢ ( 𝐷 ∈ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝐼 ) )
26	24 25	syl	⊢ ( 𝜑 → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝐼 ) )
27	26	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑗 ) ∈ ( 0 ... 𝐼 ) )
28	21 27	sselid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑗 ) ∈ ℂ )
29	28	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑗 ) ∈ ℂ )
30		fveq2	⊢ ( 𝑗 = 0 → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 0 ) )
31	20 29 30	fsum1p	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = ( ( 𝐷 ‘ 0 ) + Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) )
32		simplr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) )
33		0p1e1	⊢ ( 0 + 1 ) = 1
34	33	oveq1i	⊢ ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 )
35	34	sumeq1i	⊢ Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐷 ‘ 𝑗 )
36	35	a1i	⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) )
37		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐷 ‘ 𝑘 ) = ( 𝐷 ‘ 𝑗 ) )
38	37	eleq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐷 ‘ 𝑘 ) ∈ ℕ ↔ ( 𝐷 ‘ 𝑗 ) ∈ ℕ ) )
39	38	notbid	⊢ ( 𝑘 = 𝑗 → ( ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ↔ ¬ ( 𝐷 ‘ 𝑗 ) ∈ ℕ ) )
40	39	rspccva	⊢ ( ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ¬ ( 𝐷 ‘ 𝑗 ) ∈ ℕ )
41	40	adantll	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ¬ ( 𝐷 ‘ 𝑗 ) ∈ ℕ )
42		fzssnn0	⊢ ( 0 ... 𝐼 ) ⊆ ℕ₀
43		fz1ssfz0	⊢ ( 1 ... 𝑀 ) ⊆ ( 0 ... 𝑀 )
44	43	sseli	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
45	44 27	sylan2	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑗 ) ∈ ( 0 ... 𝐼 ) )
46	42 45	sselid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑗 ) ∈ ℕ₀ )
47		elnn0	⊢ ( ( 𝐷 ‘ 𝑗 ) ∈ ℕ₀ ↔ ( ( 𝐷 ‘ 𝑗 ) ∈ ℕ ∨ ( 𝐷 ‘ 𝑗 ) = 0 ) )
48	46 47	sylib	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐷 ‘ 𝑗 ) ∈ ℕ ∨ ( 𝐷 ‘ 𝑗 ) = 0 ) )
49	48	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐷 ‘ 𝑗 ) ∈ ℕ ∨ ( 𝐷 ‘ 𝑗 ) = 0 ) )
50		orel1	⊢ ( ¬ ( 𝐷 ‘ 𝑗 ) ∈ ℕ → ( ( ( 𝐷 ‘ 𝑗 ) ∈ ℕ ∨ ( 𝐷 ‘ 𝑗 ) = 0 ) → ( 𝐷 ‘ 𝑗 ) = 0 ) )
51	41 49 50	sylc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑗 ) = 0 )
52	51	sumeq2dv	⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) 0 )
53		fzfi	⊢ ( 1 ... 𝑀 ) ∈ Fin
54	53	olci	⊢ ( ( 1 ... 𝑀 ) ⊆ ( ℤ_≥ ‘ 𝐴 ) ∨ ( 1 ... 𝑀 ) ∈ Fin )
55		sumz	⊢ ( ( ( 1 ... 𝑀 ) ⊆ ( ℤ_≥ ‘ 𝐴 ) ∨ ( 1 ... 𝑀 ) ∈ Fin ) → Σ 𝑗 ∈ ( 1 ... 𝑀 ) 0 = 0 )
56	54 55	mp1i	⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑀 ) 0 = 0 )
57	36 52 56	3eqtrd	⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 0 )
58	57	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 0 )
59	32 58	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( ( 𝐷 ‘ 0 ) + Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝑃 − 1 ) + 0 ) )
60		nnm1nn0	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ₀ )
61	1 60	syl	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ₀ )
62	61	nn0red	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ )
63	62	recnd	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℂ )
64	63	addid1d	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) + 0 ) = ( 𝑃 − 1 ) )
65	64	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( ( 𝑃 − 1 ) + 0 ) = ( 𝑃 − 1 ) )
66	31 59 65	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = ( 𝑃 − 1 ) )
67	4	necomd	⊢ ( 𝜑 → ( 𝑃 − 1 ) ≠ 𝐼 )
68	67	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( 𝑃 − 1 ) ≠ 𝐼 )
69	66 68	eqnetrd	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ≠ 𝐼 )
70	69	neneqd	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ¬ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ¬ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝐼 )
71	17 70	sylan2br	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ ¬ ∃ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ¬ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝐼 )
72	16 71	condan	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ∃ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝐷 ‘ 𝑘 ) ∈ ℕ )
73	1	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
74	15	eqcomd	⊢ ( 𝜑 → 𝐼 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) )
75	74	fveq2d	⊢ ( 𝜑 → ( ! ‘ 𝐼 ) = ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) )
76	75	oveq1d	⊢ ( 𝜑 → ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
77		nfcv	⊢ Ⅎ 𝑗 𝐷
78		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
79		nn0ex	⊢ ℕ₀ ∈ V
80		mapss	⊢ ( ( ℕ₀ ∈ V ∧ ( 0 ... 𝐼 ) ⊆ ℕ₀ ) → ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) ⊆ ( ℕ₀ ↑_m ( 0 ... 𝑀 ) ) )
81	79 42 80	mp2an	⊢ ( ( 0 ... 𝐼 ) ↑_m ( 0 ... 𝑀 ) ) ⊆ ( ℕ₀ ↑_m ( 0 ... 𝑀 ) )
82	81 24	sselid	⊢ ( 𝜑 → 𝐷 ∈ ( ℕ₀ ↑_m ( 0 ... 𝑀 ) ) )
83	77 78 82	mccl	⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℕ )
84	76 83	eqeltrd	⊢ ( 𝜑 → ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℕ )
85	84	nnzd	⊢ ( 𝜑 → ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℤ )
86		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
87	1	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
88	26	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝐼 ) )
89	44	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
90		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
91	5 90	eqeltrd	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
92	91	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐽 ∈ ℤ )
93	87 88 89 92	etransclem3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
94	86 93	fprodzcl	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
95	73 85 94	3jca	⊢ ( 𝜑 → ( 𝑃 ∈ ℤ ∧ ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) )
96	95	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( 𝑃 ∈ ℤ ∧ ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) )
97	73	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℤ )
98	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
99	26	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝐼 ) )
100	43	sseli	⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
101	100	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
102	91	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝐽 ∈ ℤ )
103	98 99 101 102	etransclem3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) ∈ ℤ )
104		difss	⊢ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ⊆ ( 1 ... 𝑀 )
105		ssfi	⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ⊆ ( 1 ... 𝑀 ) ) → ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ∈ Fin )
106	53 104 105	mp2an	⊢ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ∈ Fin
107	106	a1i	⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ∈ Fin )
108	1	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ) → 𝑃 ∈ ℕ )
109	26	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝐼 ) )
110	104 43	sstri	⊢ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ⊆ ( 0 ... 𝑀 )
111	110	sseli	⊢ ( 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
112	111	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
113	91	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ) → 𝐽 ∈ ℤ )
114	108 109 112 113	etransclem3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) ) → if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
115	107 114	fprodzcl	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
116	115	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
117	97 103 116	3jca	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 ∈ ℤ ∧ if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) )
118	117	3adant3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( 𝑃 ∈ ℤ ∧ if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) )
119		dvds0	⊢ ( 𝑃 ∈ ℤ → 𝑃 ∥ 0 )
120	73 119	syl	⊢ ( 𝜑 → 𝑃 ∥ 0 )
121	120	adantr	⊢ ( ( 𝜑 ∧ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∥ 0 )
122	121	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∥ 0 )
123		iftrue	⊢ ( 𝑃 < ( 𝐷 ‘ 𝑘 ) → if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) = 0 )
124	123	eqcomd	⊢ ( 𝑃 < ( 𝐷 ‘ 𝑘 ) → 0 = if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
125	124	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 0 = if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
126	122 125	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∥ if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
127	97	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∈ ℤ )
128		0zd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 0 ∈ ℤ )
129	99 101	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑘 ) ∈ ( 0 ... 𝐼 ) )
130	129	elfzelzd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑘 ) ∈ ℤ )
131	97 130	zsubcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ )
132	128 97 131	3jca	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 0 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ ) )
133	132	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 0 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ ) )
134		fzssre	⊢ ( 0 ... 𝐼 ) ⊆ ℝ
135	134 129	sselid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑘 ) ∈ ℝ )
136	135	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝐷 ‘ 𝑘 ) ∈ ℝ )
137	127	zred	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∈ ℝ )
138		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) )
139	136 137 138	nltled	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝐷 ‘ 𝑘 ) ≤ 𝑃 )
140	137 136	subge0d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 0 ≤ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ↔ ( 𝐷 ‘ 𝑘 ) ≤ 𝑃 ) )
141	139 140	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 0 ≤ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) )
142		elfzle1	⊢ ( ( 𝐷 ‘ 𝑘 ) ∈ ( 0 ... 𝐼 ) → 0 ≤ ( 𝐷 ‘ 𝑘 ) )
143	129 142	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( 𝐷 ‘ 𝑘 ) )
144	143	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 0 ≤ ( 𝐷 ‘ 𝑘 ) )
145	137 136	subge02d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 0 ≤ ( 𝐷 ‘ 𝑘 ) ↔ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ≤ 𝑃 ) )
146	144 145	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ≤ 𝑃 )
147	133 141 146	jca32	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( 0 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ ) ∧ ( 0 ≤ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ≤ 𝑃 ) ) )
148		elfz2	⊢ ( ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ( 0 ... 𝑃 ) ↔ ( ( 0 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ ) ∧ ( 0 ≤ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ≤ 𝑃 ) ) )
149	147 148	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ( 0 ... 𝑃 ) )
150		permnn	⊢ ( ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ( 0 ... 𝑃 ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ℕ )
151	149 150	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ℕ )
152	151	nnzd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ℤ )
153	101	elfzelzd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑘 ∈ ℤ )
154	102 153	zsubcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝐽 − 𝑘 ) ∈ ℤ )
155	154	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝐽 − 𝑘 ) ∈ ℤ )
156	131	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ )
157		elnn0z	⊢ ( ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℕ₀ ↔ ( ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ ∧ 0 ≤ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) )
158	156 141 157	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℕ₀ )
159		zexpcl	⊢ ( ( ( 𝐽 − 𝑘 ) ∈ ℤ ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℕ₀ ) → ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℤ )
160	155 158 159	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℤ )
161	127 152 160	3jca	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝑃 ∈ ℤ ∧ ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ℤ ∧ ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℤ ) )
162	161	3adantl3	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝑃 ∈ ℤ ∧ ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ℤ ∧ ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℤ ) )
163	127	3adantl3	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∈ ℤ )
164	61	nn0zd	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℤ )
165	164	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 − 1 ) ∈ ℤ )
166	128 165 131	3jca	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 0 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ ) )
167	166	3adant3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( 0 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ ) )
168	167	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 0 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ ) )
169	141	3adantl3	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 0 ≤ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) )
170		1red	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 1 ∈ ℝ )
171		nnre	⊢ ( ( 𝐷 ‘ 𝑘 ) ∈ ℕ → ( 𝐷 ‘ 𝑘 ) ∈ ℝ )
172	171	adantl	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( 𝐷 ‘ 𝑘 ) ∈ ℝ )
173	1	nnred	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
174	173	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 𝑃 ∈ ℝ )
175		nnge1	⊢ ( ( 𝐷 ‘ 𝑘 ) ∈ ℕ → 1 ≤ ( 𝐷 ‘ 𝑘 ) )
176	175	adantl	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 1 ≤ ( 𝐷 ‘ 𝑘 ) )
177	170 172 174 176	lesub2dd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ≤ ( 𝑃 − 1 ) )
178	177	3adant2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ≤ ( 𝑃 − 1 ) )
179	178	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ≤ ( 𝑃 − 1 ) )
180	168 169 179	jca32	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( 0 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ ) ∧ ( 0 ≤ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ≤ ( 𝑃 − 1 ) ) ) )
181		elfz2	⊢ ( ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ( 0 ... ( 𝑃 − 1 ) ) ↔ ( ( 0 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ℤ ) ∧ ( 0 ≤ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∧ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ≤ ( 𝑃 − 1 ) ) ) )
182	180 181	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
183		permnn	⊢ ( ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ∈ ( 0 ... ( 𝑃 − 1 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ℕ )
184	182 183	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ℕ )
185	184	nnzd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ℤ )
186		dvdsmul1	⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ℤ ) → 𝑃 ∥ ( 𝑃 · ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
187	163 185 186	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∥ ( 𝑃 · ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
188	1	nncnd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
189		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
190	188 189	npcand	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) + 1 ) = 𝑃 )
191	190	eqcomd	⊢ ( 𝜑 → 𝑃 = ( ( 𝑃 − 1 ) + 1 ) )
192	191	fveq2d	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) = ( ! ‘ ( ( 𝑃 − 1 ) + 1 ) ) )
193		facp1	⊢ ( ( 𝑃 − 1 ) ∈ ℕ₀ → ( ! ‘ ( ( 𝑃 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) )
194	61 193	syl	⊢ ( 𝜑 → ( ! ‘ ( ( 𝑃 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) )
195	190	oveq2d	⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · 𝑃 ) )
196	61	faccld	⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
197	196	nncnd	⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
198	197 188	mulcomd	⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · 𝑃 ) = ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) )
199	195 198	eqtrd	⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) = ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) )
200	192 194 199	3eqtrd	⊢ ( 𝜑 → ( ! ‘ 𝑃 ) = ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) )
201	200	oveq1d	⊢ ( 𝜑 → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) = ( ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) )
202	201	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) = ( ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) )
203	202	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) = ( ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) )
204	188	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∈ ℂ )
205	197	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
206	158	faccld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℕ )
207	206	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℂ )
208	206	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ≠ 0 )
209	204 205 207 208	divassd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) = ( 𝑃 · ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
210	209	3adantl3	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) = ( 𝑃 · ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
211	203 210	eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → ( 𝑃 · ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) = ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) )
212	187 211	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∥ ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) )
213		dvdsmultr1	⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ℤ ∧ ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) → 𝑃 ∥ ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
214	162 212 213	sylc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∥ ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) )
215		iffalse	⊢ ( ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) → if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) )
216	215	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) )
217	214 216	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ ¬ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) → 𝑃 ∥ if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
218	126 217	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 𝑃 ∥ if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
219		dvdsmultr1	⊢ ( ( 𝑃 ∈ ℤ ∧ if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) → ( 𝑃 ∥ if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) → 𝑃 ∥ ( if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) · ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
220	118 218 219	sylc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 𝑃 ∥ ( if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) · ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
221		fzfid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( 1 ... 𝑀 ) ∈ Fin )
222	93	zcnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℂ )
223	222	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℂ )
224		simp2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 𝑘 ∈ ( 1 ... 𝑀 ) )
225		fveq2	⊢ ( 𝑗 = 𝑘 → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑘 ) )
226	225	breq2d	⊢ ( 𝑗 = 𝑘 → ( 𝑃 < ( 𝐷 ‘ 𝑗 ) ↔ 𝑃 < ( 𝐷 ‘ 𝑘 ) ) )
227	225	oveq2d	⊢ ( 𝑗 = 𝑘 → ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) = ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) )
228	227	fveq2d	⊢ ( 𝑗 = 𝑘 → ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) = ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) )
229	228	oveq2d	⊢ ( 𝑗 = 𝑘 → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) = ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) )
230		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝐽 − 𝑗 ) = ( 𝐽 − 𝑘 ) )
231	230 227	oveq12d	⊢ ( 𝑗 = 𝑘 → ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) )
232	229 231	oveq12d	⊢ ( 𝑗 = 𝑘 → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) )
233	226 232	ifbieq2d	⊢ ( 𝑗 = 𝑘 → if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) = if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
234	233	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) ∧ 𝑗 = 𝑘 ) → if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) = if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) )
235	221 223 224 234	fprodsplit1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( if ( 𝑃 < ( 𝐷 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑘 ) ) ) ) ) · ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑘 } ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
236	220 235	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 𝑃 ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
237		dvdsmultr2	⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) → ( 𝑃 ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) → 𝑃 ∥ ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
238	96 236 237	sylc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 𝑃 ∥ ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
239	238	3adant1r	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 𝑃 ∥ ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
240		simpr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) )
241		eluzfz1	⊢ ( 𝑀 ∈ ( ℤ_≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
242	19 241	syl	⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
243	26 242	ffvelrnd	⊢ ( 𝜑 → ( 𝐷 ‘ 0 ) ∈ ( 0 ... 𝐼 ) )
244	134 243	sselid	⊢ ( 𝜑 → ( 𝐷 ‘ 0 ) ∈ ℝ )
245	244	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( 𝐷 ‘ 0 ) ∈ ℝ )
246	62	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( 𝑃 − 1 ) ∈ ℝ )
247	245 246	lttri3d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ↔ ( ¬ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) ) )
248	240 247	mpbid	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ¬ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) )
249	248	simprd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) )
250	249	iffalsed	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) )
251		oveq2	⊢ ( ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) → ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) = ( ( 𝑃 − 1 ) − ( 𝑃 − 1 ) ) )
252	63	subidd	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) − ( 𝑃 − 1 ) ) = 0 )
253	251 252	sylan9eqr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) = 0 )
254	253	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = ( ! ‘ 0 ) )
255		fac0	⊢ ( ! ‘ 0 ) = 1
256	254 255	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = 1 )
257	256	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) / 1 ) )
258	197	div1d	⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) / 1 ) = ( ! ‘ ( 𝑃 − 1 ) ) )
259	258	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / 1 ) = ( ! ‘ ( 𝑃 − 1 ) ) )
260	257 259	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
261	253	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = ( 𝐽 ↑ 0 ) )
262	91	zcnd	⊢ ( 𝜑 → 𝐽 ∈ ℂ )
263	262	exp0d	⊢ ( 𝜑 → ( 𝐽 ↑ 0 ) = 1 )
264	263	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( 𝐽 ↑ 0 ) = 1 )
265	261 264	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = 1 )
266	260 265	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · 1 ) )
267	197	mulid1d	⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · 1 ) = ( ! ‘ ( 𝑃 − 1 ) ) )
268	267	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) · 1 ) = ( ! ‘ ( 𝑃 − 1 ) ) )
269	250 266 268	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
270	269	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
271	270	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) = ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
272	271	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
273	84	nncnd	⊢ ( 𝜑 → ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℂ )
274	94	zcnd	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℂ )
275	197 274	mulcld	⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℂ )
276	196	nnne0d	⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
277	273 275 197 276	divassd	⊢ ( 𝜑 → ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
278	277	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
279	274 197 276	divcan3d	⊢ ( 𝜑 → ( ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
280	279	oveq2d	⊢ ( 𝜑 → ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) = ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
281	280	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) = ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
282	272 278 281	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
283	282	3ad2ant1	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
284	239 283	breqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐷 ‘ 𝑘 ) ∈ ℕ ) → 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
285	284	rexlimdv3a	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ∃ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝐷 ‘ 𝑘 ) ∈ ℕ → 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
286	72 285	mpd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
287	120	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → 𝑃 ∥ 0 )
288		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) )
289	288	iftrued	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) = 0 )
290		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) )
291	290	iffalsed	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) )
292		simpll	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → 𝜑 )
293	244	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → ( 𝐷 ‘ 0 ) ∈ ℝ )
294	62	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → ( 𝑃 − 1 ) ∈ ℝ )
295	293 294 290	nltled	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → ( 𝐷 ‘ 0 ) ≤ ( 𝑃 − 1 ) )
296		id	⊢ ( ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) → ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) )
297	296	necomd	⊢ ( ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) → ( 𝑃 − 1 ) ≠ ( 𝐷 ‘ 0 ) )
298	297	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → ( 𝑃 − 1 ) ≠ ( 𝐷 ‘ 0 ) )
299	293 294 295 298	leneltd	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) )
300	5	oveq1d	⊢ ( 𝜑 → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) )
301	300	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) )
302	243	elfzelzd	⊢ ( 𝜑 → ( 𝐷 ‘ 0 ) ∈ ℤ )
303	164 302	zsubcld	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ∈ ℤ )
304	303	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ∈ ℤ )
305		simpr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) )
306	244	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( 𝐷 ‘ 0 ) ∈ ℝ )
307	62	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( 𝑃 − 1 ) ∈ ℝ )
308	306 307	posdifd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ↔ 0 < ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) )
309	305 308	mpbid	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → 0 < ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) )
310		elnnz	⊢ ( ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ∈ ℕ ↔ ( ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ∈ ℤ ∧ 0 < ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) )
311	304 309 310	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ∈ ℕ )
312	311	0expd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = 0 )
313	301 312	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = 0 )
314	313	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · 0 ) )
315	197	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
316	311	nnnn0d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ∈ ℕ₀ )
317	316	faccld	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ∈ ℕ )
318	317	nncnd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ∈ ℂ )
319	317	nnne0d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ≠ 0 )
320	315 318 319	divcld	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ∈ ℂ )
321	320	mul01d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · 0 ) = 0 )
322	314 321	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) = 0 )
323	292 299 322	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) = 0 )
324	291 323	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) → if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) = 0 )
325	289 324	pm2.61dan	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) = 0 )
326	325	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = ( 0 · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
327	274	mul02d	⊢ ( 𝜑 → ( 0 · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = 0 )
328	327	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → ( 0 · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = 0 )
329	326 328	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = 0 )
330	329	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) = ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · 0 ) )
331	273	mul01d	⊢ ( 𝜑 → ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · 0 ) = 0 )
332	331	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · 0 ) = 0 )
333	330 332	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) = 0 )
334	333	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( 0 / ( ! ‘ ( 𝑃 − 1 ) ) ) )
335	197 276	div0d	⊢ ( 𝜑 → ( 0 / ( ! ‘ ( 𝑃 − 1 ) ) ) = 0 )
336	335	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → ( 0 / ( ! ‘ ( 𝑃 − 1 ) ) ) = 0 )
337	334 336	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = 0 )
338	287 337	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) ) → 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
339	286 338	pm2.61dane	⊢ ( 𝜑 → 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )

Metamath Proof Explorer

Theorem etransclem24

Proof