Metamath Proof Explorer


Theorem infxrre

Description: The real and extended real infima match when the real infimum exists. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infxrre A A x y A x y inf A * < = inf A <

Proof

Step Hyp Ref Expression
1 simp1 A A x y A x y A
2 ressxr *
3 1 2 sstrdi A A x y A x y A *
4 infxrcl A * inf A * < *
5 3 4 syl A A x y A x y inf A * < *
6 infrecl A A x y A x y inf A <
7 6 rexrd A A x y A x y inf A < *
8 5 xrleidd A A x y A x y inf A * < inf A * <
9 infxrgelb A * inf A * < * inf A * < inf A * < x A inf A * < x
10 3 5 9 syl2anc A A x y A x y inf A * < inf A * < x A inf A * < x
11 simp2 A A x y A x y A
12 n0 A z z A
13 11 12 sylib A A x y A x y z z A
14 5 adantr A A x y A x y z A inf A * < *
15 1 sselda A A x y A x y z A z
16 mnfxr −∞ *
17 16 a1i A A x y A x y −∞ *
18 6 mnfltd A A x y A x y −∞ < inf A <
19 6 leidd A A x y A x y inf A < inf A <
20 infregelb A A x y A x y inf A < inf A < inf A < x A inf A < x
21 6 20 mpdan A A x y A x y inf A < inf A < x A inf A < x
22 infxrgelb A * inf A < * inf A < inf A * < x A inf A < x
23 3 7 22 syl2anc A A x y A x y inf A < inf A * < x A inf A < x
24 21 23 bitr4d A A x y A x y inf A < inf A < inf A < inf A * <
25 19 24 mpbid A A x y A x y inf A < inf A * <
26 17 7 5 18 25 xrltletrd A A x y A x y −∞ < inf A * <
27 26 adantr A A x y A x y z A −∞ < inf A * <
28 infxrlb A * z A inf A * < z
29 3 28 sylan A A x y A x y z A inf A * < z
30 xrre inf A * < * z −∞ < inf A * < inf A * < z inf A * <
31 14 15 27 29 30 syl22anc A A x y A x y z A inf A * <
32 13 31 exlimddv A A x y A x y inf A * <
33 infregelb A A x y A x y inf A * < inf A * < inf A < x A inf A * < x
34 32 33 mpdan A A x y A x y inf A * < inf A < x A inf A * < x
35 10 34 bitr4d A A x y A x y inf A * < inf A * < inf A * < inf A <
36 8 35 mpbid A A x y A x y inf A * < inf A <
37 5 7 36 25 xrletrid A A x y A x y inf A * < = inf A <