Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐵 ∈ ( ℕ0 ↑m 𝐴 ) )
Assertion mccl ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 mccl.kb ⊢ Ⅎ 𝑘 𝐵
2 mccl.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 mccl.b ⊢ ( 𝜑 → 𝐵 ∈ ( ℕ0 ↑m 𝐴 ) )
4 sumeq1 ⊢ ( 𝑎 = ∅ → Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) )
5 4 fveq2d ⊢ ( 𝑎 = ∅ → ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) )
6 prodeq1 ⊢ ( 𝑎 = ∅ → ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) )
7 5 6 oveq12d ⊢ ( 𝑎 = ∅ → ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) )
8 7 eleq1d ⊢ ( 𝑎 = ∅ → ( ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
9 8 ralbidv ⊢ ( 𝑎 = ∅ → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
10 oveq2 ⊢ ( 𝑎 = ∅ → ( ℕ0 ↑m 𝑎 ) = ( ℕ0 ↑m ∅ ) )
11 10 raleqdv ⊢ ( 𝑎 = ∅ → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m ∅ ) ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
12 9 11 bitrd ⊢ ( 𝑎 = ∅ → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m ∅ ) ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
13 sumeq1 ⊢ ( 𝑎 = 𝑐 → Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) )
14 13 fveq2d ⊢ ( 𝑎 = 𝑐 → ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) )
15 prodeq1 ⊢ ( 𝑎 = 𝑐 → ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) )
16 14 15 oveq12d ⊢ ( 𝑎 = 𝑐 → ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) )
17 16 eleq1d ⊢ ( 𝑎 = 𝑐 → ( ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
18 17 ralbidv ⊢ ( 𝑎 = 𝑐 → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
19 oveq2 ⊢ ( 𝑎 = 𝑐 → ( ℕ0 ↑m 𝑎 ) = ( ℕ0 ↑m 𝑐 ) )
20 19 raleqdv ⊢ ( 𝑎 = 𝑐 → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
21 18 20 bitrd ⊢ ( 𝑎 = 𝑐 → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
22 sumeq1 ⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) )
23 22 fveq2d ⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) )
24 prodeq1 ⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) )
25 23 24 oveq12d ⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) )
26 25 eleq1d ⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
27 26 ralbidv ⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
28 oveq2 ⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ℕ0 ↑m 𝑎 ) = ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) )
29 28 raleqdv ⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
30 27 29 bitrd ⊢ ( 𝑎 = ( 𝑐 ∪ { 𝑑 } ) → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
31 sumeq1 ⊢ ( 𝑎 = 𝐴 → Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) )
32 31 fveq2d ⊢ ( 𝑎 = 𝐴 → ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) )
33 prodeq1 ⊢ ( 𝑎 = 𝐴 → ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) )
34 32 33 oveq12d ⊢ ( 𝑎 = 𝐴 → ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) )
35 34 eleq1d ⊢ ( 𝑎 = 𝐴 → ( ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
36 35 ralbidv ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
37 oveq2 ⊢ ( 𝑎 = 𝐴 → ( ℕ0 ↑m 𝑎 ) = ( ℕ0 ↑m 𝐴 ) )
38 37 raleqdv ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝐴 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
39 36 38 bitrd ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑎 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑎 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑎 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑏 ∈ ( ℕ0 ↑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 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( ℕ0 ↑m ∅ ) ) → ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
51 50 ralrimiva ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( ℕ0 ↑m ∅ ) ( ( ! ‘ Σ 𝑘 ∈ ∅ ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ∅ ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
52 nfv ⊢ Ⅎ 𝑏 ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) )
53 nfra1 ⊢ Ⅎ 𝑏 ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ
54 52 53 nfan ⊢ Ⅎ 𝑏 ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
55 simpll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ0 ↑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 ⊢ ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ )
72 71 biimpi ⊢ ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ → ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ )
73 72 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ) → ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ )
74 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ) → 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) )
75 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ) → 𝐴 ∈ Fin )
76 simprl ⊢ ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) → 𝑐 ⊆ 𝐴 )
77 76 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ) → 𝑐 ⊆ 𝐴 )
78 simprr ⊢ ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) → 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) )
79 78 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ) → 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) )
80 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ) → 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) )
81 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑒 ‘ 𝑗 ) = ( 𝑒 ‘ 𝑘 ) )
82 81 cbvsumv ⊢ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) = Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 )
83 82 fveq2i ⊢ ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) = ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) )
84 2fveq3 ⊢ ( 𝑗 = 𝑘 → ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) = ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) )
85 84 cbvprodv ⊢ ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) = ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) )
86 83 85 oveq12i ⊢ ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) )
87 86 eleq1i ⊢ ( ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) ) ∈ ℕ )
88 87 ralbii ⊢ ( ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ↔ ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) ) ∈ ℕ )
89 88 biimpi ⊢ ( ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ → ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) ) ∈ ℕ )
90 89 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ) → ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑒 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑘 ) ) ) ∈ ℕ )
91 75 77 79 80 90 mccllem ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑒 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑗 ∈ 𝑐 ( 𝑒 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ 𝑐 ( ! ‘ ( 𝑒 ‘ 𝑗 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ) → ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
92 55 73 74 91 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) ∧ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ) → ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
93 92 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) → ( 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) → ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
94 54 93 ralrimi ⊢ ( ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) ∧ ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) → ∀ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
95 94 ex ⊢ ( ( 𝜑 ∧ ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ∈ ( 𝐴 ∖ 𝑐 ) ) ) → ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝑐 ) ( ( ! ‘ Σ 𝑘 ∈ 𝑐 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝑐 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ → ∀ 𝑏 ∈ ( ℕ0 ↑m ( 𝑐 ∪ { 𝑑 } ) ) ( ( ! ‘ Σ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝑐 ∪ { 𝑑 } ) ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ) )
96 12 21 30 39 51 95 2 findcard2d ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( ℕ0 ↑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 ⊢ ( ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝐴 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ∧ 𝐵 ∈ ( ℕ0 ↑m 𝐴 ) ) → ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )
111 96 3 110 syl2anc ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐴 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )