logtayllem

		Ref	Expression
	Assertion	logtayllem	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ (n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n})) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3	2	a1i	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 \in ℕ_{0}$
4		oveq2	$⊢ n = k \to {\|A\|}^{n} = {\|A\|}^{k}$
5		eqid	$⊢ (n \in ℕ_{0} ⟼ {\|A\|}^{n}) = (n \in ℕ_{0} ⟼ {\|A\|}^{n})$
6		ovex	$⊢ {\|A\|}^{k} \in V$
7	4 5 6	fvmpt	$⊢ k \in ℕ_{0} \to (n \in ℕ_{0} ⟼ {\|A\|}^{n}) (k) = {\|A\|}^{k}$
8	7	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ {\|A\|}^{n}) (k) = {\|A\|}^{k}$
9		abscl	$⊢ A \in ℂ \to \|A\| \in ℝ$
10	9	adantr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| \in ℝ$
11		reexpcl	$⊢ (\|A\| \in ℝ \land k \in ℕ_{0}) \to {\|A\|}^{k} \in ℝ$
12	10 11	sylan	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to {\|A\|}^{k} \in ℝ$
13	8 12	eqeltrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ {\|A\|}^{n}) (k) \in ℝ$
14		eqeq1	$⊢ n = k \to (n = 0 \leftrightarrow k = 0)$
15		oveq2	$⊢ n = k \to \frac{1}{n} = \frac{1}{k}$
16	14 15	ifbieq2d	$⊢ n = k \to if (n = 0, 0, \frac{1}{n}) = if (k = 0, 0, \frac{1}{k})$
17		oveq2	$⊢ n = k \to A^{n} = A^{k}$
18	16 17	oveq12d	$⊢ n = k \to if (n = 0, 0, \frac{1}{n}) A^{n} = if (k = 0, 0, \frac{1}{k}) A^{k}$
19		eqid	$⊢ (n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n}) = (n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n})$
20		ovex	$⊢ if (k = 0, 0, \frac{1}{k}) A^{k} \in V$
21	18 19 20	fvmpt	$⊢ k \in ℕ_{0} \to (n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n}) (k) = if (k = 0, 0, \frac{1}{k}) A^{k}$
22	21	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n}) (k) = if (k = 0, 0, \frac{1}{k}) A^{k}$
23		0cnd	$⊢ (((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \land k = 0) \to 0 \in ℂ$
24		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
25	24	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to k \in ℂ$
26		neqne	$⊢ \neg k = 0 \to k \neq 0$
27		reccl	$⊢ (k \in ℂ \land k \neq 0) \to \frac{1}{k} \in ℂ$
28	25 26 27	syl2an	$⊢ (((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \land \neg k = 0) \to \frac{1}{k} \in ℂ$
29	23 28	ifclda	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to if (k = 0, 0, \frac{1}{k}) \in ℂ$
30		expcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} \in ℂ$
31	30	adantlr	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to A^{k} \in ℂ$
32	29 31	mulcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to if (k = 0, 0, \frac{1}{k}) A^{k} \in ℂ$
33	22 32	eqeltrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n}) (k) \in ℂ$
34	10	recnd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| \in ℂ$
35		absidm	$⊢ A \in ℂ \to \|\|A\|\| = \|A\|$
36	35	adantr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|\|A\|\| = \|A\|$
37		simpr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| < 1$
38	36 37	eqbrtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|\|A\|\| < 1$
39	34 38 8	geolim	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ (n \in ℕ_{0} ⟼ {\|A\|}^{n})) ⇝ (\frac{1}{1 - \|A\|})$
40		seqex	$⊢ seq 0 (+ (n \in ℕ_{0} ⟼ {\|A\|}^{n})) \in V$
41		ovex	$⊢ \frac{1}{1 - \|A\|} \in V$
42	40 41	breldm	$⊢ seq 0 (+ (n \in ℕ_{0} ⟼ {\|A\|}^{n})) ⇝ (\frac{1}{1 - \|A\|}) \to seq 0 (+ (n \in ℕ_{0} ⟼ {\|A\|}^{n})) \in dom ⇝$
43	39 42	syl	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ (n \in ℕ_{0} ⟼ {\|A\|}^{n})) \in dom ⇝$
44		1red	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 \in ℝ$
45		elnnuz	$⊢ k \in ℕ \leftrightarrow k \in ℤ_{\geq 1}$
46		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
47	46	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \frac{1}{k} \in ℝ$
48	47	recnd	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \frac{1}{k} \in ℂ$
49		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
50	49 31	sylan2	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to A^{k} \in ℂ$
51	48 50	absmuld	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \|(\frac{1}{k}) A^{k}\| = \|\frac{1}{k}\| \|A^{k}\|$
52		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
53	52	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to k \in ℝ^{+}$
54	53	rpreccld	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \frac{1}{k} \in ℝ^{+}$
55	54	rpge0d	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to 0 \leq \frac{1}{k}$
56	47 55	absidd	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \|\frac{1}{k}\| = \frac{1}{k}$
57		simpl	$⊢ (A \in ℂ \land \|A\| < 1) \to A \in ℂ$
58		absexp	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \|A^{k}\| = {\|A\|}^{k}$
59	57 49 58	syl2an	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \|A^{k}\| = {\|A\|}^{k}$
60	56 59	oveq12d	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \|\frac{1}{k}\| \|A^{k}\| = (\frac{1}{k}) {\|A\|}^{k}$
61	51 60	eqtrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \|(\frac{1}{k}) A^{k}\| = (\frac{1}{k}) {\|A\|}^{k}$
62		1red	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to 1 \in ℝ$
63	49 12	sylan2	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to {\|A\|}^{k} \in ℝ$
64	50	absge0d	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to 0 \leq \|A^{k}\|$
65	64 59	breqtrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to 0 \leq {\|A\|}^{k}$
66		nnge1	$⊢ k \in ℕ \to 1 \leq k$
67	66	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to 1 \leq k$
68		0lt1	$⊢ 0 < 1$
69	68	a1i	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to 0 < 1$
70		nnre	$⊢ k \in ℕ \to k \in ℝ$
71	70	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to k \in ℝ$
72		nngt0	$⊢ k \in ℕ \to 0 < k$
73	72	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to 0 < k$
74		lerec	$⊢ ((1 \in ℝ \land 0 < 1) \land (k \in ℝ \land 0 < k)) \to (1 \leq k \leftrightarrow \frac{1}{k} \leq \frac{1}{1})$
75	62 69 71 73 74	syl22anc	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to (1 \leq k \leftrightarrow \frac{1}{k} \leq \frac{1}{1})$
76	67 75	mpbid	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \frac{1}{k} \leq \frac{1}{1}$
77		1div1e1	$⊢ \frac{1}{1} = 1$
78	76 77	breqtrdi	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \frac{1}{k} \leq 1$
79	47 62 63 65 78	lemul1ad	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to (\frac{1}{k}) {\|A\|}^{k} \leq 1 {\|A\|}^{k}$
80	61 79	eqbrtrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \|(\frac{1}{k}) A^{k}\| \leq 1 {\|A\|}^{k}$
81	49 22	sylan2	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to (n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n}) (k) = if (k = 0, 0, \frac{1}{k}) A^{k}$
82		nnne0	$⊢ k \in ℕ \to k \neq 0$
83	82	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to k \neq 0$
84	83	neneqd	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \neg k = 0$
85	84	iffalsed	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to if (k = 0, 0, \frac{1}{k}) = \frac{1}{k}$
86	85	oveq1d	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to if (k = 0, 0, \frac{1}{k}) A^{k} = (\frac{1}{k}) A^{k}$
87	81 86	eqtrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to (n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n}) (k) = (\frac{1}{k}) A^{k}$
88	87	fveq2d	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \|(n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n}) (k)\| = \|(\frac{1}{k}) A^{k}\|$
89	49 8	sylan2	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to (n \in ℕ_{0} ⟼ {\|A\|}^{n}) (k) = {\|A\|}^{k}$
90	89	oveq2d	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to 1 (n \in ℕ_{0} ⟼ {\|A\|}^{n}) (k) = 1 {\|A\|}^{k}$
91	80 88 90	3brtr4d	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \|(n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n}) (k)\| \leq 1 (n \in ℕ_{0} ⟼ {\|A\|}^{n}) (k)$
92	45 91	sylan2br	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℤ_{\geq 1}) \to \|(n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n}) (k)\| \leq 1 (n \in ℕ_{0} ⟼ {\|A\|}^{n}) (k)$
93	1 3 13 33 43 44 92	cvgcmpce	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ (n \in ℕ_{0} ⟼ if (n = 0, 0, \frac{1}{n}) A^{n})) \in dom ⇝$

Metamath Proof Explorer

Theorem logtayllem

Proof