xrlttri3 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > xrlttri3		Unicode version

Theorem xrlttri3 8488

Description: Extended real version of lttri3 6895. (Contributed by NM, 9-Feb-2006.)

**Assertion**
Ref	Expression
xrlttri3	$/\$ $/\$

**Proof of Theorem xrlttri3**
Step	Hyp	Ref	Expression
1		elxr 8466	. 2 $\/$ $\/$
2		elxr 8466	. 2 $\/$ $\/$
3		lttri3 6895	. . . . . 6 $/\$ $/\$
4	3	ancoms 255	. . . . 5 $/\$ $/\$
5		renepnf 6870	. . . . . . . . . 10
6	5	adantr 261	. . . . . . . . 9 $/\$
7		neeq2 2214	. . . . . . . . . 10
8	7	adantl 262	. . . . . . . . 9 $/\$
9	6, 8	mpbird 156	. . . . . . . 8 $/\$
10	9	necomd 2285	. . . . . . 7 $/\$
11	10	neneqd 2221	. . . . . 6 $/\$
12		ltpnf 8472	. . . . . . . . 9
13	12	adantr 261	. . . . . . . 8 $/\$
14		breq2 3759	. . . . . . . . 9
15	14	adantl 262	. . . . . . . 8 $/\$
16	13, 15	mpbird 156	. . . . . . 7 $/\$
17		notnot1 559	. . . . . . . . 9 $\/$ $\/$
18	17	olcs 654	. . . . . . . 8 $\/$
19		ioran 668	. . . . . . . 8 $\/$ $/\$
20	18, 19	sylnib 600	. . . . . . 7 $/\$
21	16, 20	syl 14	. . . . . 6 $/\$ $/\$
22	11, 21	2falsed 617	. . . . 5 $/\$ $/\$
23		renemnf 6871	. . . . . . . . . 10
24	23	adantr 261	. . . . . . . . 9 $/\$
25		neeq2 2214	. . . . . . . . . 10
26	25	adantl 262	. . . . . . . . 9 $/\$
27	24, 26	mpbird 156	. . . . . . . 8 $/\$
28	27	necomd 2285	. . . . . . 7 $/\$
29	28	neneqd 2221	. . . . . 6 $/\$
30		mnflt 8474	. . . . . . . . 9
31	30	adantr 261	. . . . . . . 8 $/\$
32		breq1 3758	. . . . . . . . 9
33	32	adantl 262	. . . . . . . 8 $/\$
34	31, 33	mpbird 156	. . . . . . 7 $/\$
35		orc 632	. . . . . . 7 $\/$
36		oranim 806	. . . . . . 7 $\/$ $/\$
37	34, 35, 36	3syl 17	. . . . . 6 $/\$ $/\$
38	29, 37	2falsed 617	. . . . 5 $/\$ $/\$
39	4, 22, 38	3jaodan 1200	. . . 4 $/\$ $\/$ $\/$ $/\$
40	39	ancoms 255	. . 3 $\/$ $\/$ $/\$ $/\$
41		renepnf 6870	. . . . . . . . 9
42	41	adantl 262	. . . . . . . 8 $/\$
43		neeq2 2214	. . . . . . . . 9
44	43	adantr 261	. . . . . . . 8 $/\$
45	42, 44	mpbird 156	. . . . . . 7 $/\$
46	45	neneqd 2221	. . . . . 6 $/\$
47		ltpnf 8472	. . . . . . . . 9
48	47	adantl 262	. . . . . . . 8 $/\$
49		breq2 3759	. . . . . . . . 9
50	49	adantr 261	. . . . . . . 8 $/\$
51	48, 50	mpbird 156	. . . . . . 7 $/\$
52	51, 35, 36	3syl 17	. . . . . 6 $/\$ $/\$
53	46, 52	2falsed 617	. . . . 5 $/\$ $/\$
54		eqtr3 2056	. . . . . . 7 $/\$
55	54	eqcomd 2042	. . . . . 6 $/\$
56		pnfxr 8462	. . . . . . . . 9
57		xrltnr 8471	. . . . . . . . 9
58	56, 57	ax-mp 7	. . . . . . . 8
59		breq12 3760	. . . . . . . . 9 $/\$
60	59	ancoms 255	. . . . . . . 8 $/\$
61	58, 60	mtbiri 599	. . . . . . 7 $/\$
62		breq12 3760	. . . . . . . 8 $/\$
63	58, 62	mtbiri 599	. . . . . . 7 $/\$
64	61, 63	jca 290	. . . . . 6 $/\$ $/\$
65	55, 64	2thd 164	. . . . 5 $/\$ $/\$
66		mnfnepnf 8468	. . . . . . . . 9
67		eqeq12 2049	. . . . . . . . . 10 $/\$
68	67	necon3bid 2240	. . . . . . . . 9 $/\$
69	66, 68	mpbiri 157	. . . . . . . 8 $/\$
70	69	ancoms 255	. . . . . . 7 $/\$
71	70	neneqd 2221	. . . . . 6 $/\$
72		mnfltpnf 8476	. . . . . . . . 9
73		breq12 3760	. . . . . . . . 9 $/\$
74	72, 73	mpbiri 157	. . . . . . . 8 $/\$
75	74	ancoms 255	. . . . . . 7 $/\$
76	75, 35, 36	3syl 17	. . . . . 6 $/\$ $/\$
77	71, 76	2falsed 617	. . . . 5 $/\$ $/\$
78	53, 65, 77	3jaodan 1200	. . . 4 $/\$ $\/$ $\/$ $/\$
79	78	ancoms 255	. . 3 $\/$ $\/$ $/\$ $/\$
80		renemnf 6871	. . . . . . . . 9
81	80	adantl 262	. . . . . . . 8 $/\$
82		neeq2 2214	. . . . . . . . 9
83	82	adantr 261	. . . . . . . 8 $/\$
84	81, 83	mpbird 156	. . . . . . 7 $/\$
85	84	neneqd 2221	. . . . . 6 $/\$
86		mnflt 8474	. . . . . . . . 9
87	86	adantl 262	. . . . . . . 8 $/\$
88		breq1 3758	. . . . . . . . 9
89	88	adantr 261	. . . . . . . 8 $/\$
90	87, 89	mpbird 156	. . . . . . 7 $/\$
91	90, 20	syl 14	. . . . . 6 $/\$ $/\$
92	85, 91	2falsed 617	. . . . 5 $/\$ $/\$
93	66	neii 2205	. . . . . . . . . 10
94		eqeq12 2049	. . . . . . . . . 10 $/\$
95	93, 94	mtbiri 599	. . . . . . . . 9 $/\$
96	95	neneqad 2278	. . . . . . . 8 $/\$
97	96	necomd 2285	. . . . . . 7 $/\$
98	97	neneqd 2221	. . . . . 6 $/\$
99		breq12 3760	. . . . . . . 8 $/\$
100	72, 99	mpbiri 157	. . . . . . 7 $/\$
101	100, 20	syl 14	. . . . . 6 $/\$ $/\$
102	98, 101	2falsed 617	. . . . 5 $/\$ $/\$
103		eqtr3 2056	. . . . . . 7 $/\$
104	103	ancoms 255	. . . . . 6 $/\$
105		mnfxr 8464	. . . . . . . . 9
106		xrltnr 8471	. . . . . . . . 9
107	105, 106	ax-mp 7	. . . . . . . 8
108		breq12 3760	. . . . . . . . 9 $/\$
109	108	ancoms 255	. . . . . . . 8 $/\$
110	107, 109	mtbiri 599	. . . . . . 7 $/\$
111		breq12 3760	. . . . . . . 8 $/\$
112	107, 111	mtbiri 599	. . . . . . 7 $/\$
113	110, 112	jca 290	. . . . . 6 $/\$ $/\$
114	104, 113	2thd 164	. . . . 5 $/\$ $/\$
115	92, 102, 114	3jaodan 1200	. . . 4 $/\$ $\/$ $\/$ $/\$
116	115	ancoms 255	. . 3 $\/$ $\/$ $/\$ $/\$
117	40, 79, 116	3jaodan 1200	. 2 $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
118	1, 2, 117	syl2anb 275	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 97

wb 98 $\/$ wo 628 $\/$ w3o 883

wceq 1242

wcel 1390

wne 2201 class class class wbr 3755

cr 6710

cpnf 6854

cmnf 6855

cxr 6856

clt 6857

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-13 1401 ax-14 1402 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 ax-sep 3866 ax-pow 3918 ax-pr 3935 ax-un 4136 ax-setind 4220 ax-cnex 6774 ax-resscn 6775 ax-pre-ltirr 6795 ax-pre-apti 6798

This theorem depends on definitions: df-bi 110 df-3or 885 df-3an 886 df-tru 1245 df-fal 1248 df-nf 1347 df-sb 1643 df-eu 1900 df-mo 1901 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ne 2203 df-nel 2204 df-ral 2305 df-rex 2306 df-rab 2309 df-v 2553 df-dif 2914 df-un 2916 df-in 2918 df-ss 2925 df-pw 3353 df-sn 3373 df-pr 3374 df-op 3376 df-uni 3572 df-br 3756 df-opab 3810 df-xp 4294 df-pnf 6859 df-mnf 6860 df-xr 6861 df-ltxr 6862

This theorem is referenced by: xrletri3 8491 iccid 8564

W3C validator