Proof of Theorem fvmptnn04if
| Step | Hyp | Ref
| Expression |
| 1 | | fvmptnn04if.n |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 2 | | csbif 4583 |
. . . . 5
⊢
⦋𝑁 /
𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) = if([𝑁 / 𝑛]𝑛 = 0, ⦋𝑁 / 𝑛⦌𝐴, ⦋𝑁 / 𝑛⦌if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) |
| 3 | | eqsbc1 3835 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ([𝑁 / 𝑛]𝑛 = 0 ↔ 𝑁 = 0)) |
| 4 | 1, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → ([𝑁 / 𝑛]𝑛 = 0 ↔ 𝑁 = 0)) |
| 5 | | csbif 4583 |
. . . . . . 7
⊢
⦋𝑁 /
𝑛⦌if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)) = if([𝑁 / 𝑛]𝑛 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, ⦋𝑁 / 𝑛⦌if(𝑆 < 𝑛, 𝐷, 𝐵)) |
| 6 | | eqsbc1 3835 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ([𝑁 / 𝑛]𝑛 = 𝑆 ↔ 𝑁 = 𝑆)) |
| 7 | 1, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ([𝑁 / 𝑛]𝑛 = 𝑆 ↔ 𝑁 = 𝑆)) |
| 8 | | csbif 4583 |
. . . . . . . . 9
⊢
⦋𝑁 /
𝑛⦌if(𝑆 < 𝑛, 𝐷, 𝐵) = if([𝑁 / 𝑛]𝑆 < 𝑛, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵) |
| 9 | | sbcbr2g 5201 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ ([𝑁 / 𝑛]𝑆 < 𝑛 ↔ 𝑆 < ⦋𝑁 / 𝑛⦌𝑛)) |
| 10 | 1, 9 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ([𝑁 / 𝑛]𝑆 < 𝑛 ↔ 𝑆 < ⦋𝑁 / 𝑛⦌𝑛)) |
| 11 | | csbvarg 4434 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ ⦋𝑁 /
𝑛⦌𝑛 = 𝑁) |
| 12 | 1, 11 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ⦋𝑁 / 𝑛⦌𝑛 = 𝑁) |
| 13 | 12 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 < ⦋𝑁 / 𝑛⦌𝑛 ↔ 𝑆 < 𝑁)) |
| 14 | 10, 13 | bitrd 279 |
. . . . . . . . . 10
⊢ (𝜑 → ([𝑁 / 𝑛]𝑆 < 𝑛 ↔ 𝑆 < 𝑁)) |
| 15 | 14 | ifbid 4549 |
. . . . . . . . 9
⊢ (𝜑 → if([𝑁 / 𝑛]𝑆 < 𝑛, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵) = if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)) |
| 16 | 8, 15 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝜑 → ⦋𝑁 / 𝑛⦌if(𝑆 < 𝑛, 𝐷, 𝐵) = if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)) |
| 17 | 7, 16 | ifbieq2d 4552 |
. . . . . . 7
⊢ (𝜑 → if([𝑁 / 𝑛]𝑛 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, ⦋𝑁 / 𝑛⦌if(𝑆 < 𝑛, 𝐷, 𝐵)) = if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵))) |
| 18 | 5, 17 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → ⦋𝑁 / 𝑛⦌if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)) = if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵))) |
| 19 | 4, 18 | ifbieq2d 4552 |
. . . . 5
⊢ (𝜑 → if([𝑁 / 𝑛]𝑛 = 0, ⦋𝑁 / 𝑛⦌𝐴, ⦋𝑁 / 𝑛⦌if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) = if(𝑁 = 0, ⦋𝑁 / 𝑛⦌𝐴, if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)))) |
| 20 | 2, 19 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → ⦋𝑁 / 𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) = if(𝑁 = 0, ⦋𝑁 / 𝑛⦌𝐴, if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)))) |
| 21 | | fvmptnn04if.a |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 = 0) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐴) |
| 22 | | fvmptnn04if.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 = 0) → 𝑌 ∈ 𝑉) |
| 24 | 21, 23 | eqeltrrd 2842 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 = 0) → ⦋𝑁 / 𝑛⦌𝐴 ∈ 𝑉) |
| 25 | | fvmptnn04if.c |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 = 𝑆) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐶) |
| 26 | 25 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 = 𝑆) → ⦋𝑁 / 𝑛⦌𝐶 = 𝑌) |
| 27 | 26 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ 𝑁 = 𝑆) → ⦋𝑁 / 𝑛⦌𝐶 = 𝑌) |
| 28 | 22 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ 𝑁 = 𝑆) → 𝑌 ∈ 𝑉) |
| 29 | 27, 28 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ 𝑁 = 𝑆) → ⦋𝑁 / 𝑛⦌𝐶 ∈ 𝑉) |
| 30 | | fvmptnn04if.d |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < 𝑁) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐷) |
| 31 | 30 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐷 = 𝑌) |
| 32 | 31 | ad4ant14 752 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐷 = 𝑌) |
| 33 | 22 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ 𝑆 < 𝑁) → 𝑌 ∈ 𝑉) |
| 34 | 32, 33 | eqeltrd 2841 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐷 ∈ 𝑉) |
| 35 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → 𝜑) |
| 36 | | anass 468 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) ↔ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) |
| 37 | 36 | bicomi 224 |
. . . . . . . . . . . 12
⊢ ((¬
𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁)) ↔ ((¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁)) |
| 38 | 37 | bianassc 643 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) ↔ (((¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ 𝜑) ∧ ¬ 𝑆 < 𝑁)) |
| 39 | | an32 646 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ 𝜑) ↔ ((¬ 𝑁 = 0 ∧ 𝜑) ∧ ¬ 𝑁 = 𝑆)) |
| 40 | | ancom 460 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑁 = 0 ∧ 𝜑) ↔ (𝜑 ∧ ¬ 𝑁 = 0)) |
| 41 | 40 | anbi1i 624 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑁 = 0 ∧ 𝜑) ∧ ¬ 𝑁 = 𝑆) ↔ ((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆)) |
| 42 | 39, 41 | bitri 275 |
. . . . . . . . . . . 12
⊢ (((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ 𝜑) ↔ ((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆)) |
| 43 | 42 | anbi1i 624 |
. . . . . . . . . . 11
⊢ ((((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ 𝜑) ∧ ¬ 𝑆 < 𝑁) ↔ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁)) |
| 44 | 38, 43 | bitri 275 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) ↔ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁)) |
| 45 | | df-ne 2941 |
. . . . . . . . . . . . 13
⊢ (𝑁 ≠ 0 ↔ ¬ 𝑁 = 0) |
| 46 | | elnnne0 12540 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0
∧ 𝑁 ≠
0)) |
| 47 | | nngt0 12297 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
| 48 | 46, 47 | sylbir 235 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑁 ≠ 0) → 0
< 𝑁) |
| 49 | 48 | expcom 413 |
. . . . . . . . . . . . 13
⊢ (𝑁 ≠ 0 → (𝑁 ∈ ℕ0
→ 0 < 𝑁)) |
| 50 | 45, 49 | sylbir 235 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 = 0 → (𝑁 ∈ ℕ0
→ 0 < 𝑁)) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . 11
⊢ ((¬
𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁)) → (𝑁 ∈ ℕ0 → 0 <
𝑁)) |
| 52 | 1, 51 | mpan9 506 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 0 < 𝑁) |
| 53 | 44, 52 | sylbir 235 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → 0 < 𝑁) |
| 54 | 1 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 55 | 54 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 𝑁 ∈ ℝ) |
| 56 | | fvmptnn04if.s |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ ℕ) |
| 57 | 56 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ ℝ) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 𝑆 ∈ ℝ) |
| 59 | 54, 57 | lenltd 11407 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑁)) |
| 60 | 59 | biimprd 248 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (¬ 𝑆 < 𝑁 → 𝑁 ≤ 𝑆)) |
| 61 | 60 | adantld 490 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁) → 𝑁 ≤ 𝑆)) |
| 62 | 61 | adantld 490 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁)) → 𝑁 ≤ 𝑆)) |
| 63 | 62 | imp 406 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 𝑁 ≤ 𝑆) |
| 64 | | nesym 2997 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ≠ 𝑁 ↔ ¬ 𝑁 = 𝑆) |
| 65 | 64 | biimpri 228 |
. . . . . . . . . . . . 13
⊢ (¬
𝑁 = 𝑆 → 𝑆 ≠ 𝑁) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((¬
𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁) → 𝑆 ≠ 𝑁) |
| 67 | 66 | ad2antll 729 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 𝑆 ≠ 𝑁) |
| 68 | 55, 58, 63, 67 | leneltd 11415 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 𝑁 < 𝑆) |
| 69 | 44, 68 | sylbir 235 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → 𝑁 < 𝑆) |
| 70 | | fvmptnn04if.b |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐵) |
| 71 | 70 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆) → ⦋𝑁 / 𝑛⦌𝐵 = 𝑌) |
| 72 | 35, 53, 69, 71 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐵 = 𝑌) |
| 73 | 22 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → 𝑌 ∈ 𝑉) |
| 74 | 72, 73 | eqeltrd 2841 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) |
| 75 | 34, 74 | ifclda 4561 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) → if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵) ∈ 𝑉) |
| 76 | 29, 75 | ifclda 4561 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 = 0) → if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)) ∈ 𝑉) |
| 77 | 24, 76 | ifclda 4561 |
. . . 4
⊢ (𝜑 → if(𝑁 = 0, ⦋𝑁 / 𝑛⦌𝐴, if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵))) ∈ 𝑉) |
| 78 | 20, 77 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → ⦋𝑁 / 𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) ∈ 𝑉) |
| 79 | | fvmptnn04if.g |
. . . 4
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) |
| 80 | 79 | fvmpts 7019 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ⦋𝑁 /
𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) |
| 81 | 1, 78, 80 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) |
| 82 | 21 | eqcomd 2743 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = 0) → ⦋𝑁 / 𝑛⦌𝐴 = 𝑌) |
| 83 | 32, 72 | ifeqda 4562 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) → if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵) = 𝑌) |
| 84 | 27, 83 | ifeqda 4562 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 = 0) → if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)) = 𝑌) |
| 85 | 82, 84 | ifeqda 4562 |
. 2
⊢ (𝜑 → if(𝑁 = 0, ⦋𝑁 / 𝑛⦌𝐴, if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵))) = 𝑌) |
| 86 | 81, 20, 85 | 3eqtrd 2781 |
1
⊢ (𝜑 → (𝐺‘𝑁) = 𝑌) |