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	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = +∞ ↔ ∀ 𝑥 ∈ ℝ 𝑥 ≤ 𝐴 ) )

Proof

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