Theorem fzonmapblen

Description: The result of subtracting a nonnegative integer from a positive integer and adding another nonnegative integer which is less than the first one is less than the positive integer. (Contributed by Alexander van der Vekens, 19-May-2018)

	Ref	Expression
Assertion	fzonmapblen	⊢ ( ( 𝐴 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐵 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐵 < 𝐴 ) → ( 𝐵 + ( 𝑁 − 𝐴 ) ) < 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		elfzo0	⊢ ( 𝐴 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐴 < 𝑁 ) )
2		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
3		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
4	2 3	anim12i	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
5	4	3adant3	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐴 < 𝑁 ) → ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
6	1 5	sylbi	⊢ ( 𝐴 ∈ ( 0 ..^ 𝑁 ) → ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
7		elfzoelz	⊢ ( 𝐵 ∈ ( 0 ..^ 𝑁 ) → 𝐵 ∈ ℤ )
8	7	zred	⊢ ( 𝐵 ∈ ( 0 ..^ 𝑁 ) → 𝐵 ∈ ℝ )
9		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
10		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
11		resubcl	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 − 𝐴 ) ∈ ℝ )
12	11	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑁 − 𝐴 ) ∈ ℝ )
13	12	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) → ( 𝑁 − 𝐴 ) ∈ ℝ )
14	9 10 13	ltadd1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ ( 𝐵 + ( 𝑁 − 𝐴 ) ) < ( 𝐴 + ( 𝑁 − 𝐴 ) ) ) )
15	14	biimpa	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( 𝐵 + ( 𝑁 − 𝐴 ) ) < ( 𝐴 + ( 𝑁 − 𝐴 ) ) )
16		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
17		recn	⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
18	16 17	anim12i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
19	18	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
20	19	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
21		pncan3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐴 + ( 𝑁 − 𝐴 ) ) = 𝑁 )
22	20 21	syl	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( 𝐴 + ( 𝑁 − 𝐴 ) ) = 𝑁 )
23	15 22	breqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( 𝐵 + ( 𝑁 − 𝐴 ) ) < 𝑁 )
24	23	ex	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < 𝐴 → ( 𝐵 + ( 𝑁 − 𝐴 ) ) < 𝑁 ) )
25	6 8 24	syl2an	⊢ ( ( 𝐴 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐵 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 < 𝐴 → ( 𝐵 + ( 𝑁 − 𝐴 ) ) < 𝑁 ) )
26	25	3impia	⊢ ( ( 𝐴 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐵 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐵 < 𝐴 ) → ( 𝐵 + ( 𝑁 − 𝐴 ) ) < 𝑁 )