# Metamath Proof Explorer

## Theorem ply1mulgsumlem1

Description: Lemma 1 for ply1mulgsum . (Contributed by AV, 19-Oct-2019)

Ref Expression
Hypotheses ply1mulgsum.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
ply1mulgsum.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
ply1mulgsum.a ${⊢}{A}={\mathrm{coe}}_{1}\left({K}\right)$
ply1mulgsum.c ${⊢}{C}={\mathrm{coe}}_{1}\left({L}\right)$
ply1mulgsum.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
ply1mulgsum.pm
ply1mulgsum.sm
ply1mulgsum.rm
ply1mulgsum.m ${⊢}{M}={\mathrm{mulGrp}}_{{P}}$
ply1mulgsum.e
Assertion ply1mulgsumlem1 ${⊢}\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ply1mulgsum.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 ply1mulgsum.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
3 ply1mulgsum.a ${⊢}{A}={\mathrm{coe}}_{1}\left({K}\right)$
4 ply1mulgsum.c ${⊢}{C}={\mathrm{coe}}_{1}\left({L}\right)$
5 ply1mulgsum.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
6 ply1mulgsum.pm
7 ply1mulgsum.sm
8 ply1mulgsum.rm
9 ply1mulgsum.m ${⊢}{M}={\mathrm{mulGrp}}_{{P}}$
10 ply1mulgsum.e
11 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
12 3 2 1 11 coe1ae0 ${⊢}{K}\in {B}\to \exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)$
13 12 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)$
14 4 2 1 11 coe1ae0 ${⊢}{L}\in {B}\to \exists {a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)$
15 14 3ad2ant3 ${⊢}\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \exists {a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)$
16 nn0addcl ${⊢}\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\to {a}+{b}\in {ℕ}_{0}$
17 16 adantr ${⊢}\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\to {a}+{b}\in {ℕ}_{0}$
18 17 adantr ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\right)\to {a}+{b}\in {ℕ}_{0}$
19 breq1 ${⊢}{s}={a}+{b}\to \left({s}<{n}↔{a}+{b}<{n}\right)$
20 19 imbi1d ${⊢}{s}={a}+{b}\to \left(\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)↔\left({a}+{b}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)$
21 20 ralbidv ${⊢}{s}={a}+{b}\to \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)↔\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}+{b}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)$
22 21 adantl ${⊢}\left(\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\right)\wedge {s}={a}+{b}\right)\to \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)↔\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}+{b}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)$
23 r19.26 ${⊢}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)↔\left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)$
24 nn0cn ${⊢}{a}\in {ℕ}_{0}\to {a}\in ℂ$
25 24 adantl ${⊢}\left({b}\in {ℕ}_{0}\wedge {a}\in {ℕ}_{0}\right)\to {a}\in ℂ$
26 nn0cn ${⊢}{b}\in {ℕ}_{0}\to {b}\in ℂ$
27 26 adantr ${⊢}\left({b}\in {ℕ}_{0}\wedge {a}\in {ℕ}_{0}\right)\to {b}\in ℂ$
28 25 27 addcomd ${⊢}\left({b}\in {ℕ}_{0}\wedge {a}\in {ℕ}_{0}\right)\to {a}+{b}={b}+{a}$
29 28 3adant3 ${⊢}\left({b}\in {ℕ}_{0}\wedge {a}\in {ℕ}_{0}\wedge {n}\in {ℕ}_{0}\right)\to {a}+{b}={b}+{a}$
30 29 breq1d ${⊢}\left({b}\in {ℕ}_{0}\wedge {a}\in {ℕ}_{0}\wedge {n}\in {ℕ}_{0}\right)\to \left({a}+{b}<{n}↔{b}+{a}<{n}\right)$
31 nn0sumltlt ${⊢}\left({b}\in {ℕ}_{0}\wedge {a}\in {ℕ}_{0}\wedge {n}\in {ℕ}_{0}\right)\to \left({b}+{a}<{n}\to {a}<{n}\right)$
32 30 31 sylbid ${⊢}\left({b}\in {ℕ}_{0}\wedge {a}\in {ℕ}_{0}\wedge {n}\in {ℕ}_{0}\right)\to \left({a}+{b}<{n}\to {a}<{n}\right)$
33 32 3expia ${⊢}\left({b}\in {ℕ}_{0}\wedge {a}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}\to \left({a}+{b}<{n}\to {a}<{n}\right)\right)$
34 33 ancoms ${⊢}\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}\to \left({a}+{b}<{n}\to {a}<{n}\right)\right)$
35 34 adantr ${⊢}\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\to \left({n}\in {ℕ}_{0}\to \left({a}+{b}<{n}\to {a}<{n}\right)\right)$
36 35 imp ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({a}+{b}<{n}\to {a}<{n}\right)$
37 36 imim1d ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left(\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\to \left({a}+{b}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\right)$
38 37 com23 ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({a}+{b}<{n}\to \left(\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\to {C}\left({n}\right)={0}_{{R}}\right)\right)$
39 38 imp ${⊢}\left(\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {a}+{b}<{n}\right)\to \left(\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\to {C}\left({n}\right)={0}_{{R}}\right)$
40 nn0sumltlt ${⊢}\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\wedge {n}\in {ℕ}_{0}\right)\to \left({a}+{b}<{n}\to {b}<{n}\right)$
41 40 3expia ${⊢}\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}\to \left({a}+{b}<{n}\to {b}<{n}\right)\right)$
42 41 adantr ${⊢}\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\to \left({n}\in {ℕ}_{0}\to \left({a}+{b}<{n}\to {b}<{n}\right)\right)$
43 42 imp ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({a}+{b}<{n}\to {b}<{n}\right)$
44 43 imim1d ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left(\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to \left({a}+{b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)$
45 44 com23 ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({a}+{b}<{n}\to \left(\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to {A}\left({n}\right)={0}_{{R}}\right)\right)$
46 45 imp ${⊢}\left(\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {a}+{b}<{n}\right)\to \left(\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to {A}\left({n}\right)={0}_{{R}}\right)$
47 39 46 anim12d ${⊢}\left(\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {a}+{b}<{n}\right)\to \left(\left(\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\to \left({C}\left({n}\right)={0}_{{R}}\wedge {A}\left({n}\right)={0}_{{R}}\right)\right)$
48 47 imp ${⊢}\left(\left(\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {a}+{b}<{n}\right)\wedge \left(\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\right)\to \left({C}\left({n}\right)={0}_{{R}}\wedge {A}\left({n}\right)={0}_{{R}}\right)$
49 48 ancomd ${⊢}\left(\left(\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge {a}+{b}<{n}\right)\wedge \left(\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\right)\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)$
50 49 exp31 ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({a}+{b}<{n}\to \left(\left(\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)$
51 50 com23 ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left(\left(\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\to \left({a}+{b}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)$
52 51 ralimdva ${⊢}\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\to \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\to \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}+{b}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)$
53 23 52 syl5bir ${⊢}\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\to \left(\left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\to \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}+{b}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)$
54 53 imp ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\right)\to \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}+{b}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)$
55 18 22 54 rspcedvd ${⊢}\left(\left(\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\wedge \left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\right)\wedge \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)$
56 55 exp31 ${⊢}\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\to \left(\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \left(\left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)\right)$
57 56 com23 ${⊢}\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\to \left(\left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\to \left(\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)\right)$
58 57 expd ${⊢}\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\to \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\to \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to \left(\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)\right)\right)$
59 58 com34 ${⊢}\left({a}\in {ℕ}_{0}\wedge {b}\in {ℕ}_{0}\right)\to \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\to \left(\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)\right)\right)$
60 59 impancom ${⊢}\left({a}\in {ℕ}_{0}\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\right)\to \left({b}\in {ℕ}_{0}\to \left(\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)\right)\right)$
61 60 com14 ${⊢}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to \left({b}\in {ℕ}_{0}\to \left(\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \left(\left({a}\in {ℕ}_{0}\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)\right)\right)$
62 61 impcom ${⊢}\left({b}\in {ℕ}_{0}\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\right)\to \left(\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \left(\left({a}\in {ℕ}_{0}\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)\right)$
63 62 rexlimiva ${⊢}\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to \left(\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \left(\left({a}\in {ℕ}_{0}\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)\right)$
64 63 com13 ${⊢}\left({a}\in {ℕ}_{0}\wedge \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\right)\to \left(\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \left(\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)\right)$
65 64 rexlimiva ${⊢}\exists {a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}<{n}\to {C}\left({n}\right)={0}_{{R}}\right)\to \left(\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \left(\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)\right)$
66 15 65 mpcom ${⊢}\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \left(\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({b}<{n}\to {A}\left({n}\right)={0}_{{R}}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)\right)$
67 13 66 mpd ${⊢}\left({R}\in \mathrm{Ring}\wedge {K}\in {B}\wedge {L}\in {B}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \left({A}\left({n}\right)={0}_{{R}}\wedge {C}\left({n}\right)={0}_{{R}}\right)\right)$