Theorem ply1mulgsumlem1

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

	Ref	Expression
Hypotheses	ply1mulgsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1mulgsum.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1mulgsum.a	⊢ 𝐴 = ( coe1 ‘ 𝐾 )
	ply1mulgsum.c	⊢ 𝐶 = ( coe1 ‘ 𝐿 )
	ply1mulgsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	ply1mulgsum.pm	⊢ × = ( .r ‘ 𝑃 )
	ply1mulgsum.sm	⊢ · = ( ·𝑠 ‘ 𝑃 )
	ply1mulgsum.rm	⊢ ∗ = ( .r ‘ 𝑅 )
	ply1mulgsum.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
	ply1mulgsum.e	⊢ ↑ = ( .g ‘ 𝑀 )
Assertion	ply1mulgsumlem1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1mulgsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1mulgsum.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		ply1mulgsum.a	⊢ 𝐴 = ( coe1 ‘ 𝐾 )
4		ply1mulgsum.c	⊢ 𝐶 = ( coe1 ‘ 𝐿 )
5		ply1mulgsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
6		ply1mulgsum.pm	⊢ × = ( .r ‘ 𝑃 )
7		ply1mulgsum.sm	⊢ · = ( ·𝑠 ‘ 𝑃 )
8		ply1mulgsum.rm	⊢ ∗ = ( .r ‘ 𝑅 )
9		ply1mulgsum.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
10		ply1mulgsum.e	⊢ ↑ = ( .g ‘ 𝑀 )
11		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
12	3 2 1 11	coe1ae0	⊢ ( 𝐾 ∈ 𝐵 → ∃ 𝑏 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
13	12	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑏 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
14	4 2 1 11	coe1ae0	⊢ ( 𝐿 ∈ 𝐵 → ∃ 𝑎 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
15	14	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑎 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
16		nn0addcl	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑎 + 𝑏 ) ∈ ℕ0 )
17	16	adantr	⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) → ( 𝑎 + 𝑏 ) ∈ ℕ0 )
18	17	adantr	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ ( ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑎 + 𝑏 ) ∈ ℕ0 )
19		breq1	⊢ ( 𝑠 = ( 𝑎 + 𝑏 ) → ( 𝑠 < 𝑛 ↔ ( 𝑎 + 𝑏 ) < 𝑛 ) )
20	19	imbi1d	⊢ ( 𝑠 = ( 𝑎 + 𝑏 ) → ( ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ↔ ( ( 𝑎 + 𝑏 ) < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) )
21	20	ralbidv	⊢ ( 𝑠 = ( 𝑎 + 𝑏 ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( 𝑎 + 𝑏 ) < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) )
22	21	adantl	⊢ ( ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ ( ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ 𝑠 = ( 𝑎 + 𝑏 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( 𝑎 + 𝑏 ) < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) )
23		r19.26	⊢ ( ∀ 𝑛 ∈ ℕ0 ( ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ↔ ( ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) )
24		nn0cn	⊢ ( 𝑎 ∈ ℕ0 → 𝑎 ∈ ℂ )
25	24	adantl	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝑎 ∈ ℕ0 ) → 𝑎 ∈ ℂ )
26		nn0cn	⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℂ )
27	26	adantr	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝑎 ∈ ℕ0 ) → 𝑏 ∈ ℂ )
28	25 27	addcomd	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝑎 ∈ ℕ0 ) → ( 𝑎 + 𝑏 ) = ( 𝑏 + 𝑎 ) )
29	28	3adant3	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝑎 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑎 + 𝑏 ) = ( 𝑏 + 𝑎 ) )
30	29	breq1d	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝑎 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑛 ↔ ( 𝑏 + 𝑎 ) < 𝑛 ) )
31		nn0sumltlt	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝑎 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑏 + 𝑎 ) < 𝑛 → 𝑎 < 𝑛 ) )
32	30 31	sylbid	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝑎 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑛 → 𝑎 < 𝑛 ) )
33	32	3expia	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝑎 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 + 𝑏 ) < 𝑛 → 𝑎 < 𝑛 ) ) )
34	33	ancoms	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 + 𝑏 ) < 𝑛 → 𝑎 < 𝑛 ) ) )
35	34	adantr	⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 + 𝑏 ) < 𝑛 → 𝑎 < 𝑛 ) ) )
36	35	imp	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑛 → 𝑎 < 𝑛 ) )
37	36	imim1d	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑎 + 𝑏 ) < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) )
38	37	com23	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑛 → ( ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) )
39	38	imp	⊢ ( ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 + 𝑏 ) < 𝑛 ) → ( ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
40		nn0sumltlt	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑛 → 𝑏 < 𝑛 ) )
41	40	3expia	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 + 𝑏 ) < 𝑛 → 𝑏 < 𝑛 ) ) )
42	41	adantr	⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 + 𝑏 ) < 𝑛 → 𝑏 < 𝑛 ) ) )
43	42	imp	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑛 → 𝑏 < 𝑛 ) )
44	43	imim1d	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑎 + 𝑏 ) < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) )
45	44	com23	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑛 → ( ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) )
46	45	imp	⊢ ( ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 + 𝑏 ) < 𝑛 ) → ( ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
47	39 46	anim12d	⊢ ( ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 + 𝑏 ) < 𝑛 ) → ( ( ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) )
48	47	imp	⊢ ( ( ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 + 𝑏 ) < 𝑛 ) ∧ ( ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
49	48	ancomd	⊢ ( ( ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑎 + 𝑏 ) < 𝑛 ) ∧ ( ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
50	49	exp31	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑛 → ( ( ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) )
51	50	com23	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ( ( 𝑎 + 𝑏 ) < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) )
52	51	ralimdva	⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ∀ 𝑛 ∈ ℕ0 ( ( 𝑎 + 𝑏 ) < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) )
53	23 52	syl5bir	⊢ ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) → ( ( ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ∀ 𝑛 ∈ ℕ0 ( ( 𝑎 + 𝑏 ) < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) )
54	53	imp	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ ( ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) → ∀ 𝑛 ∈ ℕ0 ( ( 𝑎 + 𝑏 ) < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) )
55	18 22 54	rspcedvd	⊢ ( ( ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ ( ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) )
56	55	exp31	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ( ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ) )
57	56	com23	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( ( ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ) )
58	57	expd	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ) ) )
59	58	com34	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ) ) )
60	59	impancom	⊢ ( ( 𝑎 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑏 ∈ ℕ0 → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ) ) )
61	60	com14	⊢ ( ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑏 ∈ ℕ0 → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ( 𝑎 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ) ) )
62	61	impcom	⊢ ( ( 𝑏 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ( 𝑎 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ) )
63	62	rexlimiva	⊢ ( ∃ 𝑏 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ( 𝑎 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ) )
64	63	com13	⊢ ( ( 𝑎 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∃ 𝑏 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ) )
65	64	rexlimiva	⊢ ( ∃ 𝑎 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑎 < 𝑛 → ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∃ 𝑏 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) ) )
66	15 65	mpcom	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∃ 𝑏 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑏 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) ) )
67	13 66	mpd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝐴 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ) )