xrralrecnnle

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

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

Proof

Step	Hyp	Ref	Expression
1		xrralrecnnle.n	$⊢ Ⅎ n φ$
2		xrralrecnnle.a	$⊢ φ \to A \in ℝ^{*}$
3		xrralrecnnle.b	$⊢ φ \to B \in ℝ$
4		nfv	$⊢ Ⅎ n A \leq B$
5	1 4	nfan	$⊢ Ⅎ n (φ \land A \leq B)$
6	2	ad2antrr	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to A \in ℝ^{*}$
7	3	adantr	$⊢ (φ \land n \in ℕ) \to B \in ℝ$
8		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
9	8	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ$
10	7 9	readdcld	$⊢ (φ \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ$
11	10	rexrd	$⊢ (φ \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ^{*}$
12	11	adantlr	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to B + (\frac{1}{n}) \in ℝ^{*}$
13		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
14	3 13	syl	$⊢ φ \to B \in ℝ^{*}$
15	14	ad2antrr	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to B \in ℝ^{*}$
16		simplr	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to A \leq B$
17		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
18		rpreccl	$⊢ n \in ℝ^{+} \to \frac{1}{n} \in ℝ^{+}$
19	17 18	syl	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
20	19	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ^{+}$
21	7 20	ltaddrpd	$⊢ (φ \land n \in ℕ) \to B < B + (\frac{1}{n})$
22	21	adantlr	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to B < B + (\frac{1}{n})$
23	6 15 12 16 22	xrlelttrd	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to A < B + (\frac{1}{n})$
24	6 12 23	xrltled	$⊢ ((φ \land A \leq B) \land n \in ℕ) \to A \leq B + (\frac{1}{n})$
25	24	ex	$⊢ (φ \land A \leq B) \to (n \in ℕ \to A \leq B + (\frac{1}{n}))$
26	5 25	ralrimi	$⊢ (φ \land A \leq B) \to \forall n \in ℕ A \leq B + (\frac{1}{n})$
27	26	ex	$⊢ φ \to (A \leq B \to \forall n \in ℕ A \leq B + (\frac{1}{n}))$
28		rpgtrecnn	$⊢ x \in ℝ^{+} \to \exists n \in ℕ \frac{1}{n} < x$
29	28	adantl	$⊢ ((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \to \exists n \in ℕ \frac{1}{n} < x$
30		nfra1	$⊢ Ⅎ n \forall n \in ℕ A \leq B + (\frac{1}{n})$
31	1 30	nfan	$⊢ Ⅎ n (φ \land \forall n \in ℕ A \leq B + (\frac{1}{n}))$
32		nfv	$⊢ Ⅎ n x \in ℝ^{+}$
33	31 32	nfan	$⊢ Ⅎ n ((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land x \in ℝ^{+})$
34		nfv	$⊢ Ⅎ n A \leq B + x$
35		simpll	$⊢ ((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land n \in ℕ) \to φ$
36		rspa	$⊢ (\forall n \in ℕ A \leq B + (\frac{1}{n}) \land n \in ℕ) \to A \leq B + (\frac{1}{n})$
37	36	adantll	$⊢ ((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land n \in ℕ) \to A \leq B + (\frac{1}{n})$
38	35 37	jca	$⊢ ((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land n \in ℕ) \to (φ \land A \leq B + (\frac{1}{n}))$
39	38	adantlr	$⊢ (((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \to (φ \land A \leq B + (\frac{1}{n}))$
40		simplr	$⊢ (((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \to x \in ℝ^{+}$
41		simpr	$⊢ (((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \to n \in ℕ$
42	2	ad4antr	$⊢ ((((φ \land A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to A \in ℝ^{*}$
43	3	adantr	$⊢ (φ \land x \in ℝ^{+}) \to B \in ℝ$
44		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
45	44	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
46	43 45	readdcld	$⊢ (φ \land x \in ℝ^{+}) \to B + x \in ℝ$
47	46	rexrd	$⊢ (φ \land x \in ℝ^{+}) \to B + x \in ℝ^{*}$
48	47	ad5ant13	$⊢ ((((φ \land A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to B + x \in ℝ^{*}$
49	11	ad5ant14	$⊢ ((((φ \land A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to B + (\frac{1}{n}) \in ℝ^{*}$
50		simp-4r	$⊢ ((((φ \land A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to A \leq B + (\frac{1}{n})$
51	8	ad2antlr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to \frac{1}{n} \in ℝ$
52	45	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to x \in ℝ$
53	43	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to B \in ℝ$
54		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to \frac{1}{n} < x$
55	51 52 53 54	ltadd2dd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to B + (\frac{1}{n}) < B + x$
56	55	adantl3r	$⊢ ((((φ \land A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to B + (\frac{1}{n}) < B + x$
57	42 49 48 50 56	xrlelttrd	$⊢ ((((φ \land A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to A < B + x$
58	42 48 57	xrltled	$⊢ ((((φ \land A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \land \frac{1}{n} < x) \to A \leq B + x$
59	58	ex	$⊢ (((φ \land A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \to (\frac{1}{n} < x \to A \leq B + x)$
60	39 40 41 59	syl21anc	$⊢ (((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \land n \in ℕ) \to (\frac{1}{n} < x \to A \leq B + x)$
61	60	ex	$⊢ ((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \to (n \in ℕ \to (\frac{1}{n} < x \to A \leq B + x))$
62	33 34 61	rexlimd	$⊢ ((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \to (\exists n \in ℕ \frac{1}{n} < x \to A \leq B + x)$
63	29 62	mpd	$⊢ ((φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \land x \in ℝ^{+}) \to A \leq B + x$
64	63	ralrimiva	$⊢ (φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \to \forall x \in ℝ^{+} A \leq B + x$
65		xralrple	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + x)$
66	2 3 65	syl2anc	$⊢ φ \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + x)$
67	66	adantr	$⊢ (φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + x)$
68	64 67	mpbird	$⊢ (φ \land \forall n \in ℕ A \leq B + (\frac{1}{n})) \to A \leq B$
69	68	ex	$⊢ φ \to (\forall n \in ℕ A \leq B + (\frac{1}{n}) \to A \leq B)$
70	27 69	impbid	$⊢ φ \to (A \leq B \leftrightarrow \forall n \in ℕ A \leq B + (\frac{1}{n}))$

Metamath Proof Explorer

Theorem xrralrecnnle

Proof