mccl

Description: A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	mccl.kb	⊢ Ⅎ 𝑘 𝐵
	mccl.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	mccl.b	⊢ ( 𝜑 → 𝐵 ∈ ( ℕ₀ ↑_m 𝐴 ) )
Assertion	mccl	⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		mccl.kb	⊢ Ⅎ 𝑘 𝐵
2		mccl.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		mccl.b	⊢ ( 𝜑 → 𝐵 ∈ ( ℕ₀ ↑_m 𝐴 ) )
4		sumeq1	⊢ ( 𝑎 = ∅ → Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) )
5	4	fveq2d	⊢ ( 𝑎 = ∅ → ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) )
6		prodeq1	⊢ ( 𝑎 = ∅ → ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) )
7	5 6	oveq12d	⊢ ( 𝑎 = ∅ → ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) )
8	7	eleq1d	⊢ ( 𝑎 = ∅ → ( ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
9	8	ralbidv	⊢ ( 𝑎 = ∅ → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
10		oveq2	⊢ ( 𝑎 = ∅ → ( ℕ₀ ↑_m 𝑎 ) = ( ℕ₀ ↑_m ∅ ) )
11	10	raleqdv	⊢ ( 𝑎 = ∅ → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m ∅ ) ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
12	9 11	bitrd	⊢ ( 𝑎 = ∅ → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m ∅ ) ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
13		sumeq1	⊢ ( 𝑎 = 𝑐 → Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) )
14	13	fveq2d	⊢ ( 𝑎 = 𝑐 → ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) )
15		prodeq1	⊢ ( 𝑎 = 𝑐 → ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) )
16	14 15	oveq12d	⊢ ( 𝑎 = 𝑐 → ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) )
17	16	eleq1d	⊢ ( 𝑎 = 𝑐 → ( ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
18	17	ralbidv	⊢ ( 𝑎 = 𝑐 → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
19		oveq2	⊢ ( 𝑎 = 𝑐 → ( ℕ₀ ↑_m 𝑎 ) = ( ℕ₀ ↑_m 𝑐 ) )
20	19	raleqdv	⊢ ( 𝑎 = 𝑐 → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
21	18 20	bitrd	⊢ ( 𝑎 = 𝑐 → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
22		sumeq1	⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) )
23	22	fveq2d	⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) )
24		prodeq1	⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) )
25	23 24	oveq12d	⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) )
26	25	eleq1d	⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
27	26	ralbidv	⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
28		oveq2	⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ℕ₀ ↑_m 𝑎 ) = ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) )
29	28	raleqdv	⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
30	27 29	bitrd	⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
31		sumeq1	⊢ ( 𝑎 = 𝐴 → Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) )
32	31	fveq2d	⊢ ( 𝑎 = 𝐴 → ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) )
33		prodeq1	⊢ ( 𝑎 = 𝐴 → ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) )
34	32 33	oveq12d	⊢ ( 𝑎 = 𝐴 → ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) )
35	34	eleq1d	⊢ ( 𝑎 = 𝐴 → ( ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
36	35	ralbidv	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
37		oveq2	⊢ ( 𝑎 = 𝐴 → ( ℕ₀ ↑_m 𝑎 ) = ( ℕ₀ ↑_m 𝐴 ) )
38	37	raleqdv	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝐴 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
39	36 38	bitrd	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝐴 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
40		sum0	⊢ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) = 0
41	40	fveq2i	⊢ ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ 0 )
42		fac0	⊢ ( ! ‘ 0 ) = 1
43	41 42	eqtri	⊢ ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) = 1
44		prod0	⊢ ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = 1
45	43 44	oveq12i	⊢ ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( 1 / 1 )
46		1div1e1	⊢ ( 1 / 1 ) = 1
47	45 46	eqtri	⊢ ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = 1
48		1nn	⊢ 1 ∈ ℕ
49	47 48	eqeltri	⊢ ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ
50	49	a1i	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( ℕ₀ ↑_m ∅ ) ) → ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
51	50	ralrimiva	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( ℕ₀ ↑_m ∅ ) ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
52		nfv	⊢ Ⅎ 𝑏 ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) )
53		nfra1	⊢ Ⅎ 𝑏 ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ
54	52 53	nfan	⊢ Ⅎ 𝑏 ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
55		simpll	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ) → ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) )
56		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝑏 ‘ 𝑘 ) = ( 𝑏 ‘ 𝑗 ) )
57	56	cbvsumv	⊢ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) = Σ 𝑗 ∈ 𝑐 ( 𝑏 ‘ 𝑗 )
58	57	a1i	⊢ ( 𝑏 = 𝑒 → Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) = Σ 𝑗 ∈ 𝑐 ( 𝑏 ‘ 𝑗 ) )
59		fveq1	⊢ ( 𝑏 = 𝑒 → ( 𝑏 ‘ 𝑗 ) = ( 𝑒 ‘ 𝑗 ) )
60	59	sumeq2sdv	⊢ ( 𝑏 = 𝑒 → Σ 𝑗 ∈ 𝑐 ( 𝑏 ‘ 𝑗 ) = Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) )
61	58 60	eqtrd	⊢ ( 𝑏 = 𝑒 → Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) = Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) )
62	61	fveq2d	⊢ ( 𝑏 = 𝑒 → ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) )
63		2fveq3	⊢ ( 𝑘 = 𝑗 → ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ ( 𝑏 ‘ 𝑗 ) ) )
64	63	cbvprodv	⊢ ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑗 ) )
65	64	a1i	⊢ ( 𝑏 = 𝑒 → ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑗 ) ) )
66	59	fveq2d	⊢ ( 𝑏 = 𝑒 → ( ! ‘ ( 𝑏 ‘ 𝑗 ) ) = ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) )
67	66	prodeq2ad	⊢ ( 𝑏 = 𝑒 → ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑗 ) ) = ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) )
68	65 67	eqtrd	⊢ ( 𝑏 = 𝑒 → ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) )
69	62 68	oveq12d	⊢ ( 𝑏 = 𝑒 → ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) )
70	69	eleq1d	⊢ ( 𝑏 = 𝑒 → ( ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) )
71	70	cbvralvw	⊢ ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ )
72	71	biimpi	⊢ ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ → ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ )
73	72	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ) → ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ )
74		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ) → 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) )
75	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ) → 𝐴 ∈ Fin )
76		simprl	⊢ ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) → 𝑐 ⊆ 𝐴 )
77	76	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ) → 𝑐 ⊆ 𝐴 )
78		simprr	⊢ ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) → 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) )
79	78	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ) → 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) )
80		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ) → 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) )
81		fveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑒 ‘ 𝑗 ) = ( 𝑒 ‘ 𝑘 ) )
82	81	cbvsumv	⊢ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) = Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 )
83	82	fveq2i	⊢ ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) = ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) )
84		2fveq3	⊢ ( 𝑗 = 𝑘 → ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) = ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) )
85	84	cbvprodv	⊢ ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) = ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) )
86	83 85	oveq12i	⊢ ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) )
87	86	eleq1i	⊢ ( ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) ) ∈ ℕ )
88	87	ralbii	⊢ ( ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ↔ ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) ) ∈ ℕ )
89	88	biimpi	⊢ ( ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ → ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) ) ∈ ℕ )
90	89	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ) → ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) ) ∈ ℕ )
91	75 77 79 80 90	mccllem	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ) → ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
92	55 73 74 91	syl21anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ) → ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
93	92	ex	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) → ( 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) → ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
94	54 93	ralrimi	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) → ∀ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
95	94	ex	⊢ ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) → ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ → ∀ 𝑏 ∈ ( ℕ₀ ↑_m ( 𝑐 ∪ { 𝑑 } ) ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
96	12 21 30 39 51 95 2	findcard2d	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝐴 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
97		nfcv	⊢ Ⅎ 𝑘 𝑏
98	97 1	nfeq	⊢ Ⅎ 𝑘 𝑏 = 𝐵
99		fveq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
100	99	a1d	⊢ ( 𝑏 = 𝐵 → ( 𝑘 ∈ 𝐴 → ( 𝑏 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) ) )
101	98 100	ralrimi	⊢ ( 𝑏 = 𝐵 → ∀ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
102	101	sumeq2d	⊢ ( 𝑏 = 𝐵 → Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 ‘ 𝑘 ) )
103	102	fveq2d	⊢ ( 𝑏 = 𝐵 → ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ‘ 𝑘 ) ) )
104	99	fveq2d	⊢ ( 𝑏 = 𝐵 → ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) )
105	104	a1d	⊢ ( 𝑏 = 𝐵 → ( 𝑘 ∈ 𝐴 → ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
106	98 105	ralrimi	⊢ ( 𝑏 = 𝐵 → ∀ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) )
107	106	prodeq2d	⊢ ( 𝑏 = 𝐵 → ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) )
108	103 107	oveq12d	⊢ ( 𝑏 = 𝐵 → ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
109	108	eleq1d	⊢ ( 𝑏 = 𝐵 → ( ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ ) )
110	109	rspccva	⊢ ( ( ∀ 𝑏 ∈ ( ℕ₀ ↑_m 𝐴 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ∧ 𝐵 ∈ ( ℕ₀ ↑_m 𝐴 ) ) → ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )
111	96 3 110	syl2anc	⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )

Metamath Proof Explorer

Theorem mccl

Proof