abelthlem5

	Ref	Expression
Hypotheses	abelth.1	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	abelth.2	$⊢ φ \to seq 0 (+ A) \in dom ⇝$
	abelth.3	$⊢ φ \to M \in ℝ$
	abelth.4	$⊢ φ \to 0 \leq M$
	abelth.5	$⊢ S = \{z \in ℂ \| \|1 - z\| \leq M (1 - \|z\|)\}$
	abelth.6	$⊢ F = (x \in S ⟼ \sum_{n \in ℕ_{0}} A (n) x^{n})$
	abelth.7	$⊢ φ \to seq 0 (+ A) ⇝ 0$
Assertion	abelthlem5	$⊢ (φ \land X \in (0 ball (abs \circ -) 1)) \to seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		abelth.1	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
2		abelth.2	$⊢ φ \to seq 0 (+ A) \in dom ⇝$
3		abelth.3	$⊢ φ \to M \in ℝ$
4		abelth.4	$⊢ φ \to 0 \leq M$
5		abelth.5	$⊢ S = \{z \in ℂ \| \|1 - z\| \leq M (1 - \|z\|)\}$
6		abelth.6	$⊢ F = (x \in S ⟼ \sum_{n \in ℕ_{0}} A (n) x^{n})$
7		abelth.7	$⊢ φ \to seq 0 (+ A) ⇝ 0$
8		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9		0zd	$⊢ φ \to 0 \in ℤ$
10		1rp	$⊢ 1 \in ℝ^{+}$
11	10	a1i	$⊢ φ \to 1 \in ℝ^{+}$
12		eqidd	$⊢ (φ \land m \in ℕ_{0}) \to seq 0 (+ A) (m) = seq 0 (+ A) (m)$
13	8 9 11 12 7	climi0	$⊢ φ \to \exists j \in ℕ_{0} \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1$
14	13	adantr	$⊢ (φ \land X \in (0 ball (abs \circ -) 1)) \to \exists j \in ℕ_{0} \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1$
15		simprl	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to j \in ℕ_{0}$
16		oveq2	$⊢ n = i \to {\|X\|}^{n} = {\|X\|}^{i}$
17		eqid	$⊢ (n \in ℕ_{0} ⟼ {\|X\|}^{n}) = (n \in ℕ_{0} ⟼ {\|X\|}^{n})$
18		ovex	$⊢ {\|X\|}^{i} \in V$
19	16 17 18	fvmpt	$⊢ i \in ℕ_{0} \to (n \in ℕ_{0} ⟼ {\|X\|}^{n}) (i) = {\|X\|}^{i}$
20	19	adantl	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ {\|X\|}^{n}) (i) = {\|X\|}^{i}$
21		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
22		0cn	$⊢ 0 \in ℂ$
23		1xr	$⊢ 1 \in ℝ^{*}$
24		blssm	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land 1 \in ℝ^{*}) \to 0 ball (abs \circ -) 1 \subseteq ℂ$
25	21 22 23 24	mp3an	$⊢ 0 ball (abs \circ -) 1 \subseteq ℂ$
26		simplr	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to X \in (0 ball (abs \circ -) 1)$
27	25 26	sselid	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to X \in ℂ$
28	27	abscld	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to \|X\| \in ℝ$
29		reexpcl	$⊢ (\|X\| \in ℝ \land i \in ℕ_{0}) \to {\|X\|}^{i} \in ℝ$
30	28 29	sylan	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℕ_{0}) \to {\|X\|}^{i} \in ℝ$
31	20 30	eqeltrd	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ {\|X\|}^{n}) (i) \in ℝ$
32		fveq2	$⊢ k = i \to seq 0 (+ A) (k) = seq 0 (+ A) (i)$
33		oveq2	$⊢ k = i \to X^{k} = X^{i}$
34	32 33	oveq12d	$⊢ k = i \to seq 0 (+ A) (k) X^{k} = seq 0 (+ A) (i) X^{i}$
35		eqid	$⊢ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) = (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})$
36		ovex	$⊢ seq 0 (+ A) (i) X^{i} \in V$
37	34 35 36	fvmpt	$⊢ i \in ℕ_{0} \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i) = seq 0 (+ A) (i) X^{i}$
38	37	adantl	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i) = seq 0 (+ A) (i) X^{i}$
39	1	ffvelcdmda	$⊢ (φ \land x \in ℕ_{0}) \to A (x) \in ℂ$
40	8 9 39	serf	$⊢ φ \to seq 0 (+ A) : ℕ_{0} ⟶ ℂ$
41	40	ad2antrr	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to seq 0 (+ A) : ℕ_{0} ⟶ ℂ$
42	41	ffvelcdmda	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℕ_{0}) \to seq 0 (+ A) (i) \in ℂ$
43		expcl	$⊢ (X \in ℂ \land i \in ℕ_{0}) \to X^{i} \in ℂ$
44	27 43	sylan	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℕ_{0}) \to X^{i} \in ℂ$
45	42 44	mulcld	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℕ_{0}) \to seq 0 (+ A) (i) X^{i} \in ℂ$
46	38 45	eqeltrd	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i) \in ℂ$
47	28	recnd	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to \|X\| \in ℂ$
48		absidm	$⊢ X \in ℂ \to \|\|X\|\| = \|X\|$
49	27 48	syl	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to \|\|X\|\| = \|X\|$
50		eqid	$⊢ abs \circ - = abs \circ -$
51	50	cnmetdval	$⊢ (X \in ℂ \land 0 \in ℂ) \to X (abs \circ -) 0 = \|X - 0\|$
52	27 22 51	sylancl	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to X (abs \circ -) 0 = \|X - 0\|$
53	27	subid1d	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to X - 0 = X$
54	53	fveq2d	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to \|X - 0\| = \|X\|$
55	52 54	eqtrd	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to X (abs \circ -) 0 = \|X\|$
56		elbl3	$⊢ ((abs \circ - \in ∞Met (ℂ) \land 1 \in ℝ^{*}) \land (0 \in ℂ \land X \in ℂ)) \to (X \in (0 ball (abs \circ -) 1) \leftrightarrow X (abs \circ -) 0 < 1)$
57	21 23 56	mpanl12	$⊢ (0 \in ℂ \land X \in ℂ) \to (X \in (0 ball (abs \circ -) 1) \leftrightarrow X (abs \circ -) 0 < 1)$
58	22 27 57	sylancr	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to (X \in (0 ball (abs \circ -) 1) \leftrightarrow X (abs \circ -) 0 < 1)$
59	26 58	mpbid	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to X (abs \circ -) 0 < 1$
60	55 59	eqbrtrrd	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to \|X\| < 1$
61	49 60	eqbrtrd	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to \|\|X\|\| < 1$
62	47 61 20	geolim	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to seq 0 (+ (n \in ℕ_{0} ⟼ {\|X\|}^{n})) ⇝ (\frac{1}{1 - \|X\|})$
63		climrel	$⊢ Rel ⇝$
64	63	releldmi	$⊢ seq 0 (+ (n \in ℕ_{0} ⟼ {\|X\|}^{n})) ⇝ (\frac{1}{1 - \|X\|}) \to seq 0 (+ (n \in ℕ_{0} ⟼ {\|X\|}^{n})) \in dom ⇝$
65	62 64	syl	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to seq 0 (+ (n \in ℕ_{0} ⟼ {\|X\|}^{n})) \in dom ⇝$
66		1red	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to 1 \in ℝ$
67	41	adantr	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to seq 0 (+ A) : ℕ_{0} ⟶ ℂ$
68		eluznn0	$⊢ (j \in ℕ_{0} \land i \in ℤ_{\geq j}) \to i \in ℕ_{0}$
69	15 68	sylan	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to i \in ℕ_{0}$
70	67 69	ffvelcdmd	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to seq 0 (+ A) (i) \in ℂ$
71	69 44	syldan	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to X^{i} \in ℂ$
72	70 71	absmuld	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|seq 0 (+ A) (i) X^{i}\| = \|seq 0 (+ A) (i)\| \|X^{i}\|$
73	27	adantr	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to X \in ℂ$
74	73 69	absexpd	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|X^{i}\| = {\|X\|}^{i}$
75	74	oveq2d	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|seq 0 (+ A) (i)\| \|X^{i}\| = \|seq 0 (+ A) (i)\| {\|X\|}^{i}$
76	72 75	eqtrd	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|seq 0 (+ A) (i) X^{i}\| = \|seq 0 (+ A) (i)\| {\|X\|}^{i}$
77	70	abscld	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|seq 0 (+ A) (i)\| \in ℝ$
78		1red	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to 1 \in ℝ$
79	69 30	syldan	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to {\|X\|}^{i} \in ℝ$
80	71	absge0d	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to 0 \leq \|X^{i}\|$
81	80 74	breqtrd	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to 0 \leq {\|X\|}^{i}$
82		simprr	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1$
83		2fveq3	$⊢ m = i \to \|seq 0 (+ A) (m)\| = \|seq 0 (+ A) (i)\|$
84	83	breq1d	$⊢ m = i \to (\|seq 0 (+ A) (m)\| < 1 \leftrightarrow \|seq 0 (+ A) (i)\| < 1)$
85	84	rspccva	$⊢ (\forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1 \land i \in ℤ_{\geq j}) \to \|seq 0 (+ A) (i)\| < 1$
86	82 85	sylan	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|seq 0 (+ A) (i)\| < 1$
87		1re	$⊢ 1 \in ℝ$
88		ltle	$⊢ (\|seq 0 (+ A) (i)\| \in ℝ \land 1 \in ℝ) \to (\|seq 0 (+ A) (i)\| < 1 \to \|seq 0 (+ A) (i)\| \leq 1)$
89	77 87 88	sylancl	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to (\|seq 0 (+ A) (i)\| < 1 \to \|seq 0 (+ A) (i)\| \leq 1)$
90	86 89	mpd	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|seq 0 (+ A) (i)\| \leq 1$
91	77 78 79 81 90	lemul1ad	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|seq 0 (+ A) (i)\| {\|X\|}^{i} \leq 1 {\|X\|}^{i}$
92	76 91	eqbrtrd	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|seq 0 (+ A) (i) X^{i}\| \leq 1 {\|X\|}^{i}$
93	69 37	syl	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i) = seq 0 (+ A) (i) X^{i}$
94	93	fveq2d	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|(k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i)\| = \|seq 0 (+ A) (i) X^{i}\|$
95	69 19	syl	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to (n \in ℕ_{0} ⟼ {\|X\|}^{n}) (i) = {\|X\|}^{i}$
96	95	oveq2d	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to 1 (n \in ℕ_{0} ⟼ {\|X\|}^{n}) (i) = 1 {\|X\|}^{i}$
97	92 94 96	3brtr4d	$⊢ (((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \land i \in ℤ_{\geq j}) \to \|(k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (i)\| \leq 1 (n \in ℕ_{0} ⟼ {\|X\|}^{n}) (i)$
98	8 15 31 46 65 66 97	cvgcmpce	$⊢ ((φ \land X \in (0 ball (abs \circ -) 1)) \land (j \in ℕ_{0} \land \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < 1)) \to seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) \in dom ⇝$
99	14 98	rexlimddv	$⊢ (φ \land X \in (0 ball (abs \circ -) 1)) \to seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) \in dom ⇝$

Metamath Proof Explorer

Theorem abelthlem5

Proof