Metamath Proof Explorer

Theorem iocinif

Description: Relate intersection of two open-below, closed-above intervals with the same upper bound with a conditional construct. (Contributed by Thierry Arnoux, 7-Aug-2017)

Ref Expression
Assertion iocinif ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→AC∩BC=ifA<BBCAC

Proof

Step Hyp Ref Expression
1 exmid ⊢A<B∨¬A<B
2 xrltle ⊢A∈ℝ*∧B∈ℝ*→A<B→A≤B
3 2 imp ⊢A∈ℝ*∧B∈ℝ*∧A<B→A≤B
4 3 3adantl3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B→A≤B
5 iocinioc2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A≤B→AC∩BC=BC
6 4 5 syldan ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B→AC∩BC=BC
7 6 ex ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A<B→AC∩BC=BC
8 7 ancld ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A<B→A<B∧AC∩BC=BC
9 simpl2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧¬A<B→B∈ℝ*
10 simpl1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧¬A<B→A∈ℝ*
11 simpr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧¬A<B→¬A<B
12 xrlenlt ⊢B∈ℝ*∧A∈ℝ*→B≤A↔¬A<B
13 12 biimpar ⊢B∈ℝ*∧A∈ℝ*∧¬A<B→B≤A
14 9 10 11 13 syl21anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧¬A<B→B≤A
15 3ancoma ⊢B∈ℝ*∧A∈ℝ*∧C∈ℝ*↔A∈ℝ*∧B∈ℝ*∧C∈ℝ*
16 incom ⊢BC∩AC=AC∩BC
17 iocinioc2 ⊢B∈ℝ*∧A∈ℝ*∧C∈ℝ*∧B≤A→BC∩AC=AC
18 16 17 eqtr3id ⊢B∈ℝ*∧A∈ℝ*∧C∈ℝ*∧B≤A→AC∩BC=AC
19 15 18 sylanbr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧B≤A→AC∩BC=AC
20 14 19 syldan ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧¬A<B→AC∩BC=AC
21 20 ex ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→¬A<B→AC∩BC=AC
22 21 ancld ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→¬A<B→¬A<B∧AC∩BC=AC
23 8 22 orim12d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A<B∨¬A<B→A<B∧AC∩BC=BC∨¬A<B∧AC∩BC=AC
24 1 23 mpi ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A<B∧AC∩BC=BC∨¬A<B∧AC∩BC=AC
25 eqif ⊢AC∩BC=ifA<BBCAC↔A<B∧AC∩BC=BC∨¬A<B∧AC∩BC=AC
26 24 25 sylibr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→AC∩BC=ifA<BBCAC