Step |
Hyp |
Ref |
Expression |
1 |
|
xrmin1 |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 ) |
2 |
1
|
3adant1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 ) |
3 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → 𝐴 ∈ ℝ* ) |
4 |
|
ifcl |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∈ ℝ* ) |
5 |
4
|
3adant1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∈ ℝ* ) |
6 |
|
simp2 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → 𝐵 ∈ ℝ* ) |
7 |
|
xrletr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) ) |
8 |
3 5 6 7
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) ) |
9 |
2 8
|
mpan2d |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) → 𝐴 ≤ 𝐵 ) ) |
10 |
|
xrmin2 |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 ) |
11 |
10
|
3adant1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 ) |
12 |
|
xrletr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 ) → 𝐴 ≤ 𝐶 ) ) |
13 |
5 12
|
syld3an2 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 ) → 𝐴 ≤ 𝐶 ) ) |
14 |
11 13
|
mpan2d |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) → 𝐴 ≤ 𝐶 ) ) |
15 |
9 14
|
jcad |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) → ( 𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶 ) ) ) |
16 |
|
breq2 |
⊢ ( 𝐵 = if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) → ( 𝐴 ≤ 𝐵 ↔ 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ) ) |
17 |
|
breq2 |
⊢ ( 𝐶 = if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) → ( 𝐴 ≤ 𝐶 ↔ 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ) ) |
18 |
16 17
|
ifboth |
⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶 ) → 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ) |
19 |
15 18
|
impbid1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶 ) ) ) |