fldivp1 - Intuitionistic Logic Explorer

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

Theorem fldivp1 13127

Description: The difference between the floors of adjacent fractions is either 1 or 0. (Contributed by Mario Carneiro, 8-Mar-2014.)

**Assertion**
Ref	Expression
fldivp1	$/\$

**Proof of Theorem fldivp1**
Step	Hyp	Ref	Expression
1		nnz 9663	. . . . . . . . 9
2		nnne0 9332	. . . . . . . . 9
3		peano2z 9680	. . . . . . . . . 10
4	3	adantr 276	. . . . . . . . 9 $/\$
5		dvdsval2 12557	. . . . . . . . 9 $/\$ $/\$
6	1, 2, 4, 5	syl2an23an 1340	. . . . . . . 8 $/\$
7	6	biimpa 296	. . . . . . 7 $/\$ $/\$
8		flid 10719	. . . . . . 7
9	7, 8	syl 14	. . . . . 6 $/\$ $/\$
10		nnm1nn0 9604	. . . . . . . . . 10
11	10	nn0red 9621	. . . . . . . . 9
12	10	nn0ge0d 9623	. . . . . . . . 9
13		nnre 9311	. . . . . . . . 9
14		nngt0 9329	. . . . . . . . 9
15		divge0 9203	. . . . . . . . 9 $/\$ $/\$ $/\$
16	11, 12, 13, 14, 15	syl22anc 1279	. . . . . . . 8
17	16	ad2antlr 493	. . . . . . 7 $/\$ $/\$
18	13	ltm1d 9262	. . . . . . . . . 10
19		nncn 9312	. . . . . . . . . . 11
20	19	mulridd 8343	. . . . . . . . . 10
21	18, 20	breqtrrd 4158	. . . . . . . . 9
22		1red 8341	. . . . . . . . . 10
23		ltdivmul 9206	. . . . . . . . . 10 $/\$ $/\$ $/\$
24	11, 22, 13, 14, 23	syl112anc 1282	. . . . . . . . 9
25	21, 24	mpbird 167	. . . . . . . 8
26	25	ad2antlr 493	. . . . . . 7 $/\$ $/\$
27	10	nn0zd 9766	. . . . . . . . . 10
28		znq 10024	. . . . . . . . . 10 $/\$
29	27, 28	mpancom 426	. . . . . . . . 9
30	29	ad2antlr 493	. . . . . . . 8 $/\$ $/\$
31		flqbi2 10726	. . . . . . . 8 $/\$ $/\$
32	7, 30, 31	syl2anc 415	. . . . . . 7 $/\$ $/\$ $/\$
33	17, 26, 32	mpbir2and 957	. . . . . 6 $/\$ $/\$
34	9, 33	eqtr4d 2274	. . . . 5 $/\$ $/\$
35		zcn 9649	. . . . . . . . . 10
36	35	adantr 276	. . . . . . . . 9 $/\$
37	19	adantl 277	. . . . . . . . 9 $/\$
38		nnap0 9333	. . . . . . . . . 10 #
39	38	adantl 277	. . . . . . . . 9 $/\$ #
40	36, 37, 37, 39	divdirapd 9159	. . . . . . . 8 $/\$
41		ax-1cn 8272	. . . . . . . . . . . 12
42	41	a1i 9	. . . . . . . . . . 11 $/\$
43	36, 42, 37	ppncand 8677	. . . . . . . . . 10 $/\$
44	43	oveq1d 6100	. . . . . . . . 9 $/\$
45	4	zcnd 9769	. . . . . . . . . 10 $/\$
46		subcl 8525	. . . . . . . . . . . 12 $/\$
47	19, 41, 46	sylancl 417	. . . . . . . . . . 11
48	47	adantl 277	. . . . . . . . . 10 $/\$
49	45, 48, 37, 39	divdirapd 9159	. . . . . . . . 9 $/\$
50	44, 49	eqtr3d 2273	. . . . . . . 8 $/\$
51	37, 39	dividapd 9116	. . . . . . . . 9 $/\$
52	51	oveq2d 6101	. . . . . . . 8 $/\$
53	40, 50, 52	3eqtr3d 2279	. . . . . . 7 $/\$
54	53	fveq2d 5699	. . . . . 6 $/\$
55	54	adantr 276	. . . . 5 $/\$ $/\$
56		znq 10024	. . . . . . 7 $/\$
57		1z 9670	. . . . . . 7
58		flqaddz 10732	. . . . . . 7 $/\$
59	56, 57, 58	sylancl 417	. . . . . 6 $/\$
60	59	adantr 276	. . . . 5 $/\$ $/\$
61	34, 55, 60	3eqtrrd 2276	. . . 4 $/\$ $/\$
62		znq 10024	. . . . . . . . 9 $/\$
63	3, 62	sylan 283	. . . . . . . 8 $/\$
64	63	flqcld 10712	. . . . . . 7 $/\$
65	64	zcnd 9769	. . . . . 6 $/\$
66	56	flqcld 10712	. . . . . . 7 $/\$
67	66	zcnd 9769	. . . . . 6 $/\$
68	65, 67, 42	subaddd 8655	. . . . 5 $/\$
69	68	adantr 276	. . . 4 $/\$ $/\$
70	61, 69	mpbird 167	. . 3 $/\$ $/\$
71		iftrue 3645	. . . 4
72	71	adantl 277	. . 3 $/\$ $/\$
73	70, 72	eqtr4d 2274	. 2 $/\$ $/\$
74		zmodcl 10781	. . . . . . . . . . 11 $/\$
75	3, 74	sylan 283	. . . . . . . . . 10 $/\$
76	75	nn0red 9621	. . . . . . . . 9 $/\$
77		1re 8325	. . . . . . . . 9
78		resubcl 8590	. . . . . . . . 9 $/\$
79	76, 77, 78	sylancl 417	. . . . . . . 8 $/\$
80	79	adantr 276	. . . . . . 7 $/\$ $/\$
81	75	nn0zd 9766	. . . . . . . . . . . 12 $/\$
82		elnndc 10012	. . . . . . . . . . . 12 DECID
83	81, 82	syl 14	. . . . . . . . . . 11 $/\$ DECID
84		elnn0 9565	. . . . . . . . . . . . . 14 $\/$
85	75, 84	sylib 122	. . . . . . . . . . . . 13 $/\$ $\/$
86	85	ord 736	. . . . . . . . . . . 12 $/\$
87		id 19	. . . . . . . . . . . . 13
88		dvdsval3 12558	. . . . . . . . . . . . 13 $/\$
89	87, 3, 88	syl2anr 290	. . . . . . . . . . . 12 $/\$
90	86, 89	sylibrd 169	. . . . . . . . . . 11 $/\$
91		con1dc 868	. . . . . . . . . . 11 DECID
92	83, 90, 91	sylc 62	. . . . . . . . . 10 $/\$
93	92	imp 124	. . . . . . . . 9 $/\$ $/\$
94		nnm1nn0 9604	. . . . . . . . 9
95	93, 94	syl 14	. . . . . . . 8 $/\$ $/\$
96	95	nn0ge0d 9623	. . . . . . 7 $/\$ $/\$
97	13, 14	jca 306	. . . . . . . 8 $/\$
98	97	ad2antlr 493	. . . . . . 7 $/\$ $/\$ $/\$
99		divge0 9203	. . . . . . 7 $/\$ $/\$ $/\$
100	80, 96, 98, 99	syl21anc 1277	. . . . . 6 $/\$ $/\$
101	13	adantl 277	. . . . . . . . . 10 $/\$
102	76	ltm1d 9262	. . . . . . . . . 10 $/\$
103		zq 10026	. . . . . . . . . . . . 13
104	3, 103	syl 14	. . . . . . . . . . . 12
105	104	adantr 276	. . . . . . . . . . 11 $/\$
106		nnq 10033	. . . . . . . . . . . 12
107	106	adantl 277	. . . . . . . . . . 11 $/\$
108	14	adantl 277	. . . . . . . . . . 11 $/\$
109		modqlt 10770	. . . . . . . . . . 11 $/\$ $/\$
110	105, 107, 108, 109	syl3anc 1278	. . . . . . . . . 10 $/\$
111	79, 76, 101, 102, 110	lttrd 8452	. . . . . . . . 9 $/\$
112	37	mulridd 8343	. . . . . . . . 9 $/\$
113	111, 112	breqtrrd 4158	. . . . . . . 8 $/\$
114		1red 8341	. . . . . . . . 9 $/\$
115		ltdivmul 9206	. . . . . . . . 9 $/\$ $/\$ $/\$
116	79, 114, 101, 108, 115	syl112anc 1282	. . . . . . . 8 $/\$
117	113, 116	mpbird 167	. . . . . . 7 $/\$
118	117	adantr 276	. . . . . 6 $/\$ $/\$
119		peano2zm 9682	. . . . . . . . . 10
120	81, 119	syl 14	. . . . . . . . 9 $/\$
121		znq 10024	. . . . . . . . 9 $/\$
122	120, 121	sylancom 424	. . . . . . . 8 $/\$
123		flqbi2 10726	. . . . . . . 8 $/\$ $/\$
124	64, 122, 123	syl2anc 415	. . . . . . 7 $/\$ $/\$
125	124	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
126	100, 118, 125	mpbir2and 957	. . . . 5 $/\$ $/\$
127		modqval 10761	. . . . . . . . . . . . 13 $/\$ $/\$
128	105, 107, 108, 127	syl3anc 1278	. . . . . . . . . . . 12 $/\$
129	128	oveq1d 6100	. . . . . . . . . . 11 $/\$
130	37, 65	mulcld 8346	. . . . . . . . . . . 12 $/\$
131	45, 42, 130	sub32d 8669	. . . . . . . . . . 11 $/\$
132		pncan 8532	. . . . . . . . . . . . 13 $/\$
133	36, 41, 132	sylancl 417	. . . . . . . . . . . 12 $/\$
134	133	oveq1d 6100	. . . . . . . . . . 11 $/\$
135	129, 131, 134	3eqtr2d 2277	. . . . . . . . . 10 $/\$
136	135	oveq1d 6100	. . . . . . . . 9 $/\$
137	36, 130, 37, 39	divsubdirapd 9160	. . . . . . . . 9 $/\$
138	65, 37, 39	divcanap3d 9125	. . . . . . . . . 10 $/\$
139	138	oveq2d 6101	. . . . . . . . 9 $/\$
140	136, 137, 139	3eqtrrd 2276	. . . . . . . 8 $/\$
141		zre 9648	. . . . . . . . . . 11
142		nndivre 9340	. . . . . . . . . . 11 $/\$
143	141, 142	sylan 283	. . . . . . . . . 10 $/\$
144	143	recnd 8354	. . . . . . . . 9 $/\$
145		nndivre 9340	. . . . . . . . . . 11 $/\$
146	79, 145	sylancom 424	. . . . . . . . . 10 $/\$
147	146	recnd 8354	. . . . . . . . 9 $/\$
148	144, 65, 147	subaddd 8655	. . . . . . . 8 $/\$
149	140, 148	mpbid 147	. . . . . . 7 $/\$
150	149	adantr 276	. . . . . 6 $/\$ $/\$
151	150	fveq2d 5699	. . . . 5 $/\$ $/\$
152	126, 151	eqtr3d 2273	. . . 4 $/\$ $/\$
153	65, 67	subeq0ad 8647	. . . . 5 $/\$
154	153	adantr 276	. . . 4 $/\$ $/\$
155	152, 154	mpbird 167	. . 3 $/\$ $/\$
156		iffalse 3648	. . . 4
157	156	adantl 277	. . 3 $/\$ $/\$
158	155, 157	eqtr4d 2274	. 2 $/\$ $/\$
159		simpr 110	. . . 4 $/\$
160		dvdsdc 12565	. . . 4 $/\$ DECID
161	159, 4, 160	syl2anc 415	. . 3 $/\$ DECID
162		exmiddc 848	. . 3 DECID $\/$
163	161, 162	syl 14	. 2 $/\$ $\/$
164	73, 158, 163	mpjaodan 810	1 $/\$

Colors of variables: wff set class

This proof depends on syntax axioms:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 720 DECID wdc 846

wceq 1402

wcel 2209

wne 2420

cif 3638 class class class wbr 4130

cfv 5377 (class class class)co 6085

cc 8177

cr 8178

cc0 8179

c1 8180

caddc 8182

cmul 8184

clt 8360

cle 8361

cmin 8497 # cap 8909

cdiv 9002

cn 9304

cn0 9563

cz 9644

cq 10019

cfl 10703

cmo 10759

cdvds 12554

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4249 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-id 4438 df-po 4441 df-iso 4442 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-fv 5385 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8903 df-ap 8910 df-div 9003 df-inn 9305 df-n0 9564 df-z 9645 df-uz 9922 df-q 10020 df-rp 10055 df-fl 10705 df-mod 10760 df-dvds 12555

This theorem is used by: pcfac 13129

W3C validator