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

Metamath Proof Explorer

Theorem hashunlei

Description: Get an upper bound on a concretely specified finite set. Induction step: union of two finite bounded sets. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses hashunlei.c ⊢ C = A ∪ B
hashunlei.a ⊢ A ∈ Fin ∧ A ≤ K
hashunlei.b ⊢ B ∈ Fin ∧ B ≤ M
hashunlei.k ⊢ K ∈ ℕ 0
hashunlei.m ⊢ M ∈ ℕ 0
hashunlei.n ⊢ K + M = N
Assertion hashunlei ⊢ C ∈ Fin ∧ C ≤ N

Proof

Step Hyp Ref Expression
1 hashunlei.c ⊢ C = A ∪ B
2 hashunlei.a ⊢ A ∈ Fin ∧ A ≤ K
3 hashunlei.b ⊢ B ∈ Fin ∧ B ≤ M
4 hashunlei.k ⊢ K ∈ ℕ 0
5 hashunlei.m ⊢ M ∈ ℕ 0
6 hashunlei.n ⊢ K + M = N
7 2 simpli ⊢ A ∈ Fin
8 3 simpli ⊢ B ∈ Fin
9 unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin
10 7 8 9 mp2an ⊢ A ∪ B ∈ Fin
11 1 10 eqeltri ⊢ C ∈ Fin
12 1 fveq2i ⊢ C = A ∪ B
13 hashun2 ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ≤ A + B
14 7 8 13 mp2an ⊢ A ∪ B ≤ A + B
15 12 14 eqbrtri ⊢ C ≤ A + B
16 2 simpri ⊢ A ≤ K
17 3 simpri ⊢ B ≤ M
18 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
19 7 18 ax-mp ⊢ A ∈ ℕ 0
20 19 nn0rei ⊢ A ∈ ℝ
21 hashcl ⊢ B ∈ Fin → B ∈ ℕ 0
22 8 21 ax-mp ⊢ B ∈ ℕ 0
23 22 nn0rei ⊢ B ∈ ℝ
24 4 nn0rei ⊢ K ∈ ℝ
25 5 nn0rei ⊢ M ∈ ℝ
26 20 23 24 25 le2addi ⊢ A ≤ K ∧ B ≤ M → A + B ≤ K + M
27 16 17 26 mp2an ⊢ A + B ≤ K + M
28 27 6 breqtri ⊢ A + B ≤ N
29 hashcl ⊢ C ∈ Fin → C ∈ ℕ 0
30 11 29 ax-mp ⊢ C ∈ ℕ 0
31 30 nn0rei ⊢ C ∈ ℝ
32 20 23 readdcli ⊢ A + B ∈ ℝ
33 24 25 readdcli ⊢ K + M ∈ ℝ
34 6 33 eqeltrri ⊢ N ∈ ℝ
35 31 32 34 letri ⊢ C ≤ A + B ∧ A + B ≤ N → C ≤ N
36 15 28 35 mp2an ⊢ C ≤ N
37 11 36 pm3.2i ⊢ C ∈ Fin ∧ C ≤ N