elicc3

Description: An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009)

		Ref	Expression
	Assertion	elicc3	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elicc1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
2		simp1	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) → 𝐶 ∈ ℝ^* )
3	2	a1i	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) → 𝐶 ∈ ℝ^* ) )
4		xrletr	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) )
5	4	exp5o	⊢ ( 𝐴 ∈ ℝ^* → ( 𝐶 ∈ ℝ^* → ( 𝐵 ∈ ℝ^* → ( 𝐴 ≤ 𝐶 → ( 𝐶 ≤ 𝐵 → 𝐴 ≤ 𝐵 ) ) ) ) )
6	5	com23	⊢ ( 𝐴 ∈ ℝ^* → ( 𝐵 ∈ ℝ^* → ( 𝐶 ∈ ℝ^* → ( 𝐴 ≤ 𝐶 → ( 𝐶 ≤ 𝐵 → 𝐴 ≤ 𝐵 ) ) ) ) )
7	6	imp5q	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) )
8		df-ne	⊢ ( 𝐶 ≠ 𝐴 ↔ ¬ 𝐶 = 𝐴 )
9		xrleltne	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ) → ( 𝐴 < 𝐶 ↔ 𝐶 ≠ 𝐴 ) )
10	9	biimprd	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ) → ( 𝐶 ≠ 𝐴 → 𝐴 < 𝐶 ) )
11	8 10	syl5bir	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ) → ( ¬ 𝐶 = 𝐴 → 𝐴 < 𝐶 ) )
12	11	3adant3r3	⊢ ( ( 𝐴 ∈ ℝ^* ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) → ( ¬ 𝐶 = 𝐴 → 𝐴 < 𝐶 ) )
13	12	adantlr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) → ( ¬ 𝐶 = 𝐴 → 𝐴 < 𝐶 ) )
14		eqcom	⊢ ( 𝐶 = 𝐵 ↔ 𝐵 = 𝐶 )
15	14	necon3bbii	⊢ ( ¬ 𝐶 = 𝐵 ↔ 𝐵 ≠ 𝐶 )
16		xrleltne	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ≤ 𝐵 ) → ( 𝐶 < 𝐵 ↔ 𝐵 ≠ 𝐶 ) )
17	16	biimprd	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ≤ 𝐵 ) → ( 𝐵 ≠ 𝐶 → 𝐶 < 𝐵 ) )
18	15 17	syl5bi	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ≤ 𝐵 ) → ( ¬ 𝐶 = 𝐵 → 𝐶 < 𝐵 ) )
19	18	3exp	⊢ ( 𝐶 ∈ ℝ^* → ( 𝐵 ∈ ℝ^* → ( 𝐶 ≤ 𝐵 → ( ¬ 𝐶 = 𝐵 → 𝐶 < 𝐵 ) ) ) )
20	19	com12	⊢ ( 𝐵 ∈ ℝ^* → ( 𝐶 ∈ ℝ^* → ( 𝐶 ≤ 𝐵 → ( ¬ 𝐶 = 𝐵 → 𝐶 < 𝐵 ) ) ) )
21	20	imp32	⊢ ( ( 𝐵 ∈ ℝ^* ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐶 ≤ 𝐵 ) ) → ( ¬ 𝐶 = 𝐵 → 𝐶 < 𝐵 ) )
22	21	3adantr2	⊢ ( ( 𝐵 ∈ ℝ^* ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) → ( ¬ 𝐶 = 𝐵 → 𝐶 < 𝐵 ) )
23	22	adantll	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) → ( ¬ 𝐶 = 𝐵 → 𝐶 < 𝐵 ) )
24	13 23	anim12d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) → ( ( ¬ 𝐶 = 𝐴 ∧ ¬ 𝐶 = 𝐵 ) → ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
25	24	ex	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) → ( ( ¬ 𝐶 = 𝐴 ∧ ¬ 𝐶 = 𝐵 ) → ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) ) )
26		df-or	⊢ ( ( 𝐶 = 𝐴 ∨ ( ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) ↔ ( ¬ 𝐶 = 𝐴 → ( ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) )
27		3orass	⊢ ( ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ↔ ( 𝐶 = 𝐴 ∨ ( ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) )
28		pm5.6	⊢ ( ( ( ¬ 𝐶 = 𝐴 ∧ ¬ 𝐶 = 𝐵 ) → ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) ↔ ( ¬ 𝐶 = 𝐴 → ( 𝐶 = 𝐵 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) ) )
29		orcom	⊢ ( ( 𝐶 = 𝐵 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) ↔ ( ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) )
30	29	imbi2i	⊢ ( ( ¬ 𝐶 = 𝐴 → ( 𝐶 = 𝐵 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) ) ↔ ( ¬ 𝐶 = 𝐴 → ( ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) )
31	28 30	bitri	⊢ ( ( ( ¬ 𝐶 = 𝐴 ∧ ¬ 𝐶 = 𝐵 ) → ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) ↔ ( ¬ 𝐶 = 𝐴 → ( ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) )
32	26 27 31	3bitr4ri	⊢ ( ( ( ¬ 𝐶 = 𝐴 ∧ ¬ 𝐶 = 𝐵 ) → ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) ↔ ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) )
33	25 32	syl6ib	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) → ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) )
34	3 7 33	3jcad	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) → ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) ) )
35		simp1	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) → 𝐶 ∈ ℝ^* )
36	35	a1i	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) → 𝐶 ∈ ℝ^* ) )
37		xrleid	⊢ ( 𝐴 ∈ ℝ^* → 𝐴 ≤ 𝐴 )
38	37	ad3antrrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐴 )
39		breq2	⊢ ( 𝐶 = 𝐴 → ( 𝐴 ≤ 𝐶 ↔ 𝐴 ≤ 𝐴 ) )
40	38 39	syl5ibrcom	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐶 = 𝐴 → 𝐴 ≤ 𝐶 ) )
41		xrltle	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝐴 < 𝐶 → 𝐴 ≤ 𝐶 ) )
42	41	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐶 → 𝐴 ≤ 𝐶 ) )
43	42	adantllr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐶 → 𝐴 ≤ 𝐶 ) )
44	43	adantrd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) → 𝐴 ≤ 𝐶 ) )
45		simpr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
46		breq2	⊢ ( 𝐶 = 𝐵 → ( 𝐴 ≤ 𝐶 ↔ 𝐴 ≤ 𝐵 ) )
47	45 46	syl5ibrcom	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐶 = 𝐵 → 𝐴 ≤ 𝐶 ) )
48	40 44 47	3jaod	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) → 𝐴 ≤ 𝐶 ) )
49	48	exp31	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐶 ∈ ℝ^* → ( 𝐴 ≤ 𝐵 → ( ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) → 𝐴 ≤ 𝐶 ) ) ) )
50	49	3impd	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) → 𝐴 ≤ 𝐶 ) )
51		breq1	⊢ ( 𝐶 = 𝐴 → ( 𝐶 ≤ 𝐵 ↔ 𝐴 ≤ 𝐵 ) )
52	45 51	syl5ibrcom	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐶 = 𝐴 → 𝐶 ≤ 𝐵 ) )
53		xrltle	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐶 < 𝐵 → 𝐶 ≤ 𝐵 ) )
54	53	ancoms	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝐶 < 𝐵 → 𝐶 ≤ 𝐵 ) )
55	54	adantld	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) → 𝐶 ≤ 𝐵 ) )
56	55	adantll	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) → 𝐶 ≤ 𝐵 ) )
57	56	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) → 𝐶 ≤ 𝐵 ) )
58		xrleid	⊢ ( 𝐵 ∈ ℝ^* → 𝐵 ≤ 𝐵 )
59	58	ad3antlr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ≤ 𝐵 )
60		breq1	⊢ ( 𝐶 = 𝐵 → ( 𝐶 ≤ 𝐵 ↔ 𝐵 ≤ 𝐵 ) )
61	59 60	syl5ibrcom	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐶 = 𝐵 → 𝐶 ≤ 𝐵 ) )
62	52 57 61	3jaod	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ 𝐶 ∈ ℝ^* ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) → 𝐶 ≤ 𝐵 ) )
63	62	exp31	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐶 ∈ ℝ^* → ( 𝐴 ≤ 𝐵 → ( ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) → 𝐶 ≤ 𝐵 ) ) ) )
64	63	3impd	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) → 𝐶 ≤ 𝐵 ) )
65	36 50 64	3jcad	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) → ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
66	34 65	impbid	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ↔ ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) ) )
67	1 66	bitrd	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝐶 = 𝐴 ∨ ( 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ∨ 𝐶 = 𝐵 ) ) ) )

Metamath Proof Explorer

Theorem elicc3

Proof