isxmet2d - Intuitionistic Logic Explorer

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

Theorem isxmet2d 13933

Description: It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample:

satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015.)

**Hypotheses**
Ref	Expression
isxmetd.0
isxmetd.1
isxmet2d.2	$/\$ $/\$
isxmet2d.3	$/\$ $/\$
isxmet2d.4	$/\$ $/\$ $/\$ $/\$ $/\$

**Assertion**
Ref	Expression
isxmet2d

Distinct variable groups:

**Proof of Theorem isxmet2d**
Step	Hyp	Ref	Expression
1		isxmetd.0	. 2
2		isxmetd.1	. 2
3	2	fovcdmda 6020	. . . 4 $/\$ $/\$
4		0xr 8006	. . . 4
5		xrletri3 9806	. . . 4 $/\$ $/\$
6	3, 4, 5	sylancl 413	. . 3 $/\$ $/\$ $/\$
7		isxmet2d.2	. . . 4 $/\$ $/\$
8	7	biantrud 304	. . 3 $/\$ $/\$ $/\$
9		isxmet2d.3	. . 3 $/\$ $/\$
10	6, 8, 9	3bitr2d 216	. 2 $/\$ $/\$
11		isxmet2d.4	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
12	11	3expa 1203	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
13		rexadd 9854	. . . . . . 7 $/\$
14	13	adantl 277	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
15	12, 14	breqtrrd 4033	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	anassrs 400	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
17	3	3adantr3 1158	. . . . . . 7 $/\$ $/\$ $/\$
18		pnfge 9791	. . . . . . 7
19	17, 18	syl 14	. . . . . 6 $/\$ $/\$ $/\$
20	19	ad2antrr 488	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
21		oveq2 5885	. . . . . 6
22	2	ffnd 5368	. . . . . . . . . . 11
23		elxrge0 9980	. . . . . . . . . . . . 13 $/\$
24	3, 7, 23	sylanbrc 417	. . . . . . . . . . . 12 $/\$ $/\$
25	24	ralrimivva 2559	. . . . . . . . . . 11
26		ffnov 5981	. . . . . . . . . . 11 $/\$
27	22, 25, 26	sylanbrc 417	. . . . . . . . . 10
28	27	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$
29		simpr3 1005	. . . . . . . . 9 $/\$ $/\$ $/\$
30		simpr1 1003	. . . . . . . . 9 $/\$ $/\$ $/\$
31	28, 29, 30	fovcdmd 6021	. . . . . . . 8 $/\$ $/\$ $/\$
32		elxrge0 9980	. . . . . . . . 9 $/\$
33	32	simplbi 274	. . . . . . . 8
34	31, 33	syl 14	. . . . . . 7 $/\$ $/\$ $/\$
35		renemnf 8008	. . . . . . 7
36		xaddpnf1 9848	. . . . . . 7 $/\$
37	34, 35, 36	syl2an 289	. . . . . 6 $/\$ $/\$ $/\$ $/\$
38	21, 37	sylan9eqr 2232	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
39	20, 38	breqtrrd 4033	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
40		simpr2 1004	. . . . . . . . . . 11 $/\$ $/\$ $/\$
41	28, 29, 40	fovcdmd 6021	. . . . . . . . . 10 $/\$ $/\$ $/\$
42		elxrge0 9980	. . . . . . . . . . 11 $/\$
43	42	simplbi 274	. . . . . . . . . 10
44	41, 43	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$
45	42	simprbi 275	. . . . . . . . . 10
46	41, 45	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$
47		ge0nemnf 9826	. . . . . . . . 9 $/\$
48	44, 46, 47	syl2anc 411	. . . . . . . 8 $/\$ $/\$ $/\$
49	48	neneqd 2368	. . . . . . 7 $/\$ $/\$ $/\$
50	49	pm2.21d 619	. . . . . 6 $/\$ $/\$ $/\$
51	50	adantr 276	. . . . 5 $/\$ $/\$ $/\$ $/\$
52	51	imp 124	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
53	44	adantr 276	. . . . 5 $/\$ $/\$ $/\$ $/\$
54		elxr 9778	. . . . 5 $\/$ $\/$
55	53, 54	sylib 122	. . . 4 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
56	16, 39, 52, 55	mpjao3dan 1307	. . 3 $/\$ $/\$ $/\$ $/\$
57	19	adantr 276	. . . 4 $/\$ $/\$ $/\$ $/\$
58		oveq1 5884	. . . . 5
59		xaddpnf2 9849	. . . . . 6 $/\$
60	44, 48, 59	syl2anc 411	. . . . 5 $/\$ $/\$ $/\$
61	58, 60	sylan9eqr 2232	. . . 4 $/\$ $/\$ $/\$ $/\$
62	57, 61	breqtrrd 4033	. . 3 $/\$ $/\$ $/\$ $/\$
63	32	simprbi 275	. . . . . . . 8
64	31, 63	syl 14	. . . . . . 7 $/\$ $/\$ $/\$
65		ge0nemnf 9826	. . . . . . 7 $/\$
66	34, 64, 65	syl2anc 411	. . . . . 6 $/\$ $/\$ $/\$
67	66	neneqd 2368	. . . . 5 $/\$ $/\$ $/\$
68	67	pm2.21d 619	. . . 4 $/\$ $/\$ $/\$
69	68	imp 124	. . 3 $/\$ $/\$ $/\$ $/\$
70		elxr 9778	. . . 4 $\/$ $\/$
71	34, 70	sylib 122	. . 3 $/\$ $/\$ $/\$ $\/$ $\/$
72	56, 62, 69, 71	mpjao3dan 1307	. 2 $/\$ $/\$ $/\$
73	1, 2, 10, 72	isxmetd 13932	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ w3o 977 $/\$ w3a 978

wceq 1353

wcel 2148

wne 2347

wral 2455

cvv 2739 class class class wbr 4005

cxp 4626

wfn 5213

wf 5214

cfv 5218 (class class class)co 5877

cr 7812

cc0 7813

caddc 7816

cpnf 7991

cmnf 7992

cxr 7993

cle 7995

cxad 9772

cicc 9893

cxmet 13525

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4123 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-cnex 7904 ax-resscn 7905 ax-1re 7907 ax-addrcl 7910 ax-rnegex 7922 ax-pre-ltirr 7925 ax-pre-ltwlin 7926 ax-pre-lttrn 7927 ax-pre-apti 7928

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2741 df-sbc 2965 df-csb 3060 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-if 3537 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-iun 3890 df-br 4006 df-opab 4067 df-mpt 4068 df-id 4295 df-po 4298 df-iso 4299 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-rn 4639 df-res 4640 df-ima 4641 df-iota 5180 df-fun 5220 df-fn 5221 df-f 5222 df-fv 5226 df-ov 5880 df-oprab 5881 df-mpo 5882 df-1st 6143 df-2nd 6144 df-map 6652 df-pnf 7996 df-mnf 7997 df-xr 7998 df-ltxr 7999 df-le 8000 df-xadd 9775 df-icc 9897 df-xmet 13533

This theorem is referenced by: (None)

W3C validator