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 13899

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 13620	. . . . . . . 8 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → 𝐵 ∈ ℤ)
2	1	zred 12638	. . . . . . 7 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → 𝐵 ∈ ℝ)
3	2	adantr 480	. . . . . 6 ⊢ ((𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → 𝐵 ∈ ℝ)
4		zmodcl 13853	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ∈ ℕ₀)
5	4	nn0red 12504	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ∈ ℝ)
6	5	adantl 481	. . . . . 6 ⊢ ((𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐴 mod 𝑀) ∈ ℝ)
7	3, 6	readdcld 11203	. . . . 5 ⊢ ((𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐵 + (𝐴 mod 𝑀)) ∈ ℝ)
8	7	ancoms 458	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → (𝐵 + (𝐴 mod 𝑀)) ∈ ℝ)
9		nnrp 12963	. . . . 5 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ⁺)
10	9	ad2antlr 727	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → 𝑀 ∈ ℝ⁺)
11		elfzo2 13623	. . . . . 6 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ↔ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ∧ 𝑀 ∈ ℤ ∧ 𝐵 < 𝑀))
12		eluz2 12799	. . . . . . . 8 ⊢ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ↔ ((𝑀 − (𝐴 mod 𝑀)) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵))
13		nnre 12193	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
14	13	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ∈ ℝ)
15	14	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → 𝑀 ∈ ℝ)
16	5	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐴 mod 𝑀) ∈ ℝ)
17		zre 12533	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℝ)
18	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → 𝐵 ∈ ℝ)
19	15, 16, 18	lesubaddd 11775	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → ((𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵 ↔ 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
20	19	biimpd 229	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → ((𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵 → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
21	20	impancom 451	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℤ ∧ (𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
22	21	3adant1 1130	. . . . . . . 8 ⊢ (((𝑀 − (𝐴 mod 𝑀)) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
23	12, 22	sylbi 217	. . . . . . 7 ⊢ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
24	23	3ad2ant1 1133	. . . . . 6 ⊢ ((𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ∧ 𝑀 ∈ ℤ ∧ 𝐵 < 𝑀) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
25	11, 24	sylbi 217	. . . . 5 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀))))
26	25	impcom 407	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → 𝑀 ≤ (𝐵 + (𝐴 mod 𝑀)))
27		eluzelz 12803	. . . . . . . . 9 ⊢ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) → 𝐵 ∈ ℤ)
28	17, 5	anim12i 613	. . . . . . . . . . . . . . 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 12533	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
36		modlt 13842	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) → (𝐴 mod 𝑀) < 𝑀)
37	35, 9, 36	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) < 𝑀)
38	5, 14, 37	ltled 11322	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ≤ 𝑀)
39	38	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (𝐴 mod 𝑀) ≤ 𝑀)
40	34, 39	jca 511	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (𝐵 < 𝑀 ∧ (𝐴 mod 𝑀) ≤ 𝑀))
41		ltleadd 11661	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ ℝ ∧ (𝐴 mod 𝑀) ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → ((𝐵 < 𝑀 ∧ (𝐴 mod 𝑀) ≤ 𝑀) → (𝐵 + (𝐴 mod 𝑀)) < (𝑀 + 𝑀)))
42	33, 40, 41	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (𝐵 + (𝐴 mod 𝑀)) < (𝑀 + 𝑀))
43		nncn 12194	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
44	43	2timesd 12425	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) = (𝑀 + 𝑀))
45	44	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) = (𝑀 + 𝑀))
46	45	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (2 · 𝑀) = (𝑀 + 𝑀))
47	42, 46	breqtrrd 5135	. . . . . . . . . . 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 1131	. . . . . 6 ⊢ ((𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ∧ 𝑀 ∈ ℤ ∧ 𝐵 < 𝑀) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀)))
53	11, 52	sylbi 217	. . . . 5 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀)))
54	53	impcom 407	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))
55		2submod 13897	. . . . 5 ⊢ ((((𝐵 + (𝐴 mod 𝑀)) ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) ∧ (𝑀 ≤ (𝐵 + (𝐴 mod 𝑀)) ∧ (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + (𝐴 mod 𝑀)) − 𝑀))
56	55	eqcomd 2735	. . . 4 ⊢ ((((𝐵 + (𝐴 mod 𝑀)) ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) ∧ (𝑀 ≤ (𝐵 + (𝐴 mod 𝑀)) ∧ (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))) → ((𝐵 + (𝐴 mod 𝑀)) − 𝑀) = ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀))
57	8, 10, 26, 54, 56	syl22anc 838	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → ((𝐵 + (𝐴 mod 𝑀)) − 𝑀) = ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀))
58	35	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝐴 ∈ ℝ)
59	58	adantr 480	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → 𝐴 ∈ ℝ)
60	2	adantl 481	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → 𝐵 ∈ ℝ)
61		modadd2mod 13886	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀))
62	59, 60, 10, 61	syl3anc 1373	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀))
63	57, 62	eqtrd 2764	. 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 1086 = wceq 1540 ∈ wcel 2109 class class class wbr 5107 ‘cfv 6511 (class class class)co 7387 ℝcr 11067 + caddc 11071 · cmul 11073 < clt 11208 ≤ cle 11209 − cmin 11405 ℕcn 12186 2c2 12241 ℤcz 12529 ℤ_≥cuz 12793 ℝ⁺crp 12951 ..^cfzo 13615 mod cmo 13831

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-sup 9393 df-inf 9394 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-n0 12443 df-z 12530 df-uz 12794 df-rp 12952 df-fz 13469 df-fzo 13616 df-fl 13754 df-mod 13832

This theorem is referenced by: cshwidxmod 14768

W3C validator