Theorem fvmptnn04ifa

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

	Ref	Expression
Hypotheses	fvmptnn04if.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) )
	fvmptnn04if.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ )
	fvmptnn04if.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	fvmptnn04ifa	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑁 ) = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fvmptnn04if.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) )
2		fvmptnn04if.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ )
3		fvmptnn04if.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → 𝑆 ∈ ℕ )
5	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → 𝑁 ∈ ℕ0 )
6		simp3	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 )
7		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) ∧ 𝑁 = 0 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 )
8		simpr	⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 0 < 𝑁 )
9	8	gt0ne0d	⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑁 ≠ 0 )
10	9	neneqd	⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ¬ 𝑁 = 0 )
11	10	pm2.21d	⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( 𝑁 = 0 → ( 𝑁 < 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) )
12	11	impancom	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 0 < 𝑁 → ( 𝑁 < 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) )
13	12	3adant3	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → ( 0 < 𝑁 → ( 𝑁 < 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) )
14	13	3imp	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 )
15	2	nnne0d	⊢ ( 𝜑 → 𝑆 ≠ 0 )
16	15	necomd	⊢ ( 𝜑 → 0 ≠ 𝑆 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 0 ≠ 𝑆 )
18		neeq1	⊢ ( 𝑁 = 0 → ( 𝑁 ≠ 𝑆 ↔ 0 ≠ 𝑆 ) )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝑁 ≠ 𝑆 ↔ 0 ≠ 𝑆 ) )
20	17 19	mpbird	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑁 ≠ 𝑆 )
21	20	3adant3	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → 𝑁 ≠ 𝑆 )
22	21	neneqd	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → ¬ 𝑁 = 𝑆 )
23	22	pm2.21d	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → ( 𝑁 = 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ) )
24	23	imp	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) ∧ 𝑁 = 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 )
25		nnnn0	⊢ ( 𝑆 ∈ ℕ → 𝑆 ∈ ℕ0 )
26		nn0nlt0	⊢ ( 𝑆 ∈ ℕ0 → ¬ 𝑆 < 0 )
27	2 25 26	3syl	⊢ ( 𝜑 → ¬ 𝑆 < 0 )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ¬ 𝑆 < 0 )
29		breq2	⊢ ( 𝑁 = 0 → ( 𝑆 < 𝑁 ↔ 𝑆 < 0 ) )
30	29	notbid	⊢ ( 𝑁 = 0 → ( ¬ 𝑆 < 𝑁 ↔ ¬ 𝑆 < 0 ) )
31	30	adantl	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( ¬ 𝑆 < 𝑁 ↔ ¬ 𝑆 < 0 ) )
32	28 31	mpbird	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ¬ 𝑆 < 𝑁 )
33	32	3adant3	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → ¬ 𝑆 < 𝑁 )
34	33	pm2.21d	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → ( 𝑆 < 𝑁 → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 = ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ) )
35	34	imp	⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) ∧ 𝑆 < 𝑁 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 = ⦋ 𝑁 / 𝑛 ⦌ 𝐷 )
36	1 4 5 6 7 14 24 35	fvmptnn04if	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑁 ) = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 )