Theorem xrmaxiflemab 11932

Description: Lemma for xrmaxif 11936. A variation of xrmaxleim 11929- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 26-Apr-2023.)

Hypotheses

Ref	Expression
xrmaxiflemab.a	⊢ (𝜑 → 𝐴 ∈ ℝ*)
xrmaxiflemab.b	⊢ (𝜑 → 𝐵 ∈ ℝ*)
xrmaxiflemab.ab	⊢ (𝜑 → 𝐴 < 𝐵)

Assertion

Ref	Expression
xrmaxiflemab	⊢ (𝜑 → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)

Proof of Theorem xrmaxiflemab

Step	Hyp	Ref	Expression
1		simpr 110	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = +∞) → 𝐵 = +∞)
2	1	iftrued 3629	. . 3 ⊢ ((𝜑 ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = +∞)
3	2, 1	eqtr4d 2268	. 2 ⊢ ((𝜑 ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)
4		simpr 110	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → ¬ 𝐵 = +∞)
5	4	iffalsed 3632	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))))
6		xrmaxiflemab.ab	. . . . . . 7 ⊢ (𝜑 → 𝐴 < 𝐵)
7	6	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 < 𝐵)
8		simpr 110	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐵 = -∞)
9	7, 8	breqtrd 4135	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 < -∞)
10		xrmaxiflemab.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
11		nltmnf 10121	. . . . . . 7 ⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)
12	10, 11	syl 14	. . . . . 6 ⊢ (𝜑 → ¬ 𝐴 < -∞)
13	12	ad2antrr 488	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
14	9, 13	pm2.21dd 625	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐵)
15		simpr 110	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → ¬ 𝐵 = -∞)
16	15	iffalsed 3632	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
17		simpr 110	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → 𝐴 = +∞)
18	6	ad3antrrr 492	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → 𝐴 < 𝐵)
19	17, 18	eqbrtrrd 4133	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → +∞ < 𝐵)
20		xrmaxiflemab.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
21		pnfnlt 10120	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ* → ¬ +∞ < 𝐵)
22	20, 21	syl 14	. . . . . . . 8 ⊢ (𝜑 → ¬ +∞ < 𝐵)
23	22	ad3antrrr 492	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → ¬ +∞ < 𝐵)
24	19, 23	pm2.21dd 625	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = 𝐵)
25		simpr 110	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → ¬ 𝐴 = +∞)
26	25	iffalsed 3632	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
27		simpr 110	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ 𝐴 = -∞) → 𝐴 = -∞)
28	27	iftrued 3629	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = 𝐵)
29		simpr 110	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐴 = -∞)
30	29	iffalsed 3632	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = sup({𝐴, 𝐵}, ℝ, < ))
31	25	adantr 276	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐴 = +∞)
32		elxr 10109	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
33	10, 32	sylib 122	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
34	33	ad4antr 494	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
35	31, 29, 34	ecase23d 1387	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ∈ ℝ)
36	4	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐵 = +∞)
37	15	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐵 = -∞)
38		elxr 10109	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
39	20, 38	sylib 122	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
40	39	ad4antr 494	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
41	36, 37, 40	ecase23d 1387	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐵 ∈ ℝ)
42	35, 41	jca 306	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
43	6	ad4antr 494	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 < 𝐵)
44	35, 41, 43	ltled 8392	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ≤ 𝐵)
45		maxleim 11890	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵))
46	42, 44, 45	sylc 62	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵)
47	30, 46	eqtrd 2265	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = 𝐵)
48		xrmnfdc 10176	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ* → DECID 𝐴 = -∞)
49		exmiddc 844	. . . . . . . . . 10 ⊢ (DECID 𝐴 = -∞ → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
50	10, 48, 49	3syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
51	50	ad3antrrr 492	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
52	28, 47, 51	mpjaodan 806	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = 𝐵)
53	26, 52	eqtrd 2265	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = 𝐵)
54		xrpnfdc 10175	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → DECID 𝐴 = +∞)
55		exmiddc 844	. . . . . . . 8 ⊢ (DECID 𝐴 = +∞ → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
56	10, 54, 55	3syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
57	56	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
58	24, 53, 57	mpjaodan 806	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = 𝐵)
59	16, 58	eqtrd 2265	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐵)
60		xrmnfdc 10176	. . . . . 6 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = -∞)
61		exmiddc 844	. . . . . 6 ⊢ (DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
62	20, 60, 61	3syl 17	. . . . 5 ⊢ (𝜑 → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
63	62	adantr 276	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
64	14, 59, 63	mpjaodan 806	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐵)
65	5, 64	eqtrd 2265	. 2 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)
66		xrpnfdc 10175	. . 3 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = +∞)
67		exmiddc 844	. . 3 ⊢ (DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
68	20, 66, 67	3syl 17	. 2 ⊢ (𝜑 → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
69	3, 65, 68	mpjaodan 806	1 ⊢ (𝜑 → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 716  DECID wdc 842   ∨ w3o 1004   = wceq 1398   ∈ wcel 2203  ifcif 3620  {cpr 3690   class class class wbr 4109  supcsup 7273  ℝcr 8126  +∞cpnf 8305  -∞cmnf 8306  ℝ^*cxr 8307   < clt 8308   ≤ cle 8309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-cnex 8218  ax-resscn 8219  ax-pre-ltirr 8239  ax-pre-lttrn 8241  ax-pre-apti 8242

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rmo 2528  df-rab 2529  df-v 2815  df-sbc 3043  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-if 3621  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-xp 4755  df-cnv 4757  df-iota 5312  df-riota 6003  df-sup 7275  df-pnf 8310  df-mnf 8311  df-xr 8312  df-ltxr 8313  df-le 8314

This theorem is referenced by:  xrmaxiflemlub  11933