Theorem xrmaxiflemab 11016

Description: Lemma for xrmaxif 11020. A variation of xrmaxleim 11013- 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 109	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = +∞) → 𝐵 = +∞)
2	1	iftrued 3481	. . 3 ⊢ ((𝜑 ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = +∞)
3	2, 1	eqtr4d 2175	. 2 ⊢ ((𝜑 ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)
4		simpr 109	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → ¬ 𝐵 = +∞)
5	4	iffalsed 3484	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))))
6		xrmaxiflemab.ab	. . . . . . 7 ⊢ (𝜑 → 𝐴 < 𝐵)
7	6	ad2antrr 479	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 < 𝐵)
8		simpr 109	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐵 = -∞)
9	7, 8	breqtrd 3954	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 < -∞)
10		xrmaxiflemab.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
11		nltmnf 9574	. . . . . . 7 ⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)
12	10, 11	syl 14	. . . . . 6 ⊢ (𝜑 → ¬ 𝐴 < -∞)
13	12	ad2antrr 479	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
14	9, 13	pm2.21dd 609	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐵)
15		simpr 109	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → ¬ 𝐵 = -∞)
16	15	iffalsed 3484	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
17		simpr 109	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → 𝐴 = +∞)
18	6	ad3antrrr 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → 𝐴 < 𝐵)
19	17, 18	eqbrtrrd 3952	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → +∞ < 𝐵)
20		xrmaxiflemab.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
21		pnfnlt 9573	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ* → ¬ +∞ < 𝐵)
22	20, 21	syl 14	. . . . . . . 8 ⊢ (𝜑 → ¬ +∞ < 𝐵)
23	22	ad3antrrr 483	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → ¬ +∞ < 𝐵)
24	19, 23	pm2.21dd 609	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = 𝐵)
25		simpr 109	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → ¬ 𝐴 = +∞)
26	25	iffalsed 3484	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
27		simpr 109	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ 𝐴 = -∞) → 𝐴 = -∞)
28	27	iftrued 3481	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = 𝐵)
29		simpr 109	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐴 = -∞)
30	29	iffalsed 3484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = sup({𝐴, 𝐵}, ℝ, < ))
31	25	adantr 274	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐴 = +∞)
32		elxr 9563	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
33	10, 32	sylib 121	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
34	33	ad4antr 485	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
35	31, 29, 34	ecase23d 1328	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ∈ ℝ)
36	4	ad3antrrr 483	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐵 = +∞)
37	15	ad2antrr 479	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐵 = -∞)
38		elxr 9563	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
39	20, 38	sylib 121	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
40	39	ad4antr 485	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
41	36, 37, 40	ecase23d 1328	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐵 ∈ ℝ)
42	35, 41	jca 304	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
43	6	ad4antr 485	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 < 𝐵)
44	35, 41, 43	ltled 7881	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ≤ 𝐵)
45		maxleim 10977	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵))
46	42, 44, 45	sylc 62	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵)
47	30, 46	eqtrd 2172	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = 𝐵)
48		xrmnfdc 9626	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ* → DECID 𝐴 = -∞)
49		exmiddc 821	. . . . . . . . . 10 ⊢ (DECID 𝐴 = -∞ → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
50	10, 48, 49	3syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
51	50	ad3antrrr 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
52	28, 47, 51	mpjaodan 787	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = 𝐵)
53	26, 52	eqtrd 2172	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = 𝐵)
54		xrpnfdc 9625	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → DECID 𝐴 = +∞)
55		exmiddc 821	. . . . . . . 8 ⊢ (DECID 𝐴 = +∞ → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
56	10, 54, 55	3syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
57	56	ad2antrr 479	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
58	24, 53, 57	mpjaodan 787	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = 𝐵)
59	16, 58	eqtrd 2172	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐵)
60		xrmnfdc 9626	. . . . . 6 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = -∞)
61		exmiddc 821	. . . . . 6 ⊢ (DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
62	20, 60, 61	3syl 17	. . . . 5 ⊢ (𝜑 → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
63	62	adantr 274	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
64	14, 59, 63	mpjaodan 787	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐵)
65	5, 64	eqtrd 2172	. 2 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)
66		xrpnfdc 9625	. . 3 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = +∞)
67		exmiddc 821	. . 3 ⊢ (DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
68	20, 66, 67	3syl 17	. 2 ⊢ (𝜑 → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
69	3, 65, 68	mpjaodan 787	1 ⊢ (𝜑 → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∨ wo 697  DECID wdc 819   ∨ w3o 961   = wceq 1331   ∈ wcel 1480  ifcif 3474  {cpr 3528   class class class wbr 3929  supcsup 6869  ℝcr 7619  +∞cpnf 7797  -∞cmnf 7798  ℝ^*cxr 7799   < clt 7800   ≤ cle 7801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-cnex 7711  ax-resscn 7712  ax-pre-ltirr 7732  ax-pre-lttrn 7734  ax-pre-apti 7735

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-opab 3990  df-xp 4545  df-cnv 4547  df-iota 5088  df-riota 5730  df-sup 6871  df-pnf 7802  df-mnf 7803  df-xr 7804  df-ltxr 7805  df-le 7806

This theorem is referenced by:  xrmaxiflemlub  11017