Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  infrpge Structured version   Visualization version   GIF version

Theorem infrpge 38508
 Description: The infimum of a non empty, bounded subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
Hypotheses
Ref Expression
infrpge.xph 𝑥𝜑
infrpge.a (𝜑𝐴 ⊆ ℝ*)
infrpge.an0 (𝜑𝐴 ≠ ∅)
infrpge.bnd (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑥𝑦)
infrpge.b (𝜑𝐵 ∈ ℝ+)
Assertion
Ref Expression
infrpge (𝜑 → ∃𝑧𝐴 𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑧,𝐴   𝑧,𝐵   𝜑,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem infrpge
StepHypRef Expression
1 infrpge.an0 . . . . . 6 (𝜑𝐴 ≠ ∅)
2 n0 3890 . . . . . . 7 (𝐴 ≠ ∅ ↔ ∃𝑧 𝑧𝐴)
32biimpi 205 . . . . . 6 (𝐴 ≠ ∅ → ∃𝑧 𝑧𝐴)
41, 3syl 17 . . . . 5 (𝜑 → ∃𝑧 𝑧𝐴)
54adantr 480 . . . 4 ((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) → ∃𝑧 𝑧𝐴)
6 nfv 1830 . . . . 5 𝑧(𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞)
7 simpr 476 . . . . . . 7 (((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) ∧ 𝑧𝐴) → 𝑧𝐴)
8 infrpge.a . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ*)
98adantr 480 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → 𝐴 ⊆ ℝ*)
10 simpr 476 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → 𝑧𝐴)
119, 10sseldd 3569 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑧 ∈ ℝ*)
12 pnfge 11840 . . . . . . . . . 10 (𝑧 ∈ ℝ*𝑧 ≤ +∞)
1311, 12syl 17 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑧 ≤ +∞)
1413adantlr 747 . . . . . . . 8 (((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) ∧ 𝑧𝐴) → 𝑧 ≤ +∞)
15 oveq1 6556 . . . . . . . . . . 11 (inf(𝐴, ℝ*, < ) = +∞ → (inf(𝐴, ℝ*, < ) +𝑒 𝐵) = (+∞ +𝑒 𝐵))
1615adantl 481 . . . . . . . . . 10 ((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) → (inf(𝐴, ℝ*, < ) +𝑒 𝐵) = (+∞ +𝑒 𝐵))
17 infrpge.b . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ+)
1817rpxrd 11749 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ*)
1917rpred 11748 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ)
20 renemnf 9967 . . . . . . . . . . . . 13 (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
2119, 20syl 17 . . . . . . . . . . . 12 (𝜑𝐵 ≠ -∞)
22 xaddpnf2 11932 . . . . . . . . . . . 12 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
2318, 21, 22syl2anc 691 . . . . . . . . . . 11 (𝜑 → (+∞ +𝑒 𝐵) = +∞)
2423adantr 480 . . . . . . . . . 10 ((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) → (+∞ +𝑒 𝐵) = +∞)
2516, 24eqtr2d 2645 . . . . . . . . 9 ((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) → +∞ = (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
2625adantr 480 . . . . . . . 8 (((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) ∧ 𝑧𝐴) → +∞ = (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
2714, 26breqtrd 4609 . . . . . . 7 (((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) ∧ 𝑧𝐴) → 𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
287, 27jca 553 . . . . . 6 (((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) ∧ 𝑧𝐴) → (𝑧𝐴𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵)))
2928ex 449 . . . . 5 ((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) → (𝑧𝐴 → (𝑧𝐴𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵))))
306, 29eximd 2072 . . . 4 ((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) → (∃𝑧 𝑧𝐴 → ∃𝑧(𝑧𝐴𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵))))
315, 30mpd 15 . . 3 ((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) → ∃𝑧(𝑧𝐴𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵)))
32 df-rex 2902 . . 3 (∃𝑧𝐴 𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ↔ ∃𝑧(𝑧𝐴𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵)))
3331, 32sylibr 223 . 2 ((𝜑 ∧ inf(𝐴, ℝ*, < ) = +∞) → ∃𝑧𝐴 𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
34 simpl 472 . . . 4 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → 𝜑)
35 infrpge.bnd . . . . . . . . 9 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑥𝑦)
36 infrpge.xph . . . . . . . . . 10 𝑥𝜑
37 nfv 1830 . . . . . . . . . 10 𝑥-∞ < inf(𝐴, ℝ*, < )
38 mnfxr 9975 . . . . . . . . . . . . 13 -∞ ∈ ℝ*
3938a1i 11 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑥𝑦) → -∞ ∈ ℝ*)
40 rexr 9964 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
41403ad2ant2 1076 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑥𝑦) → 𝑥 ∈ ℝ*)
42 infxrcl 12035 . . . . . . . . . . . . . 14 (𝐴 ⊆ ℝ* → inf(𝐴, ℝ*, < ) ∈ ℝ*)
438, 42syl 17 . . . . . . . . . . . . 13 (𝜑 → inf(𝐴, ℝ*, < ) ∈ ℝ*)
44433ad2ant1 1075 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑥𝑦) → inf(𝐴, ℝ*, < ) ∈ ℝ*)
45 mnflt 11833 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → -∞ < 𝑥)
46453ad2ant2 1076 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑥𝑦) → -∞ < 𝑥)
47 simp3 1056 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑥𝑦) → ∀𝑦𝐴 𝑥𝑦)
488adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → 𝐴 ⊆ ℝ*)
4940adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ*)
50 infxrgelb 12037 . . . . . . . . . . . . . . 15 ((𝐴 ⊆ ℝ*𝑥 ∈ ℝ*) → (𝑥 ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑦𝐴 𝑥𝑦))
5148, 49, 50syl2anc 691 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → (𝑥 ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑦𝐴 𝑥𝑦))
52513adant3 1074 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑥𝑦) → (𝑥 ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑦𝐴 𝑥𝑦))
5347, 52mpbird 246 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑥𝑦) → 𝑥 ≤ inf(𝐴, ℝ*, < ))
5439, 41, 44, 46, 53xrltletrd 11868 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ ∧ ∀𝑦𝐴 𝑥𝑦) → -∞ < inf(𝐴, ℝ*, < ))
55543exp 1256 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℝ → (∀𝑦𝐴 𝑥𝑦 → -∞ < inf(𝐴, ℝ*, < ))))
5636, 37, 55rexlimd 3008 . . . . . . . . 9 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑥𝑦 → -∞ < inf(𝐴, ℝ*, < )))
5735, 56mpd 15 . . . . . . . 8 (𝜑 → -∞ < inf(𝐴, ℝ*, < ))
5857adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → -∞ < inf(𝐴, ℝ*, < ))
59 neqne 2790 . . . . . . . . 9 (¬ inf(𝐴, ℝ*, < ) = +∞ → inf(𝐴, ℝ*, < ) ≠ +∞)
6059adantl 481 . . . . . . . 8 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → inf(𝐴, ℝ*, < ) ≠ +∞)
6143adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → inf(𝐴, ℝ*, < ) ∈ ℝ*)
6260, 61nepnfltpnf 38499 . . . . . . 7 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → inf(𝐴, ℝ*, < ) < +∞)
6358, 62jca 553 . . . . . 6 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → (-∞ < inf(𝐴, ℝ*, < ) ∧ inf(𝐴, ℝ*, < ) < +∞))
64 xrrebnd 11873 . . . . . . . 8 (inf(𝐴, ℝ*, < ) ∈ ℝ* → (inf(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < inf(𝐴, ℝ*, < ) ∧ inf(𝐴, ℝ*, < ) < +∞)))
6543, 64syl 17 . . . . . . 7 (𝜑 → (inf(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < inf(𝐴, ℝ*, < ) ∧ inf(𝐴, ℝ*, < ) < +∞)))
6665adantr 480 . . . . . 6 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → (inf(𝐴, ℝ*, < ) ∈ ℝ ↔ (-∞ < inf(𝐴, ℝ*, < ) ∧ inf(𝐴, ℝ*, < ) < +∞)))
6763, 66mpbird 246 . . . . 5 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → inf(𝐴, ℝ*, < ) ∈ ℝ)
68 simpr 476 . . . . . . . 8 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → inf(𝐴, ℝ*, < ) ∈ ℝ)
6917adantr 480 . . . . . . . 8 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ∈ ℝ+)
7068, 69ltaddrpd 11781 . . . . . . 7 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → inf(𝐴, ℝ*, < ) < (inf(𝐴, ℝ*, < ) + 𝐵))
7119adantr 480 . . . . . . . . 9 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → 𝐵 ∈ ℝ)
72 rexadd 11937 . . . . . . . . 9 ((inf(𝐴, ℝ*, < ) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (inf(𝐴, ℝ*, < ) +𝑒 𝐵) = (inf(𝐴, ℝ*, < ) + 𝐵))
7368, 71, 72syl2anc 691 . . . . . . . 8 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → (inf(𝐴, ℝ*, < ) +𝑒 𝐵) = (inf(𝐴, ℝ*, < ) + 𝐵))
7473eqcomd 2616 . . . . . . 7 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → (inf(𝐴, ℝ*, < ) + 𝐵) = (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
7570, 74breqtrd 4609 . . . . . 6 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → inf(𝐴, ℝ*, < ) < (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
7643adantr 480 . . . . . . 7 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → inf(𝐴, ℝ*, < ) ∈ ℝ*)
7743, 18xaddcld 12003 . . . . . . . 8 (𝜑 → (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ∈ ℝ*)
7877adantr 480 . . . . . . 7 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ∈ ℝ*)
79 xrltnle 9984 . . . . . . 7 ((inf(𝐴, ℝ*, < ) ∈ ℝ* ∧ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ∈ ℝ*) → (inf(𝐴, ℝ*, < ) < (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ↔ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < )))
8076, 78, 79syl2anc 691 . . . . . 6 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → (inf(𝐴, ℝ*, < ) < (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ↔ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < )))
8175, 80mpbid 221 . . . . 5 ((𝜑 ∧ inf(𝐴, ℝ*, < ) ∈ ℝ) → ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < ))
8234, 67, 81syl2anc 691 . . . 4 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < ))
83 simpr 476 . . . . . 6 ((𝜑 ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < )) → ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < ))
84 simpl 472 . . . . . . 7 ((𝜑 ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < )) → 𝜑)
85 infxrgelb 12037 . . . . . . . 8 ((𝐴 ⊆ ℝ* ∧ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ∈ ℝ*) → ((inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑧𝐴 (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧))
868, 77, 85syl2anc 691 . . . . . . 7 (𝜑 → ((inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑧𝐴 (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧))
8784, 86syl 17 . . . . . 6 ((𝜑 ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < )) → ((inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑧𝐴 (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧))
8883, 87mtbid 313 . . . . 5 ((𝜑 ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < )) → ¬ ∀𝑧𝐴 (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧)
89 rexnal 2978 . . . . 5 (∃𝑧𝐴 ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧 ↔ ¬ ∀𝑧𝐴 (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧)
9088, 89sylibr 223 . . . 4 ((𝜑 ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ inf(𝐴, ℝ*, < )) → ∃𝑧𝐴 ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧)
9134, 82, 90syl2anc 691 . . 3 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → ∃𝑧𝐴 ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧)
9211adantr 480 . . . . . . 7 (((𝜑𝑧𝐴) ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧) → 𝑧 ∈ ℝ*)
9377ad2antrr 758 . . . . . . 7 (((𝜑𝑧𝐴) ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧) → (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ∈ ℝ*)
94 simpr 476 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧) → ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧)
95 xrltnle 9984 . . . . . . . . 9 ((𝑧 ∈ ℝ* ∧ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ∈ ℝ*) → (𝑧 < (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ↔ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧))
9692, 93, 95syl2anc 691 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧) → (𝑧 < (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ↔ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧))
9794, 96mpbird 246 . . . . . . 7 (((𝜑𝑧𝐴) ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧) → 𝑧 < (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
9892, 93, 97xrltled 38427 . . . . . 6 (((𝜑𝑧𝐴) ∧ ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧) → 𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
9998ex 449 . . . . 5 ((𝜑𝑧𝐴) → (¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵)))
10099adantlr 747 . . . 4 (((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) ∧ 𝑧𝐴) → (¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵)))
101100reximdva 3000 . . 3 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → (∃𝑧𝐴 ¬ (inf(𝐴, ℝ*, < ) +𝑒 𝐵) ≤ 𝑧 → ∃𝑧𝐴 𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵)))
10291, 101mpd 15 . 2 ((𝜑 ∧ ¬ inf(𝐴, ℝ*, < ) = +∞) → ∃𝑧𝐴 𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
10333, 102pm2.61dan 828 1 (𝜑 → ∃𝑧𝐴 𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583  (class class class)co 6549  infcinf 8230  ℝcr 9814   + caddc 9818  +∞cpnf 9950  -∞cmnf 9951  ℝ*cxr 9952   < clt 9953   ≤ cle 9954  ℝ+crp 11708   +𝑒 cxad 11820 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-rp 11709  df-xadd 11823 This theorem is referenced by:  infleinf  38529  ovnlerp  39452
 Copyright terms: Public domain W3C validator