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

Metamath Proof Explorer

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 ..^ 𝑁 ) ∧ 𝐵 < 𝐴 ) → ( 𝐵 + ( 𝑁 − 𝐴 ) ) < 𝑁 )