leagne2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > leagne2		Structured version Visualization version GIF version

Theorem leagne2 27090

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

**Hypotheses**
Ref	Expression
isleag.p	⊢ 𝑃 = (Base‘𝐺)
isleag.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
isleag.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
isleag.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
isleag.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
isleag.d	⊢ (𝜑 → 𝐷 ∈ 𝑃)
isleag.e	⊢ (𝜑 → 𝐸 ∈ 𝑃)
isleag.f	⊢ (𝜑 → 𝐹 ∈ 𝑃)
leagne.1	⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(≤_∠‘𝐺)⟨“𝐷𝐸𝐹”⟩)

**Assertion**
Ref	Expression
leagne2	⊢ (𝜑 → 𝐶 ≠ 𝐵)

Proof of Theorem leagne2 Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isleag.p	. . . 4 ⊢ 𝑃 = (Base‘𝐺)
2		eqid 2739	. . . 4 ⊢ (Itv‘𝐺) = (Itv‘𝐺)
3		eqid 2739	. . . 4 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
4		isleag.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)) → 𝐺 ∈ TarskiG)
6		isleag.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
7	6	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)) → 𝐴 ∈ 𝑃)
8		isleag.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
9	8	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)) → 𝐵 ∈ 𝑃)
10		isleag.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
11	10	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)) → 𝐶 ∈ 𝑃)
12		isleag.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
13	12	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)) → 𝐷 ∈ 𝑃)
14		isleag.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
15	14	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)) → 𝐸 ∈ 𝑃)
16		simplr 769	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)) → 𝑥 ∈ 𝑃)
17		simprr 773	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)
18	1, 2, 3, 5, 7, 9, 11, 13, 15, 16, 17	cgrane2 27053	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)) → 𝐵 ≠ 𝐶)
19	18	necomd 2999	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)) → 𝐶 ≠ 𝐵)
20		leagne.1	. . 3 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(≤_∠‘𝐺)⟨“𝐷𝐸𝐹”⟩)
21		isleag.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
22	1, 4, 6, 8, 10, 12, 14, 21	isleag 27087	. . 3 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(≤_∠‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ∃𝑥 ∈ 𝑃 (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩)))
23	20, 22	mpbid 235	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥(inA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑥”⟩))
24	19, 23	r19.29a 3218	1 ⊢ (𝜑 → 𝐶 ≠ 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2112 ≠ wne 2943 ∃wrex 3065 class class class wbr 5070 ‘cfv 6415 ⟨“cs3 14458 Basecbs 16815 TarskiGcstrkg 26668 Itvcitv 26674 hlGchlg 26840 cgrAccgra 27047 inAcinag 27075 ≤_∠cleag 27076

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-rep 5203 ax-sep 5216 ax-nul 5223 ax-pow 5282 ax-pr 5346 ax-un 7563 ax-cnex 10833 ax-resscn 10834 ax-1cn 10835 ax-icn 10836 ax-addcl 10837 ax-addrcl 10838 ax-mulcl 10839 ax-mulrcl 10840 ax-mulcom 10841 ax-addass 10842 ax-mulass 10843 ax-distr 10844 ax-i2m1 10845 ax-1ne0 10846 ax-1rid 10847 ax-rnegex 10848 ax-rrecex 10849 ax-cnre 10850 ax-pre-lttri 10851 ax-pre-lttrn 10852 ax-pre-ltadd 10853 ax-pre-mulgt0 10854

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rab 3073 df-v 3425 df-sbc 3713 df-csb 3830 df-dif 3887 df-un 3889 df-in 3891 df-ss 3901 df-pss 3903 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5153 df-tr 5186 df-id 5479 df-eprel 5485 df-po 5493 df-so 5494 df-fr 5534 df-we 5536 df-xp 5585 df-rel 5586 df-cnv 5587 df-co 5588 df-dm 5589 df-rn 5590 df-res 5591 df-ima 5592 df-pred 6189 df-ord 6251 df-on 6252 df-lim 6253 df-suc 6254 df-iota 6373 df-fun 6417 df-fn 6418 df-f 6419 df-f1 6420 df-fo 6421 df-f1o 6422 df-fv 6423 df-riota 7209 df-ov 7255 df-oprab 7256 df-mpo 7257 df-om 7685 df-1st 7801 df-2nd 7802 df-wrecs 8089 df-recs 8150 df-rdg 8188 df-1o 8244 df-er 8433 df-map 8552 df-pm 8553 df-en 8669 df-dom 8670 df-sdom 8671 df-fin 8672 df-card 9603 df-pnf 10917 df-mnf 10918 df-xr 10919 df-ltxr 10920 df-le 10921 df-sub 11112 df-neg 11113 df-nn 11879 df-2 11941 df-3 11942 df-n0 12139 df-z 12225 df-uz 12487 df-fz 13144 df-fzo 13287 df-hash 13948 df-word 14121 df-concat 14177 df-s1 14204 df-s2 14464 df-s3 14465 df-trkgc 26688 df-trkgcb 26690 df-trkg 26693 df-cgrg 26751 df-hlg 26841 df-cgra 27048 df-leag 27086

This theorem is referenced by: (None)

W3C validator