fldivp1

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

		Ref	Expression
	Assertion	fldivp1	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M + 1}{N}⌋ - ⌊\frac{M}{N}⌋ = if (N ∥ (M + 1), 1, 0)$

Proof

Step	Hyp	Ref	Expression
1		nnz	$⊢ N \in ℕ \to N \in ℤ$
2		nnne0	$⊢ N \in ℕ \to N \neq 0$
3		peano2z	$⊢ M \in ℤ \to M + 1 \in ℤ$
4	3	adantr	$⊢ (M \in ℤ \land N \in ℕ) \to M + 1 \in ℤ$
5		dvdsval2	$⊢ (N \in ℤ \land N \neq 0 \land M + 1 \in ℤ) \to (N ∥ (M + 1) \leftrightarrow \frac{M + 1}{N} \in ℤ)$
6	1 2 4 5	syl2an23an	$⊢ (M \in ℤ \land N \in ℕ) \to (N ∥ (M + 1) \leftrightarrow \frac{M + 1}{N} \in ℤ)$
7	6	biimpa	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to \frac{M + 1}{N} \in ℤ$
8		flid	$⊢ \frac{M + 1}{N} \in ℤ \to ⌊\frac{M + 1}{N}⌋ = \frac{M + 1}{N}$
9	7 8	syl	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to ⌊\frac{M + 1}{N}⌋ = \frac{M + 1}{N}$
10		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
11	10	nn0red	$⊢ N \in ℕ \to N - 1 \in ℝ$
12	10	nn0ge0d	$⊢ N \in ℕ \to 0 \leq N - 1$
13		nnre	$⊢ N \in ℕ \to N \in ℝ$
14		nngt0	$⊢ N \in ℕ \to 0 < N$
15		divge0	$⊢ ((N - 1 \in ℝ \land 0 \leq N - 1) \land (N \in ℝ \land 0 < N)) \to 0 \leq \frac{N - 1}{N}$
16	11 12 13 14 15	syl22anc	$⊢ N \in ℕ \to 0 \leq \frac{N - 1}{N}$
17	16	ad2antlr	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to 0 \leq \frac{N - 1}{N}$
18	13	ltm1d	$⊢ N \in ℕ \to N - 1 < N$
19		nncn	$⊢ N \in ℕ \to N \in ℂ$
20	19	mulridd	$⊢ N \in ℕ \to N \cdot 1 = N$
21	18 20	breqtrrd	$⊢ N \in ℕ \to N - 1 < N \cdot 1$
22		1re	$⊢ 1 \in ℝ$
23	22	a1i	$⊢ N \in ℕ \to 1 \in ℝ$
24		ltdivmul	$⊢ (N - 1 \in ℝ \land 1 \in ℝ \land (N \in ℝ \land 0 < N)) \to (\frac{N - 1}{N} < 1 \leftrightarrow N - 1 < N \cdot 1)$
25	11 23 13 14 24	syl112anc	$⊢ N \in ℕ \to (\frac{N - 1}{N} < 1 \leftrightarrow N - 1 < N \cdot 1)$
26	21 25	mpbird	$⊢ N \in ℕ \to \frac{N - 1}{N} < 1$
27	26	ad2antlr	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to \frac{N - 1}{N} < 1$
28		nndivre	$⊢ (N - 1 \in ℝ \land N \in ℕ) \to \frac{N - 1}{N} \in ℝ$
29	11 28	mpancom	$⊢ N \in ℕ \to \frac{N - 1}{N} \in ℝ$
30	29	ad2antlr	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to \frac{N - 1}{N} \in ℝ$
31		flbi2	$⊢ (\frac{M + 1}{N} \in ℤ \land \frac{N - 1}{N} \in ℝ) \to (⌊(\frac{M + 1}{N}) + (\frac{N - 1}{N})⌋ = \frac{M + 1}{N} \leftrightarrow (0 \leq \frac{N - 1}{N} \land \frac{N - 1}{N} < 1))$
32	7 30 31	syl2anc	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to (⌊(\frac{M + 1}{N}) + (\frac{N - 1}{N})⌋ = \frac{M + 1}{N} \leftrightarrow (0 \leq \frac{N - 1}{N} \land \frac{N - 1}{N} < 1))$
33	17 27 32	mpbir2and	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to ⌊(\frac{M + 1}{N}) + (\frac{N - 1}{N})⌋ = \frac{M + 1}{N}$
34	9 33	eqtr4d	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to ⌊\frac{M + 1}{N}⌋ = ⌊(\frac{M + 1}{N}) + (\frac{N - 1}{N})⌋$
35		zcn	$⊢ M \in ℤ \to M \in ℂ$
36	35	adantr	$⊢ (M \in ℤ \land N \in ℕ) \to M \in ℂ$
37		ax-1cn	$⊢ 1 \in ℂ$
38	37	a1i	$⊢ (M \in ℤ \land N \in ℕ) \to 1 \in ℂ$
39	19	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N \in ℂ$
40	36 38 39	ppncand	$⊢ (M \in ℤ \land N \in ℕ) \to M + 1 + (N - 1) = M + N$
41	40	oveq1d	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M + 1 + (N - 1)}{N} = \frac{M + N}{N}$
42	4	zcnd	$⊢ (M \in ℤ \land N \in ℕ) \to M + 1 \in ℂ$
43		subcl	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 \in ℂ$
44	19 37 43	sylancl	$⊢ N \in ℕ \to N - 1 \in ℂ$
45	44	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N - 1 \in ℂ$
46	2	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N \neq 0$
47	42 45 39 46	divdird	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M + 1 + (N - 1)}{N} = (\frac{M + 1}{N}) + (\frac{N - 1}{N})$
48	41 47	eqtr3d	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M + N}{N} = (\frac{M + 1}{N}) + (\frac{N - 1}{N})$
49	36 39 39 46	divdird	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M + N}{N} = (\frac{M}{N}) + (\frac{N}{N})$
50	48 49	eqtr3d	$⊢ (M \in ℤ \land N \in ℕ) \to (\frac{M + 1}{N}) + (\frac{N - 1}{N}) = (\frac{M}{N}) + (\frac{N}{N})$
51	39 46	dividd	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{N}{N} = 1$
52	51	oveq2d	$⊢ (M \in ℤ \land N \in ℕ) \to (\frac{M}{N}) + (\frac{N}{N}) = (\frac{M}{N}) + 1$
53	50 52	eqtrd	$⊢ (M \in ℤ \land N \in ℕ) \to (\frac{M + 1}{N}) + (\frac{N - 1}{N}) = (\frac{M}{N}) + 1$
54	53	fveq2d	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊(\frac{M + 1}{N}) + (\frac{N - 1}{N})⌋ = ⌊(\frac{M}{N}) + 1⌋$
55	54	adantr	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to ⌊(\frac{M + 1}{N}) + (\frac{N - 1}{N})⌋ = ⌊(\frac{M}{N}) + 1⌋$
56		zre	$⊢ M \in ℤ \to M \in ℝ$
57		nndivre	$⊢ (M \in ℝ \land N \in ℕ) \to \frac{M}{N} \in ℝ$
58	56 57	sylan	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M}{N} \in ℝ$
59		1z	$⊢ 1 \in ℤ$
60		fladdz	$⊢ (\frac{M}{N} \in ℝ \land 1 \in ℤ) \to ⌊(\frac{M}{N}) + 1⌋ = ⌊\frac{M}{N}⌋ + 1$
61	58 59 60	sylancl	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊(\frac{M}{N}) + 1⌋ = ⌊\frac{M}{N}⌋ + 1$
62	61	adantr	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to ⌊(\frac{M}{N}) + 1⌋ = ⌊\frac{M}{N}⌋ + 1$
63	34 55 62	3eqtrrd	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to ⌊\frac{M}{N}⌋ + 1 = ⌊\frac{M + 1}{N}⌋$
64		zre	$⊢ M + 1 \in ℤ \to M + 1 \in ℝ$
65	3 64	syl	$⊢ M \in ℤ \to M + 1 \in ℝ$
66		nndivre	$⊢ (M + 1 \in ℝ \land N \in ℕ) \to \frac{M + 1}{N} \in ℝ$
67	65 66	sylan	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M + 1}{N} \in ℝ$
68	67	flcld	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M + 1}{N}⌋ \in ℤ$
69	68	zcnd	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M + 1}{N}⌋ \in ℂ$
70	58	flcld	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M}{N}⌋ \in ℤ$
71	70	zcnd	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M}{N}⌋ \in ℂ$
72	69 71 38	subaddd	$⊢ (M \in ℤ \land N \in ℕ) \to (⌊\frac{M + 1}{N}⌋ - ⌊\frac{M}{N}⌋ = 1 \leftrightarrow ⌊\frac{M}{N}⌋ + 1 = ⌊\frac{M + 1}{N}⌋)$
73	72	adantr	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to (⌊\frac{M + 1}{N}⌋ - ⌊\frac{M}{N}⌋ = 1 \leftrightarrow ⌊\frac{M}{N}⌋ + 1 = ⌊\frac{M + 1}{N}⌋)$
74	63 73	mpbird	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to ⌊\frac{M + 1}{N}⌋ - ⌊\frac{M}{N}⌋ = 1$
75		iftrue	$⊢ N ∥ (M + 1) \to if (N ∥ (M + 1), 1, 0) = 1$
76	75	adantl	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to if (N ∥ (M + 1), 1, 0) = 1$
77	74 76	eqtr4d	$⊢ ((M \in ℤ \land N \in ℕ) \land N ∥ (M + 1)) \to ⌊\frac{M + 1}{N}⌋ - ⌊\frac{M}{N}⌋ = if (N ∥ (M + 1), 1, 0)$
78		zmodcl	$⊢ (M + 1 \in ℤ \land N \in ℕ) \to (M + 1) \mod N \in ℕ_{0}$
79	3 78	sylan	$⊢ (M \in ℤ \land N \in ℕ) \to (M + 1) \mod N \in ℕ_{0}$
80	79	nn0red	$⊢ (M \in ℤ \land N \in ℕ) \to (M + 1) \mod N \in ℝ$
81		resubcl	$⊢ ((M + 1) \mod N \in ℝ \land 1 \in ℝ) \to ((M + 1) \mod N) - 1 \in ℝ$
82	80 22 81	sylancl	$⊢ (M \in ℤ \land N \in ℕ) \to ((M + 1) \mod N) - 1 \in ℝ$
83	82	adantr	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to ((M + 1) \mod N) - 1 \in ℝ$
84		elnn0	$⊢ (M + 1) \mod N \in ℕ_{0} \leftrightarrow ((M + 1) \mod N \in ℕ \lor (M + 1) \mod N = 0)$
85	79 84	sylib	$⊢ (M \in ℤ \land N \in ℕ) \to ((M + 1) \mod N \in ℕ \lor (M + 1) \mod N = 0)$
86	85	ord	$⊢ (M \in ℤ \land N \in ℕ) \to (\neg (M + 1) \mod N \in ℕ \to (M + 1) \mod N = 0)$
87		id	$⊢ N \in ℕ \to N \in ℕ$
88		dvdsval3	$⊢ (N \in ℕ \land M + 1 \in ℤ) \to (N ∥ (M + 1) \leftrightarrow (M + 1) \mod N = 0)$
89	87 3 88	syl2anr	$⊢ (M \in ℤ \land N \in ℕ) \to (N ∥ (M + 1) \leftrightarrow (M + 1) \mod N = 0)$
90	86 89	sylibrd	$⊢ (M \in ℤ \land N \in ℕ) \to (\neg (M + 1) \mod N \in ℕ \to N ∥ (M + 1))$
91	90	con1d	$⊢ (M \in ℤ \land N \in ℕ) \to (\neg N ∥ (M + 1) \to (M + 1) \mod N \in ℕ)$
92	91	imp	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to (M + 1) \mod N \in ℕ$
93		nnm1nn0	$⊢ (M + 1) \mod N \in ℕ \to ((M + 1) \mod N) - 1 \in ℕ_{0}$
94	92 93	syl	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to ((M + 1) \mod N) - 1 \in ℕ_{0}$
95	94	nn0ge0d	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to 0 \leq ((M + 1) \mod N) - 1$
96	13 14	jca	$⊢ N \in ℕ \to (N \in ℝ \land 0 < N)$
97	96	ad2antlr	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to (N \in ℝ \land 0 < N)$
98		divge0	$⊢ ((((M + 1) \mod N) - 1 \in ℝ \land 0 \leq ((M + 1) \mod N) - 1) \land (N \in ℝ \land 0 < N)) \to 0 \leq \frac{((M + 1) \mod N) - 1}{N}$
99	83 95 97 98	syl21anc	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to 0 \leq \frac{((M + 1) \mod N) - 1}{N}$
100	13	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N \in ℝ$
101	80	ltm1d	$⊢ (M \in ℤ \land N \in ℕ) \to ((M + 1) \mod N) - 1 < (M + 1) \mod N$
102		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
103		modlt	$⊢ (M + 1 \in ℝ \land N \in ℝ^{+}) \to (M + 1) \mod N < N$
104	65 102 103	syl2an	$⊢ (M \in ℤ \land N \in ℕ) \to (M + 1) \mod N < N$
105	82 80 100 101 104	lttrd	$⊢ (M \in ℤ \land N \in ℕ) \to ((M + 1) \mod N) - 1 < N$
106	39	mulridd	$⊢ (M \in ℤ \land N \in ℕ) \to N \cdot 1 = N$
107	105 106	breqtrrd	$⊢ (M \in ℤ \land N \in ℕ) \to ((M + 1) \mod N) - 1 < N \cdot 1$
108	22	a1i	$⊢ (M \in ℤ \land N \in ℕ) \to 1 \in ℝ$
109	14	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to 0 < N$
110		ltdivmul	$⊢ (((M + 1) \mod N) - 1 \in ℝ \land 1 \in ℝ \land (N \in ℝ \land 0 < N)) \to (\frac{((M + 1) \mod N) - 1}{N} < 1 \leftrightarrow ((M + 1) \mod N) - 1 < N \cdot 1)$
111	82 108 100 109 110	syl112anc	$⊢ (M \in ℤ \land N \in ℕ) \to (\frac{((M + 1) \mod N) - 1}{N} < 1 \leftrightarrow ((M + 1) \mod N) - 1 < N \cdot 1)$
112	107 111	mpbird	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{((M + 1) \mod N) - 1}{N} < 1$
113	112	adantr	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to \frac{((M + 1) \mod N) - 1}{N} < 1$
114		nndivre	$⊢ (((M + 1) \mod N) - 1 \in ℝ \land N \in ℕ) \to \frac{((M + 1) \mod N) - 1}{N} \in ℝ$
115	82 114	sylancom	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{((M + 1) \mod N) - 1}{N} \in ℝ$
116		flbi2	$⊢ (⌊\frac{M + 1}{N}⌋ \in ℤ \land \frac{((M + 1) \mod N) - 1}{N} \in ℝ) \to (⌊⌊\frac{M + 1}{N}⌋ + (\frac{((M + 1) \mod N) - 1}{N})⌋ = ⌊\frac{M + 1}{N}⌋ \leftrightarrow (0 \leq \frac{((M + 1) \mod N) - 1}{N} \land \frac{((M + 1) \mod N) - 1}{N} < 1))$
117	68 115 116	syl2anc	$⊢ (M \in ℤ \land N \in ℕ) \to (⌊⌊\frac{M + 1}{N}⌋ + (\frac{((M + 1) \mod N) - 1}{N})⌋ = ⌊\frac{M + 1}{N}⌋ \leftrightarrow (0 \leq \frac{((M + 1) \mod N) - 1}{N} \land \frac{((M + 1) \mod N) - 1}{N} < 1))$
118	117	adantr	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to (⌊⌊\frac{M + 1}{N}⌋ + (\frac{((M + 1) \mod N) - 1}{N})⌋ = ⌊\frac{M + 1}{N}⌋ \leftrightarrow (0 \leq \frac{((M + 1) \mod N) - 1}{N} \land \frac{((M + 1) \mod N) - 1}{N} < 1))$
119	99 113 118	mpbir2and	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to ⌊⌊\frac{M + 1}{N}⌋ + (\frac{((M + 1) \mod N) - 1}{N})⌋ = ⌊\frac{M + 1}{N}⌋$
120		modval	$⊢ (M + 1 \in ℝ \land N \in ℝ^{+}) \to (M + 1) \mod N = M + 1 - N ⌊\frac{M + 1}{N}⌋$
121	65 102 120	syl2an	$⊢ (M \in ℤ \land N \in ℕ) \to (M + 1) \mod N = M + 1 - N ⌊\frac{M + 1}{N}⌋$
122	121	oveq1d	$⊢ (M \in ℤ \land N \in ℕ) \to ((M + 1) \mod N) - 1 = (M + 1) - N ⌊\frac{M + 1}{N}⌋ - 1$
123	39 69	mulcld	$⊢ (M \in ℤ \land N \in ℕ) \to N ⌊\frac{M + 1}{N}⌋ \in ℂ$
124	42 38 123	sub32d	$⊢ (M \in ℤ \land N \in ℕ) \to (M + 1) - 1 - N ⌊\frac{M + 1}{N}⌋ = (M + 1) - N ⌊\frac{M + 1}{N}⌋ - 1$
125	122 124	eqtr4d	$⊢ (M \in ℤ \land N \in ℕ) \to ((M + 1) \mod N) - 1 = (M + 1) - 1 - N ⌊\frac{M + 1}{N}⌋$
126		pncan	$⊢ (M \in ℂ \land 1 \in ℂ) \to M + 1 - 1 = M$
127	36 37 126	sylancl	$⊢ (M \in ℤ \land N \in ℕ) \to M + 1 - 1 = M$
128	127	oveq1d	$⊢ (M \in ℤ \land N \in ℕ) \to (M + 1) - 1 - N ⌊\frac{M + 1}{N}⌋ = M - N ⌊\frac{M + 1}{N}⌋$
129	125 128	eqtrd	$⊢ (M \in ℤ \land N \in ℕ) \to ((M + 1) \mod N) - 1 = M - N ⌊\frac{M + 1}{N}⌋$
130	129	oveq1d	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{((M + 1) \mod N) - 1}{N} = \frac{M - N ⌊\frac{M + 1}{N}⌋}{N}$
131	36 123 39 46	divsubdird	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M - N ⌊\frac{M + 1}{N}⌋}{N} = (\frac{M}{N}) - (\frac{N ⌊\frac{M + 1}{N}⌋}{N})$
132	69 39 46	divcan3d	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{N ⌊\frac{M + 1}{N}⌋}{N} = ⌊\frac{M + 1}{N}⌋$
133	132	oveq2d	$⊢ (M \in ℤ \land N \in ℕ) \to (\frac{M}{N}) - (\frac{N ⌊\frac{M + 1}{N}⌋}{N}) = (\frac{M}{N}) - ⌊\frac{M + 1}{N}⌋$
134	130 131 133	3eqtrrd	$⊢ (M \in ℤ \land N \in ℕ) \to (\frac{M}{N}) - ⌊\frac{M + 1}{N}⌋ = \frac{((M + 1) \mod N) - 1}{N}$
135	58	recnd	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M}{N} \in ℂ$
136	115	recnd	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{((M + 1) \mod N) - 1}{N} \in ℂ$
137	135 69 136	subaddd	$⊢ (M \in ℤ \land N \in ℕ) \to ((\frac{M}{N}) - ⌊\frac{M + 1}{N}⌋ = \frac{((M + 1) \mod N) - 1}{N} \leftrightarrow ⌊\frac{M + 1}{N}⌋ + (\frac{((M + 1) \mod N) - 1}{N}) = \frac{M}{N})$
138	134 137	mpbid	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M + 1}{N}⌋ + (\frac{((M + 1) \mod N) - 1}{N}) = \frac{M}{N}$
139	138	adantr	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to ⌊\frac{M + 1}{N}⌋ + (\frac{((M + 1) \mod N) - 1}{N}) = \frac{M}{N}$
140	139	fveq2d	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to ⌊⌊\frac{M + 1}{N}⌋ + (\frac{((M + 1) \mod N) - 1}{N})⌋ = ⌊\frac{M}{N}⌋$
141	119 140	eqtr3d	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to ⌊\frac{M + 1}{N}⌋ = ⌊\frac{M}{N}⌋$
142	69 71	subeq0ad	$⊢ (M \in ℤ \land N \in ℕ) \to (⌊\frac{M + 1}{N}⌋ - ⌊\frac{M}{N}⌋ = 0 \leftrightarrow ⌊\frac{M + 1}{N}⌋ = ⌊\frac{M}{N}⌋)$
143	142	adantr	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to (⌊\frac{M + 1}{N}⌋ - ⌊\frac{M}{N}⌋ = 0 \leftrightarrow ⌊\frac{M + 1}{N}⌋ = ⌊\frac{M}{N}⌋)$
144	141 143	mpbird	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to ⌊\frac{M + 1}{N}⌋ - ⌊\frac{M}{N}⌋ = 0$
145		iffalse	$⊢ \neg N ∥ (M + 1) \to if (N ∥ (M + 1), 1, 0) = 0$
146	145	adantl	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to if (N ∥ (M + 1), 1, 0) = 0$
147	144 146	eqtr4d	$⊢ ((M \in ℤ \land N \in ℕ) \land \neg N ∥ (M + 1)) \to ⌊\frac{M + 1}{N}⌋ - ⌊\frac{M}{N}⌋ = if (N ∥ (M + 1), 1, 0)$
148	77 147	pm2.61dan	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M + 1}{N}⌋ - ⌊\frac{M}{N}⌋ = if (N ∥ (M + 1), 1, 0)$

Metamath Proof Explorer

Theorem fldivp1

Proof