Theorem fvmptnn04ifb

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

	Ref	Expression
Hypotheses	fvmptnn04if.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) )
	fvmptnn04if.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ )
	fvmptnn04if.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	fvmptnn04ifb	⊢ ( ( 𝜑 ∧ ( 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		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
8		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
9	7 8	jca	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) )
10		ne0gt0	⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) → ( 𝑁 ≠ 0 ↔ 0 < 𝑁 ) )
11	3 9 10	3syl	⊢ ( 𝜑 → ( 𝑁 ≠ 0 ↔ 0 < 𝑁 ) )
12	11	biimprcd	⊢ ( 0 < 𝑁 → ( 𝜑 → 𝑁 ≠ 0 ) )
13	12	adantr	⊢ ( ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) → ( 𝜑 → 𝑁 ≠ 0 ) )
14	13	impcom	⊢ ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ) → 𝑁 ≠ 0 )
15	14	3adant3	⊢ ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) → 𝑁 ≠ 0 )
16		neneq	⊢ ( 𝑁 ≠ 0 → ¬ 𝑁 = 0 )
17	16	pm2.21d	⊢ ( 𝑁 ≠ 0 → ( 𝑁 = 0 → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ) )
18	15 17	syl	⊢ ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) → ( 𝑁 = 0 → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ) )
19	18	imp	⊢ ( ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) ∧ 𝑁 = 0 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 )
20		eqidd	⊢ ( ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 )
21	3 7	syl	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑁 < 𝑆 ) → 𝑁 ∈ ℝ )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑁 < 𝑆 ) → 𝑁 < 𝑆 )
24	22 23	ltned	⊢ ( ( 𝜑 ∧ 𝑁 < 𝑆 ) → 𝑁 ≠ 𝑆 )
25	24	neneqd	⊢ ( ( 𝜑 ∧ 𝑁 < 𝑆 ) → ¬ 𝑁 = 𝑆 )
26	25	adantrl	⊢ ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ) → ¬ 𝑁 = 𝑆 )
27	26	3adant3	⊢ ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) → ¬ 𝑁 = 𝑆 )
28	27	pm2.21d	⊢ ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) → ( 𝑁 = 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ) )
29	28	imp	⊢ ( ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) ∧ 𝑁 = 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 )
30	2	nnred	⊢ ( 𝜑 → 𝑆 ∈ ℝ )
31		ltnsym	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( 𝑁 < 𝑆 → ¬ 𝑆 < 𝑁 ) )
32	21 30 31	syl2anc	⊢ ( 𝜑 → ( 𝑁 < 𝑆 → ¬ 𝑆 < 𝑁 ) )
33	32	com12	⊢ ( 𝑁 < 𝑆 → ( 𝜑 → ¬ 𝑆 < 𝑁 ) )
34	33	adantl	⊢ ( ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) → ( 𝜑 → ¬ 𝑆 < 𝑁 ) )
35	34	impcom	⊢ ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ) → ¬ 𝑆 < 𝑁 )
36	35	3adant3	⊢ ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) → ¬ 𝑆 < 𝑁 )
37	36	pm2.21d	⊢ ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) → ( 𝑆 < 𝑁 → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 = ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ) )
38	37	imp	⊢ ( ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) ∧ 𝑆 < 𝑁 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 = ⦋ 𝑁 / 𝑛 ⦌ 𝐷 )
39	1 4 5 6 19 20 29 38	fvmptnn04if	⊢ ( ( 𝜑 ∧ ( 0 < 𝑁 ∧ 𝑁 < 𝑆 ) ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑁 ) = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 )