fldivp1 - Intuitionistic Logic Explorer

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

Theorem fldivp1 12486

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 9336	. . . . . . . . 9
2		nnne0 9010	. . . . . . . . 9
3		peano2z 9353	. . . . . . . . . 10
4	3	adantr 276	. . . . . . . . 9 $/\$
5		dvdsval2 11933	. . . . . . . . 9 $/\$ $/\$
6	1, 2, 4, 5	syl2an23an 1310	. . . . . . . 8 $/\$
7	6	biimpa 296	. . . . . . 7 $/\$ $/\$
8		flid 10353	. . . . . . 7
9	7, 8	syl 14	. . . . . 6 $/\$ $/\$
10		nnm1nn0 9281	. . . . . . . . . 10
11	10	nn0red 9294	. . . . . . . . 9
12	10	nn0ge0d 9296	. . . . . . . . 9
13		nnre 8989	. . . . . . . . 9
14		nngt0 9007	. . . . . . . . 9
15		divge0 8892	. . . . . . . . 9 $/\$ $/\$ $/\$
16	11, 12, 13, 14, 15	syl22anc 1250	. . . . . . . 8
17	16	ad2antlr 489	. . . . . . 7 $/\$ $/\$
18	13	ltm1d 8951	. . . . . . . . . 10
19		nncn 8990	. . . . . . . . . . 11
20	19	mulridd 8036	. . . . . . . . . 10
21	18, 20	breqtrrd 4057	. . . . . . . . 9
22		1red 8034	. . . . . . . . . 10
23		ltdivmul 8895	. . . . . . . . . 10 $/\$ $/\$ $/\$
24	11, 22, 13, 14, 23	syl112anc 1253	. . . . . . . . 9
25	21, 24	mpbird 167	. . . . . . . 8
26	25	ad2antlr 489	. . . . . . 7 $/\$ $/\$
27	10	nn0zd 9437	. . . . . . . . . 10
28		znq 9689	. . . . . . . . . 10 $/\$
29	27, 28	mpancom 422	. . . . . . . . 9
30	29	ad2antlr 489	. . . . . . . 8 $/\$ $/\$
31		flqbi2 10360	. . . . . . . 8 $/\$ $/\$
32	7, 30, 31	syl2anc 411	. . . . . . 7 $/\$ $/\$ $/\$
33	17, 26, 32	mpbir2and 946	. . . . . 6 $/\$ $/\$
34	9, 33	eqtr4d 2229	. . . . 5 $/\$ $/\$
35		zcn 9322	. . . . . . . . . 10
36	35	adantr 276	. . . . . . . . 9 $/\$
37	19	adantl 277	. . . . . . . . 9 $/\$
38		nnap0 9011	. . . . . . . . . 10 #
39	38	adantl 277	. . . . . . . . 9 $/\$ #
40	36, 37, 37, 39	divdirapd 8848	. . . . . . . 8 $/\$
41		ax-1cn 7965	. . . . . . . . . . . 12
42	41	a1i 9	. . . . . . . . . . 11 $/\$
43	36, 42, 37	ppncand 8370	. . . . . . . . . 10 $/\$
44	43	oveq1d 5933	. . . . . . . . 9 $/\$
45	4	zcnd 9440	. . . . . . . . . 10 $/\$
46		subcl 8218	. . . . . . . . . . . 12 $/\$
47	19, 41, 46	sylancl 413	. . . . . . . . . . 11
48	47	adantl 277	. . . . . . . . . 10 $/\$
49	45, 48, 37, 39	divdirapd 8848	. . . . . . . . 9 $/\$
50	44, 49	eqtr3d 2228	. . . . . . . 8 $/\$
51	37, 39	dividapd 8805	. . . . . . . . 9 $/\$
52	51	oveq2d 5934	. . . . . . . 8 $/\$
53	40, 50, 52	3eqtr3d 2234	. . . . . . 7 $/\$
54	53	fveq2d 5558	. . . . . 6 $/\$
55	54	adantr 276	. . . . 5 $/\$ $/\$
56		znq 9689	. . . . . . 7 $/\$
57		1z 9343	. . . . . . 7
58		flqaddz 10366	. . . . . . 7 $/\$
59	56, 57, 58	sylancl 413	. . . . . 6 $/\$
60	59	adantr 276	. . . . 5 $/\$ $/\$
61	34, 55, 60	3eqtrrd 2231	. . . 4 $/\$ $/\$
62		znq 9689	. . . . . . . . 9 $/\$
63	3, 62	sylan 283	. . . . . . . 8 $/\$
64	63	flqcld 10346	. . . . . . 7 $/\$
65	64	zcnd 9440	. . . . . 6 $/\$
66	56	flqcld 10346	. . . . . . 7 $/\$
67	66	zcnd 9440	. . . . . 6 $/\$
68	65, 67, 42	subaddd 8348	. . . . 5 $/\$
69	68	adantr 276	. . . 4 $/\$ $/\$
70	61, 69	mpbird 167	. . 3 $/\$ $/\$
71		iftrue 3562	. . . 4
72	71	adantl 277	. . 3 $/\$ $/\$
73	70, 72	eqtr4d 2229	. 2 $/\$ $/\$
74		zmodcl 10415	. . . . . . . . . . 11 $/\$
75	3, 74	sylan 283	. . . . . . . . . 10 $/\$
76	75	nn0red 9294	. . . . . . . . 9 $/\$
77		1re 8018	. . . . . . . . 9
78		resubcl 8283	. . . . . . . . 9 $/\$
79	76, 77, 78	sylancl 413	. . . . . . . 8 $/\$
80	79	adantr 276	. . . . . . 7 $/\$ $/\$
81	75	nn0zd 9437	. . . . . . . . . . . 12 $/\$
82		elnndc 9677	. . . . . . . . . . . 12 DECID
83	81, 82	syl 14	. . . . . . . . . . 11 $/\$ DECID
84		elnn0 9242	. . . . . . . . . . . . . 14 $\/$
85	75, 84	sylib 122	. . . . . . . . . . . . 13 $/\$ $\/$
86	85	ord 725	. . . . . . . . . . . 12 $/\$
87		id 19	. . . . . . . . . . . . 13
88		dvdsval3 11934	. . . . . . . . . . . . 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 9281	. . . . . . . . 9
95	93, 94	syl 14	. . . . . . . 8 $/\$ $/\$
96	95	nn0ge0d 9296	. . . . . . 7 $/\$ $/\$
97	13, 14	jca 306	. . . . . . . 8 $/\$
98	97	ad2antlr 489	. . . . . . 7 $/\$ $/\$ $/\$
99		divge0 8892	. . . . . . 7 $/\$ $/\$ $/\$
100	80, 96, 98, 99	syl21anc 1248	. . . . . 6 $/\$ $/\$
101	13	adantl 277	. . . . . . . . . 10 $/\$
102	76	ltm1d 8951	. . . . . . . . . 10 $/\$
103		zq 9691	. . . . . . . . . . . . 13
104	3, 103	syl 14	. . . . . . . . . . . 12
105	104	adantr 276	. . . . . . . . . . 11 $/\$
106		nnq 9698	. . . . . . . . . . . 12
107	106	adantl 277	. . . . . . . . . . 11 $/\$
108	14	adantl 277	. . . . . . . . . . 11 $/\$
109		modqlt 10404	. . . . . . . . . . 11 $/\$ $/\$
110	105, 107, 108, 109	syl3anc 1249	. . . . . . . . . 10 $/\$
111	79, 76, 101, 102, 110	lttrd 8145	. . . . . . . . 9 $/\$
112	37	mulridd 8036	. . . . . . . . 9 $/\$
113	111, 112	breqtrrd 4057	. . . . . . . 8 $/\$
114		1red 8034	. . . . . . . . 9 $/\$
115		ltdivmul 8895	. . . . . . . . 9 $/\$ $/\$ $/\$
116	79, 114, 101, 108, 115	syl112anc 1253	. . . . . . . 8 $/\$
117	113, 116	mpbird 167	. . . . . . 7 $/\$
118	117	adantr 276	. . . . . 6 $/\$ $/\$
119		peano2zm 9355	. . . . . . . . . 10
120	81, 119	syl 14	. . . . . . . . 9 $/\$
121		znq 9689	. . . . . . . . 9 $/\$
122	120, 121	sylancom 420	. . . . . . . 8 $/\$
123		flqbi2 10360	. . . . . . . 8 $/\$ $/\$
124	64, 122, 123	syl2anc 411	. . . . . . 7 $/\$ $/\$
125	124	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
126	100, 118, 125	mpbir2and 946	. . . . 5 $/\$ $/\$
127		modqval 10395	. . . . . . . . . . . . 13 $/\$ $/\$
128	105, 107, 108, 127	syl3anc 1249	. . . . . . . . . . . 12 $/\$
129	128	oveq1d 5933	. . . . . . . . . . 11 $/\$
130	37, 65	mulcld 8040	. . . . . . . . . . . 12 $/\$
131	45, 42, 130	sub32d 8362	. . . . . . . . . . 11 $/\$
132		pncan 8225	. . . . . . . . . . . . 13 $/\$
133	36, 41, 132	sylancl 413	. . . . . . . . . . . 12 $/\$
134	133	oveq1d 5933	. . . . . . . . . . 11 $/\$
135	129, 131, 134	3eqtr2d 2232	. . . . . . . . . 10 $/\$
136	135	oveq1d 5933	. . . . . . . . 9 $/\$
137	36, 130, 37, 39	divsubdirapd 8849	. . . . . . . . 9 $/\$
138	65, 37, 39	divcanap3d 8814	. . . . . . . . . 10 $/\$
139	138	oveq2d 5934	. . . . . . . . 9 $/\$
140	136, 137, 139	3eqtrrd 2231	. . . . . . . 8 $/\$
141		zre 9321	. . . . . . . . . . 11
142		nndivre 9018	. . . . . . . . . . 11 $/\$
143	141, 142	sylan 283	. . . . . . . . . 10 $/\$
144	143	recnd 8048	. . . . . . . . 9 $/\$
145		nndivre 9018	. . . . . . . . . . 11 $/\$
146	79, 145	sylancom 420	. . . . . . . . . 10 $/\$
147	146	recnd 8048	. . . . . . . . 9 $/\$
148	144, 65, 147	subaddd 8348	. . . . . . . 8 $/\$
149	140, 148	mpbid 147	. . . . . . 7 $/\$
150	149	adantr 276	. . . . . 6 $/\$ $/\$
151	150	fveq2d 5558	. . . . 5 $/\$ $/\$
152	126, 151	eqtr3d 2228	. . . 4 $/\$ $/\$
153	65, 67	subeq0ad 8340	. . . . 5 $/\$
154	153	adantr 276	. . . 4 $/\$ $/\$
155	152, 154	mpbird 167	. . 3 $/\$ $/\$
156		iffalse 3565	. . . 4
157	156	adantl 277	. . 3 $/\$ $/\$
158	155, 157	eqtr4d 2229	. 2 $/\$ $/\$
159		simpr 110	. . . 4 $/\$
160		dvdsdc 11941	. . . 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 1364

wcel 2164

wne 2364

cif 3557 class class class wbr 4029

cfv 5254 (class class class)co 5918

cc 7870

cr 7871

cc0 7872

c1 7873

caddc 7875

cmul 7877

clt 8054

cle 8055

cmin 8190 # cap 8600

cdiv 8691

cn 8982

cn0 9240

cz 9317

cq 9684

cfl 10337

cmo 10393

cdvds 11930

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-mulrcl 7971 ax-addcom 7972 ax-mulcom 7973 ax-addass 7974 ax-mulass 7975 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-1rid 7979 ax-0id 7980 ax-rnegex 7981 ax-precex 7982 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988 ax-pre-mulgt0 7989 ax-pre-mulext 7990 ax-arch 7991

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-id 4324 df-po 4327 df-iso 4328 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-fv 5262 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-reap 8594 df-ap 8601 df-div 8692 df-inn 8983 df-n0 9241 df-z 9318 df-uz 9593 df-q 9685 df-rp 9720 df-fl 10339 df-mod 10394 df-dvds 11931

This theorem is referenced by: pcfac 12488

W3C validator