Theorem xrmaxiflemab 11773

Description: Lemma for xrmaxif 11777. A variation of xrmaxleim 11770- 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 3609	. . 3 ⊢ ((𝜑 ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = +∞)
3	2, 1	eqtr4d 2265	. 2 ⊢ ((𝜑 ∧ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)
4		simpr 110	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → ¬ 𝐵 = +∞)
5	4	iffalsed 3612	. . 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 4109	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → 𝐴 < -∞)
10		xrmaxiflemab.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
11		nltmnf 9996	. . . . . . 7 ⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)
12	10, 11	syl 14	. . . . . 6 ⊢ (𝜑 → ¬ 𝐴 < -∞)
13	12	ad2antrr 488	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
14	9, 13	pm2.21dd 623	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐵)
15		simpr 110	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → ¬ 𝐵 = -∞)
16	15	iffalsed 3612	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))
17		simpr 110	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → 𝐴 = +∞)
18	6	ad3antrrr 492	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → 𝐴 < 𝐵)
19	17, 18	eqbrtrrd 4107	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → +∞ < 𝐵)
20		xrmaxiflemab.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
21		pnfnlt 9995	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ* → ¬ +∞ < 𝐵)
22	20, 21	syl 14	. . . . . . . 8 ⊢ (𝜑 → ¬ +∞ < 𝐵)
23	22	ad3antrrr 492	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → ¬ +∞ < 𝐵)
24	19, 23	pm2.21dd 623	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = 𝐵)
25		simpr 110	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → ¬ 𝐴 = +∞)
26	25	iffalsed 3612	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))
27		simpr 110	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ 𝐴 = -∞) → 𝐴 = -∞)
28	27	iftrued 3609	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = 𝐵)
29		simpr 110	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐴 = -∞)
30	29	iffalsed 3612	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = sup({𝐴, 𝐵}, ℝ, < ))
31	25	adantr 276	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐴 = +∞)
32		elxr 9984	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
33	10, 32	sylib 122	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
34	33	ad4antr 494	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
35	31, 29, 34	ecase23d 1384	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ∈ ℝ)
36	4	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐵 = +∞)
37	15	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → ¬ 𝐵 = -∞)
38		elxr 9984	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
39	20, 38	sylib 122	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
40	39	ad4antr 494	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
41	36, 37, 40	ecase23d 1384	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐵 ∈ ℝ)
42	35, 41	jca 306	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
43	6	ad4antr 494	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 < 𝐵)
44	35, 41, 43	ltled 8276	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → 𝐴 ≤ 𝐵)
45		maxleim 11731	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵))
46	42, 44, 45	sylc 62	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵)
47	30, 46	eqtrd 2262	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) ∧ ¬ 𝐴 = -∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = 𝐵)
48		xrmnfdc 10051	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ* → DECID 𝐴 = -∞)
49		exmiddc 841	. . . . . . . . . 10 ⊢ (DECID 𝐴 = -∞ → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
50	10, 48, 49	3syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
51	50	ad3antrrr 492	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → (𝐴 = -∞ ∨ ¬ 𝐴 = -∞))
52	28, 47, 51	mpjaodan 803	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )) = 𝐵)
53	26, 52	eqtrd 2262	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) ∧ ¬ 𝐴 = +∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = 𝐵)
54		xrpnfdc 10050	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → DECID 𝐴 = +∞)
55		exmiddc 841	. . . . . . . 8 ⊢ (DECID 𝐴 = +∞ → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
56	10, 54, 55	3syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
57	56	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞))
58	24, 53, 57	mpjaodan 803	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))) = 𝐵)
59	16, 58	eqtrd 2262	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐵 = +∞) ∧ ¬ 𝐵 = -∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐵)
60		xrmnfdc 10051	. . . . . 6 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = -∞)
61		exmiddc 841	. . . . . 6 ⊢ (DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
62	20, 60, 61	3syl 17	. . . . 5 ⊢ (𝜑 → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
63	62	adantr 276	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
64	14, 59, 63	mpjaodan 803	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < )))) = 𝐵)
65	5, 64	eqtrd 2262	. 2 ⊢ ((𝜑 ∧ ¬ 𝐵 = +∞) → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)
66		xrpnfdc 10050	. . 3 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = +∞)
67		exmiddc 841	. . 3 ⊢ (DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
68	20, 66, 67	3syl 17	. 2 ⊢ (𝜑 → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
69	3, 65, 68	mpjaodan 803	1 ⊢ (𝜑 → if(𝐵 = +∞, +∞, if(𝐵 = -∞, 𝐴, if(𝐴 = +∞, +∞, if(𝐴 = -∞, 𝐵, sup({𝐴, 𝐵}, ℝ, < ))))) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 713  DECID wdc 839   ∨ w3o 1001   = wceq 1395   ∈ wcel 2200  ifcif 3602  {cpr 3667   class class class wbr 4083  supcsup 7160  ℝcr 8009  +∞cpnf 8189  -∞cmnf 8190  ℝ^*cxr 8191   < clt 8192   ≤ cle 8193

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8101  ax-resscn 8102  ax-pre-ltirr 8122  ax-pre-lttrn 8124  ax-pre-apti 8125

This theorem depends on definitions:  df-bi 117  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-if 3603  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-xp 4725  df-cnv 4727  df-iota 5278  df-riota 5960  df-sup 7162  df-pnf 8194  df-mnf 8195  df-xr 8196  df-ltxr 8197  df-le 8198

This theorem is referenced by:  xrmaxiflemlub  11774