Theorem climbddf

Description: A converging sequence of complex numbers is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	climbddf.1	$$⊢\underset{\_}{Ⅎ}kF$$
	climbddf.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	climbddf	$$⊢\left(M\in \mathbb{Z}\wedge F\in \mathrm{dom}⇝\wedge \forall k\in ZF\left(k\right)\in ℂ\right)\to \exists x\in ℝ\forall k\in Z\left|F\left(k\right)\right|\le x$$

Proof

Step	Hyp	Ref	Expression
1		climbddf.1	$$⊢\underset{\_}{Ⅎ}kF$$
2		climbddf.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		simp1	$$⊢\left(M\in \mathbb{Z}\wedge F\in \mathrm{dom}⇝\wedge \forall k\in ZF\left(k\right)\in ℂ\right)\to M\in \mathbb{Z}$$
4		simp2	$$⊢\left(M\in \mathbb{Z}\wedge F\in \mathrm{dom}⇝\wedge \forall k\in ZF\left(k\right)\in ℂ\right)\to F\in \mathrm{dom}⇝$$
5		nfv	$$⊢ℲjF\left(k\right)\in ℂ$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
7	1 6	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}kℂ$$
9	7 8	nfel	$$⊢ℲkF\left(j\right)\in ℂ$$
10		fveq2	$$⊢k=j\to F\left(k\right)=F\left(j\right)$$
11	10	eleq1d	$$⊢k=j\to \left(F\left(k\right)\in ℂ\leftrightarrow F\left(j\right)\in ℂ\right)$$
12	5 9 11	cbvralw	$$⊢\forall k\in ZF\left(k\right)\in ℂ\leftrightarrow \forall j\in ZF\left(j\right)\in ℂ$$
13	12	biimpi	$$⊢\forall k\in ZF\left(k\right)\in ℂ\to \forall j\in ZF\left(j\right)\in ℂ$$
14	13	3ad2ant3	$$⊢\left(M\in \mathbb{Z}\wedge F\in \mathrm{dom}⇝\wedge \forall k\in ZF\left(k\right)\in ℂ\right)\to \forall j\in ZF\left(j\right)\in ℂ$$
15	2	climbdd	$$⊢\left(M\in \mathbb{Z}\wedge F\in \mathrm{dom}⇝\wedge \forall j\in ZF\left(j\right)\in ℂ\right)\to \exists x\in ℝ\forall j\in Z\left|F\left(j\right)\right|\le x$$
16	3 4 14 15	syl3anc	$$⊢\left(M\in \mathbb{Z}\wedge F\in \mathrm{dom}⇝\wedge \forall k\in ZF\left(k\right)\in ℂ\right)\to \exists x\in ℝ\forall j\in Z\left|F\left(j\right)\right|\le x$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}k\mathrm{abs}$$
18	17 7	nffv	$$⊢\underset{\_}{Ⅎ}k\left|F\left(j\right)\right|$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}k\le$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}kx$$
21	18 19 20	nfbr	$$⊢Ⅎk\left|F\left(j\right)\right|\le x$$
22		nfv	$$⊢Ⅎj\left|F\left(k\right)\right|\le x$$
23		2fveq3	$$⊢j=k\to \left|F\left(j\right)\right|=\left|F\left(k\right)\right|$$
24	23	breq1d	$$⊢j=k\to \left(\left|F\left(j\right)\right|\le x\leftrightarrow \left|F\left(k\right)\right|\le x\right)$$
25	21 22 24	cbvralw	$$⊢\forall j\in Z\left|F\left(j\right)\right|\le x\leftrightarrow \forall k\in Z\left|F\left(k\right)\right|\le x$$
26	25	rexbii	$$⊢\exists x\in ℝ\forall j\in Z\left|F\left(j\right)\right|\le x\leftrightarrow \exists x\in ℝ\forall k\in Z\left|F\left(k\right)\right|\le x$$
27	16 26	sylib	$$⊢\left(M\in \mathbb{Z}\wedge F\in \mathrm{dom}⇝\wedge \forall k\in ZF\left(k\right)\in ℂ\right)\to \exists x\in ℝ\forall k\in Z\left|F\left(k\right)\right|\le x$$