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 ) )