This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )