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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℕ0 )
18	17	faccld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ∈ ℕ )
19	18	nncnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ∈ ℂ )
20		2fveq3	⊢ ( 𝑘 = 𝐷 → ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) = ( ! ‘ ( 𝐵 ‘ 𝐷 ) ) )
21		snidg	⊢ ( 𝐷 ∈ ( 𝐴 ∖ 𝐶 ) → 𝐷 ∈ { 𝐷 } )
22	3 21	syl	⊢ ( 𝜑 → 𝐷 ∈ { 𝐷 } )
23		elun2	⊢ ( 𝐷 ∈ { 𝐷 } → 𝐷 ∈ ( 𝐶 ∪ { 𝐷 } ) )
24	22 23	syl	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ∪ { 𝐷 } ) )
25	13 24	ffvelcdmd	⊢ ( 𝜑 → ( 𝐵 ‘ 𝐷 ) ∈ ℕ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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℕ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	mullidd	⊢ ( 𝜑 → ( 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	⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( 𝐵 ‘ 𝑘 ) ) / ∏ 𝑘 ∈ ( 𝐶 ∪ { 𝐷 } ) ( ! ‘ ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℕ )