lmdvg

Description: If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017)

	Ref	Expression
Hypotheses	lmdvg.1	$⊢ φ \to F : ℕ ⟶ [0, +∞)$
	lmdvg.2	$⊢ (φ \land k \in ℕ) \to F (k) \leq F (k + 1)$
	lmdvg.3	$⊢ φ \to \neg F \in dom ⇝$
Assertion	lmdvg	$⊢ φ \to \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < F (k)$

Proof

Step	Hyp	Ref	Expression
1		lmdvg.1	$⊢ φ \to F : ℕ ⟶ [0, +∞)$
2		lmdvg.2	$⊢ (φ \land k \in ℕ) \to F (k) \leq F (k + 1)$
3		lmdvg.3	$⊢ φ \to \neg F \in dom ⇝$
4		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
5		1zzd	$⊢ (φ \land \exists x \in ℝ \forall j \in ℕ F (j) \leq x) \to 1 \in ℤ$
6		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
7		fss	$⊢ (F : ℕ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F : ℕ ⟶ ℝ$
8	1 6 7	sylancl	$⊢ φ \to F : ℕ ⟶ ℝ$
9	8	adantr	$⊢ (φ \land \exists x \in ℝ \forall j \in ℕ F (j) \leq x) \to F : ℕ ⟶ ℝ$
10	2	ralrimiva	$⊢ φ \to \forall k \in ℕ F (k) \leq F (k + 1)$
11		fveq2	$⊢ k = l \to F (k) = F (l)$
12		fvoveq1	$⊢ k = l \to F (k + 1) = F (l + 1)$
13	11 12	breq12d	$⊢ k = l \to (F (k) \leq F (k + 1) \leftrightarrow F (l) \leq F (l + 1))$
14	13	cbvralvw	$⊢ \forall k \in ℕ F (k) \leq F (k + 1) \leftrightarrow \forall l \in ℕ F (l) \leq F (l + 1)$
15	10 14	sylib	$⊢ φ \to \forall l \in ℕ F (l) \leq F (l + 1)$
16	15	r19.21bi	$⊢ (φ \land l \in ℕ) \to F (l) \leq F (l + 1)$
17	16	adantlr	$⊢ ((φ \land \exists x \in ℝ \forall j \in ℕ F (j) \leq x) \land l \in ℕ) \to F (l) \leq F (l + 1)$
18		simpr	$⊢ (φ \land \exists x \in ℝ \forall j \in ℕ F (j) \leq x) \to \exists x \in ℝ \forall j \in ℕ F (j) \leq x$
19		fveq2	$⊢ j = l \to F (j) = F (l)$
20	19	breq1d	$⊢ j = l \to (F (j) \leq x \leftrightarrow F (l) \leq x)$
21	20	cbvralvw	$⊢ \forall j \in ℕ F (j) \leq x \leftrightarrow \forall l \in ℕ F (l) \leq x$
22	21	rexbii	$⊢ \exists x \in ℝ \forall j \in ℕ F (j) \leq x \leftrightarrow \exists x \in ℝ \forall l \in ℕ F (l) \leq x$
23	18 22	sylib	$⊢ (φ \land \exists x \in ℝ \forall j \in ℕ F (j) \leq x) \to \exists x \in ℝ \forall l \in ℕ F (l) \leq x$
24	4 5 9 17 23	climsup	$⊢ (φ \land \exists x \in ℝ \forall j \in ℕ F (j) \leq x) \to F ⇝ sup (ran F ℝ <)$
25		nnex	$⊢ ℕ \in V$
26		fex	$⊢ (F : ℕ ⟶ [0, +∞) \land ℕ \in V) \to F \in V$
27	1 25 26	sylancl	$⊢ φ \to F \in V$
28	27	adantr	$⊢ (φ \land F ⇝ sup (ran F ℝ <)) \to F \in V$
29		ltso	$⊢ < Or ℝ$
30	29	supex	$⊢ sup (ran F ℝ <) \in V$
31	30	a1i	$⊢ (φ \land F ⇝ sup (ran F ℝ <)) \to sup (ran F ℝ <) \in V$
32		simpr	$⊢ (φ \land F ⇝ sup (ran F ℝ <)) \to F ⇝ sup (ran F ℝ <)$
33		breldmg	$⊢ (F \in V \land sup (ran F ℝ <) \in V \land F ⇝ sup (ran F ℝ <)) \to F \in dom ⇝$
34	28 31 32 33	syl3anc	$⊢ (φ \land F ⇝ sup (ran F ℝ <)) \to F \in dom ⇝$
35	24 34	syldan	$⊢ (φ \land \exists x \in ℝ \forall j \in ℕ F (j) \leq x) \to F \in dom ⇝$
36	3 35	mtand	$⊢ φ \to \neg \exists x \in ℝ \forall j \in ℕ F (j) \leq x$
37		ralnex	$⊢ \forall x \in ℝ \neg \forall j \in ℕ F (j) \leq x \leftrightarrow \neg \exists x \in ℝ \forall j \in ℕ F (j) \leq x$
38	36 37	sylibr	$⊢ φ \to \forall x \in ℝ \neg \forall j \in ℕ F (j) \leq x$
39		simplr	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to x \in ℝ$
40	8	adantr	$⊢ (φ \land x \in ℝ) \to F : ℕ ⟶ ℝ$
41	40	ffvelrnda	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to F (j) \in ℝ$
42	39 41	ltnled	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to (x < F (j) \leftrightarrow \neg F (j) \leq x)$
43	42	rexbidva	$⊢ (φ \land x \in ℝ) \to (\exists j \in ℕ x < F (j) \leftrightarrow \exists j \in ℕ \neg F (j) \leq x)$
44		rexnal	$⊢ \exists j \in ℕ \neg F (j) \leq x \leftrightarrow \neg \forall j \in ℕ F (j) \leq x$
45	43 44	syl6bb	$⊢ (φ \land x \in ℝ) \to (\exists j \in ℕ x < F (j) \leftrightarrow \neg \forall j \in ℕ F (j) \leq x)$
46	45	ralbidva	$⊢ φ \to (\forall x \in ℝ \exists j \in ℕ x < F (j) \leftrightarrow \forall x \in ℝ \neg \forall j \in ℕ F (j) \leq x)$
47	38 46	mpbird	$⊢ φ \to \forall x \in ℝ \exists j \in ℕ x < F (j)$
48	47	r19.21bi	$⊢ (φ \land x \in ℝ) \to \exists j \in ℕ x < F (j)$
49	39	ad2antrr	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to x \in ℝ$
50	41	ad2antrr	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to F (j) \in ℝ$
51	40	ad3antrrr	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to F : ℕ ⟶ ℝ$
52		uznnssnn	$⊢ j \in ℕ \to ℤ_{\geq j} \subseteq ℕ$
53	52	ad3antlr	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to ℤ_{\geq j} \subseteq ℕ$
54		simpr	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to k \in ℤ_{\geq j}$
55	53 54	sseldd	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to k \in ℕ$
56	51 55	ffvelrnd	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to F (k) \in ℝ$
57		simplr	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to x < F (j)$
58		simp-4l	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to φ$
59		simpllr	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to j \in ℕ$
60		simpr	$⊢ ((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \to k \in ℤ_{\geq j}$
61	8	ad3antrrr	$⊢ (((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \land l \in (j \dots k)) \to F : ℕ ⟶ ℝ$
62		fzssnn	$⊢ j \in ℕ \to (j \dots k) \subseteq ℕ$
63	62	ad3antlr	$⊢ (((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \land l \in (j \dots k)) \to (j \dots k) \subseteq ℕ$
64		simpr	$⊢ (((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \land l \in (j \dots k)) \to l \in (j \dots k)$
65	63 64	sseldd	$⊢ (((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \land l \in (j \dots k)) \to l \in ℕ$
66	61 65	ffvelrnd	$⊢ (((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \land l \in (j \dots k)) \to F (l) \in ℝ$
67		simplll	$⊢ (((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \land l \in (j \dots k - 1)) \to φ$
68		fzssnn	$⊢ j \in ℕ \to (j \dots k - 1) \subseteq ℕ$
69	68	ad3antlr	$⊢ (((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \land l \in (j \dots k - 1)) \to (j \dots k - 1) \subseteq ℕ$
70		simpr	$⊢ (((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \land l \in (j \dots k - 1)) \to l \in (j \dots k - 1)$
71	69 70	sseldd	$⊢ (((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \land l \in (j \dots k - 1)) \to l \in ℕ$
72	67 71 16	syl2anc	$⊢ (((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \land l \in (j \dots k - 1)) \to F (l) \leq F (l + 1)$
73	60 66 72	monoord	$⊢ ((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (j) \leq F (k)$
74	58 59 54 73	syl21anc	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to F (j) \leq F (k)$
75	49 50 56 57 74	ltletrd	$⊢ ((((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \land k \in ℤ_{\geq j}) \to x < F (k)$
76	75	ralrimiva	$⊢ (((φ \land x \in ℝ) \land j \in ℕ) \land x < F (j)) \to \forall k \in ℤ_{\geq j} x < F (k)$
77	76	ex	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to (x < F (j) \to \forall k \in ℤ_{\geq j} x < F (k))$
78	77	reximdva	$⊢ (φ \land x \in ℝ) \to (\exists j \in ℕ x < F (j) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} x < F (k))$
79	48 78	mpd	$⊢ (φ \land x \in ℝ) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} x < F (k)$
80	79	ralrimiva	$⊢ φ \to \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < F (k)$

Metamath Proof Explorer

Theorem lmdvg

Proof