This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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