Theorem modmuladdnn0

Description: Implication of a decomposition of a nonnegative integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021)

	Ref	Expression
Assertion	modmuladdnn0	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 → ∃ 𝑘 ∈ ℕ0 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 · 𝑀 ) = ( 𝑖 · 𝑀 ) )
2	1	oveq1d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 · 𝑀 ) + 𝐵 ) = ( ( 𝑖 · 𝑀 ) + 𝐵 ) )
3	2	eqeq2d	⊢ ( 𝑘 = 𝑖 → ( 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ↔ 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ) )
4		simpr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℤ )
5	4	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ) → 𝑖 ∈ ℤ )
6		eqcom	⊢ ( 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ↔ ( ( 𝑖 · 𝑀 ) + 𝐵 ) = 𝐴 )
7		nn0cn	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ )
8	7	adantr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
9	8	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → 𝐴 ∈ ℂ )
10		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
11		modcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
12	10 11	sylan	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
13	12	recnd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℂ )
14	13	adantr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → ( 𝐴 mod 𝑀 ) ∈ ℂ )
15		eleq1	⊢ ( ( 𝐴 mod 𝑀 ) = 𝐵 → ( ( 𝐴 mod 𝑀 ) ∈ ℂ ↔ 𝐵 ∈ ℂ ) )
16	15	adantl	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → ( ( 𝐴 mod 𝑀 ) ∈ ℂ ↔ 𝐵 ∈ ℂ ) )
17	14 16	mpbid	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → 𝐵 ∈ ℂ )
18	17	adantr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → 𝐵 ∈ ℂ )
19		zcn	⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℂ )
20	19	adantl	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℂ )
21		rpcn	⊢ ( 𝑀 ∈ ℝ+ → 𝑀 ∈ ℂ )
22	21	adantl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ∈ ℂ )
23	22	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → 𝑀 ∈ ℂ )
24	20 23	mulcld	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( 𝑖 · 𝑀 ) ∈ ℂ )
25	9 18 24	subadd2d	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( ( 𝐴 − 𝐵 ) = ( 𝑖 · 𝑀 ) ↔ ( ( 𝑖 · 𝑀 ) + 𝐵 ) = 𝐴 ) )
26	6 25	bitr4id	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝑖 · 𝑀 ) ) )
27	7	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → 𝐴 ∈ ℂ )
28	27 17	subcld	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
29	28	adantr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
30		rpcnne0	⊢ ( 𝑀 ∈ ℝ+ → ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) )
31	30	adantl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) )
32	31	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) )
33		divmul3	⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ 𝑖 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ) → ( ( ( 𝐴 − 𝐵 ) / 𝑀 ) = 𝑖 ↔ ( 𝐴 − 𝐵 ) = ( 𝑖 · 𝑀 ) ) )
34	29 20 32 33	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( ( ( 𝐴 − 𝐵 ) / 𝑀 ) = 𝑖 ↔ ( 𝐴 − 𝐵 ) = ( 𝑖 · 𝑀 ) ) )
35		oveq2	⊢ ( 𝐵 = ( 𝐴 mod 𝑀 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 − ( 𝐴 mod 𝑀 ) ) )
36	35	oveq1d	⊢ ( 𝐵 = ( 𝐴 mod 𝑀 ) → ( ( 𝐴 − 𝐵 ) / 𝑀 ) = ( ( 𝐴 − ( 𝐴 mod 𝑀 ) ) / 𝑀 ) )
37	36	eqcoms	⊢ ( ( 𝐴 mod 𝑀 ) = 𝐵 → ( ( 𝐴 − 𝐵 ) / 𝑀 ) = ( ( 𝐴 − ( 𝐴 mod 𝑀 ) ) / 𝑀 ) )
38	37	adantl	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → ( ( 𝐴 − 𝐵 ) / 𝑀 ) = ( ( 𝐴 − ( 𝐴 mod 𝑀 ) ) / 𝑀 ) )
39	38	adantr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( ( 𝐴 − 𝐵 ) / 𝑀 ) = ( ( 𝐴 − ( 𝐴 mod 𝑀 ) ) / 𝑀 ) )
40		moddiffl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐴 mod 𝑀 ) ) / 𝑀 ) = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) )
41	10 40	sylan	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐴 mod 𝑀 ) ) / 𝑀 ) = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) )
42	41	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( ( 𝐴 − ( 𝐴 mod 𝑀 ) ) / 𝑀 ) = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) )
43	39 42	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( ( 𝐴 − 𝐵 ) / 𝑀 ) = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) )
44	43	eqeq1d	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( ( ( 𝐴 − 𝐵 ) / 𝑀 ) = 𝑖 ↔ ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) = 𝑖 ) )
45	26 34 44	3bitr2d	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ↔ ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) = 𝑖 ) )
46		nn0ge0	⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
47	10 46	jca	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
48		rpregt0	⊢ ( 𝑀 ∈ ℝ+ → ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) )
49		divge0	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → 0 ≤ ( 𝐴 / 𝑀 ) )
50	47 48 49	syl2an	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → 0 ≤ ( 𝐴 / 𝑀 ) )
51	10	adantr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
52		rpre	⊢ ( 𝑀 ∈ ℝ+ → 𝑀 ∈ ℝ )
53	52	adantl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ∈ ℝ )
54		rpne0	⊢ ( 𝑀 ∈ ℝ+ → 𝑀 ≠ 0 )
55	54	adantl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ≠ 0 )
56	51 53 55	redivcld	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 / 𝑀 ) ∈ ℝ )
57		0z	⊢ 0 ∈ ℤ
58		flge	⊢ ( ( ( 𝐴 / 𝑀 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( 𝐴 / 𝑀 ) ↔ 0 ≤ ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) ) )
59	56 57 58	sylancl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → ( 0 ≤ ( 𝐴 / 𝑀 ) ↔ 0 ≤ ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) ) )
60	50 59	mpbid	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → 0 ≤ ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) )
61		breq2	⊢ ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) = 𝑖 → ( 0 ≤ ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) ↔ 0 ≤ 𝑖 ) )
62	60 61	syl5ibcom	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) = 𝑖 → 0 ≤ 𝑖 ) )
63	62	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) = 𝑖 → 0 ≤ 𝑖 ) )
64	45 63	sylbid	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) → ( 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) → 0 ≤ 𝑖 ) )
65	64	imp	⊢ ( ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ) → 0 ≤ 𝑖 )
66		elnn0z	⊢ ( 𝑖 ∈ ℕ0 ↔ ( 𝑖 ∈ ℤ ∧ 0 ≤ 𝑖 ) )
67	5 65 66	sylanbrc	⊢ ( ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ) → 𝑖 ∈ ℕ0 )
68		simpr	⊢ ( ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ) → 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) )
69	3 67 68	rspcedvdw	⊢ ( ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) ∧ 𝑖 ∈ ℤ ) ∧ 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ) → ∃ 𝑘 ∈ ℕ0 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) )
70		nn0z	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
71		modmuladdim	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 → ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ) )
72	70 71	sylan	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 → ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) ) )
73	72	imp	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → ∃ 𝑖 ∈ ℤ 𝐴 = ( ( 𝑖 · 𝑀 ) + 𝐵 ) )
74	69 73	r19.29a	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → ∃ 𝑘 ∈ ℕ0 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) )
75	74	ex	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 → ∃ 𝑘 ∈ ℕ0 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )