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

Metamath Proof Explorer

Theorem modm1p1mod0

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

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

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 modaddmod ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( ( 𝐴 + 1 ) mod 𝑀 ) )
3 1 2 mp3an2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( ( 𝐴 + 1 ) mod 𝑀 ) )
4 3 eqcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 + 1 ) mod 𝑀 ) = ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) )
5 4 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = ( 𝑀 − 1 ) ) → ( ( 𝐴 + 1 ) mod 𝑀 ) = ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) )
6 oveq1 ⊢ ( ( 𝐴 mod 𝑀 ) = ( 𝑀 − 1 ) → ( ( 𝐴 mod 𝑀 ) + 1 ) = ( ( 𝑀 − 1 ) + 1 ) )
7 6 oveq1d ⊢ ( ( 𝐴 mod 𝑀 ) = ( 𝑀 − 1 ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = ( ( ( 𝑀 − 1 ) + 1 ) mod 𝑀 ) )
8 rpcn ⊢ ( 𝑀 ∈ ℝ+ → 𝑀 ∈ ℂ )
9 npcan1 ⊢ ( 𝑀 ∈ ℂ → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
10 8 9 syl ⊢ ( 𝑀 ∈ ℝ+ → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
11 10 oveq1d ⊢ ( 𝑀 ∈ ℝ+ → ( ( ( 𝑀 − 1 ) + 1 ) mod 𝑀 ) = ( 𝑀 mod 𝑀 ) )
12 modid0 ⊢ ( 𝑀 ∈ ℝ+ → ( 𝑀 mod 𝑀 ) = 0 )
13 11 12 eqtrd ⊢ ( 𝑀 ∈ ℝ+ → ( ( ( 𝑀 − 1 ) + 1 ) mod 𝑀 ) = 0 )
14 13 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝑀 − 1 ) + 1 ) mod 𝑀 ) = 0 )
15 7 14 sylan9eqr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = ( 𝑀 − 1 ) ) → ( ( ( 𝐴 mod 𝑀 ) + 1 ) mod 𝑀 ) = 0 )
16 5 15 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = ( 𝑀 − 1 ) ) → ( ( 𝐴 + 1 ) mod 𝑀 ) = 0 )
17 16 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = ( 𝑀 − 1 ) → ( ( 𝐴 + 1 ) mod 𝑀 ) = 0 ) )