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 ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) )
fvmptnn04if.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
fvmptnn04if.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion fvmptnn04ifc ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑁 ) = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 )

Proof

Step Hyp Ref Expression
1 fvmptnn04if.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) )
2 fvmptnn04if.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
3 fvmptnn04if.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → 𝑆 ∈ ℕ )
5 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → 𝑁 ∈ ℕ0 )
6 simp3 ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 )
7 nnne0 ⊢ ( 𝑆 ∈ ℕ → 𝑆 ≠ 0 )
8 7 neneqd ⊢ ( 𝑆 ∈ ℕ → ¬ 𝑆 = 0 )
9 2 8 syl ⊢ ( 𝜑 → ¬ 𝑆 = 0 )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ) → ¬ 𝑆 = 0 )
11 eqeq1 ⊢ ( 𝑁 = 𝑆 → ( 𝑁 = 0 ↔ 𝑆 = 0 ) )
12 11 notbid ⊢ ( 𝑁 = 𝑆 → ( ¬ 𝑁 = 0 ↔ ¬ 𝑆 = 0 ) )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ) → ( ¬ 𝑁 = 0 ↔ ¬ 𝑆 = 0 ) )
14 10 13 mpbird ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ) → ¬ 𝑁 = 0 )
15 14 3adant3 ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → ¬ 𝑁 = 0 )
16 15 pm2.21d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → ( 𝑁 = 0 → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ) )
17 16 imp ⊢ ( ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) ∧ 𝑁 = 0 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 )
18 3 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
19 2 nnred ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
20 18 19 lttri3d ⊢ ( 𝜑 → ( 𝑁 = 𝑆 ↔ ( ¬ 𝑁 < 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) )
21 20 simprbda ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ) → ¬ 𝑁 < 𝑆 )
22 21 pm2.21d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ) → ( 𝑁 < 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) )
23 22 3adant3 ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → ( 𝑁 < 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) )
24 23 a1d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → ( 0 < 𝑁 → ( 𝑁 < 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) )
25 24 3imp ⊢ ( ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 )
26 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) ∧ 𝑁 = 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 )
27 20 simplbda ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ) → ¬ 𝑆 < 𝑁 )
28 27 3adant3 ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → ¬ 𝑆 < 𝑁 )
29 28 pm2.21d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → ( 𝑆 < 𝑁 → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ) )
30 29 imp ⊢ ( ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) ∧ 𝑆 < 𝑁 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = ⦋ 𝑁 / 𝑛 ⦌ 𝐷 )
31 1 4 5 6 17 25 26 30 fvmptnn04if ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑁 ) = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 )