Theorem leagne4

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	leagne4	$$⊢\phi \to F\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		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$$
13	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$$
14	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$$
15	8	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 F\in P$$
16	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}}$$
17		simprl	$$⊢\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 }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩$$
18	1 10 11 12 13 14 15 16 17	inagne2	$$⊢\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 F\ne E$$
19	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)$$
20	9 19	mpbid	$$⊢\phi \to \exists x\in P\left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)$$
21	18 20	r19.29a	$$⊢\phi \to F\ne E$$