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 16990

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 12637	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
2		nnne0 12295	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
3		peano2z 12660	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
4	3	adantr 486	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈ ℤ)
5		dvdsval2 16346	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑀 + 1) ∈ ℤ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) / 𝑁) ∈ ℤ))
6	1, 2, 4, 5	syl2an23an 1450	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ (𝑀 + 1) ↔ ((𝑀 + 1) / 𝑁) ∈ ℤ))
7	6	biimpa 482	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑀 + 1) / 𝑁) ∈ ℤ)
8		flid 13870	. . . . . . 7 ⊢ (((𝑀 + 1) / 𝑁) ∈ ℤ → (⌊‘((𝑀 + 1) / 𝑁)) = ((𝑀 + 1) / 𝑁))
9	7, 8	syl 18	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = ((𝑀 + 1) / 𝑁))
10		nnm1nn0 12570	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
11	10	nn0red 12591	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℝ)
12	10	nn0ge0d 12593	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 0 ≤ (𝑁 − 1))
13		nnre 12265	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
14		nngt0 12292	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
15		divge0 12109	. . . . . . . . 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 12172	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁)
19		nncn 12266	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
20	19	mulridd 11251	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 · 1) = 𝑁)
21	18, 20	breqtrrd 5133	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < (𝑁 · 1))
22		1re 11233	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℝ)
24		ltdivmul 12115	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝑁 − 1) / 𝑁) < 1 ↔ (𝑁 − 1) < (𝑁 · 1)))
25	11, 23, 13, 14, 24	syl112anc 1401	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) / 𝑁) < 1 ↔ (𝑁 − 1) < (𝑁 · 1)))
26	21, 25	mpbird 260	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) < 1)
27	26	ad2antlr 740	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑁 − 1) / 𝑁) < 1)
28		nndivre 12302	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 1) / 𝑁) ∈ ℝ)
29	11, 28	mpancom 701	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) ∈ ℝ)
30	29	ad2antlr 740	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((𝑁 − 1) / 𝑁) ∈ ℝ)
31		flbi2 13879	. . . . . . . 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 2798	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))))
35		zcn 12621	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
36	35	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℂ)
37		ax-1cn 11183	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
38	37	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℂ)
39	19	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℂ)
40	36, 38, 39	ppncand 11634	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) + (𝑁 − 1)) = (𝑀 + 𝑁))
41	40	oveq1d 7429	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) + (𝑁 − 1)) / 𝑁) = ((𝑀 + 𝑁) / 𝑁))
42	4	zcnd 12727	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 1) ∈ ℂ)
43		subcl 11481	. . . . . . . . . . . . 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 12054	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) + (𝑁 − 1)) / 𝑁) = (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)))
48	41, 47	eqtr3d 2797	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) / 𝑁) = (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)))
49	36, 39, 39, 46	divdird 12054	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) / 𝑁) = ((𝑀 / 𝑁) + (𝑁 / 𝑁)))
50	48, 49	eqtr3d 2797	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)) = ((𝑀 / 𝑁) + (𝑁 / 𝑁)))
51	39, 46	dividd 12014	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 / 𝑁) = 1)
52	51	oveq2d 7430	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) + (𝑁 / 𝑁)) = ((𝑀 / 𝑁) + 1))
53	50, 52	eqtrd 2795	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁)) = ((𝑀 / 𝑁) + 1))
54	53	fveq2d 6883	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = (⌊‘((𝑀 / 𝑁) + 1)))
55	54	adantr 486	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → (⌊‘(((𝑀 + 1) / 𝑁) + ((𝑁 − 1) / 𝑁))) = (⌊‘((𝑀 / 𝑁) + 1)))
56		zre 12620	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
57		nndivre 12302	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ)
58	56, 57	sylan 592	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ)
59		1z 12649	. . . . . . 7 ⊢ 1 ∈ ℤ
60		fladdz 13887	. . . . . . 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 2800	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘(𝑀 / 𝑁)) + 1) = (⌊‘((𝑀 + 1) / 𝑁)))
64		zre 12620	. . . . . . . . . 10 ⊢ ((𝑀 + 1) ∈ ℤ → (𝑀 + 1) ∈ ℝ)
65	3, 64	syl 18	. . . . . . . . 9 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℝ)
66		nndivre 12302	. . . . . . . . 9 ⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) / 𝑁) ∈ ℝ)
67	65, 66	sylan 592	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) / 𝑁) ∈ ℝ)
68	67	flcld 13860	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝑀 + 1) / 𝑁)) ∈ ℤ)
69	68	zcnd 12727	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝑀 + 1) / 𝑁)) ∈ ℂ)
70	58	flcld 13860	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘(𝑀 / 𝑁)) ∈ ℤ)
71	70	zcnd 12727	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (⌊‘(𝑀 / 𝑁)) ∈ ℂ)
72	69, 71, 38	subaddd 11612	. . . . 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 4488	. . . 4 ⊢ (𝑁 ∥ (𝑀 + 1) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 1)
76	75	adantl 487	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 1)
77	74, 76	eqtr4d 2798	. 2 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0))
78		zmodcl 13953	. . . . . . . . . . 11 ⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℕ₀)
79	3, 78	sylan 592	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℕ₀)
80	79	nn0red 12591	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) ∈ ℝ)
81		resubcl 11547	. . . . . . . . 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 12531	. . . . . . . . . . . . . 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 16347	. . . . . . . . . . . . 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 12570	. . . . . . . . 9 ⊢ (((𝑀 + 1) mod 𝑁) ∈ ℕ → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℕ₀)
94	92, 93	syl 18	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (((𝑀 + 1) mod 𝑁) − 1) ∈ ℕ₀)
95	94	nn0ge0d 12593	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → 0 ≤ (((𝑀 + 1) mod 𝑁) − 1))
96	13, 14	jca 521	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
97	96	ad2antlr 740	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
98		divge0 12109	. . . . . . 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 12172	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < ((𝑀 + 1) mod 𝑁))
102		nnrp 13055	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺)
103		modlt 13942	. . . . . . . . . . 11 ⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → ((𝑀 + 1) mod 𝑁) < 𝑁)
104	65, 102, 103	syl2an 608	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) < 𝑁)
105	82, 80, 100, 101, 104	lttrd 11396	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < 𝑁)
106	39	mulridd 11251	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 1) = 𝑁)
107	105, 106	breqtrrd 5133	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1))
108	22	a1i 11	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 1 ∈ ℝ)
109	14	adantl 487	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 < 𝑁)
110		ltdivmul 12115	. . . . . . . . 9 ⊢ (((((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) < 1 ↔ (((𝑀 + 1) mod 𝑁) − 1) < (𝑁 · 1)))
111	82, 108, 100, 109, 110	syl112anc 1401	. . . . . . . 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 12302	. . . . . . . . 9 ⊢ (((((𝑀 + 1) mod 𝑁) − 1) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ)
115	82, 114	sylancom 600	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℝ)
116		flbi2 13879	. . . . . . . 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 13933	. . . . . . . . . . . . . 14 ⊢ (((𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺) → ((𝑀 + 1) mod 𝑁) = ((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
121	65, 102, 120	syl2an 608	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) mod 𝑁) = ((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
122	121	oveq1d 7429	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) − 1))
123	39, 69	mulcld 11254	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) ∈ ℂ)
124	42, 38, 123	sub32d 11626	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) = (((𝑀 + 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) − 1))
125	122, 124	eqtr4d 2798	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
126		pncan 11488	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
127	36, 37, 126	sylancl 598	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 + 1) − 1) = 𝑀)
128	127	oveq1d 7429	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) − 1) − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
129	125, 128	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑀 + 1) mod 𝑁) − 1) = (𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))))
130	129	oveq1d 7429	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) = ((𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) / 𝑁))
131	36, 123, 39, 46	divsubdird 12055	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 − (𝑁 · (⌊‘((𝑀 + 1) / 𝑁)))) / 𝑁) = ((𝑀 / 𝑁) − ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁)))
132	69, 39, 46	divcan3d 12021	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁) = (⌊‘((𝑀 + 1) / 𝑁)))
133	132	oveq2d 7430	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − ((𝑁 · (⌊‘((𝑀 + 1) / 𝑁))) / 𝑁)) = ((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))))
134	130, 131, 133	3eqtrrd 2800	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − (⌊‘((𝑀 + 1) / 𝑁))) = ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))
135	58	recnd 11262	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℂ)
136	115	recnd 11262	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁) ∈ ℂ)
137	135, 69, 136	subaddd 11612	. . . . . . . 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 6883	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((⌊‘((𝑀 + 1) / 𝑁)) + ((((𝑀 + 1) mod 𝑁) − 1) / 𝑁))) = (⌊‘(𝑀 / 𝑁)))
141	119, 140	eqtr3d 2797	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(𝑀 / 𝑁)))
142	69, 71	subeq0ad 11602	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 0 ↔ (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(𝑀 / 𝑁))))
143	142	adantr 486	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → (((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 0 ↔ (⌊‘((𝑀 + 1) / 𝑁)) = (⌊‘(𝑀 / 𝑁))))
144	141, 143	mpbird 260	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = 0)
145		iffalse 4491	. . . 4 ⊢ (¬ 𝑁 ∥ (𝑀 + 1) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 0)
146	145	adantl 487	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑁 ∥ (𝑀 + 1)) → if(𝑁 ∥ (𝑀 + 1), 1, 0) = 0)
147	144, 146	eqtr4d 2798	. 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 2145 ≠ wne 2955 ifcif 4482 class class class wbr 5103 ‘cfv 6533 (class class class)co 7414 ℂcc 11123 ℝcr 11124 0cc0 11125 1c1 11126 + caddc 11128 · cmul 11130 < clt 11268 ≤ cle 11269 − cmin 11466 / cdiv 11896 ℕcn 12258 ℕ₀cn0 12529 ℤcz 12616 ℝ⁺crp 13043 ⌊cfl 13852 mod cmo 13931 ∥ cdvds 16343

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202 ax-pre-sup 11203

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 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-er 8697 df-en 8954 df-dom 8955 df-sdom 8956 df-sup 9413 df-inf 9414 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-div 11897 df-nn 12259 df-n0 12530 df-z 12617 df-uz 12889 df-rp 13044 df-fl 13854 df-mod 13932 df-dvds 16344

This theorem is used by: pcfac 16992

W3C validator