Theorem 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 \left(A=\mathrm{+\infty }\leftrightarrow \forall x\in ℝx\le A\right)$$

Proof

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