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 13833

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 13551	. . . . . . . 8 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → 𝐵 ∈ ℤ)
2	1	zred 12569	. . . . . . 7 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → 𝐵 ∈ ℝ)
3	2	adantr 480	. . . . . 6 ⊢ ((𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → 𝐵 ∈ ℝ)
4		zmodcl 13787	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ∈ ℕ₀)
5	4	nn0red 12435	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ∈ ℝ)
6	5	adantl 481	. . . . . 6 ⊢ ((𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐴 mod 𝑀) ∈ ℝ)
7	3, 6	readdcld 11133	. . . . 5 ⊢ ((𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐵 + (𝐴 mod 𝑀)) ∈ ℝ)
8	7	ancoms 458	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → (𝐵 + (𝐴 mod 𝑀)) ∈ ℝ)
9		nnrp 12894	. . . . 5 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ⁺)
10	9	ad2antlr 727	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → 𝑀 ∈ ℝ⁺)
11		elfzo2 13554	. . . . . 6 ⊢ (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) ↔ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ∧ 𝑀 ∈ ℤ ∧ 𝐵 < 𝑀))
12		eluz2 12730	. . . . . . . 8 ⊢ (𝐵 ∈ (ℤ_≥‘(𝑀 − (𝐴 mod 𝑀))) ↔ ((𝑀 − (𝐴 mod 𝑀)) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑀 − (𝐴 mod 𝑀)) ≤ 𝐵))
13		nnre 12124	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
14	13	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ∈ ℝ)
15	14	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → 𝑀 ∈ ℝ)
16	5	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐴 mod 𝑀) ∈ ℝ)
17		zre 12464	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℝ)
18	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → 𝐵 ∈ ℝ)
19	15, 16, 18	lesubaddd 11706	. . . . . . . . . . 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 12734	. . . . . . . . 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 12464	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
36		modlt 13776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) → (𝐴 mod 𝑀) < 𝑀)
37	35, 9, 36	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) < 𝑀)
38	5, 14, 37	ltled 11253	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ≤ 𝑀)
39	38	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (𝐴 mod 𝑀) ≤ 𝑀)
40	34, 39	jca 511	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (𝐵 < 𝑀 ∧ (𝐴 mod 𝑀) ≤ 𝑀))
41		ltleadd 11592	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ ℝ ∧ (𝐴 mod 𝑀) ∈ ℝ) ∧ (𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → ((𝐵 < 𝑀 ∧ (𝐴 mod 𝑀) ≤ 𝑀) → (𝐵 + (𝐴 mod 𝑀)) < (𝑀 + 𝑀)))
42	33, 40, 41	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (𝐵 + (𝐴 mod 𝑀)) < (𝑀 + 𝑀))
43		nncn 12125	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
44	43	2timesd 12356	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) = (𝑀 + 𝑀))
45	44	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) = (𝑀 + 𝑀))
46	45	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) ∧ 𝐵 < 𝑀) → (2 · 𝑀) = (𝑀 + 𝑀))
47	42, 46	breqtrrd 5117	. . . . . . . . . . 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 13831	. . . . 5 ⊢ ((((𝐵 + (𝐴 mod 𝑀)) ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) ∧ (𝑀 ≤ (𝐵 + (𝐴 mod 𝑀)) ∧ (𝐵 + (𝐴 mod 𝑀)) < (2 · 𝑀))) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + (𝐴 mod 𝑀)) − 𝑀))
56	55	eqcomd 2736	. . . 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 13820	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀))
62	59, 60, 10, 61	syl3anc 1373	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀)) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀))
63	57, 62	eqtrd 2765	. 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 1541 ∈ wcel 2110 class class class wbr 5089 ‘cfv 6477 (class class class)co 7341 ℝcr 10997 + caddc 11001 · cmul 11003 < clt 11138 ≤ cle 11139 − cmin 11336 ℕcn 12117 2c2 12172 ℤcz 12460 ℤ_≥cuz 12724 ℝ⁺crp 12882 ..^cfzo 13546 mod cmo 13765

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-cnex 11054 ax-resscn 11055 ax-1cn 11056 ax-icn 11057 ax-addcl 11058 ax-addrcl 11059 ax-mulcl 11060 ax-mulrcl 11061 ax-mulcom 11062 ax-addass 11063 ax-mulass 11064 ax-distr 11065 ax-i2m1 11066 ax-1ne0 11067 ax-1rid 11068 ax-rnegex 11069 ax-rrecex 11070 ax-cnre 11071 ax-pre-lttri 11072 ax-pre-lttrn 11073 ax-pre-ltadd 11074 ax-pre-mulgt0 11075 ax-pre-sup 11076

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3344 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6244 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-sup 9321 df-inf 9322 df-pnf 11140 df-mnf 11141 df-xr 11142 df-ltxr 11143 df-le 11144 df-sub 11338 df-neg 11339 df-div 11767 df-nn 12118 df-2 12180 df-n0 12374 df-z 12461 df-uz 12725 df-rp 12883 df-fz 13400 df-fzo 13547 df-fl 13688 df-mod 13766

This theorem is referenced by: cshwidxmod 14702

W3C validator