Theorem 2submod

Description: If a real number is between a positive real number and twice the positive real number, the real number modulo the positive real number equals the real number minus the positive real number. (Contributed by Alexander van der Vekens, 13-May-2018)

	Ref	Expression
Assertion	2submod	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
2		ax-1rid	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 1 ) = 𝐵 )
3	1 2	syl	⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 · 1 ) = 𝐵 )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · 1 ) = 𝐵 )
5	4	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 − ( 𝐵 · 1 ) ) = ( 𝐴 − 𝐵 ) )
6	5	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐵 · 1 ) ) mod 𝐵 ) = ( ( 𝐴 − 𝐵 ) mod 𝐵 ) )
7	6	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( ( 𝐴 − ( 𝐵 · 1 ) ) mod 𝐵 ) = ( ( 𝐴 − 𝐵 ) mod 𝐵 ) )
8		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
9		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
10		1zzd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 1 ∈ ℤ )
11	8 9 10	3jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 1 ∈ ℤ ) )
12	11	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 1 ∈ ℤ ) )
13		modcyc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 1 ∈ ℤ ) → ( ( 𝐴 − ( 𝐵 · 1 ) ) mod 𝐵 ) = ( 𝐴 mod 𝐵 ) )
14	12 13	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( ( 𝐴 − ( 𝐵 · 1 ) ) mod 𝐵 ) = ( 𝐴 mod 𝐵 ) )
15		resubcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
16	1 15	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
17	16 9	jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 − 𝐵 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) )
18		subge0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ ( 𝐴 − 𝐵 ) ↔ 𝐵 ≤ 𝐴 ) )
19	1 18	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 0 ≤ ( 𝐴 − 𝐵 ) ↔ 𝐵 ≤ 𝐴 ) )
20	19	bicomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 ≤ 𝐴 ↔ 0 ≤ ( 𝐴 − 𝐵 ) ) )
21		rpcn	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
22	21	2timesd	⊢ ( 𝐵 ∈ ℝ+ → ( 2 · 𝐵 ) = ( 𝐵 + 𝐵 ) )
23	22	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 2 · 𝐵 ) = ( 𝐵 + 𝐵 ) )
24	23	breq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 < ( 2 · 𝐵 ) ↔ 𝐴 < ( 𝐵 + 𝐵 ) ) )
25	1	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
26	8 25 25	ltsubaddd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 − 𝐵 ) < 𝐵 ↔ 𝐴 < ( 𝐵 + 𝐵 ) ) )
27	24 26	bitr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 < ( 2 · 𝐵 ) ↔ ( 𝐴 − 𝐵 ) < 𝐵 ) )
28	20 27	anbi12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 2 · 𝐵 ) ) ↔ ( 0 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐴 − 𝐵 ) < 𝐵 ) ) )
29	28	biimpa	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( 0 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐴 − 𝐵 ) < 𝐵 ) )
30		modid	⊢ ( ( ( ( 𝐴 − 𝐵 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐴 − 𝐵 ) < 𝐵 ) ) → ( ( 𝐴 − 𝐵 ) mod 𝐵 ) = ( 𝐴 − 𝐵 ) )
31	17 29 30	syl2an2r	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( ( 𝐴 − 𝐵 ) mod 𝐵 ) = ( 𝐴 − 𝐵 ) )
32	7 14 31	3eqtr3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − 𝐵 ) )