fldivp1 - Intuitionistic Logic Explorer

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

Theorem fldivp1 12941

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 9500	. . . . . . . . 9
2		nnne0 9173	. . . . . . . . 9
3		peano2z 9517	. . . . . . . . . 10
4	3	adantr 276	. . . . . . . . 9 $/\$
5		dvdsval2 12371	. . . . . . . . 9 $/\$ $/\$
6	1, 2, 4, 5	syl2an23an 1335	. . . . . . . 8 $/\$
7	6	biimpa 296	. . . . . . 7 $/\$ $/\$
8		flid 10547	. . . . . . 7
9	7, 8	syl 14	. . . . . 6 $/\$ $/\$
10		nnm1nn0 9445	. . . . . . . . . 10
11	10	nn0red 9458	. . . . . . . . 9
12	10	nn0ge0d 9460	. . . . . . . . 9
13		nnre 9152	. . . . . . . . 9
14		nngt0 9170	. . . . . . . . 9
15		divge0 9055	. . . . . . . . 9 $/\$ $/\$ $/\$
16	11, 12, 13, 14, 15	syl22anc 1274	. . . . . . . 8
17	16	ad2antlr 489	. . . . . . 7 $/\$ $/\$
18	13	ltm1d 9114	. . . . . . . . . 10
19		nncn 9153	. . . . . . . . . . 11
20	19	mulridd 8198	. . . . . . . . . 10
21	18, 20	breqtrrd 4115	. . . . . . . . 9
22		1red 8196	. . . . . . . . . 10
23		ltdivmul 9058	. . . . . . . . . 10 $/\$ $/\$ $/\$
24	11, 22, 13, 14, 23	syl112anc 1277	. . . . . . . . 9
25	21, 24	mpbird 167	. . . . . . . 8
26	25	ad2antlr 489	. . . . . . 7 $/\$ $/\$
27	10	nn0zd 9602	. . . . . . . . . 10
28		znq 9860	. . . . . . . . . 10 $/\$
29	27, 28	mpancom 422	. . . . . . . . 9
30	29	ad2antlr 489	. . . . . . . 8 $/\$ $/\$
31		flqbi2 10554	. . . . . . . 8 $/\$ $/\$
32	7, 30, 31	syl2anc 411	. . . . . . 7 $/\$ $/\$ $/\$
33	17, 26, 32	mpbir2and 952	. . . . . 6 $/\$ $/\$
34	9, 33	eqtr4d 2266	. . . . 5 $/\$ $/\$
35		zcn 9486	. . . . . . . . . 10
36	35	adantr 276	. . . . . . . . 9 $/\$
37	19	adantl 277	. . . . . . . . 9 $/\$
38		nnap0 9174	. . . . . . . . . 10 #
39	38	adantl 277	. . . . . . . . 9 $/\$ #
40	36, 37, 37, 39	divdirapd 9011	. . . . . . . 8 $/\$
41		ax-1cn 8127	. . . . . . . . . . . 12
42	41	a1i 9	. . . . . . . . . . 11 $/\$
43	36, 42, 37	ppncand 8532	. . . . . . . . . 10 $/\$
44	43	oveq1d 6035	. . . . . . . . 9 $/\$
45	4	zcnd 9605	. . . . . . . . . 10 $/\$
46		subcl 8380	. . . . . . . . . . . 12 $/\$
47	19, 41, 46	sylancl 413	. . . . . . . . . . 11
48	47	adantl 277	. . . . . . . . . 10 $/\$
49	45, 48, 37, 39	divdirapd 9011	. . . . . . . . 9 $/\$
50	44, 49	eqtr3d 2265	. . . . . . . 8 $/\$
51	37, 39	dividapd 8968	. . . . . . . . 9 $/\$
52	51	oveq2d 6036	. . . . . . . 8 $/\$
53	40, 50, 52	3eqtr3d 2271	. . . . . . 7 $/\$
54	53	fveq2d 5643	. . . . . 6 $/\$
55	54	adantr 276	. . . . 5 $/\$ $/\$
56		znq 9860	. . . . . . 7 $/\$
57		1z 9507	. . . . . . 7
58		flqaddz 10560	. . . . . . 7 $/\$
59	56, 57, 58	sylancl 413	. . . . . 6 $/\$
60	59	adantr 276	. . . . 5 $/\$ $/\$
61	34, 55, 60	3eqtrrd 2268	. . . 4 $/\$ $/\$
62		znq 9860	. . . . . . . . 9 $/\$
63	3, 62	sylan 283	. . . . . . . 8 $/\$
64	63	flqcld 10540	. . . . . . 7 $/\$
65	64	zcnd 9605	. . . . . 6 $/\$
66	56	flqcld 10540	. . . . . . 7 $/\$
67	66	zcnd 9605	. . . . . 6 $/\$
68	65, 67, 42	subaddd 8510	. . . . 5 $/\$
69	68	adantr 276	. . . 4 $/\$ $/\$
70	61, 69	mpbird 167	. . 3 $/\$ $/\$
71		iftrue 3609	. . . 4
72	71	adantl 277	. . 3 $/\$ $/\$
73	70, 72	eqtr4d 2266	. 2 $/\$ $/\$
74		zmodcl 10609	. . . . . . . . . . 11 $/\$
75	3, 74	sylan 283	. . . . . . . . . 10 $/\$
76	75	nn0red 9458	. . . . . . . . 9 $/\$
77		1re 8180	. . . . . . . . 9
78		resubcl 8445	. . . . . . . . 9 $/\$
79	76, 77, 78	sylancl 413	. . . . . . . 8 $/\$
80	79	adantr 276	. . . . . . 7 $/\$ $/\$
81	75	nn0zd 9602	. . . . . . . . . . . 12 $/\$
82		elnndc 9848	. . . . . . . . . . . 12 DECID
83	81, 82	syl 14	. . . . . . . . . . 11 $/\$ DECID
84		elnn0 9406	. . . . . . . . . . . . . 14 $\/$
85	75, 84	sylib 122	. . . . . . . . . . . . 13 $/\$ $\/$
86	85	ord 731	. . . . . . . . . . . 12 $/\$
87		id 19	. . . . . . . . . . . . 13
88		dvdsval3 12372	. . . . . . . . . . . . 13 $/\$
89	87, 3, 88	syl2anr 290	. . . . . . . . . . . 12 $/\$
90	86, 89	sylibrd 169	. . . . . . . . . . 11 $/\$
91		con1dc 863	. . . . . . . . . . 11 DECID
92	83, 90, 91	sylc 62	. . . . . . . . . 10 $/\$
93	92	imp 124	. . . . . . . . 9 $/\$ $/\$
94		nnm1nn0 9445	. . . . . . . . 9
95	93, 94	syl 14	. . . . . . . 8 $/\$ $/\$
96	95	nn0ge0d 9460	. . . . . . 7 $/\$ $/\$
97	13, 14	jca 306	. . . . . . . 8 $/\$
98	97	ad2antlr 489	. . . . . . 7 $/\$ $/\$ $/\$
99		divge0 9055	. . . . . . 7 $/\$ $/\$ $/\$
100	80, 96, 98, 99	syl21anc 1272	. . . . . 6 $/\$ $/\$
101	13	adantl 277	. . . . . . . . . 10 $/\$
102	76	ltm1d 9114	. . . . . . . . . 10 $/\$
103		zq 9862	. . . . . . . . . . . . 13
104	3, 103	syl 14	. . . . . . . . . . . 12
105	104	adantr 276	. . . . . . . . . . 11 $/\$
106		nnq 9869	. . . . . . . . . . . 12
107	106	adantl 277	. . . . . . . . . . 11 $/\$
108	14	adantl 277	. . . . . . . . . . 11 $/\$
109		modqlt 10598	. . . . . . . . . . 11 $/\$ $/\$
110	105, 107, 108, 109	syl3anc 1273	. . . . . . . . . 10 $/\$
111	79, 76, 101, 102, 110	lttrd 8307	. . . . . . . . 9 $/\$
112	37	mulridd 8198	. . . . . . . . 9 $/\$
113	111, 112	breqtrrd 4115	. . . . . . . 8 $/\$
114		1red 8196	. . . . . . . . 9 $/\$
115		ltdivmul 9058	. . . . . . . . 9 $/\$ $/\$ $/\$
116	79, 114, 101, 108, 115	syl112anc 1277	. . . . . . . 8 $/\$
117	113, 116	mpbird 167	. . . . . . 7 $/\$
118	117	adantr 276	. . . . . 6 $/\$ $/\$
119		peano2zm 9519	. . . . . . . . . 10
120	81, 119	syl 14	. . . . . . . . 9 $/\$
121		znq 9860	. . . . . . . . 9 $/\$
122	120, 121	sylancom 420	. . . . . . . 8 $/\$
123		flqbi2 10554	. . . . . . . 8 $/\$ $/\$
124	64, 122, 123	syl2anc 411	. . . . . . 7 $/\$ $/\$
125	124	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
126	100, 118, 125	mpbir2and 952	. . . . 5 $/\$ $/\$
127		modqval 10589	. . . . . . . . . . . . 13 $/\$ $/\$
128	105, 107, 108, 127	syl3anc 1273	. . . . . . . . . . . 12 $/\$
129	128	oveq1d 6035	. . . . . . . . . . 11 $/\$
130	37, 65	mulcld 8202	. . . . . . . . . . . 12 $/\$
131	45, 42, 130	sub32d 8524	. . . . . . . . . . 11 $/\$
132		pncan 8387	. . . . . . . . . . . . 13 $/\$
133	36, 41, 132	sylancl 413	. . . . . . . . . . . 12 $/\$
134	133	oveq1d 6035	. . . . . . . . . . 11 $/\$
135	129, 131, 134	3eqtr2d 2269	. . . . . . . . . 10 $/\$
136	135	oveq1d 6035	. . . . . . . . 9 $/\$
137	36, 130, 37, 39	divsubdirapd 9012	. . . . . . . . 9 $/\$
138	65, 37, 39	divcanap3d 8977	. . . . . . . . . 10 $/\$
139	138	oveq2d 6036	. . . . . . . . 9 $/\$
140	136, 137, 139	3eqtrrd 2268	. . . . . . . 8 $/\$
141		zre 9485	. . . . . . . . . . 11
142		nndivre 9181	. . . . . . . . . . 11 $/\$
143	141, 142	sylan 283	. . . . . . . . . 10 $/\$
144	143	recnd 8210	. . . . . . . . 9 $/\$
145		nndivre 9181	. . . . . . . . . . 11 $/\$
146	79, 145	sylancom 420	. . . . . . . . . 10 $/\$
147	146	recnd 8210	. . . . . . . . 9 $/\$
148	144, 65, 147	subaddd 8510	. . . . . . . 8 $/\$
149	140, 148	mpbid 147	. . . . . . 7 $/\$
150	149	adantr 276	. . . . . 6 $/\$ $/\$
151	150	fveq2d 5643	. . . . 5 $/\$ $/\$
152	126, 151	eqtr3d 2265	. . . 4 $/\$ $/\$
153	65, 67	subeq0ad 8502	. . . . 5 $/\$
154	153	adantr 276	. . . 4 $/\$ $/\$
155	152, 154	mpbird 167	. . 3 $/\$ $/\$
156		iffalse 3612	. . . 4
157	156	adantl 277	. . 3 $/\$ $/\$
158	155, 157	eqtr4d 2266	. 2 $/\$ $/\$
159		simpr 110	. . . 4 $/\$
160		dvdsdc 12379	. . . 4 $/\$ DECID
161	159, 4, 160	syl2anc 411	. . 3 $/\$ DECID
162		exmiddc 843	. . 3 DECID $\/$
163	161, 162	syl 14	. 2 $/\$ $\/$
164	73, 158, 163	mpjaodan 805	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 715 DECID wdc 841

wceq 1397

wcel 2201

wne 2401

cif 3604 class class class wbr 4087

cfv 5325 (class class class)co 6020

cc 8032

cr 8033

cc0 8034

c1 8035

caddc 8037

cmul 8039

clt 8216

cle 8217

cmin 8352 # cap 8763

cdiv 8854

cn 9145

cn0 9404

cz 9481

cq 9855

cfl 10531

cmo 10587

cdvds 12368

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2203 ax-14 2204 ax-ext 2212 ax-sep 4206 ax-pow 4263 ax-pr 4298 ax-un 4529 ax-setind 4634 ax-cnex 8125 ax-resscn 8126 ax-1cn 8127 ax-1re 8128 ax-icn 8129 ax-addcl 8130 ax-addrcl 8131 ax-mulcl 8132 ax-mulrcl 8133 ax-addcom 8134 ax-mulcom 8135 ax-addass 8136 ax-mulass 8137 ax-distr 8138 ax-i2m1 8139 ax-0lt1 8140 ax-1rid 8141 ax-0id 8142 ax-rnegex 8143 ax-precex 8144 ax-cnre 8145 ax-pre-ltirr 8146 ax-pre-ltwlin 8147 ax-pre-lttrn 8148 ax-pre-apti 8149 ax-pre-ltadd 8150 ax-pre-mulgt0 8151 ax-pre-mulext 8152 ax-arch 8153

This theorem depends on definitions: df-bi 117 df-stab 838 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1810 df-eu 2081 df-mo 2082 df-clab 2217 df-cleq 2223 df-clel 2226 df-nfc 2362 df-ne 2402 df-nel 2497 df-ral 2514 df-rex 2515 df-reu 2516 df-rmo 2517 df-rab 2518 df-v 2803 df-sbc 3031 df-csb 3127 df-dif 3201 df-un 3203 df-in 3205 df-ss 3212 df-if 3605 df-pw 3653 df-sn 3674 df-pr 3675 df-op 3677 df-uni 3893 df-int 3928 df-iun 3971 df-br 4088 df-opab 4150 df-mpt 4151 df-id 4389 df-po 4392 df-iso 4393 df-xp 4730 df-rel 4731 df-cnv 4732 df-co 4733 df-dm 4734 df-rn 4735 df-res 4736 df-ima 4737 df-iota 5285 df-fun 5327 df-fn 5328 df-f 5329 df-fv 5333 df-riota 5973 df-ov 6023 df-oprab 6024 df-mpo 6025 df-1st 6305 df-2nd 6306 df-pnf 8218 df-mnf 8219 df-xr 8220 df-ltxr 8221 df-le 8222 df-sub 8354 df-neg 8355 df-reap 8757 df-ap 8764 df-div 8855 df-inn 9146 df-n0 9405 df-z 9482 df-uz 9758 df-q 9856 df-rp 9891 df-fl 10533 df-mod 10588 df-dvds 12369

This theorem is referenced by: pcfac 12943

W3C validator