Metamath Proof Explorer

Theorem mccllem

Description: * Induction step for mccl . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses mccllem.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
mccllem.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
mccllem.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 ∖ 𝐶 ) )
mccllem.b ⊢ ( 𝜑 → 𝐵 ∈ ( ℕ0 ↑m ( 𝐶 ∪ { 𝐷 } ) ) )
mccllem.6 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( ℕ0 ↑m 𝐶 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
Assertion mccllem ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 mccllem.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 mccllem.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3 mccllem.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 ∖ 𝐶 ) )
4 mccllem.b ⊢ ( 𝜑 → 𝐵 ∈ ( ℕ0 ↑m ( 𝐶 ∪ { 𝐷 } ) ) )
5 mccllem.6 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( ℕ0 ↑m 𝐶 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ )
6 nfv ⊢ Ⅎ 𝑘 𝜑
7 nfcv ⊢ Ⅎ 𝑘 ( ! ‘ ( 𝐵 ‘ 𝐷 ) )
8 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ∈ Fin )
9 1 2 8 syl2anc ⊢ ( 𝜑 → 𝐶 ∈ Fin )
10 eldifn ⊢ ( 𝐷 ∈ ( 𝐴 ∖ 𝐶 ) → ¬ 𝐷 ∈ 𝐶 )
11 3 10 syl ⊢ ( 𝜑 → ¬ 𝐷 ∈ 𝐶 )
12 elmapi ⊢ ( 𝐵 ∈ ( ℕ0 ↑m ( 𝐶 ∪ { 𝐷 } ) ) → 𝐵 : ( 𝐶 ∪ { 𝐷 } ) ⟶ ℕ0 )
13 4 12 syl ⊢ ( 𝜑 → 𝐵 : ( 𝐶 ∪ { 𝐷 } ) ⟶ ℕ0 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐵 : ( 𝐶 ∪ { 𝐷 } ) ⟶ ℕ0 )
15 elun1 ⊢ ( 𝑘 ∈ 𝐶 → 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) )
17 14 16 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℕ0 )
18 17 faccld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ∈ ℕ )
19 18 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ∈ ℂ )
20 2fveq3 ⊢ ( 𝑘 = 𝐷 → ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) = ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) )
21 snidg ⊢ ( 𝐷 ∈ ( 𝐴 ∖ 𝐶 ) → 𝐷 ∈ { 𝐷 } )
22 3 21 syl ⊢ ( 𝜑 → 𝐷 ∈ { 𝐷 } )
23 elun2 ⊢ ( 𝐷 ∈ { 𝐷 } → 𝐷 ∈ ( 𝐶 ∪ { 𝐷 } ) )
24 22 23 syl ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ∪ { 𝐷 } ) )
25 13 24 ffvelrnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐷 ) ∈ ℕ0 )
26 25 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ∈ ℕ )
27 26 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ∈ ℂ )
28 6 7 9 3 11 19 20 27 fprodsplitsn ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) = ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) )
29 28 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ) )
30 3 eldifad ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
31 snssi ⊢ ( 𝐷 ∈ 𝐴 → { 𝐷 } ⊆ 𝐴 )
32 30 31 syl ⊢ ( 𝜑 → { 𝐷 } ⊆ 𝐴 )
33 2 32 unssd ⊢ ( 𝜑 → ( 𝐶 ∪ { 𝐷 } ) ⊆ 𝐴 )
34 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐶 ∪ { 𝐷 } ) ⊆ 𝐴 ) → ( 𝐶 ∪ { 𝐷 } ) ∈ Fin )
35 1 33 34 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∪ { 𝐷 } ) ∈ Fin )
36 13 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℕ0 )
37 35 36 fsumnn0cl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ∈ ℕ0 )
38 37 faccld ⊢ ( 𝜑 → ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) ∈ ℕ )
39 38 nncnd ⊢ ( 𝜑 → ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) ∈ ℂ )
40 6 9 19 fprodclf ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ∈ ℂ )
41 40 27 mulcld ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ∈ ℂ )
42 18 nnne0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ≠ 0 )
43 9 19 42 fprodn0 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ≠ 0 )
44 26 nnne0d ⊢ ( 𝜑 → ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ≠ 0 )
45 40 27 43 44 mulne0d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ≠ 0 )
46 39 41 45 divcld ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ) ∈ ℂ )
47 46 mulid2d ⊢ ( 𝜑 → ( 1 · ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ) )
48 47 eqcomd ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ) = ( 1 · ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ) ) )
49 9 17 fsumnn0cl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ℕ0 )
50 49 faccld ⊢ ( 𝜑 → ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ∈ ℕ )
51 50 nncnd ⊢ ( 𝜑 → ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ∈ ℂ )
52 nnne0 ⊢ ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ∈ ℕ → ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ≠ 0 )
53 50 52 syl ⊢ ( 𝜑 → ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ≠ 0 )
54 51 53 dividd ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) = 1 )
55 54 eqcomd ⊢ ( 𝜑 → 1 = ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) )
56 40 27 mulcomd ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) = ( ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) · ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
57 56 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) · ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) )
58 39 27 40 44 43 divdiv1d ⊢ ( 𝜑 → ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) · ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) )
59 58 eqcomd ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) · ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) = ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
60 57 59 eqtrd ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ) = ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
61 55 60 oveq12d ⊢ ( 𝜑 → ( 1 · ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ) ) = ( ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) )
62 39 27 44 divcld ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ∈ ℂ )
63 51 51 62 40 53 43 divmul13d ⊢ ( 𝜑 → ( ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) = ( ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) )
64 61 63 eqtrd ⊢ ( 𝜑 → ( 1 · ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) · ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) ) ) = ( ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) )
65 29 48 64 3eqtrd ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) = ( ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) )
66 39 27 51 44 53 divdiv1d ⊢ ( 𝜑 → ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ) )
67 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 )
68 17 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℂ )
69 csbeq1a ⊢ ( 𝑘 = 𝐷 → ( 𝐵 ‘ 𝑘 ) = ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) )
70 csbfv ⊢ ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝐷 )
71 70 a1i ⊢ ( 𝜑 → ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝐷 ) )
72 25 nn0cnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐷 ) ∈ ℂ )
73 71 72 eqeltrd ⊢ ( 𝜑 → ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ∈ ℂ )
74 6 67 9 30 11 68 69 73 fsumsplitsn ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) = ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) + ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ) )
75 74 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) = ( ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) + ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) )
76 49 nn0cnd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ℂ )
77 76 73 pncan2d ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) + ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) = ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) )
78 75 77 71 3eqtrrd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐷 ) = ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) )
79 78 fveq2d ⊢ ( 𝜑 → ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) = ( ! ‘ ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) )
80 79 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) = ( ( ! ‘ ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) )
81 80 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ) )
82 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
83 37 nn0zd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ∈ ℤ )
84 49 nn0zd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ℤ )
85 82 83 84 3jca ⊢ ( 𝜑 → ( 0 ∈ ℤ ∧ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ∈ ℤ ∧ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ℤ ) )
86 49 nn0ge0d ⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) )
87 25 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐵 ‘ 𝐷 ) )
88 71 eqcomd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐷 ) = ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) )
89 87 88 breqtrd ⊢ ( 𝜑 → 0 ≤ ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) )
90 49 nn0red ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
91 25 nn0red ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐷 ) ∈ ℝ )
92 71 91 eqeltrd ⊢ ( 𝜑 → ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
93 90 92 addge01d ⊢ ( 𝜑 → ( 0 ≤ ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ↔ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ≤ ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) + ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ) ) )
94 89 93 mpbid ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ≤ ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) + ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ) )
95 74 eqcomd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) + ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) )
96 94 95 breqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) )
97 85 86 96 jca32 ⊢ ( 𝜑 → ( ( 0 ∈ ℤ ∧ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ∈ ℤ ∧ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ℤ ) ∧ ( 0 ≤ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∧ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) ) )
98 elfz2 ⊢ ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ( 0 ... Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) ↔ ( ( 0 ∈ ℤ ∧ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ∈ ℤ ∧ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ℤ ) ∧ ( 0 ≤ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∧ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) ) )
99 97 98 sylibr ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ( 0 ... Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) )
100 bcval2 ⊢ ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ( 0 ... Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) → ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ) )
101 99 100 syl ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ) )
102 101 eqcomd ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) )
103 66 81 102 3eqtrd ⊢ ( 𝜑 → ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) )
104 bccl2 ⊢ ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ( 0 ... Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) → ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ∈ ℕ )
105 99 104 syl ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ∈ ℕ )
106 103 105 eqeltrd ⊢ ( 𝜑 → ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )
107 ssun1 ⊢ 𝐶 ⊆ ( 𝐶 ∪ { 𝐷 } )
108 107 a1i ⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐶 ∪ { 𝐷 } ) )
109 elmapssres ⊢ ( ( 𝐵 ∈ ( ℕ0 ↑m ( 𝐶 ∪ { 𝐷 } ) ) ∧ 𝐶 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) → ( 𝐵 ↾ 𝐶 ) ∈ ( ℕ0 ↑m 𝐶 ) )
110 4 108 109 syl2anc ⊢ ( 𝜑 → ( 𝐵 ↾ 𝐶 ) ∈ ( ℕ0 ↑m 𝐶 ) )
111 fveq1 ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → ( 𝑏 ‘ 𝑘 ) = ( ( 𝐵 ↾ 𝐶 ) ‘ 𝑘 ) )
112 111 adantr ⊢ ( ( 𝑏 = ( 𝐵 ↾ 𝐶 ) ∧ 𝑘 ∈ 𝐶 ) → ( 𝑏 ‘ 𝑘 ) = ( ( 𝐵 ↾ 𝐶 ) ‘ 𝑘 ) )
113 fvres ⊢ ( 𝑘 ∈ 𝐶 → ( ( 𝐵 ↾ 𝐶 ) ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
114 113 adantl ⊢ ( ( 𝑏 = ( 𝐵 ↾ 𝐶 ) ∧ 𝑘 ∈ 𝐶 ) → ( ( 𝐵 ↾ 𝐶 ) ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
115 112 114 eqtrd ⊢ ( ( 𝑏 = ( 𝐵 ↾ 𝐶 ) ∧ 𝑘 ∈ 𝐶 ) → ( 𝑏 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
116 115 sumeq2dv ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) )
117 116 fveq2d ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) )
118 115 fveq2d ⊢ ( ( 𝑏 = ( 𝐵 ↾ 𝐶 ) ∧ 𝑘 ∈ 𝐶 ) → ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) )
119 118 prodeq2dv ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) )
120 117 119 oveq12d ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
121 120 eleq1d ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → ( ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ ) )
122 121 rspccva ⊢ ( ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝐶 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ∧ ( 𝐵 ↾ 𝐶 ) ∈ ( ℕ0 ↑m 𝐶 ) ) → ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )
123 5 110 122 syl2anc ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )
124 106 123 nnmulcld ⊢ ( 𝜑 → ( ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) ∈ ℕ )
125 65 124 eqeltrd ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )