Metamath Proof Explorer


Theorem mccllem

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

Ref Expression
Hypotheses mccllem.a φ A Fin
mccllem.c φ C A
mccllem.d φ D A C
mccllem.b φ B 0 C D
mccllem.6 φ b 0 C k C b k ! k C b k !
Assertion mccllem φ k C D B k ! k C D B k !

Proof

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