Metamath Proof Explorer

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 e. RR* -> ( A = +oo <-> A. x e. RR x <_ A ) )

Proof

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