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 17119

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 12754	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
2		nnne0 12412	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
3		peano2z 12777	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
4	3	adantr 486	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈ ℤ)
5		dvdsval2 16469	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑀 + 1) ∈ ℤ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) / 𝑁) ∈ ℤ))
6	1, 2, 4, 5	syl2an23an 1451	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) / 𝑁) ∈ ℤ))
7	6	biimpa 482	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑀 + 1) / 𝑁) ∈ ℤ)
8		flid 13988	. . . . . . 7 ⊢ (((𝑀 + 1) / 𝑁) ∈ ℤ → (⌊‘((𝑀 + 1) / 𝑁)) = ((𝑀 + 1) / 𝑁))
9	7, 8	syl 18	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = ((𝑀 + 1) / 𝑁))
10		nnm1nn0 12687	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
11	10	nn0red 12708	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℝ)
12	10	nn0ge0d 12710	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 0 ≤ (𝑁 − 1))
13		nnre 12382	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
14		nngt0 12409	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
15		divge0 12226	. . . . . . . . 9 ⊢ ((((𝑁 − 1) ∈ ℝ ∧ 0 ≤ (𝑁 − 1)) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ ((𝑁 − 1) / 𝑁))
16	11, 12, 13, 14, 15	syl22anc 852	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 0 ≤ ((𝑁 − 1) / 𝑁))
17	16	ad2antlr 740	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → 0 ≤ ((𝑁 − 1) / 𝑁))
18	13	ltm1d 12289	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁)
19		nncn 12383	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
20	19	mulridd 11365	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 · 1) = 𝑁)
21	18, 20	breqtrrd 5139	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < (𝑁 · 1))
22		1re 11347	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℝ)
24		ltdivmul 12232	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝑁 − 1) / 𝑁) < 1 ↔ (𝑁 − 1) < (𝑁 · 1)))
25	11, 23, 13, 14, 24	syl112anc 1402	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) / 𝑁) < 1 ↔ (𝑁 − 1) < (𝑁 · 1)))
26	21, 25	mpbird 260	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) < 1)
27	26	ad2antlr 740	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑁 − 1) / 𝑁) < 1)
28		nndivre 12419	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 1) / 𝑁) ∈ ℝ)
29	11, 28	mpancom 701	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) ∈ ℝ)
30	29	ad2antlr 740	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑁 − 1) / 𝑁) ∈ ℝ)
31		flbi2 13997	. . . . . . . 8 ⊢ ((((𝑀 + 1) / 𝑁) ∈ ℤ ∧ ((𝑁 − 1) / 𝑁) ∈ ℝ) → ((⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁) ↔ (0 ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝑁 − 1) / 𝑁) < 1)))
32	7, 30, 31	syl2anc 596	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁) ↔ (0 ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝑁 − 1) / 𝑁) < 1)))
33	17, 27, 32	mpbir2and 726	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = ((𝑀 + 1) / 𝑁))
34	9, 33	eqtr4d 2801	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))))
35		zcn 12738	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
36	35	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℂ)
37		ax-1cn 11297	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
38	37	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℂ)
39	19	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℂ)
40	36, 38, 39	ppncand 11748	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) + (𝑁 − 1)) = (𝑀 + 𝑁))
41	40	oveq1d 7466	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) + (𝑁 − 1)) / 𝑁) = ((𝑀 + 𝑁) / 𝑁))
42	4	zcnd 12844	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈ ℂ)
43		subcl 11595	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑁 − 1) ∈ ℂ)
44	19, 37, 43	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
45	44	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈ ℂ)
46	2	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0)
47	42, 45, 39, 46	divdird 12171	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) + (𝑁 − 1)) / 𝑁) = (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)))
48	41, 47	eqtr3d 2800	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) / 𝑁) = (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)))
49	36, 39, 39, 46	divdird 12171	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) / 𝑁) = ((𝑀 / 𝑁) + (𝑁 / 𝑁)))
50	48, 49	eqtr3d 2800	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)) = ((𝑀 / 𝑁) + (𝑁 / 𝑁)))
51	39, 46	dividd 12131	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 / 𝑁) = 1)
52	51	oveq2d 7467	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) + (𝑁 / 𝑁)) = ((𝑀 / 𝑁) + 1))
53	50, 52	eqtrd 2798	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)) = ((𝑀 / 𝑁) + 1))
54	53	fveq2d 6920	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = (⌊‘((𝑀 / 𝑁) + 1)))
55	54	adantr 486	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = (⌊‘((𝑀 / 𝑁) + 1)))
56		zre 12737	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
57		nndivre 12419	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ)
58	56, 57	sylan 592	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ)
59		1z 12766	. . . . . . 7 ⊢ 1 ∈ ℤ
60		fladdz 14005	. . . . . . 7 ⊢ (((𝑀 / 𝑁) ∈ ℝ ∧ 1 ∈ ℤ) → (⌊‘((𝑀 / 𝑁) + 1)) = ((⌊‘(𝑀 / 𝑁)) + 1))
61	58, 59, 60	sylancl 598	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝑀 / 𝑁) + 1)) = ((⌊‘(𝑀 / 𝑁)) + 1))
62	61	adantr 486	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 / 𝑁) + 1)) = ((⌊‘(𝑀 / 𝑁)) + 1))
63	34, 55, 62	3eqtrrd 2803	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁)))
64		zre 12737	. . . . . . . . . 10 ⊢ ((𝑀 + 1) ∈ ℤ → (𝑀 + 1) ∈ ℝ)
65	3, 64	syl 18	. . . . . . . . 9 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℝ)
66		nndivre 12419	. . . . . . . . 9 ⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) / 𝑁) ∈ ℝ)
67	65, 66	sylan 592	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) / 𝑁) ∈ ℝ)
68	67	flcld 13978	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝑀 + 1) / 𝑁)) ∈ ℤ)
69	68	zcnd 12844	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝑀 + 1) / 𝑁)) ∈ ℂ)
70	58	flcld 13978	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘(𝑀 / 𝑁)) ∈ ℤ)
71	70	zcnd 12844	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘(𝑀 / 𝑁)) ∈ ℂ)
72	69, 71, 38	subaddd 11726	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 1 ↔ ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁))))
73	72	adantr 486	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 1 ↔ ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁))))
74	63, 73	mpbird 260	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 1)
75		iftrue 4491	. . . 4 ⊢ (𝑁 ∥ (𝑀 + 1) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 1)
76	75	adantl 487	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 1)
77	74, 76	eqtr4d 2801	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0))
78		zmodcl 14071	. . . . . . . . . . 11 ⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℕ₀)
79	3, 78	sylan 592	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℕ₀)
80	79	nn0red 12708	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℝ)
81		resubcl 11661	. . . . . . . . 9 ⊢ ((((𝑀 + 1) mod 𝑁) ∈ ℝ ∧ 1 ∈ ℝ) → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ)
82	80, 22, 81	sylancl 598	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ)
83	82	adantr 486	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ)
84		elnn0 12648	. . . . . . . . . . . . . 14 ⊢ (((𝑀 + 1) mod 𝑁) ∈ ℕ₀ ↔ (((𝑀 + 1) mod 𝑁) ∈ ℕ ∨ ((𝑀 + 1) mod 𝑁) = 0))
85	79, 84	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) ∈ ℕ ∨ ((𝑀 + 1) mod 𝑁) = 0))
86	85	ord 878	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬ ((𝑀 + 1) mod 𝑁) ∈ ℕ → ((𝑀 + 1) mod 𝑁) = 0))
87		id 23	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
88		dvdsval3 16470	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ (𝑀 + 1) ∈ ℤ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) mod 𝑁) = 0))
89	87, 3, 88	syl2anr 609	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) mod 𝑁) = 0))
90	86, 89	sylibrd 262	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬ ((𝑀 + 1) mod 𝑁) ∈ ℕ → 𝑁 ∥ (𝑀 + 1)))
91	90	con1d 146	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬ 𝑁 ∥ (𝑀 + 1) → ((𝑀 + 1) mod 𝑁) ∈ ℕ))
92	91	imp 412	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((𝑀 + 1) mod 𝑁) ∈ ℕ)
93		nnm1nn0 12687	. . . . . . . . 9 ⊢ (((𝑀 + 1) mod 𝑁) ∈ ℕ → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℕ₀)
94	92, 93	syl 18	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℕ₀)
95	94	nn0ge0d 12710	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → 0 ≤ (((𝑀 + 1) mod 𝑁) − 1))
96	13, 14	jca 521	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
97	96	ad2antlr 740	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
98		divge0 12226	. . . . . . 7 ⊢ ((((((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ ∧ 0 ≤ (((𝑀 + 1) mod 𝑁) − 1)) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))
99	83, 95, 97, 98	syl21anc 851	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → 0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))
100	13	adantl 487	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
101	80	ltm1d 12289	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < ((𝑀 + 1) mod 𝑁))
102		nnrp 13172	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺)
103		modlt 14060	. . . . . . . . . . 11 ⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → ((𝑀 + 1) mod 𝑁) < 𝑁)
104	65, 102, 103	syl2an 608	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) < 𝑁)
105	82, 80, 100, 101, 104	lttrd 11510	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < 𝑁)
106	39	mulridd 11365	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 1) = 𝑁)
107	105, 106	breqtrrd 5139	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1))
108	22	a1i 11	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℝ)
109	14	adantl 487	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 < 𝑁)
110		ltdivmul 12232	. . . . . . . . 9 ⊢ (((((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1 ↔ (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1)))
111	82, 108, 100, 109, 110	syl112anc 1402	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1 ↔ (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1)))
112	107, 111	mpbird 260	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1)
113	112	adantr 486	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1)
114		nndivre 12419	. . . . . . . . 9 ⊢ (((((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ)
115	82, 114	sylancom 600	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ)
116		flbi2 13997	. . . . . . . 8 ⊢ (((⌊‘((𝑀 + 1) / 𝑁)) ∈ ℤ ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ) → ((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1)))
117	68, 115, 116	syl2anc 596	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1)))
118	117	adantr 486	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)) ↔ (0 ≤ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∧ ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1)))
119	99, 113, 118	mpbir2and 726	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘((𝑀 + 1) / 𝑁)))
120		modval 14051	. . . . . . . . . . . . . 14 ⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → ((𝑀 + 1) mod 𝑁) = ((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
121	65, 102, 120	syl2an 608	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) = ((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
122	121	oveq1d 7466	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) − 1))
123	39, 69	mulcld 11368	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) ∈ ℂ)
124	42, 38, 123	sub32d 11740	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) = (((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) − 1))
125	122, 124	eqtr4d 2801	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
126		pncan 11602	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
127	36, 37, 126	sylancl 598	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) − 1) = 𝑀)
128	127	oveq1d 7466	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
129	125, 128	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
130	129	oveq1d 7466	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) = ((𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) / 𝑁))
131	36, 123, 39, 46	divsubdird 12172	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) / 𝑁) = ((𝑀 / 𝑁) − ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁)))
132	69, 39, 46	divcan3d 12138	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁) = (⌊‘((𝑀 + 1) / 𝑁)))
133	132	oveq2d 7467	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁)) = ((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))))
134	130, 131, 133	3eqtrrd 2803	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))) = ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))
135	58	recnd 11376	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℂ)
136	115	recnd 11376	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℂ)
137	135, 69, 136	subaddd 11726	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))) = ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ↔ ((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁)))
138	134, 137	mpbid 235	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁))
139	138	adantr 486	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁)) = (𝑀 / 𝑁))
140	139	fveq2d 6920	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘(𝑀 / 𝑁)))
141	119, 140	eqtr3d 2800	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(𝑀 / 𝑁)))
142	69, 71	subeq0ad 11716	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 0 ↔ (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(𝑀 / 𝑁))))
143	142	adantr 486	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 0 ↔ (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(𝑀 / 𝑁))))
144	141, 143	mpbird 260	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 0)
145		iffalse 4494	. . . 4 ⊢ (¬ 𝑁 ∥ (𝑀 + 1) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 0)
146	145	adantl 487	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 0)
147	144, 146	eqtr4d 2801	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0))
148	77, 147	pm2.61dan 825	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ifcif 4485 class class class wbr 5108 ‘cfv 6566 (class class class)co 7451 ℂcc 11237 ℝcr 11238 0cc0 11239 1c1 11240 + caddc 11242 · cmul 11244 < clt 11382 ≤ cle 11383 − cmin 11580 / cdiv 12013 ℕcn 12375 ℕ₀cn0 12646 ℤcz 12733 ℝ⁺crp 13160 ⌊cfl 13970 mod cmo 14049 ∥ cdvds 16466

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-er 8755 df-en 9012 df-dom 9013 df-sdom 9014 df-sup 9471 df-inf 9472 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-n0 12647 df-z 12734 df-uz 13006 df-rp 13161 df-fl 13972 df-mod 14050 df-dvds 16467

This theorem is used by: pcfac 17121

W3C validator