modaddmodup - Metamath Proof Explorer

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

Theorem modaddmodup 13861

Description: The sum of an integer modulo a positive integer and another integer minus the positive integer equals the sum of the two integers modulo the positive integer if the other integer is in the upper part of the range between 0 and the positive integer. (Contributed by AV, 30-Oct-2018.)

**Assertion**
Ref	Expression
modaddmodup	⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → ((𝐵 + (𝐴 mod 𝑀)) − 𝑀) = ((𝐵 + 𝐴) mod 𝑀)))

**Proof of Theorem modaddmodup**
Step	Hyp	Ref	Expression
1		elfzoelz 13579	. . . . . . . 8 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → 𝐵 ∈ ℤ)
2	1	zred 12600	. . . . . . 7 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → 𝐵 ∈ ℝ)
3	2	adantr 480	. . . . . 6 ⊢ ((𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → 𝐵 ∈ ℝ)
4		zmodcl 13815	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ∈ ℕ₀)
5	4	nn0red 12467	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ∈ ℝ)
6	5	adantl 481	. . . . . 6 ⊢ ((𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐴 mod 𝑀) ∈ ℝ)
7	3, 6	readdcld 11165	. . . . 5 ⊢ ((𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐵 + (𝐴 mod 𝑀)) ∈ ℝ)
8	7	ancoms 458	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → (𝐵 + (𝐴 mod 𝑀)) ∈ ℝ)
9		nnrp 12921	. . . . 5 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ⁺)
10	9	ad2antlr 728	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → 𝑀 ∈ ℝ⁺)
11		elfzo2 13582	. . . . . 6 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ↔ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ∧ 𝑀 ∈ ℤ ∧ 𝐵 < 𝑀))
12		eluz2 12761	. . . . . . . 8 ⊢ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ↔ ((𝑀 − (𝐴 mod 𝑀)) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵))
13		nnre 12156	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
14	13	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ∈ ℝ)
15	14	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → 𝑀 ∈ ℝ)
16	5	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐴 mod 𝑀) ∈ ℝ)
17		zre 12496	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℝ)
18	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → 𝐵 ∈ ℝ)
19	15, 16, 18	lesubaddd 11738	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → ((𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵 ↔ 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
20	19	biimpd 229	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → ((𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵 → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
21	20	impancom 451	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℤ ∧ (𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
22	21	3adant1 1131	. . . . . . . 8 ⊢ (((𝑀 − (𝐴 mod 𝑀)) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
23	12, 22	sylbi 217	. . . . . . 7 ⊢ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
24	23	3ad2ant1 1134	. . . . . 6 ⊢ ((𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ∧ 𝑀 ∈ ℤ ∧ 𝐵 < 𝑀) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
25	11, 24	sylbi 217	. . . . 5 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
26	25	impcom 407	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀)))
27		eluzelz 12765	. . . . . . . . 9 ⊢ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) → 𝐵 ∈ ℤ)
28	17, 5	anim12i 614	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐵 ∈ ℝ ∧ (𝐴 mod 𝑀) ∈ ℝ))
29	13, 13	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ → (𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ))
30	29	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ))
31	30	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ))
32	28, 31	jca 511	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → ((𝐵 ∈ ℝ ∧ (𝐴 mod 𝑀) ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ)))
33	32	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → ((𝐵 ∈ ℝ ∧ (𝐴 mod 𝑀) ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ)))
34		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → 𝐵 < 𝑀)
35		zre 12496	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
36		modlt 13804	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) → (𝐴 mod 𝑀) < 𝑀)
37	35, 9, 36	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) < 𝑀)
38	5, 14, 37	ltled 11285	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ≤ 𝑀)
39	38	ad2antlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (𝐴 mod 𝑀) ≤ 𝑀)
40	34, 39	jca 511	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (𝐵 < 𝑀 ∧ (𝐴 mod 𝑀) ≤ 𝑀))
41		ltleadd 11624	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ ℝ ∧ (𝐴 mod 𝑀) ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → ((𝐵 < 𝑀 ∧ (𝐴 mod 𝑀) ≤ 𝑀) → (𝐵 + (𝐴 mod 𝑀)) < (𝑀 + 𝑀)))
42	33, 40, 41	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (𝐵 + (𝐴 mod 𝑀)) < (𝑀 + 𝑀))
43		nncn 12157	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
44	43	2timesd 12388	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) = (𝑀 + 𝑀))
45	44	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) = (𝑀 + 𝑀))
46	45	ad2antlr 728	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (2 · 𝑀) = (𝑀 + 𝑀))
47	42, 46	breqtrrd 5127	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))
48	47	exp31 419	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℤ → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 < 𝑀 → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))))
49	48	com23 86	. . . . . . . . 9 ⊢ (𝐵 ∈ ℤ → (𝐵 < 𝑀 → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))))
50	27, 49	syl 17	. . . . . . . 8 ⊢ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) → (𝐵 < 𝑀 → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))))
51	50	imp 406	. . . . . . 7 ⊢ ((𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ∧ 𝐵 < 𝑀) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀)))
52	51	3adant2 1132	. . . . . 6 ⊢ ((𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ∧ 𝑀 ∈ ℤ ∧ 𝐵 < 𝑀) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀)))
53	11, 52	sylbi 217	. . . . 5 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀)))
54	53	impcom 407	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))
55		2submod 13859	. . . . 5 ⊢ ((((𝐵 + (𝐴 mod 𝑀)) ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) ∧ (𝑀 ≤ (𝐵 + (𝐴 mod 𝑀)) ∧ (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + (𝐴 mod 𝑀)) − 𝑀))
56	55	eqcomd 2743	. . . 4 ⊢ ((((𝐵 + (𝐴 mod 𝑀)) ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) ∧ (𝑀 ≤ (𝐵 + (𝐴 mod 𝑀)) ∧ (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))) → ((𝐵 + (𝐴 mod 𝑀)) − 𝑀) = ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀))
57	8, 10, 26, 54, 56	syl22anc 839	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → ((𝐵 + (𝐴 mod 𝑀)) − 𝑀) = ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀))
58	35	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝐴 ∈ ℝ)
59	58	adantr 480	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → 𝐴 ∈ ℝ)
60	2	adantl 481	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → 𝐵 ∈ ℝ)
61		modadd2mod 13848	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀))
62	59, 60, 10, 61	syl3anc 1374	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀))
63	57, 62	eqtrd 2772	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → ((𝐵 + (𝐴 mod 𝑀)) − 𝑀) = ((𝐵 + 𝐴) mod 𝑀))
64	63	ex 412	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → ((𝐵 + (𝐴 mod 𝑀)) − 𝑀) = ((𝐵 + 𝐴) mod 𝑀)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 class class class wbr 5099 ‘cfv 6493 (class class class)co 7360 ℝcr 11029 + caddc 11033 · cmul 11035 < clt 11170 ≤ cle 11171 − cmin 11368 ℕcn 12149 2c2 12204 ℤcz 12492 ℤ_≥cuz 12755 ℝ⁺crp 12909 ..^cfzo 13574 mod cmo 13793

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-pre-sup 11108

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3351 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-iun 4949 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-sup 9349 df-inf 9350 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12150 df-2 12212 df-n0 12406 df-z 12493 df-uz 12756 df-rp 12910 df-fz 13428 df-fzo 13575 df-fl 13716 df-mod 13794

This theorem is referenced by: cshwidxmod 14730

W3C validator