climbdd

Description: A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017)

		Ref	Expression
	Hypothesis	climcau.1	$⊢ Z = ℤ_{\geq M}$
	Assertion	climbdd	$⊢ (M \in ℤ \land F \in dom ⇝ \land \forall k \in Z F (k) \in ℂ) \to \exists x \in ℝ \forall k \in Z \|F (k)\| \leq x$

Proof

Step	Hyp	Ref	Expression
1		climcau.1	$⊢ Z = ℤ_{\geq M}$
2		simp3	$⊢ (M \in ℤ \land F \in dom ⇝ \land \forall k \in Z F (k) \in ℂ) \to \forall k \in Z F (k) \in ℂ$
3	1	climcau	$⊢ (M \in ℤ \land F \in dom ⇝) \to \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < y$
4	3	3adant3	$⊢ (M \in ℤ \land F \in dom ⇝ \land \forall k \in Z F (k) \in ℂ) \to \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < y$
5	1	caubnd	$⊢ (\forall k \in Z F (k) \in ℂ \land \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < y) \to \exists x \in ℝ \forall k \in Z \|F (k)\| < x$
6	2 4 5	syl2anc	$⊢ (M \in ℤ \land F \in dom ⇝ \land \forall k \in Z F (k) \in ℂ) \to \exists x \in ℝ \forall k \in Z \|F (k)\| < x$
7		r19.26	$⊢ \forall k \in Z (F (k) \in ℂ \land \|F (k)\| < x) \leftrightarrow (\forall k \in Z F (k) \in ℂ \land \forall k \in Z \|F (k)\| < x)$
8		simpr	$⊢ ((((M \in ℤ \land F \in dom ⇝) \land x \in ℝ) \land k \in Z) \land F (k) \in ℂ) \to F (k) \in ℂ$
9	8	abscld	$⊢ ((((M \in ℤ \land F \in dom ⇝) \land x \in ℝ) \land k \in Z) \land F (k) \in ℂ) \to \|F (k)\| \in ℝ$
10		simpllr	$⊢ ((((M \in ℤ \land F \in dom ⇝) \land x \in ℝ) \land k \in Z) \land F (k) \in ℂ) \to x \in ℝ$
11		ltle	$⊢ (\|F (k)\| \in ℝ \land x \in ℝ) \to (\|F (k)\| < x \to \|F (k)\| \leq x)$
12	9 10 11	syl2anc	$⊢ ((((M \in ℤ \land F \in dom ⇝) \land x \in ℝ) \land k \in Z) \land F (k) \in ℂ) \to (\|F (k)\| < x \to \|F (k)\| \leq x)$
13	12	expimpd	$⊢ (((M \in ℤ \land F \in dom ⇝) \land x \in ℝ) \land k \in Z) \to ((F (k) \in ℂ \land \|F (k)\| < x) \to \|F (k)\| \leq x)$
14	13	ralimdva	$⊢ ((M \in ℤ \land F \in dom ⇝) \land x \in ℝ) \to (\forall k \in Z (F (k) \in ℂ \land \|F (k)\| < x) \to \forall k \in Z \|F (k)\| \leq x)$
15	7 14	syl5bir	$⊢ ((M \in ℤ \land F \in dom ⇝) \land x \in ℝ) \to ((\forall k \in Z F (k) \in ℂ \land \forall k \in Z \|F (k)\| < x) \to \forall k \in Z \|F (k)\| \leq x)$
16	15	exp4b	$⊢ (M \in ℤ \land F \in dom ⇝) \to (x \in ℝ \to (\forall k \in Z F (k) \in ℂ \to (\forall k \in Z \|F (k)\| < x \to \forall k \in Z \|F (k)\| \leq x)))$
17	16	com23	$⊢ (M \in ℤ \land F \in dom ⇝) \to (\forall k \in Z F (k) \in ℂ \to (x \in ℝ \to (\forall k \in Z \|F (k)\| < x \to \forall k \in Z \|F (k)\| \leq x)))$
18	17	3impia	$⊢ (M \in ℤ \land F \in dom ⇝ \land \forall k \in Z F (k) \in ℂ) \to (x \in ℝ \to (\forall k \in Z \|F (k)\| < x \to \forall k \in Z \|F (k)\| \leq x))$
19	18	reximdvai	$⊢ (M \in ℤ \land F \in dom ⇝ \land \forall k \in Z F (k) \in ℂ) \to (\exists x \in ℝ \forall k \in Z \|F (k)\| < x \to \exists x \in ℝ \forall k \in Z \|F (k)\| \leq x)$
20	6 19	mpd	$⊢ (M \in ℤ \land F \in dom ⇝ \land \forall k \in Z F (k) \in ℂ) \to \exists x \in ℝ \forall k \in Z \|F (k)\| \leq x$

Metamath Proof Explorer

Theorem climbdd

Proof