Theorem leagne3

Description: Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023)

	Ref	Expression
Hypotheses	isleag.p	$$⊢P={\mathrm{Base}}_G$$
	isleag.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	isleag.a	$$⊢\phi \to A\in P$$
	isleag.b	$$⊢\phi \to B\in P$$
	isleag.c	$$⊢\phi \to C\in P$$
	isleag.d	$$⊢\phi \to D\in P$$
	isleag.e	$$⊢\phi \to E\in P$$
	isleag.f	$$⊢\phi \to F\in P$$
	leagne.1	$$⊢\phi \to ⟨“ABC”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩$$
Assertion	leagne3	$$⊢\phi \to D\ne E$$

Proof

Step	Hyp	Ref	Expression
1		isleag.p	$$⊢P={\mathrm{Base}}_G$$
2		isleag.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
3		isleag.a	$$⊢\phi \to A\in P$$
4		isleag.b	$$⊢\phi \to B\in P$$
5		isleag.c	$$⊢\phi \to C\in P$$
6		isleag.d	$$⊢\phi \to D\in P$$
7		isleag.e	$$⊢\phi \to E\in P$$
8		isleag.f	$$⊢\phi \to F\in P$$
9		leagne.1	$$⊢\phi \to ⟨“ABC”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩$$
10		eqid	$$⊢\mathrm{Itv}\left(G\right)=\mathrm{Itv}\left(G\right)$$
11		eqid	$$⊢{hl}_{𝒢}\left(G\right)={hl}_{𝒢}\left(G\right)$$
12	2	ad2antrr	$$⊢\left(\left(\phi \wedge x\in P\right)\wedge \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
13	3	ad2antrr	$$⊢\left(\left(\phi \wedge x\in P\right)\wedge \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)\to A\in P$$
14	4	ad2antrr	$$⊢\left(\left(\phi \wedge x\in P\right)\wedge \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)\to B\in P$$
15	5	ad2antrr	$$⊢\left(\left(\phi \wedge x\in P\right)\wedge \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)\to C\in P$$
16	6	ad2antrr	$$⊢\left(\left(\phi \wedge x\in P\right)\wedge \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)\to D\in P$$
17	7	ad2antrr	$$⊢\left(\left(\phi \wedge x\in P\right)\wedge \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)\to E\in P$$
18		simplr	$$⊢\left(\left(\phi \wedge x\in P\right)\wedge \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)\to x\in P$$
19		simprr	$$⊢\left(\left(\phi \wedge x\in P\right)\wedge \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)\to ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩$$
20	1 10 11 12 13 14 15 16 17 18 19	cgrane3	$$⊢\left(\left(\phi \wedge x\in P\right)\wedge \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)\to E\ne D$$
21	20	necomd	$$⊢\left(\left(\phi \wedge x\in P\right)\wedge \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)\to D\ne E$$
22	1 2 3 4 5 6 7 8	isleag	$$⊢\phi \to \left(⟨“ABC”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\leftrightarrow \exists x\in P\left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)$$
23	9 22	mpbid	$$⊢\phi \to \exists x\in P\left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)$$
24	21 23	r19.29a	$$⊢\phi \to D\ne E$$