xrmax1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xrmax1		Structured version Visualization version GIF version

Theorem xrmax1 13192

Description: An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.)

**Assertion**
Ref	Expression
xrmax1	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))

**Proof of Theorem xrmax1**
Step	Hyp	Ref	Expression
1		xrleid 13167	. . . 4 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ 𝐴)
2		iffalse 4492	. . . . 5 ⊢ (¬ 𝐴 ≤ 𝐵 → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = 𝐴)
3	2	breq2d 5117	. . . 4 ⊢ (¬ 𝐴 ≤ 𝐵 → (𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴) ↔ 𝐴 ≤ 𝐴))
4	1, 3	syl5ibrcom 250	. . 3 ⊢ (𝐴 ∈ ℝ^* → (¬ 𝐴 ≤ 𝐵 → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)))
5		id 23	. . . 4 ⊢ (𝐴 ≤ 𝐵 → 𝐴 ≤ 𝐵)
6		iftrue 4489	. . . 4 ⊢ (𝐴 ≤ 𝐵 → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = 𝐵)
7	5, 6	breqtrrd 5133	. . 3 ⊢ (𝐴 ≤ 𝐵 → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
8	4, 7	pm2.61d2 183	. 2 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
9	8	adantr 485	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∈ wcel 2145 ifcif 4483 class class class wbr 5105 ℝ^*cxr 11230 ≤ cle 11232

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-pre-lttri 11162 ax-pre-lttrn 11163

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-po 5560 df-so 5561 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237

This theorem is referenced by: xrmaxlt 13198 xrmaxle 13200 max1 13202 limsupgre 15522 pnfnei 23338 ismbfd 25759 dvferm2lem 26106 mdegaddle 26192