Theorem fvmptnn04ifd

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

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

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		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
8	2	nnred	⊢ ( 𝜑 → 𝑆 ∈ ℝ )
9	2	nngt0d	⊢ ( 𝜑 → 0 < 𝑆 )
10	7 8 9	ltnsymd	⊢ ( 𝜑 → ¬ 𝑆 < 0 )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ¬ 𝑆 < 0 )
12		breq2	⊢ ( 𝑁 = 0 → ( 𝑆 < 𝑁 ↔ 𝑆 < 0 ) )
13	12	notbid	⊢ ( 𝑁 = 0 → ( ¬ 𝑆 < 𝑁 ↔ ¬ 𝑆 < 0 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( ¬ 𝑆 < 𝑁 ↔ ¬ 𝑆 < 0 ) )
15	11 14	mpbird	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ¬ 𝑆 < 𝑁 )
16	15	pm2.21d	⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 𝑆 < 𝑁 → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ) )
17	16	impancom	⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ) → ( 𝑁 = 0 → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ) )
18	17	3adant3	⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 ) → ( 𝑁 = 0 → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ) )
19	18	imp	⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 ) ∧ 𝑁 = 0 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 )
20	3	nn0red	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
21		ltnsym	⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑆 < 𝑁 → ¬ 𝑁 < 𝑆 ) )
22	8 20 21	syl2anc	⊢ ( 𝜑 → ( 𝑆 < 𝑁 → ¬ 𝑁 < 𝑆 ) )
23	22	imp	⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ) → ¬ 𝑁 < 𝑆 )
24	23	3adant3	⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 ) → ¬ 𝑁 < 𝑆 )
25	24	pm2.21d	⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 ) → ( 𝑁 < 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) )
26	25	a1d	⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 ) → ( 0 < 𝑁 → ( 𝑁 < 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) )
27	26	3imp	⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 ) ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 )
28	20 8	lttri3d	⊢ ( 𝜑 → ( 𝑁 = 𝑆 ↔ ( ¬ 𝑁 < 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) )
29	28	simplbda	⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ) → ¬ 𝑆 < 𝑁 )
30	29	pm2.21d	⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ) → ( 𝑆 < 𝑁 → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ) )
31	30	impancom	⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ) → ( 𝑁 = 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ) )
32	31	3adant3	⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 ) → ( 𝑁 = 𝑆 → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ) )
33	32	imp	⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 ) ∧ 𝑁 = 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 )
34		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 ) ∧ 𝑆 < 𝑁 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = ⦋ 𝑁 / 𝑛 ⦌ 𝐷 )
35	1 4 5 6 19 27 33 34	fvmptnn04if	⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑁 ) = ⦋ 𝑁 / 𝑛 ⦌ 𝐷 )