Metamath Proof Explorer

Theorem fvmptnn04if

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

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

Proof

Step Hyp Ref Expression
1 fvmptnn04if.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) )
2 fvmptnn04if.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
3 fvmptnn04if.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 fvmptnn04if.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
5 fvmptnn04if.a ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑌 = ⦋ 𝑁 / 𝑛 ⦌ 𝐴 )
6 fvmptnn04if.b ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆 ) → 𝑌 = ⦋ 𝑁 / 𝑛 ⦌ 𝐵 )
7 fvmptnn04if.c ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ) → 𝑌 = ⦋ 𝑁 / 𝑛 ⦌ 𝐶 )
8 fvmptnn04if.d ⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ) → 𝑌 = ⦋ 𝑁 / 𝑛 ⦌ 𝐷 )
9 csbif ⊢ ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) = if ( [ 𝑁 / 𝑛 ] 𝑛 = 0 , ⦋ 𝑁 / 𝑛 ⦌ 𝐴 , ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) )
10 eqsbc1 ⊢ ( 𝑁 ∈ ℕ0 → ( [ 𝑁 / 𝑛 ] 𝑛 = 0 ↔ 𝑁 = 0 ) )
11 3 10 syl ⊢ ( 𝜑 → ( [ 𝑁 / 𝑛 ] 𝑛 = 0 ↔ 𝑁 = 0 ) )
12 csbif ⊢ ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) = if ( [ 𝑁 / 𝑛 ] 𝑛 = 𝑆 , ⦋ 𝑁 / 𝑛 ⦌ 𝐶 , ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) )
13 eqsbc1 ⊢ ( 𝑁 ∈ ℕ0 → ( [ 𝑁 / 𝑛 ] 𝑛 = 𝑆 ↔ 𝑁 = 𝑆 ) )
14 3 13 syl ⊢ ( 𝜑 → ( [ 𝑁 / 𝑛 ] 𝑛 = 𝑆 ↔ 𝑁 = 𝑆 ) )
15 csbif ⊢ ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) = if ( [ 𝑁 / 𝑛 ] 𝑆 < 𝑛 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 )
16 sbcbr2g ⊢ ( 𝑁 ∈ ℕ0 → ( [ 𝑁 / 𝑛 ] 𝑆 < 𝑛 ↔ 𝑆 < ⦋ 𝑁 / 𝑛 ⦌ 𝑛 ) )
17 3 16 syl ⊢ ( 𝜑 → ( [ 𝑁 / 𝑛 ] 𝑆 < 𝑛 ↔ 𝑆 < ⦋ 𝑁 / 𝑛 ⦌ 𝑛 ) )
18 csbvarg ⊢ ( 𝑁 ∈ ℕ0 → ⦋ 𝑁 / 𝑛 ⦌ 𝑛 = 𝑁 )
19 3 18 syl ⊢ ( 𝜑 → ⦋ 𝑁 / 𝑛 ⦌ 𝑛 = 𝑁 )
20 19 breq2d ⊢ ( 𝜑 → ( 𝑆 < ⦋ 𝑁 / 𝑛 ⦌ 𝑛 ↔ 𝑆 < 𝑁 ) )
21 17 20 bitrd ⊢ ( 𝜑 → ( [ 𝑁 / 𝑛 ] 𝑆 < 𝑛 ↔ 𝑆 < 𝑁 ) )
22 21 ifbid ⊢ ( 𝜑 → if ( [ 𝑁 / 𝑛 ] 𝑆 < 𝑛 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) = if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) )
23 15 22 eqtrid ⊢ ( 𝜑 → ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) = if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) )
24 14 23 ifbieq2d ⊢ ( 𝜑 → if ( [ 𝑁 / 𝑛 ] 𝑛 = 𝑆 , ⦋ 𝑁 / 𝑛 ⦌ 𝐶 , ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) = if ( 𝑁 = 𝑆 , ⦋ 𝑁 / 𝑛 ⦌ 𝐶 , if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) )
25 12 24 eqtrid ⊢ ( 𝜑 → ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) = if ( 𝑁 = 𝑆 , ⦋ 𝑁 / 𝑛 ⦌ 𝐶 , if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) )
26 11 25 ifbieq2d ⊢ ( 𝜑 → if ( [ 𝑁 / 𝑛 ] 𝑛 = 0 , ⦋ 𝑁 / 𝑛 ⦌ 𝐴 , ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) = if ( 𝑁 = 0 , ⦋ 𝑁 / 𝑛 ⦌ 𝐴 , if ( 𝑁 = 𝑆 , ⦋ 𝑁 / 𝑛 ⦌ 𝐶 , if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) ) )
27 9 26 eqtrid ⊢ ( 𝜑 → ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) = if ( 𝑁 = 0 , ⦋ 𝑁 / 𝑛 ⦌ 𝐴 , if ( 𝑁 = 𝑆 , ⦋ 𝑁 / 𝑛 ⦌ 𝐶 , if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) ) )
28 4 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑌 ∈ 𝑉 )
29 5 28 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 ∈ 𝑉 )
30 7 eqcomd ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = 𝑌 )
31 30 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ 𝑁 = 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 = 𝑌 )
32 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ 𝑁 = 𝑆 ) → 𝑌 ∈ 𝑉 )
33 31 32 eqeltrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ 𝑁 = 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐶 ∈ 𝑉 )
34 8 eqcomd ⊢ ( ( 𝜑 ∧ 𝑆 < 𝑁 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = 𝑌 )
35 34 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ 𝑆 < 𝑁 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 = 𝑌 )
36 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ 𝑆 < 𝑁 ) → 𝑌 ∈ 𝑉 )
37 35 36 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ 𝑆 < 𝑁 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐷 ∈ 𝑉 )
38 simplll ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ ¬ 𝑆 < 𝑁 ) → 𝜑 )
39 anass ⊢ ( ( ( ¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆 ) ∧ ¬ 𝑆 < 𝑁 ) ↔ ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) )
40 39 bicomi ⊢ ( ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) ↔ ( ( ¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆 ) ∧ ¬ 𝑆 < 𝑁 ) )
41 40 bianassc ⊢ ( ( 𝜑 ∧ ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) ) ↔ ( ( ( ¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆 ) ∧ 𝜑 ) ∧ ¬ 𝑆 < 𝑁 ) )
42 an32 ⊢ ( ( ( ¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆 ) ∧ 𝜑 ) ↔ ( ( ¬ 𝑁 = 0 ∧ 𝜑 ) ∧ ¬ 𝑁 = 𝑆 ) )
43 ancom ⊢ ( ( ¬ 𝑁 = 0 ∧ 𝜑 ) ↔ ( 𝜑 ∧ ¬ 𝑁 = 0 ) )
44 43 anbi1i ⊢ ( ( ( ¬ 𝑁 = 0 ∧ 𝜑 ) ∧ ¬ 𝑁 = 𝑆 ) ↔ ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) )
45 42 44 bitri ⊢ ( ( ( ¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆 ) ∧ 𝜑 ) ↔ ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) )
46 45 anbi1i ⊢ ( ( ( ( ¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆 ) ∧ 𝜑 ) ∧ ¬ 𝑆 < 𝑁 ) ↔ ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ ¬ 𝑆 < 𝑁 ) )
47 41 46 bitri ⊢ ( ( 𝜑 ∧ ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) ) ↔ ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ ¬ 𝑆 < 𝑁 ) )
48 df-ne ⊢ ( 𝑁 ≠ 0 ↔ ¬ 𝑁 = 0 )
49 elnnne0 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
50 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
51 49 50 sylbir ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) → 0 < 𝑁 )
52 51 expcom ⊢ ( 𝑁 ≠ 0 → ( 𝑁 ∈ ℕ0 → 0 < 𝑁 ) )
53 48 52 sylbir ⊢ ( ¬ 𝑁 = 0 → ( 𝑁 ∈ ℕ0 → 0 < 𝑁 ) )
54 53 adantr ⊢ ( ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) → ( 𝑁 ∈ ℕ0 → 0 < 𝑁 ) )
55 3 54 mpan9 ⊢ ( ( 𝜑 ∧ ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) ) → 0 < 𝑁 )
56 47 55 sylbir ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ ¬ 𝑆 < 𝑁 ) → 0 < 𝑁 )
57 3 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
58 57 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) ) → 𝑁 ∈ ℝ )
59 2 nnred ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
60 59 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) ) → 𝑆 ∈ ℝ )
61 57 59 lenltd ⊢ ( 𝜑 → ( 𝑁 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑁 ) )
62 61 biimprd ⊢ ( 𝜑 → ( ¬ 𝑆 < 𝑁 → 𝑁 ≤ 𝑆 ) )
63 62 adantld ⊢ ( 𝜑 → ( ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) → 𝑁 ≤ 𝑆 ) )
64 63 adantld ⊢ ( 𝜑 → ( ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) → 𝑁 ≤ 𝑆 ) )
65 64 imp ⊢ ( ( 𝜑 ∧ ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) ) → 𝑁 ≤ 𝑆 )
66 nesym ⊢ ( 𝑆 ≠ 𝑁 ↔ ¬ 𝑁 = 𝑆 )
67 66 biranri ⊢ ( ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) → 𝑆 ≠ 𝑁 )
68 67 ad2antll ⊢ ( ( 𝜑 ∧ ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) ) → 𝑆 ≠ 𝑁 )
69 58 60 65 68 leneltd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑁 = 0 ∧ ( ¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁 ) ) ) → 𝑁 < 𝑆 )
70 47 69 sylbir ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ ¬ 𝑆 < 𝑁 ) → 𝑁 < 𝑆 )
71 6 eqcomd ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 = 𝑌 )
72 38 56 70 71 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ ¬ 𝑆 < 𝑁 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 = 𝑌 )
73 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ ¬ 𝑆 < 𝑁 ) → 𝑌 ∈ 𝑉 )
74 72 73 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) ∧ ¬ 𝑆 < 𝑁 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ∈ 𝑉 )
75 37 74 ifclda ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) → if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ∈ 𝑉 )
76 33 75 ifclda ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) → if ( 𝑁 = 𝑆 , ⦋ 𝑁 / 𝑛 ⦌ 𝐶 , if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) ∈ 𝑉 )
77 29 76 ifclda ⊢ ( 𝜑 → if ( 𝑁 = 0 , ⦋ 𝑁 / 𝑛 ⦌ 𝐴 , if ( 𝑁 = 𝑆 , ⦋ 𝑁 / 𝑛 ⦌ 𝐶 , if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) ) ∈ 𝑉 )
78 27 77 eqeltrd ⊢ ( 𝜑 → ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) ∈ 𝑉 )
79 1 fvmpts ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) ∈ 𝑉 ) → ( 𝐺 ‘ 𝑁 ) = ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) )
80 3 78 79 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑁 ) = ⦋ 𝑁 / 𝑛 ⦌ if ( 𝑛 = 0 , 𝐴 , if ( 𝑛 = 𝑆 , 𝐶 , if ( 𝑆 < 𝑛 , 𝐷 , 𝐵 ) ) ) )
81 5 eqcomd ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ⦋ 𝑁 / 𝑛 ⦌ 𝐴 = 𝑌 )
82 35 72 ifeqda ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) ∧ ¬ 𝑁 = 𝑆 ) → if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) = 𝑌 )
83 31 82 ifeqda ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) → if ( 𝑁 = 𝑆 , ⦋ 𝑁 / 𝑛 ⦌ 𝐶 , if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) = 𝑌 )
84 81 83 ifeqda ⊢ ( 𝜑 → if ( 𝑁 = 0 , ⦋ 𝑁 / 𝑛 ⦌ 𝐴 , if ( 𝑁 = 𝑆 , ⦋ 𝑁 / 𝑛 ⦌ 𝐶 , if ( 𝑆 < 𝑁 , ⦋ 𝑁 / 𝑛 ⦌ 𝐷 , ⦋ 𝑁 / 𝑛 ⦌ 𝐵 ) ) ) = 𝑌 )
85 80 27 84 3eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑁 ) = 𝑌 )