xrralrecnnge

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	xrralrecnnge.n	$⊢ Ⅎ n φ$
	xrralrecnnge.a	$⊢ φ \to A \in ℝ$
	xrralrecnnge.b	$⊢ φ \to B \in ℝ^{*}$
Assertion	xrralrecnnge	$⊢ φ \to (A \leq B \leftrightarrow \forall n \in ℕ A - (\frac{1}{n}) \leq B)$

Proof

Step	Hyp	Ref	Expression
1		xrralrecnnge.n	$⊢ Ⅎ n φ$
2		xrralrecnnge.a	$⊢ φ \to A \in ℝ$
3		xrralrecnnge.b	$⊢ φ \to B \in ℝ^{*}$
4		nfv	$⊢ Ⅎ n A \leq B$
5	1 4	nfan	$⊢ Ⅎ n (φ \land A \leq B)$
6	2	adantr	$⊢ (φ \land n \in ℕ) \to A \in ℝ$
7		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
8	7	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ$
9	6 8	resubcld	$⊢ (φ \land n \in ℕ) \to A - (\frac{1}{n}) \in ℝ$
10	9	rexrd	$⊢ (φ \land n \in ℕ) \to A - (\frac{1}{n}) \in ℝ^{*}$
11	10	adantlr	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to A - (\frac{1}{n}) \in ℝ^{*}$
12	3	ad2antrr	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to B \in ℝ^{*}$
13	2	rexrd	$⊢ φ \to A \in ℝ^{*}$
14	13	ad2antrr	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to A \in ℝ^{*}$
15		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
16	15	rpreccld	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
17	16	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ^{+}$
18	6 17	ltsubrpd	$⊢ (φ \land n \in ℕ) \to A - (\frac{1}{n}) < A$
19	18	adantlr	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to A - (\frac{1}{n}) < A$
20		simplr	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to A \leq B$
21	11 14 12 19 20	xrltletrd	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to A - (\frac{1}{n}) < B$
22	11 12 21	xrltled	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to A - (\frac{1}{n}) \leq B$
23	22	ex	$⊢ (φ \land A \leq B) \to (n \in ℕ \to A - (\frac{1}{n}) \leq B)$
24	5 23	ralrimi	$⊢ (φ \land A \leq B) \to \forall n \in ℕ A - (\frac{1}{n}) \leq B$
25	24	ex	$⊢ φ \to (A \leq B \to \forall n \in ℕ A - (\frac{1}{n}) \leq B)$
26		pnfxr	$⊢ +∞ \in ℝ^{*}$
27	26	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
28	2	ltpnfd	$⊢ φ \to A < +∞$
29	13 27 28	xrltled	$⊢ φ \to A \leq +∞$
30	29	ad2antrr	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land B = +∞) \to A \leq +∞$
31		id	$⊢ B = +∞ \to B = +∞$
32	31	eqcomd	$⊢ B = +∞ \to +∞ = B$
33	32	adantl	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land B = +∞) \to +∞ = B$
34	30 33	breqtrd	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land B = +∞) \to A \leq B$
35	3	ad2antrr	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land \neg B = +∞) \to B \in ℝ^{*}$
36		1nn	$⊢ 1 \in ℕ$
37	36	a1i	$⊢ \forall n \in ℕ A - (\frac{1}{n}) \leq B \to 1 \in ℕ$
38		id	$⊢ \forall n \in ℕ A - (\frac{1}{n}) \leq B \to \forall n \in ℕ A - (\frac{1}{n}) \leq B$
39		oveq2	$⊢ n = 1 \to \frac{1}{n} = \frac{1}{1}$
40	39	oveq2d	$⊢ n = 1 \to A - (\frac{1}{n}) = A - (\frac{1}{1})$
41	40	breq1d	$⊢ n = 1 \to (A - (\frac{1}{n}) \leq B \leftrightarrow A - (\frac{1}{1}) \leq B)$
42	41	rspcva	$⊢ (1 \in ℕ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \to A - (\frac{1}{1}) \leq B$
43	37 38 42	syl2anc	$⊢ \forall n \in ℕ A - (\frac{1}{n}) \leq B \to A - (\frac{1}{1}) \leq B$
44	43	adantr	$⊢ (\forall n \in ℕ A - (\frac{1}{n}) \leq B \land B = −∞) \to A - (\frac{1}{1}) \leq B$
45		simpr	$⊢ (\forall n \in ℕ A - (\frac{1}{n}) \leq B \land B = −∞) \to B = −∞$
46	44 45	breqtrd	$⊢ (\forall n \in ℕ A - (\frac{1}{n}) \leq B \land B = −∞) \to A - (\frac{1}{1}) \leq −∞$
47	46	adantll	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land B = −∞) \to A - (\frac{1}{1}) \leq −∞$
48		1red	$⊢ φ \to 1 \in ℝ$
49		ax-1ne0	$⊢ 1 \neq 0$
50	49	a1i	$⊢ φ \to 1 \neq 0$
51	48 48 50	redivcld	$⊢ φ \to \frac{1}{1} \in ℝ$
52	2 51	resubcld	$⊢ φ \to A - (\frac{1}{1}) \in ℝ$
53	52	mnfltd	$⊢ φ \to −∞ < A - (\frac{1}{1})$
54		mnfxr	$⊢ −∞ \in ℝ^{*}$
55	54	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
56	52	rexrd	$⊢ φ \to A - (\frac{1}{1}) \in ℝ^{*}$
57	55 56	xrltnled	$⊢ φ \to (−∞ < A - (\frac{1}{1}) \leftrightarrow \neg A - (\frac{1}{1}) \leq −∞)$
58	53 57	mpbid	$⊢ φ \to \neg A - (\frac{1}{1}) \leq −∞$
59	58	ad2antrr	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land B = −∞) \to \neg A - (\frac{1}{1}) \leq −∞$
60	47 59	pm2.65da	$⊢ (φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \to \neg B = −∞$
61	60	neqned	$⊢ (φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \to B \neq −∞$
62	61	adantr	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land \neg B = +∞) \to B \neq −∞$
63		neqne	$⊢ \neg B = +∞ \to B \neq +∞$
64	63	adantl	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land \neg B = +∞) \to B \neq +∞$
65	35 62 64	xrred	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land \neg B = +∞) \to B \in ℝ$
66		nfv	$⊢ Ⅎ n B \in ℝ$
67	1 66	nfan	$⊢ Ⅎ n (φ \land B \in ℝ)$
68	13	adantr	$⊢ (φ \land B \in ℝ) \to A \in ℝ^{*}$
69		simpr	$⊢ (φ \land B \in ℝ) \to B \in ℝ$
70	67 68 69	xrralrecnnle	$⊢ (φ \land B \in ℝ) \to (A \leq B \leftrightarrow \forall n \in ℕ A \leq B + (\frac{1}{n}))$
71	6	adantlr	$⊢ ((φ \land B \in ℝ) \land n \in ℕ) \to A \in ℝ$
72	7	adantl	$⊢ ((φ \land B \in ℝ) \land n \in ℕ) \to \frac{1}{n} \in ℝ$
73	69	adantr	$⊢ ((φ \land B \in ℝ) \land n \in ℕ) \to B \in ℝ$
74	71 72 73	lesubaddd	$⊢ ((φ \land B \in ℝ) \land n \in ℕ) \to (A - (\frac{1}{n}) \leq B \leftrightarrow A \leq B + (\frac{1}{n}))$
75	74	bicomd	$⊢ ((φ \land B \in ℝ) \land n \in ℕ) \to (A \leq B + (\frac{1}{n}) \leftrightarrow A - (\frac{1}{n}) \leq B)$
76	67 75	ralbida	$⊢ (φ \land B \in ℝ) \to (\forall n \in ℕ A \leq B + (\frac{1}{n}) \leftrightarrow \forall n \in ℕ A - (\frac{1}{n}) \leq B)$
77	70 76	bitr2d	$⊢ (φ \land B \in ℝ) \to (\forall n \in ℕ A - (\frac{1}{n}) \leq B \leftrightarrow A \leq B)$
78	77	biimpd	$⊢ (φ \land B \in ℝ) \to (\forall n \in ℕ A - (\frac{1}{n}) \leq B \to A \leq B)$
79	78	imp	$⊢ ((φ \land B \in ℝ) \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \to A \leq B$
80	79	an32s	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land B \in ℝ) \to A \leq B$
81	65 80	syldan	$⊢ ((φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \land \neg B = +∞) \to A \leq B$
82	34 81	pm2.61dan	$⊢ (φ \land \forall n \in ℕ A - (\frac{1}{n}) \leq B) \to A \leq B$
83	82	ex	$⊢ φ \to (\forall n \in ℕ A - (\frac{1}{n}) \leq B \to A \leq B)$
84	25 83	impbid	$⊢ φ \to (A \leq B \leftrightarrow \forall n \in ℕ A - (\frac{1}{n}) \leq B)$

Metamath Proof Explorer

Theorem xrralrecnnge

Proof