Theorem subsubelfzo0

Description: Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018)

	Ref	Expression
Assertion	subsubelfzo0	⊢ ( ( 𝐴 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( 0 ..^ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzo0	⊢ ( 𝐴 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐴 < 𝑁 ) )
2		elfzo0	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) )
3		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
4	3	3ad2ant2	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → 𝑁 ∈ ℝ )
5		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
6	5	adantr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) → 𝐴 ∈ ℝ )
7		resubcl	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 − 𝐴 ) ∈ ℝ )
8	4 6 7	syl2anr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → ( 𝑁 − 𝐴 ) ∈ ℝ )
9		nn0re	⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ )
10	9	3ad2ant1	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → 𝐼 ∈ ℝ )
11	10	adantl	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → 𝐼 ∈ ℝ )
12		lenlt	⊢ ( ( ( 𝑁 − 𝐴 ) ∈ ℝ ∧ 𝐼 ∈ ℝ ) → ( ( 𝑁 − 𝐴 ) ≤ 𝐼 ↔ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) )
13	12	bicomd	⊢ ( ( ( 𝑁 − 𝐴 ) ∈ ℝ ∧ 𝐼 ∈ ℝ ) → ( ¬ 𝐼 < ( 𝑁 − 𝐴 ) ↔ ( 𝑁 − 𝐴 ) ≤ 𝐼 ) )
14	8 11 13	syl2anc	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → ( ¬ 𝐼 < ( 𝑁 − 𝐴 ) ↔ ( 𝑁 − 𝐴 ) ≤ 𝐼 ) )
15	14	biimpa	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → ( 𝑁 − 𝐴 ) ≤ 𝐼 )
16		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
17	16	3ad2ant2	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → 𝑁 ∈ ℤ )
18		nn0z	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
19	18	adantr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) → 𝐴 ∈ ℤ )
20		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑁 − 𝐴 ) ∈ ℤ )
21	17 19 20	syl2anr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → ( 𝑁 − 𝐴 ) ∈ ℤ )
22		ltle	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐴 < 𝑁 → 𝐴 ≤ 𝑁 ) )
23	5 4 22	syl2an	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → ( 𝐴 < 𝑁 → 𝐴 ≤ 𝑁 ) )
24	23	impancom	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) → ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → 𝐴 ≤ 𝑁 ) )
25	24	imp	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → 𝐴 ≤ 𝑁 )
26		subge0	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ ( 𝑁 − 𝐴 ) ↔ 𝐴 ≤ 𝑁 ) )
27	4 6 26	syl2anr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → ( 0 ≤ ( 𝑁 − 𝐴 ) ↔ 𝐴 ≤ 𝑁 ) )
28	25 27	mpbird	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → 0 ≤ ( 𝑁 − 𝐴 ) )
29		elnn0z	⊢ ( ( 𝑁 − 𝐴 ) ∈ ℕ0 ↔ ( ( 𝑁 − 𝐴 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 − 𝐴 ) ) )
30	21 28 29	sylanbrc	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → ( 𝑁 − 𝐴 ) ∈ ℕ0 )
31	30	adantr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → ( 𝑁 − 𝐴 ) ∈ ℕ0 )
32		simplr1	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → 𝐼 ∈ ℕ0 )
33		nn0sub	⊢ ( ( ( 𝑁 − 𝐴 ) ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝑁 − 𝐴 ) ≤ 𝐼 ↔ ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 ) )
34	31 32 33	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → ( ( 𝑁 − 𝐴 ) ≤ 𝐼 ↔ ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 ) )
35	15 34	mpbid	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 )
36		elnn0uz	⊢ ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 ↔ ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) )
37	35 36	sylib	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) )
38	19	adantr	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → 𝐴 ∈ ℤ )
39	38	adantr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → 𝐴 ∈ ℤ )
40	9	adantr	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 𝐼 ∈ ℝ )
41	40	adantl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → 𝐼 ∈ ℝ )
42	3	adantl	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
43	42	adantl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℝ )
44	42 5 7	syl2anr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑁 − 𝐴 ) ∈ ℝ )
45	41 43 44	ltsub1d	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → ( 𝐼 < 𝑁 ↔ ( 𝐼 − ( 𝑁 − 𝐴 ) ) < ( 𝑁 − ( 𝑁 − 𝐴 ) ) ) )
46		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
47	46	adantl	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
48		nn0cn	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ )
49		nncan	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝑁 − ( 𝑁 − 𝐴 ) ) = 𝐴 )
50	47 48 49	syl2anr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑁 − ( 𝑁 − 𝐴 ) ) = 𝐴 )
51	50	breq2d	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) < ( 𝑁 − ( 𝑁 − 𝐴 ) ) ↔ ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) )
52	51	biimpd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) < ( 𝑁 − ( 𝑁 − 𝐴 ) ) → ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) )
53	45 52	sylbid	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → ( 𝐼 < 𝑁 → ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) )
54	53	ex	⊢ ( 𝐴 ∈ ℕ0 → ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐼 < 𝑁 → ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) ) )
55	54	adantr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) → ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐼 < 𝑁 → ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) ) )
56	55	com3l	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐼 < 𝑁 → ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) → ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) ) )
57	56	3impia	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) → ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) )
58	57	impcom	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) → ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 )
59	58	adantr	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 )
60	37 39 59	3jca	⊢ ( ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝐴 ∈ ℤ ∧ ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) )
61	60	exp31	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) → ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → ( ¬ 𝐼 < ( 𝑁 − 𝐴 ) → ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝐴 ∈ ℤ ∧ ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) ) ) )
62	2 61	syl5bi	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑁 ) → ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → ( ¬ 𝐼 < ( 𝑁 − 𝐴 ) → ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝐴 ∈ ℤ ∧ ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) ) ) )
63	62	3adant2	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐴 < 𝑁 ) → ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → ( ¬ 𝐼 < ( 𝑁 − 𝐴 ) → ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝐴 ∈ ℤ ∧ ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) ) ) )
64	1 63	sylbi	⊢ ( 𝐴 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → ( ¬ 𝐼 < ( 𝑁 − 𝐴 ) → ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝐴 ∈ ℤ ∧ ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) ) ) )
65	64	3imp	⊢ ( ( 𝐴 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝐴 ∈ ℤ ∧ ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) )
66		elfzo2	⊢ ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( 0 ..^ 𝐴 ) ↔ ( ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝐴 ∈ ℤ ∧ ( 𝐼 − ( 𝑁 − 𝐴 ) ) < 𝐴 ) )
67	65 66	sylibr	⊢ ( ( 𝐴 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ ¬ 𝐼 < ( 𝑁 − 𝐴 ) ) → ( 𝐼 − ( 𝑁 − 𝐴 ) ) ∈ ( 0 ..^ 𝐴 ) )