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

Metamath Proof Explorer

Theorem modltm1p1mod

Description: If a real number modulo a positive real number is less than the positive real number decreased by 1, the real number increased by 1 modulo the positive real number equals the real number modulo the positive real number increased by 1. (Contributed by AV, 2-Nov-2018)

Ref Expression
Assertion modltm1p1mod ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ ( 𝐴 mod 𝑀 ) < ( 𝑀 − 1 ) ) → ( ( 𝐴 + 1 ) mod 𝑀 ) = ( ( 𝐴 mod 𝑀 ) + 1 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
2 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 1 ∈ ℝ )
3 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ∈ ℝ+ )
4 1 2 3 3jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
5 4 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ ( 𝐴 mod 𝑀 ) < ( 𝑀 − 1 ) ) → ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
6 modaddmod ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( ( 𝐴 + 1 ) mod 𝑀 ) )
7 5 6 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ ( 𝐴 mod 𝑀 ) < ( 𝑀 − 1 ) ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( ( 𝐴 + 1 ) mod 𝑀 ) )
8 modcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
9 peano2re ⊢ ( ( 𝐴 mod 𝑀 ) ∈ ℝ → ( ( 𝐴 mod 𝑀 ) + 1 ) ∈ ℝ )
10 8 9 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) + 1 ) ∈ ℝ )
11 10 3 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
12 11 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ ( 𝐴 mod 𝑀 ) < ( 𝑀 − 1 ) ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
13 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 0 ∈ ℝ )
14 modge0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 0 ≤ ( 𝐴 mod 𝑀 ) )
15 8 lep1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ≤ ( ( 𝐴 mod 𝑀 ) + 1 ) )
16 13 8 10 14 15 letrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 0 ≤ ( ( 𝐴 mod 𝑀 ) + 1 ) )
17 16 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ ( 𝐴 mod 𝑀 ) < ( 𝑀 − 1 ) ) → 0 ≤ ( ( 𝐴 mod 𝑀 ) + 1 ) )
18 rpre ⊢ ( 𝑀 ∈ ℝ+ → 𝑀 ∈ ℝ )
19 18 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ∈ ℝ )
20 8 2 19 ltaddsubd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) < 𝑀 ↔ ( 𝐴 mod 𝑀 ) < ( 𝑀 − 1 ) ) )
21 20 biimp3ar ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ ( 𝐴 mod 𝑀 ) < ( 𝑀 − 1 ) ) → ( ( 𝐴 mod 𝑀 ) + 1 ) < 𝑀 )
22 modid ⊢ ( ( ( ( ( 𝐴 mod 𝑀 ) + 1 ) ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 0 ≤ ( ( 𝐴 mod 𝑀 ) + 1 ) ∧ ( ( 𝐴 mod 𝑀 ) + 1 ) < 𝑀 ) ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( ( 𝐴 mod 𝑀 ) + 1 ) )
23 12 17 21 22 syl12anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ ( 𝐴 mod 𝑀 ) < ( 𝑀 − 1 ) ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( ( 𝐴 mod 𝑀 ) + 1 ) )
24 7 23 eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ ( 𝐴 mod 𝑀 ) < ( 𝑀 − 1 ) ) → ( ( 𝐴 + 1 ) mod 𝑀 ) = ( ( 𝐴 mod 𝑀 ) + 1 ) )