fldivp1 - Intuitionistic Logic Explorer

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

Theorem fldivp1 12360

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 9286	. . . . . . . . 9
2		nnne0 8961	. . . . . . . . 9
3		peano2z 9303	. . . . . . . . . 10
4	3	adantr 276	. . . . . . . . 9 $/\$
5		dvdsval2 11811	. . . . . . . . 9 $/\$ $/\$
6	1, 2, 4, 5	syl2an23an 1309	. . . . . . . 8 $/\$
7	6	biimpa 296	. . . . . . 7 $/\$ $/\$
8		flid 10298	. . . . . . 7
9	7, 8	syl 14	. . . . . 6 $/\$ $/\$
10		nnm1nn0 9231	. . . . . . . . . 10
11	10	nn0red 9244	. . . . . . . . 9
12	10	nn0ge0d 9246	. . . . . . . . 9
13		nnre 8940	. . . . . . . . 9
14		nngt0 8958	. . . . . . . . 9
15		divge0 8844	. . . . . . . . 9 $/\$ $/\$ $/\$
16	11, 12, 13, 14, 15	syl22anc 1249	. . . . . . . 8
17	16	ad2antlr 489	. . . . . . 7 $/\$ $/\$
18	13	ltm1d 8903	. . . . . . . . . 10
19		nncn 8941	. . . . . . . . . . 11
20	19	mulridd 7988	. . . . . . . . . 10
21	18, 20	breqtrrd 4043	. . . . . . . . 9
22		1red 7986	. . . . . . . . . 10
23		ltdivmul 8847	. . . . . . . . . 10 $/\$ $/\$ $/\$
24	11, 22, 13, 14, 23	syl112anc 1252	. . . . . . . . 9
25	21, 24	mpbird 167	. . . . . . . 8
26	25	ad2antlr 489	. . . . . . 7 $/\$ $/\$
27	10	nn0zd 9387	. . . . . . . . . 10
28		znq 9638	. . . . . . . . . 10 $/\$
29	27, 28	mpancom 422	. . . . . . . . 9
30	29	ad2antlr 489	. . . . . . . 8 $/\$ $/\$
31		flqbi2 10305	. . . . . . . 8 $/\$ $/\$
32	7, 30, 31	syl2anc 411	. . . . . . 7 $/\$ $/\$ $/\$
33	17, 26, 32	mpbir2and 945	. . . . . 6 $/\$ $/\$
34	9, 33	eqtr4d 2223	. . . . 5 $/\$ $/\$
35		zcn 9272	. . . . . . . . . 10
36	35	adantr 276	. . . . . . . . 9 $/\$
37	19	adantl 277	. . . . . . . . 9 $/\$
38		nnap0 8962	. . . . . . . . . 10 #
39	38	adantl 277	. . . . . . . . 9 $/\$ #
40	36, 37, 37, 39	divdirapd 8800	. . . . . . . 8 $/\$
41		ax-1cn 7918	. . . . . . . . . . . 12
42	41	a1i 9	. . . . . . . . . . 11 $/\$
43	36, 42, 37	ppncand 8322	. . . . . . . . . 10 $/\$
44	43	oveq1d 5903	. . . . . . . . 9 $/\$
45	4	zcnd 9390	. . . . . . . . . 10 $/\$
46		subcl 8170	. . . . . . . . . . . 12 $/\$
47	19, 41, 46	sylancl 413	. . . . . . . . . . 11
48	47	adantl 277	. . . . . . . . . 10 $/\$
49	45, 48, 37, 39	divdirapd 8800	. . . . . . . . 9 $/\$
50	44, 49	eqtr3d 2222	. . . . . . . 8 $/\$
51	37, 39	dividapd 8757	. . . . . . . . 9 $/\$
52	51	oveq2d 5904	. . . . . . . 8 $/\$
53	40, 50, 52	3eqtr3d 2228	. . . . . . 7 $/\$
54	53	fveq2d 5531	. . . . . 6 $/\$
55	54	adantr 276	. . . . 5 $/\$ $/\$
56		znq 9638	. . . . . . 7 $/\$
57		1z 9293	. . . . . . 7
58		flqaddz 10311	. . . . . . 7 $/\$
59	56, 57, 58	sylancl 413	. . . . . 6 $/\$
60	59	adantr 276	. . . . 5 $/\$ $/\$
61	34, 55, 60	3eqtrrd 2225	. . . 4 $/\$ $/\$
62		znq 9638	. . . . . . . . 9 $/\$
63	3, 62	sylan 283	. . . . . . . 8 $/\$
64	63	flqcld 10291	. . . . . . 7 $/\$
65	64	zcnd 9390	. . . . . 6 $/\$
66	56	flqcld 10291	. . . . . . 7 $/\$
67	66	zcnd 9390	. . . . . 6 $/\$
68	65, 67, 42	subaddd 8300	. . . . 5 $/\$
69	68	adantr 276	. . . 4 $/\$ $/\$
70	61, 69	mpbird 167	. . 3 $/\$ $/\$
71		iftrue 3551	. . . 4
72	71	adantl 277	. . 3 $/\$ $/\$
73	70, 72	eqtr4d 2223	. 2 $/\$ $/\$
74		zmodcl 10358	. . . . . . . . . . 11 $/\$
75	3, 74	sylan 283	. . . . . . . . . 10 $/\$
76	75	nn0red 9244	. . . . . . . . 9 $/\$
77		1re 7970	. . . . . . . . 9
78		resubcl 8235	. . . . . . . . 9 $/\$
79	76, 77, 78	sylancl 413	. . . . . . . 8 $/\$
80	79	adantr 276	. . . . . . 7 $/\$ $/\$
81	75	nn0zd 9387	. . . . . . . . . . . 12 $/\$
82		elnndc 9626	. . . . . . . . . . . 12 DECID
83	81, 82	syl 14	. . . . . . . . . . 11 $/\$ DECID
84		elnn0 9192	. . . . . . . . . . . . . 14 $\/$
85	75, 84	sylib 122	. . . . . . . . . . . . 13 $/\$ $\/$
86	85	ord 725	. . . . . . . . . . . 12 $/\$
87		id 19	. . . . . . . . . . . . 13
88		dvdsval3 11812	. . . . . . . . . . . . 13 $/\$
89	87, 3, 88	syl2anr 290	. . . . . . . . . . . 12 $/\$
90	86, 89	sylibrd 169	. . . . . . . . . . 11 $/\$
91		con1dc 857	. . . . . . . . . . 11 DECID
92	83, 90, 91	sylc 62	. . . . . . . . . 10 $/\$
93	92	imp 124	. . . . . . . . 9 $/\$ $/\$
94		nnm1nn0 9231	. . . . . . . . 9
95	93, 94	syl 14	. . . . . . . 8 $/\$ $/\$
96	95	nn0ge0d 9246	. . . . . . 7 $/\$ $/\$
97	13, 14	jca 306	. . . . . . . 8 $/\$
98	97	ad2antlr 489	. . . . . . 7 $/\$ $/\$ $/\$
99		divge0 8844	. . . . . . 7 $/\$ $/\$ $/\$
100	80, 96, 98, 99	syl21anc 1247	. . . . . 6 $/\$ $/\$
101	13	adantl 277	. . . . . . . . . 10 $/\$
102	76	ltm1d 8903	. . . . . . . . . 10 $/\$
103		zq 9640	. . . . . . . . . . . . 13
104	3, 103	syl 14	. . . . . . . . . . . 12
105	104	adantr 276	. . . . . . . . . . 11 $/\$
106		nnq 9647	. . . . . . . . . . . 12
107	106	adantl 277	. . . . . . . . . . 11 $/\$
108	14	adantl 277	. . . . . . . . . . 11 $/\$
109		modqlt 10347	. . . . . . . . . . 11 $/\$ $/\$
110	105, 107, 108, 109	syl3anc 1248	. . . . . . . . . 10 $/\$
111	79, 76, 101, 102, 110	lttrd 8097	. . . . . . . . 9 $/\$
112	37	mulridd 7988	. . . . . . . . 9 $/\$
113	111, 112	breqtrrd 4043	. . . . . . . 8 $/\$
114		1red 7986	. . . . . . . . 9 $/\$
115		ltdivmul 8847	. . . . . . . . 9 $/\$ $/\$ $/\$
116	79, 114, 101, 108, 115	syl112anc 1252	. . . . . . . 8 $/\$
117	113, 116	mpbird 167	. . . . . . 7 $/\$
118	117	adantr 276	. . . . . 6 $/\$ $/\$
119		peano2zm 9305	. . . . . . . . . 10
120	81, 119	syl 14	. . . . . . . . 9 $/\$
121		znq 9638	. . . . . . . . 9 $/\$
122	120, 121	sylancom 420	. . . . . . . 8 $/\$
123		flqbi2 10305	. . . . . . . 8 $/\$ $/\$
124	64, 122, 123	syl2anc 411	. . . . . . 7 $/\$ $/\$
125	124	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
126	100, 118, 125	mpbir2and 945	. . . . 5 $/\$ $/\$
127		modqval 10338	. . . . . . . . . . . . 13 $/\$ $/\$
128	105, 107, 108, 127	syl3anc 1248	. . . . . . . . . . . 12 $/\$
129	128	oveq1d 5903	. . . . . . . . . . 11 $/\$
130	37, 65	mulcld 7992	. . . . . . . . . . . 12 $/\$
131	45, 42, 130	sub32d 8314	. . . . . . . . . . 11 $/\$
132		pncan 8177	. . . . . . . . . . . . 13 $/\$
133	36, 41, 132	sylancl 413	. . . . . . . . . . . 12 $/\$
134	133	oveq1d 5903	. . . . . . . . . . 11 $/\$
135	129, 131, 134	3eqtr2d 2226	. . . . . . . . . 10 $/\$
136	135	oveq1d 5903	. . . . . . . . 9 $/\$
137	36, 130, 37, 39	divsubdirapd 8801	. . . . . . . . 9 $/\$
138	65, 37, 39	divcanap3d 8766	. . . . . . . . . 10 $/\$
139	138	oveq2d 5904	. . . . . . . . 9 $/\$
140	136, 137, 139	3eqtrrd 2225	. . . . . . . 8 $/\$
141		zre 9271	. . . . . . . . . . 11
142		nndivre 8969	. . . . . . . . . . 11 $/\$
143	141, 142	sylan 283	. . . . . . . . . 10 $/\$
144	143	recnd 8000	. . . . . . . . 9 $/\$
145		nndivre 8969	. . . . . . . . . . 11 $/\$
146	79, 145	sylancom 420	. . . . . . . . . 10 $/\$
147	146	recnd 8000	. . . . . . . . 9 $/\$
148	144, 65, 147	subaddd 8300	. . . . . . . 8 $/\$
149	140, 148	mpbid 147	. . . . . . 7 $/\$
150	149	adantr 276	. . . . . 6 $/\$ $/\$
151	150	fveq2d 5531	. . . . 5 $/\$ $/\$
152	126, 151	eqtr3d 2222	. . . 4 $/\$ $/\$
153	65, 67	subeq0ad 8292	. . . . 5 $/\$
154	153	adantr 276	. . . 4 $/\$ $/\$
155	152, 154	mpbird 167	. . 3 $/\$ $/\$
156		iffalse 3554	. . . 4
157	156	adantl 277	. . 3 $/\$ $/\$
158	155, 157	eqtr4d 2223	. 2 $/\$ $/\$
159		simpr 110	. . . 4 $/\$
160		dvdsdc 11819	. . . 4 $/\$ DECID
161	159, 4, 160	syl2anc 411	. . 3 $/\$ DECID
162		exmiddc 837	. . 3 DECID $\/$
163	161, 162	syl 14	. 2 $/\$ $\/$
164	73, 158, 163	mpjaodan 799	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709 DECID wdc 835

wceq 1363

wcel 2158

wne 2357

cif 3546 class class class wbr 4015

cfv 5228 (class class class)co 5888

cc 7823

cr 7824

cc0 7825

c1 7826

caddc 7828

cmul 7830

clt 8006

cle 8007

cmin 8142 # cap 8552

cdiv 8643

cn 8933

cn0 9190

cz 9267

cq 9633

cfl 10282

cmo 10336

cdvds 11808

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 615 ax-in2 616 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-sep 4133 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-setind 4548 ax-cnex 7916 ax-resscn 7917 ax-1cn 7918 ax-1re 7919 ax-icn 7920 ax-addcl 7921 ax-addrcl 7922 ax-mulcl 7923 ax-mulrcl 7924 ax-addcom 7925 ax-mulcom 7926 ax-addass 7927 ax-mulass 7928 ax-distr 7929 ax-i2m1 7930 ax-0lt1 7931 ax-1rid 7932 ax-0id 7933 ax-rnegex 7934 ax-precex 7935 ax-cnre 7936 ax-pre-ltirr 7937 ax-pre-ltwlin 7938 ax-pre-lttrn 7939 ax-pre-apti 7940 ax-pre-ltadd 7941 ax-pre-mulgt0 7942 ax-pre-mulext 7943 ax-arch 7944

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ne 2358 df-nel 2453 df-ral 2470 df-rex 2471 df-reu 2472 df-rmo 2473 df-rab 2474 df-v 2751 df-sbc 2975 df-csb 3070 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-if 3547 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-int 3857 df-iun 3900 df-br 4016 df-opab 4077 df-mpt 4078 df-id 4305 df-po 4308 df-iso 4309 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-rn 4649 df-res 4650 df-ima 4651 df-iota 5190 df-fun 5230 df-fn 5231 df-f 5232 df-fv 5236 df-riota 5844 df-ov 5891 df-oprab 5892 df-mpo 5893 df-1st 6155 df-2nd 6156 df-pnf 8008 df-mnf 8009 df-xr 8010 df-ltxr 8011 df-le 8012 df-sub 8144 df-neg 8145 df-reap 8546 df-ap 8553 df-div 8644 df-inn 8934 df-n0 9191 df-z 9268 df-uz 9543 df-q 9634 df-rp 9668 df-fl 10284 df-mod 10337 df-dvds 11809

This theorem is referenced by: pcfac 12362

W3C validator