xrpnf

Description: An extended real is plus infinity iff it's larger than all real numbers. (Contributed by Glauco Siliprandi, 13-Feb-2022)

		Ref	Expression
	Assertion	xrpnf	$⊢ A \in ℝ^{*} \to (A = +∞ \leftrightarrow \forall x \in ℝ x \leq A)$

Proof

Step	Hyp	Ref	Expression
1		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
2	1	adantl	$⊢ (A = +∞ \land x \in ℝ) \to x \in ℝ^{*}$
3		id	$⊢ A = +∞ \to A = +∞$
4		pnfxr	$⊢ +∞ \in ℝ^{*}$
5	4	a1i	$⊢ A = +∞ \to +∞ \in ℝ^{*}$
6	3 5	eqeltrd	$⊢ A = +∞ \to A \in ℝ^{*}$
7	6	adantr	$⊢ (A = +∞ \land x \in ℝ) \to A \in ℝ^{*}$
8		ltpnf	$⊢ x \in ℝ \to x < +∞$
9	8	adantl	$⊢ (A = +∞ \land x \in ℝ) \to x < +∞$
10		simpl	$⊢ (A = +∞ \land x \in ℝ) \to A = +∞$
11	9 10	breqtrrd	$⊢ (A = +∞ \land x \in ℝ) \to x < A$
12	2 7 11	xrltled	$⊢ (A = +∞ \land x \in ℝ) \to x \leq A$
13	12	ralrimiva	$⊢ A = +∞ \to \forall x \in ℝ x \leq A$
14	13	adantl	$⊢ (A \in ℝ^{*} \land A = +∞) \to \forall x \in ℝ x \leq A$
15		simpll	$⊢ ((A \in ℝ^{} \land \forall x \in ℝ x \leq A) \land A < +∞) \to A \in ℝ^{}$
16		0red	$⊢ \forall x \in ℝ x \leq A \to 0 \in ℝ$
17		id	$⊢ \forall x \in ℝ x \leq A \to \forall x \in ℝ x \leq A$
18		breq1	$⊢ x = 0 \to (x \leq A \leftrightarrow 0 \leq A)$
19	18	rspcva	$⊢ (0 \in ℝ \land \forall x \in ℝ x \leq A) \to 0 \leq A$
20	16 17 19	syl2anc	$⊢ \forall x \in ℝ x \leq A \to 0 \leq A$
21	20	adantr	$⊢ (\forall x \in ℝ x \leq A \land A = −∞) \to 0 \leq A$
22		simpr	$⊢ (\forall x \in ℝ x \leq A \land A = −∞) \to A = −∞$
23	21 22	breqtrd	$⊢ (\forall x \in ℝ x \leq A \land A = −∞) \to 0 \leq −∞$
24	23	adantll	$⊢ ((A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \land A = −∞) \to 0 \leq −∞$
25		mnflt0	$⊢ −∞ < 0$
26		mnfxr	$⊢ −∞ \in ℝ^{*}$
27		0xr	$⊢ 0 \in ℝ^{*}$
28		xrltnle	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{}) \to (−∞ < 0 \leftrightarrow \neg 0 \leq −∞)$
29	26 27 28	mp2an	$⊢ −∞ < 0 \leftrightarrow \neg 0 \leq −∞$
30	25 29	mpbi	$⊢ \neg 0 \leq −∞$
31	30	a1i	$⊢ ((A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \land A = −∞) \to \neg 0 \leq −∞$
32	24 31	pm2.65da	$⊢ (A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \to \neg A = −∞$
33	32	neqned	$⊢ (A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \to A \neq −∞$
34	33	adantr	$⊢ ((A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \land A < +∞) \to A \neq −∞$
35		simpl	$⊢ (A \in ℝ^{} \land A < +∞) \to A \in ℝ^{}$
36	4	a1i	$⊢ (A \in ℝ^{} \land A < +∞) \to +∞ \in ℝ^{}$
37		simpr	$⊢ (A \in ℝ^{*} \land A < +∞) \to A < +∞$
38	35 36 37	xrltned	$⊢ (A \in ℝ^{*} \land A < +∞) \to A \neq +∞$
39	38	adantlr	$⊢ ((A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \land A < +∞) \to A \neq +∞$
40	15 34 39	xrred	$⊢ ((A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \land A < +∞) \to A \in ℝ$
41		peano2re	$⊢ A \in ℝ \to A + 1 \in ℝ$
42	41	adantl	$⊢ (\forall x \in ℝ x \leq A \land A \in ℝ) \to A + 1 \in ℝ$
43		simpl	$⊢ (\forall x \in ℝ x \leq A \land A \in ℝ) \to \forall x \in ℝ x \leq A$
44		breq1	$⊢ x = A + 1 \to (x \leq A \leftrightarrow A + 1 \leq A)$
45	44	rspcva	$⊢ (A + 1 \in ℝ \land \forall x \in ℝ x \leq A) \to A + 1 \leq A$
46	42 43 45	syl2anc	$⊢ (\forall x \in ℝ x \leq A \land A \in ℝ) \to A + 1 \leq A$
47		ltp1	$⊢ A \in ℝ \to A < A + 1$
48		id	$⊢ A \in ℝ \to A \in ℝ$
49	48 41	ltnled	$⊢ A \in ℝ \to (A < A + 1 \leftrightarrow \neg A + 1 \leq A)$
50	47 49	mpbid	$⊢ A \in ℝ \to \neg A + 1 \leq A$
51	50	adantl	$⊢ (\forall x \in ℝ x \leq A \land A \in ℝ) \to \neg A + 1 \leq A$
52	46 51	pm2.65da	$⊢ \forall x \in ℝ x \leq A \to \neg A \in ℝ$
53	52	ad2antlr	$⊢ ((A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \land A < +∞) \to \neg A \in ℝ$
54	40 53	pm2.65da	$⊢ (A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \to \neg A < +∞$
55		nltpnft	$⊢ A \in ℝ^{*} \to (A = +∞ \leftrightarrow \neg A < +∞)$
56	55	adantr	$⊢ (A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \to (A = +∞ \leftrightarrow \neg A < +∞)$
57	54 56	mpbird	$⊢ (A \in ℝ^{*} \land \forall x \in ℝ x \leq A) \to A = +∞$
58	14 57	impbida	$⊢ A \in ℝ^{*} \to (A = +∞ \leftrightarrow \forall x \in ℝ x \leq A)$

Metamath Proof Explorer

Theorem xrpnf

Proof