fldivp1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fldivp1		Structured version Visualization version GIF version

Theorem fldivp1 16598

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

**Proof of Theorem fldivp1**
Step	Hyp	Ref	Expression
1		nnz 12342	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
2		nnne0 12007	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
3		peano2z 12361	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
4	3	adantr 481	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈ ℤ)
5		dvdsval2 15966	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑀 + 1) ∈ ℤ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) / 𝑁) ∈ ℤ))
6	1, 2, 4, 5	syl2an23an 1422	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) / 𝑁) ∈ ℤ))
7	6	biimpa 477	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑀 + 1) / 𝑁) ∈ ℤ)
8		flid 13528	. . . . . . 7 ⊢ (((𝑀 + 1) / 𝑁) ∈ ℤ → (⌊‘((𝑀 + 1) / 𝑁)) = ((𝑀 + 1) / 𝑁))
9	7, 8	syl 17	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = ((𝑀 + 1) / 𝑁))
10		nnm1nn0 12274	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
11	10	nn0red 12294	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℝ)
12	10	nn0ge0d 12296	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 0 ≤ (𝑁 − 1))
13		nnre 11980	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
14		nngt0 12004	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
15		divge0 11844	. . . . . . . . 9 ⊢ ((((𝑁 − 1) ∈ ℝ ∧ 0 ≤ (𝑁 − 1)) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ ((𝑁 − 1) / 𝑁))
16	11, 12, 13, 14, 15	syl22anc 836	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 0 ≤ ((𝑁 − 1) / 𝑁))
17	16	ad2antlr 724	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → 0 ≤ ((𝑁 − 1) / 𝑁))
18	13	ltm1d 11907	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁)
19		nncn 11981	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
20	19	mulid1d 10992	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 · 1) = 𝑁)
21	18, 20	breqtrrd 5102	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < (𝑁 · 1))
22		1re 10975	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℝ)
24		ltdivmul 11850	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝑁 − 1) / 𝑁) < 1 ↔ (𝑁 − 1) < (𝑁 · 1)))
25	11, 23, 13, 14, 24	syl112anc 1373	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) / 𝑁) < 1 ↔ (𝑁 − 1) < (𝑁 · 1)))
26	21, 25	mpbird 256	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) < 1)
27	26	ad2antlr 724	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑁 − 1) / 𝑁) < 1)
28		nndivre 12014	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 1) / 𝑁) ∈ ℝ)
29	11, 28	mpancom 685	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) ∈ ℝ)
30	29	ad2antlr 724	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑁 − 1) / 𝑁) ∈ ℝ)
31		flbi2 13537	. . . . . . . 8 ⊢ ((((𝑀 + 1) / 𝑁) ∈ ℤ ∧ ((𝑁 − 1) / 𝑁) ∈ ℝ) → ((⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁) ↔ (0 ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝑁 − 1) / 𝑁) < 1)))
32	7, 30, 31	syl2anc 584	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁) ↔ (0 ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝑁 − 1) / 𝑁) < 1)))
33	17, 27, 32	mpbir2and 710	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁))
34	9, 33	eqtr4d 2781	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))))
35		zcn 12324	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
36	35	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℂ)
37		ax-1cn 10929	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
38	37	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℂ)
39	19	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℂ)
40	36, 38, 39	ppncand 11372	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) + (𝑁 − 1)) = (𝑀 + 𝑁))
41	40	oveq1d 7290	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) + (𝑁 − 1)) / 𝑁) = ((𝑀 + 𝑁) / 𝑁))
42	4	zcnd 12427	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈ ℂ)
43		subcl 11220	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑁 − 1) ∈ ℂ)
44	19, 37, 43	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
45	44	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈ ℂ)
46	2	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0)
47	42, 45, 39, 46	divdird 11789	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) + (𝑁 − 1)) / 𝑁) = (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)))
48	41, 47	eqtr3d 2780	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) / 𝑁) = (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)))
49	36, 39, 39, 46	divdird 11789	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) / 𝑁) = ((𝑀 / 𝑁) + (𝑁 / 𝑁)))
50	48, 49	eqtr3d 2780	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)) = ((𝑀 / 𝑁) + (𝑁 / 𝑁)))
51	39, 46	dividd 11749	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 / 𝑁) = 1)
52	51	oveq2d 7291	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) + (𝑁 / 𝑁)) = ((𝑀 / 𝑁) + 1))
53	50, 52	eqtrd 2778	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)) = ((𝑀 / 𝑁) + 1))
54	53	fveq2d 6778	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = (⌊‘((𝑀 / 𝑁) + 1)))
55	54	adantr 481	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = (⌊‘((𝑀 / 𝑁) + 1)))
56		zre 12323	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
57		nndivre 12014	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ)
58	56, 57	sylan 580	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ)
59		1z 12350	. . . . . . 7 ⊢ 1 ∈ ℤ
60		fladdz 13545	. . . . . . 7 ⊢ (((𝑀 / 𝑁) ∈ ℝ ∧ 1 ∈ ℤ) → (⌊‘((𝑀 / 𝑁) + 1)) = ((⌊‘(𝑀 / 𝑁)) + 1))
61	58, 59, 60	sylancl 586	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝑀 / 𝑁) + 1)) = ((⌊‘(𝑀 / 𝑁)) + 1))
62	61	adantr 481	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 / 𝑁) + 1)) = ((⌊‘(𝑀 / 𝑁)) + 1))
63	34, 55, 62	3eqtrrd 2783	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁)))
64		zre 12323	. . . . . . . . . 10 ⊢ ((𝑀 + 1) ∈ ℤ → (𝑀 + 1) ∈ ℝ)
65	3, 64	syl 17	. . . . . . . . 9 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℝ)
66		nndivre 12014	. . . . . . . . 9 ⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) / 𝑁) ∈ ℝ)
67	65, 66	sylan 580	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) / 𝑁) ∈ ℝ)
68	67	flcld 13518	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝑀 + 1) / 𝑁)) ∈ ℤ)
69	68	zcnd 12427	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝑀 + 1) / 𝑁)) ∈ ℂ)
70	58	flcld 13518	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘(𝑀 / 𝑁)) ∈ ℤ)
71	70	zcnd 12427	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘(𝑀 / 𝑁)) ∈ ℂ)
72	69, 71, 38	subaddd 11350	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 1 ↔ ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁))))
73	72	adantr 481	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 1 ↔ ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁))))
74	63, 73	mpbird 256	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 1)
75		iftrue 4465	. . . 4 ⊢ (𝑁 ∥ (𝑀 + 1) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 1)
76	75	adantl 482	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 1)
77	74, 76	eqtr4d 2781	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0))
78		zmodcl 13611	. . . . . . . . . . 11 ⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℕ₀)
79	3, 78	sylan 580	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℕ₀)
80	79	nn0red 12294	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℝ)
81		resubcl 11285	. . . . . . . . 9 ⊢ ((((𝑀 + 1) mod 𝑁) ∈ ℝ ∧ 1 ∈ ℝ) → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ)
82	80, 22, 81	sylancl 586	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ)
83	82	adantr 481	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ)
84		elnn0 12235	. . . . . . . . . . . . . 14 ⊢ (((𝑀 + 1) mod 𝑁) ∈ ℕ₀ ↔ (((𝑀 + 1) mod 𝑁) ∈ ℕ ∨ ((𝑀 + 1) mod 𝑁) = 0))
85	79, 84	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) ∈ ℕ ∨ ((𝑀 + 1) mod 𝑁) = 0))
86	85	ord 861	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬ ((𝑀 + 1) mod 𝑁) ∈ ℕ → ((𝑀 + 1) mod 𝑁) = 0))
87		id 22	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
88		dvdsval3 15967	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ (𝑀 + 1) ∈ ℤ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) mod 𝑁) = 0))
89	87, 3, 88	syl2anr 597	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) mod 𝑁) = 0))
90	86, 89	sylibrd 258	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬ ((𝑀 + 1) mod 𝑁) ∈ ℕ → 𝑁 ∥ (𝑀 + 1)))
91	90	con1d 145	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬ 𝑁 ∥ (𝑀 + 1) → ((𝑀 + 1) mod 𝑁) ∈ ℕ))
92	91	imp 407	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((𝑀 + 1) mod 𝑁) ∈ ℕ)
93		nnm1nn0 12274	. . . . . . . . 9 ⊢ (((𝑀 + 1) mod 𝑁) ∈ ℕ → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℕ₀)
94	92, 93	syl 17	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℕ₀)
95	94	nn0ge0d 12296	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → 0 ≤ (((𝑀 + 1) mod 𝑁) − 1))
96	13, 14	jca 512	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
97	96	ad2antlr 724	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
98		divge0 11844	. . . . . . 7 ⊢ ((((((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ ∧ 0 ≤ (((𝑀 + 1) mod 𝑁) − 1)) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))
99	83, 95, 97, 98	syl21anc 835	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → 0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))
100	13	adantl 482	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
101	80	ltm1d 11907	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < ((𝑀 + 1) mod 𝑁))
102		nnrp 12741	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺)
103		modlt 13600	. . . . . . . . . . 11 ⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → ((𝑀 + 1) mod 𝑁) < 𝑁)
104	65, 102, 103	syl2an 596	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) < 𝑁)
105	82, 80, 100, 101, 104	lttrd 11136	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < 𝑁)
106	39	mulid1d 10992	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 1) = 𝑁)
107	105, 106	breqtrrd 5102	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1))
108	22	a1i 11	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℝ)
109	14	adantl 482	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 < 𝑁)
110		ltdivmul 11850	. . . . . . . . 9 ⊢ (((((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1 ↔ (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1)))
111	82, 108, 100, 109, 110	syl112anc 1373	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1 ↔ (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1)))
112	107, 111	mpbird 256	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1)
113	112	adantr 481	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1)
114		nndivre 12014	. . . . . . . . 9 ⊢ (((((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ)
115	82, 114	sylancom 588	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ)
116		flbi2 13537	. . . . . . . 8 ⊢ (((⌊‘((𝑀 + 1) / 𝑁)) ∈ ℤ ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ) → ((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1)))
117	68, 115, 116	syl2anc 584	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1)))
118	117	adantr 481	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1)))
119	99, 113, 118	mpbir2and 710	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)))
120		modval 13591	. . . . . . . . . . . . . 14 ⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → ((𝑀 + 1) mod 𝑁) = ((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
121	65, 102, 120	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) = ((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
122	121	oveq1d 7290	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) − 1))
123	39, 69	mulcld 10995	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) ∈ ℂ)
124	42, 38, 123	sub32d 11364	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) = (((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) − 1))
125	122, 124	eqtr4d 2781	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
126		pncan 11227	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
127	36, 37, 126	sylancl 586	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) − 1) = 𝑀)
128	127	oveq1d 7290	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
129	125, 128	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
130	129	oveq1d 7290	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) = ((𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) / 𝑁))
131	36, 123, 39, 46	divsubdird 11790	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) / 𝑁) = ((𝑀 / 𝑁) − ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁)))
132	69, 39, 46	divcan3d 11756	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁) = (⌊‘((𝑀 + 1) / 𝑁)))
133	132	oveq2d 7291	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁)) = ((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))))
134	130, 131, 133	3eqtrrd 2783	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))) = ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))
135	58	recnd 11003	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℂ)
136	115	recnd 11003	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℂ)
137	135, 69, 136	subaddd 11350	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))) = ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ↔ ((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁)))
138	134, 137	mpbid 231	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁))
139	138	adantr 481	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁))
140	139	fveq2d 6778	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘(𝑀 / 𝑁)))
141	119, 140	eqtr3d 2780	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(𝑀 / 𝑁)))
142	69, 71	subeq0ad 11342	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 0 ↔ (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(𝑀 / 𝑁))))
143	142	adantr 481	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 0 ↔ (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(𝑀 / 𝑁))))
144	141, 143	mpbird 256	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 0)
145		iffalse 4468	. . . 4 ⊢ (¬ 𝑁 ∥ (𝑀 + 1) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 0)
146	145	adantl 482	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 0)
147	144, 146	eqtr4d 2781	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0))
148	77, 147	pm2.61dan 810	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ifcif 4459 class class class wbr 5074 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 < clt 11009 ≤ cle 11010 − cmin 11205 / cdiv 11632 ℕcn 11973 ℕ₀cn0 12233 ℤcz 12319 ℝ⁺crp 12730 ⌊cfl 13510 mod cmo 13589 ∥ cdvds 15963

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-sup 9201 df-inf 9202 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-n0 12234 df-z 12320 df-uz 12583 df-rp 12731 df-fl 13512 df-mod 13590 df-dvds 15964

This theorem is referenced by: pcfac 16600

W3C validator