Metamath Proof Explorer

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