Metamath Proof Explorer

Theorem fvmptnn04ifc

Description: The function value of a mapping from the nonnegative integers with four distinct cases for the third case. (Contributed by AV, 10-Nov-2019)

Ref Expression
Hypotheses fvmptnn04if.g ⊢ G = n ∈ ℕ 0 ⟼ if n = 0 A if n = S C if S < n D B
fvmptnn04if.s ⊢ φ → S ∈ ℕ
fvmptnn04if.n ⊢ φ → N ∈ ℕ 0
Assertion fvmptnn04ifc ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → G ⁡ N = ⦋ N / n⦌ C

Proof

Step Hyp Ref Expression
1 fvmptnn04if.g ⊢ G = n ∈ ℕ 0 ⟼ if n = 0 A if n = S C if S < n D B
2 fvmptnn04if.s ⊢ φ → S ∈ ℕ
3 fvmptnn04if.n ⊢ φ → N ∈ ℕ 0
4 2 3ad2ant1 ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → S ∈ ℕ
5 3 3ad2ant1 ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → N ∈ ℕ 0
6 simp3 ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → ⦋ N / n⦌ C ∈ V
7 nnne0 ⊢ S ∈ ℕ → S ≠ 0
8 7 neneqd ⊢ S ∈ ℕ → ¬ S = 0
9 2 8 syl ⊢ φ → ¬ S = 0
10 9 adantr ⊢ φ ∧ N = S → ¬ S = 0
11 eqeq1 ⊢ N = S → N = 0 ↔ S = 0
12 11 notbid ⊢ N = S → ¬ N = 0 ↔ ¬ S = 0
13 12 adantl ⊢ φ ∧ N = S → ¬ N = 0 ↔ ¬ S = 0
14 10 13 mpbird ⊢ φ ∧ N = S → ¬ N = 0
15 14 3adant3 ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → ¬ N = 0
16 15 pm2.21d ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → N = 0 → ⦋ N / n⦌ C = ⦋ N / n⦌ A
17 16 imp ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V ∧ N = 0 → ⦋ N / n⦌ C = ⦋ N / n⦌ A
18 3 nn0red ⊢ φ → N ∈ ℝ
19 2 nnred ⊢ φ → S ∈ ℝ
20 18 19 lttri3d ⊢ φ → N = S ↔ ¬ N < S ∧ ¬ S < N
21 20 simprbda ⊢ φ ∧ N = S → ¬ N < S
22 21 pm2.21d ⊢ φ ∧ N = S → N < S → ⦋ N / n⦌ C = ⦋ N / n⦌ B
23 22 3adant3 ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → N < S → ⦋ N / n⦌ C = ⦋ N / n⦌ B
24 23 a1d ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → 0 < N → N < S → ⦋ N / n⦌ C = ⦋ N / n⦌ B
25 24 3imp ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V ∧ 0 < N ∧ N < S → ⦋ N / n⦌ C = ⦋ N / n⦌ B
26 eqidd ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V ∧ N = S → ⦋ N / n⦌ C = ⦋ N / n⦌ C
27 20 simplbda ⊢ φ ∧ N = S → ¬ S < N
28 27 3adant3 ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → ¬ S < N
29 28 pm2.21d ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → S < N → ⦋ N / n⦌ C = ⦋ N / n⦌ D
30 29 imp ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V ∧ S < N → ⦋ N / n⦌ C = ⦋ N / n⦌ D
31 1 4 5 6 17 25 26 30 fvmptnn04if ⊢ φ ∧ N = S ∧ ⦋ N / n⦌ C ∈ V → G ⁡ N = ⦋ N / n⦌ C