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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝑀 + 1 ) / 𝑁 ) ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) = if ( 𝑁 ∥ ( 𝑀 + 1 ) , 1 , 0 ) )

Proof

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

Metamath Proof Explorer

Theorem fldivp1

Proof