fldivp1 - Intuitionistic Logic Explorer

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

Theorem fldivp1 12329

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 9261	. . . . . . . . 9
2		nnne0 8936	. . . . . . . . 9
3		peano2z 9278	. . . . . . . . . 10
4	3	adantr 276	. . . . . . . . 9 $/\$
5		dvdsval2 11781	. . . . . . . . 9 $/\$ $/\$
6	1, 2, 4, 5	syl2an23an 1299	. . . . . . . 8 $/\$
7	6	biimpa 296	. . . . . . 7 $/\$ $/\$
8		flid 10270	. . . . . . 7
9	7, 8	syl 14	. . . . . 6 $/\$ $/\$
10		nnm1nn0 9206	. . . . . . . . . 10
11	10	nn0red 9219	. . . . . . . . 9
12	10	nn0ge0d 9221	. . . . . . . . 9
13		nnre 8915	. . . . . . . . 9
14		nngt0 8933	. . . . . . . . 9
15		divge0 8819	. . . . . . . . 9 $/\$ $/\$ $/\$
16	11, 12, 13, 14, 15	syl22anc 1239	. . . . . . . 8
17	16	ad2antlr 489	. . . . . . 7 $/\$ $/\$
18	13	ltm1d 8878	. . . . . . . . . 10
19		nncn 8916	. . . . . . . . . . 11
20	19	mulid1d 7965	. . . . . . . . . 10
21	18, 20	breqtrrd 4028	. . . . . . . . 9
22		1red 7963	. . . . . . . . . 10
23		ltdivmul 8822	. . . . . . . . . 10 $/\$ $/\$ $/\$
24	11, 22, 13, 14, 23	syl112anc 1242	. . . . . . . . 9
25	21, 24	mpbird 167	. . . . . . . 8
26	25	ad2antlr 489	. . . . . . 7 $/\$ $/\$
27	10	nn0zd 9362	. . . . . . . . . 10
28		znq 9613	. . . . . . . . . 10 $/\$
29	27, 28	mpancom 422	. . . . . . . . 9
30	29	ad2antlr 489	. . . . . . . 8 $/\$ $/\$
31		flqbi2 10277	. . . . . . . 8 $/\$ $/\$
32	7, 30, 31	syl2anc 411	. . . . . . 7 $/\$ $/\$ $/\$
33	17, 26, 32	mpbir2and 944	. . . . . 6 $/\$ $/\$
34	9, 33	eqtr4d 2213	. . . . 5 $/\$ $/\$
35		zcn 9247	. . . . . . . . . 10
36	35	adantr 276	. . . . . . . . 9 $/\$
37	19	adantl 277	. . . . . . . . 9 $/\$
38		nnap0 8937	. . . . . . . . . 10 #
39	38	adantl 277	. . . . . . . . 9 $/\$ #
40	36, 37, 37, 39	divdirapd 8775	. . . . . . . 8 $/\$
41		ax-1cn 7895	. . . . . . . . . . . 12
42	41	a1i 9	. . . . . . . . . . 11 $/\$
43	36, 42, 37	ppncand 8298	. . . . . . . . . 10 $/\$
44	43	oveq1d 5884	. . . . . . . . 9 $/\$
45	4	zcnd 9365	. . . . . . . . . 10 $/\$
46		subcl 8146	. . . . . . . . . . . 12 $/\$
47	19, 41, 46	sylancl 413	. . . . . . . . . . 11
48	47	adantl 277	. . . . . . . . . 10 $/\$
49	45, 48, 37, 39	divdirapd 8775	. . . . . . . . 9 $/\$
50	44, 49	eqtr3d 2212	. . . . . . . 8 $/\$
51	37, 39	dividapd 8732	. . . . . . . . 9 $/\$
52	51	oveq2d 5885	. . . . . . . 8 $/\$
53	40, 50, 52	3eqtr3d 2218	. . . . . . 7 $/\$
54	53	fveq2d 5515	. . . . . 6 $/\$
55	54	adantr 276	. . . . 5 $/\$ $/\$
56		znq 9613	. . . . . . 7 $/\$
57		1z 9268	. . . . . . 7
58		flqaddz 10283	. . . . . . 7 $/\$
59	56, 57, 58	sylancl 413	. . . . . 6 $/\$
60	59	adantr 276	. . . . 5 $/\$ $/\$
61	34, 55, 60	3eqtrrd 2215	. . . 4 $/\$ $/\$
62		znq 9613	. . . . . . . . 9 $/\$
63	3, 62	sylan 283	. . . . . . . 8 $/\$
64	63	flqcld 10263	. . . . . . 7 $/\$
65	64	zcnd 9365	. . . . . 6 $/\$
66	56	flqcld 10263	. . . . . . 7 $/\$
67	66	zcnd 9365	. . . . . 6 $/\$
68	65, 67, 42	subaddd 8276	. . . . 5 $/\$
69	68	adantr 276	. . . 4 $/\$ $/\$
70	61, 69	mpbird 167	. . 3 $/\$ $/\$
71		iftrue 3539	. . . 4
72	71	adantl 277	. . 3 $/\$ $/\$
73	70, 72	eqtr4d 2213	. 2 $/\$ $/\$
74		zmodcl 10330	. . . . . . . . . . 11 $/\$
75	3, 74	sylan 283	. . . . . . . . . 10 $/\$
76	75	nn0red 9219	. . . . . . . . 9 $/\$
77		1re 7947	. . . . . . . . 9
78		resubcl 8211	. . . . . . . . 9 $/\$
79	76, 77, 78	sylancl 413	. . . . . . . 8 $/\$
80	79	adantr 276	. . . . . . 7 $/\$ $/\$
81	75	nn0zd 9362	. . . . . . . . . . . 12 $/\$
82		elnndc 9601	. . . . . . . . . . . 12 DECID
83	81, 82	syl 14	. . . . . . . . . . 11 $/\$ DECID
84		elnn0 9167	. . . . . . . . . . . . . 14 $\/$
85	75, 84	sylib 122	. . . . . . . . . . . . 13 $/\$ $\/$
86	85	ord 724	. . . . . . . . . . . 12 $/\$
87		id 19	. . . . . . . . . . . . 13
88		dvdsval3 11782	. . . . . . . . . . . . 13 $/\$
89	87, 3, 88	syl2anr 290	. . . . . . . . . . . 12 $/\$
90	86, 89	sylibrd 169	. . . . . . . . . . 11 $/\$
91		con1dc 856	. . . . . . . . . . 11 DECID
92	83, 90, 91	sylc 62	. . . . . . . . . 10 $/\$
93	92	imp 124	. . . . . . . . 9 $/\$ $/\$
94		nnm1nn0 9206	. . . . . . . . 9
95	93, 94	syl 14	. . . . . . . 8 $/\$ $/\$
96	95	nn0ge0d 9221	. . . . . . 7 $/\$ $/\$
97	13, 14	jca 306	. . . . . . . 8 $/\$
98	97	ad2antlr 489	. . . . . . 7 $/\$ $/\$ $/\$
99		divge0 8819	. . . . . . 7 $/\$ $/\$ $/\$
100	80, 96, 98, 99	syl21anc 1237	. . . . . 6 $/\$ $/\$
101	13	adantl 277	. . . . . . . . . 10 $/\$
102	76	ltm1d 8878	. . . . . . . . . 10 $/\$
103		zq 9615	. . . . . . . . . . . . 13
104	3, 103	syl 14	. . . . . . . . . . . 12
105	104	adantr 276	. . . . . . . . . . 11 $/\$
106		nnq 9622	. . . . . . . . . . . 12
107	106	adantl 277	. . . . . . . . . . 11 $/\$
108	14	adantl 277	. . . . . . . . . . 11 $/\$
109		modqlt 10319	. . . . . . . . . . 11 $/\$ $/\$
110	105, 107, 108, 109	syl3anc 1238	. . . . . . . . . 10 $/\$
111	79, 76, 101, 102, 110	lttrd 8073	. . . . . . . . 9 $/\$
112	37	mulid1d 7965	. . . . . . . . 9 $/\$
113	111, 112	breqtrrd 4028	. . . . . . . 8 $/\$
114		1red 7963	. . . . . . . . 9 $/\$
115		ltdivmul 8822	. . . . . . . . 9 $/\$ $/\$ $/\$
116	79, 114, 101, 108, 115	syl112anc 1242	. . . . . . . 8 $/\$
117	113, 116	mpbird 167	. . . . . . 7 $/\$
118	117	adantr 276	. . . . . 6 $/\$ $/\$
119		peano2zm 9280	. . . . . . . . . 10
120	81, 119	syl 14	. . . . . . . . 9 $/\$
121		znq 9613	. . . . . . . . 9 $/\$
122	120, 121	sylancom 420	. . . . . . . 8 $/\$
123		flqbi2 10277	. . . . . . . 8 $/\$ $/\$
124	64, 122, 123	syl2anc 411	. . . . . . 7 $/\$ $/\$
125	124	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
126	100, 118, 125	mpbir2and 944	. . . . 5 $/\$ $/\$
127		modqval 10310	. . . . . . . . . . . . 13 $/\$ $/\$
128	105, 107, 108, 127	syl3anc 1238	. . . . . . . . . . . 12 $/\$
129	128	oveq1d 5884	. . . . . . . . . . 11 $/\$
130	37, 65	mulcld 7968	. . . . . . . . . . . 12 $/\$
131	45, 42, 130	sub32d 8290	. . . . . . . . . . 11 $/\$
132		pncan 8153	. . . . . . . . . . . . 13 $/\$
133	36, 41, 132	sylancl 413	. . . . . . . . . . . 12 $/\$
134	133	oveq1d 5884	. . . . . . . . . . 11 $/\$
135	129, 131, 134	3eqtr2d 2216	. . . . . . . . . 10 $/\$
136	135	oveq1d 5884	. . . . . . . . 9 $/\$
137	36, 130, 37, 39	divsubdirapd 8776	. . . . . . . . 9 $/\$
138	65, 37, 39	divcanap3d 8741	. . . . . . . . . 10 $/\$
139	138	oveq2d 5885	. . . . . . . . 9 $/\$
140	136, 137, 139	3eqtrrd 2215	. . . . . . . 8 $/\$
141		zre 9246	. . . . . . . . . . 11
142		nndivre 8944	. . . . . . . . . . 11 $/\$
143	141, 142	sylan 283	. . . . . . . . . 10 $/\$
144	143	recnd 7976	. . . . . . . . 9 $/\$
145		nndivre 8944	. . . . . . . . . . 11 $/\$
146	79, 145	sylancom 420	. . . . . . . . . 10 $/\$
147	146	recnd 7976	. . . . . . . . 9 $/\$
148	144, 65, 147	subaddd 8276	. . . . . . . 8 $/\$
149	140, 148	mpbid 147	. . . . . . 7 $/\$
150	149	adantr 276	. . . . . 6 $/\$ $/\$
151	150	fveq2d 5515	. . . . 5 $/\$ $/\$
152	126, 151	eqtr3d 2212	. . . 4 $/\$ $/\$
153	65, 67	subeq0ad 8268	. . . . 5 $/\$
154	153	adantr 276	. . . 4 $/\$ $/\$
155	152, 154	mpbird 167	. . 3 $/\$ $/\$
156		iffalse 3542	. . . 4
157	156	adantl 277	. . 3 $/\$ $/\$
158	155, 157	eqtr4d 2213	. 2 $/\$ $/\$
159		simpr 110	. . . 4 $/\$
160		dvdsdc 11789	. . . 4 $/\$ DECID
161	159, 4, 160	syl2anc 411	. . 3 $/\$ DECID
162		exmiddc 836	. . 3 DECID $\/$
163	161, 162	syl 14	. 2 $/\$ $\/$
164	73, 158, 163	mpjaodan 798	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 708 DECID wdc 834

wceq 1353

wcel 2148

wne 2347

cif 3534 class class class wbr 4000

cfv 5212 (class class class)co 5869

cc 7800

cr 7801

cc0 7802

c1 7803

caddc 7805

cmul 7807

clt 7982

cle 7983

cmin 8118 # cap 8528

cdiv 8618

cn 8908

cn0 9165

cz 9242

cq 9608

cfl 10254

cmo 10308

cdvds 11778

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 4118 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-cnex 7893 ax-resscn 7894 ax-1cn 7895 ax-1re 7896 ax-icn 7897 ax-addcl 7898 ax-addrcl 7899 ax-mulcl 7900 ax-mulrcl 7901 ax-addcom 7902 ax-mulcom 7903 ax-addass 7904 ax-mulass 7905 ax-distr 7906 ax-i2m1 7907 ax-0lt1 7908 ax-1rid 7909 ax-0id 7910 ax-rnegex 7911 ax-precex 7912 ax-cnre 7913 ax-pre-ltirr 7914 ax-pre-ltwlin 7915 ax-pre-lttrn 7916 ax-pre-apti 7917 ax-pre-ltadd 7918 ax-pre-mulgt0 7919 ax-pre-mulext 7920 ax-arch 7921

This theorem depends on definitions: df-bi 117 df-stab 831 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-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-if 3535 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-id 4290 df-po 4293 df-iso 4294 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-fv 5220 df-riota 5825 df-ov 5872 df-oprab 5873 df-mpo 5874 df-1st 6135 df-2nd 6136 df-pnf 7984 df-mnf 7985 df-xr 7986 df-ltxr 7987 df-le 7988 df-sub 8120 df-neg 8121 df-reap 8522 df-ap 8529 df-div 8619 df-inn 8909 df-n0 9166 df-z 9243 df-uz 9518 df-q 9609 df-rp 9641 df-fl 10256 df-mod 10309 df-dvds 11779

This theorem is referenced by: pcfac 12331

W3C validator