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 49 nn0ge0d ⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) )
86 25 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐵 ‘ 𝐷 ) )
87 71 eqcomd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐷 ) = ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) )
88 86 87 breqtrd ⊢ ( 𝜑 → 0 ≤ ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) )
89 49 nn0red ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
90 25 nn0red ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐷 ) ∈ ℝ )
91 71 90 eqeltrd ⊢ ( 𝜑 → ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
92 89 91 addge01d ⊢ ( 𝜑 → ( 0 ≤ ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ↔ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ≤ ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) + ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ) ) )
93 88 92 mpbid ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ≤ ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) + ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ) )
94 74 eqcomd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) + ⦋ 𝐷 / 𝑘 ⦌ ( 𝐵 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) )
95 93 94 breqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) )
96 82 83 84 85 95 elfzd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ( 0 ... Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) )
97 bcval2 ⊢ ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ( 0 ... Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) → ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ) )
98 96 97 syl ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) = ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ) )
99 98 eqcomd ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ( ! ‘ ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) )
100 66 81 99 3eqtrd ⊢ ( 𝜑 → ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) )
101 bccl2 ⊢ ( Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ∈ ( 0 ... Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) → ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ∈ ℕ )
102 96 101 syl ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) C Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ∈ ℕ )
103 100 102 eqeltrd ⊢ ( 𝜑 → ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )
104 ssun1 ⊢ 𝐶 ⊆ ( 𝐶 ∪ { 𝐷 } )
105 104 a1i ⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐶 ∪ { 𝐷 } ) )
106 elmapssres ⊢ ( ( 𝐵 ∈ ( ℕ0 ↑m ( 𝐶 ∪ { 𝐷 } ) ) ∧ 𝐶 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) → ( 𝐵 ↾ 𝐶 ) ∈ ( ℕ0 ↑m 𝐶 ) )
107 4 105 106 syl2anc ⊢ ( 𝜑 → ( 𝐵 ↾ 𝐶 ) ∈ ( ℕ0 ↑m 𝐶 ) )
108 fveq1 ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → ( 𝑏 ‘ 𝑘 ) = ( ( 𝐵 ↾ 𝐶 ) ‘ 𝑘 ) )
109 108 adantr ⊢ ( ( 𝑏 = ( 𝐵 ↾ 𝐶 ) ∧ 𝑘 ∈ 𝐶 ) → ( 𝑏 ‘ 𝑘 ) = ( ( 𝐵 ↾ 𝐶 ) ‘ 𝑘 ) )
110 fvres ⊢ ( 𝑘 ∈ 𝐶 → ( ( 𝐵 ↾ 𝐶 ) ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
111 110 adantl ⊢ ( ( 𝑏 = ( 𝐵 ↾ 𝐶 ) ∧ 𝑘 ∈ 𝐶 ) → ( ( 𝐵 ↾ 𝐶 ) ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
112 109 111 eqtrd ⊢ ( ( 𝑏 = ( 𝐵 ↾ 𝐶 ) ∧ 𝑘 ∈ 𝐶 ) → ( 𝑏 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
113 112 sumeq2dv ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) )
114 113 fveq2d ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) )
115 112 fveq2d ⊢ ( ( 𝑏 = ( 𝐵 ↾ 𝐶 ) ∧ 𝑘 ∈ 𝐶 ) → ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) )
116 115 prodeq2dv ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) )
117 114 116 oveq12d ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) = ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
118 117 eleq1d ⊢ ( 𝑏 = ( 𝐵 ↾ 𝐶 ) → ( ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ↔ ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ ) )
119 118 rspccva ⊢ ( ( ∀ 𝑏 ∈ ( ℕ0 ↑m 𝐶 ) ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝑏 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝑏 ‘ 𝑘 ) ) ) ∈ ℕ ∧ ( 𝐵 ↾ 𝐶 ) ∈ ( ℕ0 ↑m 𝐶 ) ) → ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )
120 5 107 119 syl2anc ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )
121 103 120 nnmulcld ⊢ ( 𝜑 → ( ( ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) ) / ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) ) · ( ( ! ‘ Σ 𝑘 ∈ 𝐶 ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ 𝐶 ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) ∈ ℕ )
122 65 121 eqeltrd ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )