elfzodifsumelfzo - Intuitionistic Logic Explorer

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

Theorem elfzodifsumelfzo 9761

Description: If an integer is in a half-open range of nonnegative integers with a difference as upper bound, the sum of the integer with the subtrahend of the difference is in the a half-open range of nonnegative integers containing the minuend of the difference. (Contributed by AV, 13-Nov-2018.)

**Assertion**
Ref	Expression
elfzodifsumelfzo	$/\$ ..^ ..^

**Proof of Theorem elfzodifsumelfzo**
Step	Hyp	Ref	Expression
1		elfz2nn0 9675	. . 3 $/\$ $/\$
2		elfz2nn0 9675	. . . . 5 $/\$ $/\$
3		elfzo0 9742	. . . . . . . 8 ..^ $/\$ $/\$
4		nn0z 8868	. . . . . . . . . . . . 13
5		nn0z 8868	. . . . . . . . . . . . 13
6		znnsub 8899	. . . . . . . . . . . . 13 $/\$
7	4, 5, 6	syl2an 284	. . . . . . . . . . . 12 $/\$
8		simpr 109	. . . . . . . . . . . . . . . 16 $/\$
9		simpll 497	. . . . . . . . . . . . . . . 16 $/\$ $/\$
10		nn0addcl 8806	. . . . . . . . . . . . . . . 16 $/\$
11	8, 9, 10	syl2anr 285	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
12	11	adantr 271	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		0red 7586	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
14		nn0re 8780	. . . . . . . . . . . . . . . . . . . . . . 23
15	14	adantr 271	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
16		nn0re 8780	. . . . . . . . . . . . . . . . . . . . . . 23
17	16	adantl 272	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
18	13, 15, 17	3jca 1126	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
19	18	adantr 271	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
20		nn0ge0 8796	. . . . . . . . . . . . . . . . . . . . . 22
21	20	adantr 271	. . . . . . . . . . . . . . . . . . . . 21 $/\$
22	21	anim1i 334	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
23		lelttr 7670	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
24	19, 22, 23	sylc 62	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
25	24	ex 114	. . . . . . . . . . . . . . . . . 18 $/\$
26		0red 7586	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
27	16	adantl 272	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
28		nn0re 8780	. . . . . . . . . . . . . . . . . . . . . . . . . 26
29	28	adantr 271	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
30		ltletr 7671	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
31	26, 27, 29, 30	syl3anc 1181	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
32		nn0z 8868	. . . . . . . . . . . . . . . . . . . . . . . . . 26
33		elnnz 8858	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
34	33	simplbi2 378	. . . . . . . . . . . . . . . . . . . . . . . . . 26
35	32, 34	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25
36	35	adantr 271	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
37	31, 36	syld 45	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
38	37	exp4b 360	. . . . . . . . . . . . . . . . . . . . . 22
39	38	com24 87	. . . . . . . . . . . . . . . . . . . . 21
40	39	imp 123	. . . . . . . . . . . . . . . . . . . 20 $/\$
41	40	com13 80	. . . . . . . . . . . . . . . . . . 19 $/\$
42	41	adantl 272	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
43	25, 42	syld 45	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
44	43	imp 123	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
45	44	adantr 271	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
46	45	imp 123	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47		nn0re 8780	. . . . . . . . . . . . . . . . . . . . 21
48	47	adantl 272	. . . . . . . . . . . . . . . . . . . 20 $/\$
49	15	adantr 271	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
50		readdcl 7565	. . . . . . . . . . . . . . . . . . . 20 $/\$
51	48, 49, 50	syl2anr 285	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
52	51	adantr 271	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
53	17	adantr 271	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
54	53	adantr 271	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
55	54	adantr 271	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
56	28	adantl 272	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
57	52, 55, 56	3jca 1126	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	57	adantr 271	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	47	adantl 272	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
60	15	adantr 271	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
61	17	adantr 271	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
62	59, 60, 61	ltaddsubd 8119	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
63	62	exbiri 375	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
64	63	com23 78	. . . . . . . . . . . . . . . . . . . . 21 $/\$
65	64	impd 252	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
66	65	adantr 271	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
67	66	imp 123	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
68	67	adantr 271	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
69	68	anim1i 334	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		ltletr 7671	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
71	58, 69, 70	sylc 62	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	71	anasss 392	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73		elfzo0 9742	. . . . . . . . . . . . . 14 ..^ $/\$ $/\$
74	12, 46, 72, 73	syl3anbrc 1130	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ ..^
75	74	exp53 370	. . . . . . . . . . . 12 $/\$ $/\$ ..^
76	7, 75	sylbird 169	. . . . . . . . . . 11 $/\$ $/\$ ..^
77	76	3adant3 966	. . . . . . . . . 10 $/\$ $/\$ $/\$ ..^
78	77	com14 88	. . . . . . . . 9 $/\$ $/\$ $/\$ ..^
79	78	3imp 1140	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ ..^
80	3, 79	sylbi 120	. . . . . . 7 ..^ $/\$ $/\$ $/\$ ..^
81	80	com13 80	. . . . . 6 $/\$ $/\$ $/\$ ..^ ..^
82	81	3adant1 964	. . . . 5 $/\$ $/\$ $/\$ $/\$ ..^ ..^
83	2, 82	sylbi 120	. . . 4 $/\$ $/\$ ..^ ..^
84	83	com12 30	. . 3 $/\$ $/\$ ..^ ..^
85	1, 84	sylbi 120	. 2 ..^ ..^
86	85	imp 123	1 $/\$ ..^ ..^

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $/\$ w3a 927

wcel 1445 class class class wbr 3867 (class class class)co 5690

cr 7446

cc0 7447

caddc 7450

clt 7619

cle 7620

cmin 7750

cn 8520

cn0 8771

cz 8848

cfz 9573 ..^cfzo 9702

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-pr 4060 ax-un 4284 ax-setind 4381 ax-cnex 7533 ax-resscn 7534 ax-1cn 7535 ax-1re 7536 ax-icn 7537 ax-addcl 7538 ax-addrcl 7539 ax-mulcl 7540 ax-addcom 7542 ax-addass 7544 ax-distr 7546 ax-i2m1 7547 ax-0lt1 7548 ax-0id 7550 ax-rnegex 7551 ax-cnre 7553 ax-pre-ltirr 7554 ax-pre-ltwlin 7555 ax-pre-lttrn 7556 ax-pre-ltadd 7558

This theorem depends on definitions: df-bi 116 df-3or 928 df-3an 929 df-tru 1299 df-fal 1302 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ne 2263 df-nel 2358 df-ral 2375 df-rex 2376 df-reu 2377 df-rab 2379 df-v 2635 df-sbc 2855 df-csb 2948 df-dif 3015 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-int 3711 df-iun 3754 df-br 3868 df-opab 3922 df-mpt 3923 df-id 4144 df-xp 4473 df-rel 4474 df-cnv 4475 df-co 4476 df-dm 4477 df-rn 4478 df-res 4479 df-ima 4480 df-iota 5014 df-fun 5051 df-fn 5052 df-f 5053 df-fv 5057 df-riota 5646 df-ov 5693 df-oprab 5694 df-mpt2 5695 df-1st 5949 df-2nd 5950 df-pnf 7621 df-mnf 7622 df-xr 7623 df-ltxr 7624 df-le 7625 df-sub 7752 df-neg 7753 df-inn 8521 df-n0 8772 df-z 8849 df-uz 9119 df-fz 9574 df-fzo 9703

This theorem is referenced by: elfzom1elp1fzo 9762

W3C validator