Proof of Theorem fvmptnn04if
Step | Hyp | Ref
| Expression |
1 | | fvmptnn04if.n |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | | csbif 4088 |
. . . . 5
⊢
⦋𝑁 /
𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) = if([𝑁 / 𝑛]𝑛 = 0, ⦋𝑁 / 𝑛⦌𝐴, ⦋𝑁 / 𝑛⦌if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) |
3 | | eqsbc3 3442 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ([𝑁 / 𝑛]𝑛 = 0 ↔ 𝑁 = 0)) |
4 | 1, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → ([𝑁 / 𝑛]𝑛 = 0 ↔ 𝑁 = 0)) |
5 | | csbif 4088 |
. . . . . . 7
⊢
⦋𝑁 /
𝑛⦌if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)) = if([𝑁 / 𝑛]𝑛 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, ⦋𝑁 / 𝑛⦌if(𝑆 < 𝑛, 𝐷, 𝐵)) |
6 | | eqsbc3 3442 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ([𝑁 / 𝑛]𝑛 = 𝑆 ↔ 𝑁 = 𝑆)) |
7 | 1, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ([𝑁 / 𝑛]𝑛 = 𝑆 ↔ 𝑁 = 𝑆)) |
8 | | csbif 4088 |
. . . . . . . . 9
⊢
⦋𝑁 /
𝑛⦌if(𝑆 < 𝑛, 𝐷, 𝐵) = if([𝑁 / 𝑛]𝑆 < 𝑛, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵) |
9 | | sbcbr2g 4640 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ ([𝑁 / 𝑛]𝑆 < 𝑛 ↔ 𝑆 < ⦋𝑁 / 𝑛⦌𝑛)) |
10 | 1, 9 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ([𝑁 / 𝑛]𝑆 < 𝑛 ↔ 𝑆 < ⦋𝑁 / 𝑛⦌𝑛)) |
11 | | csbvarg 3955 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ ⦋𝑁 /
𝑛⦌𝑛 = 𝑁) |
12 | 1, 11 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ⦋𝑁 / 𝑛⦌𝑛 = 𝑁) |
13 | 12 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 < ⦋𝑁 / 𝑛⦌𝑛 ↔ 𝑆 < 𝑁)) |
14 | 10, 13 | bitrd 267 |
. . . . . . . . . 10
⊢ (𝜑 → ([𝑁 / 𝑛]𝑆 < 𝑛 ↔ 𝑆 < 𝑁)) |
15 | 14 | ifbid 4058 |
. . . . . . . . 9
⊢ (𝜑 → if([𝑁 / 𝑛]𝑆 < 𝑛, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵) = if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)) |
16 | 8, 15 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝜑 → ⦋𝑁 / 𝑛⦌if(𝑆 < 𝑛, 𝐷, 𝐵) = if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)) |
17 | 7, 16 | ifbieq2d 4061 |
. . . . . . 7
⊢ (𝜑 → if([𝑁 / 𝑛]𝑛 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, ⦋𝑁 / 𝑛⦌if(𝑆 < 𝑛, 𝐷, 𝐵)) = if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵))) |
18 | 5, 17 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → ⦋𝑁 / 𝑛⦌if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)) = if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵))) |
19 | 4, 18 | ifbieq2d 4061 |
. . . . 5
⊢ (𝜑 → if([𝑁 / 𝑛]𝑛 = 0, ⦋𝑁 / 𝑛⦌𝐴, ⦋𝑁 / 𝑛⦌if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) = if(𝑁 = 0, ⦋𝑁 / 𝑛⦌𝐴, if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)))) |
20 | 2, 19 | syl5eq 2656 |
. . . 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 2689 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 = 0) → ⦋𝑁 / 𝑛⦌𝐴 ∈ 𝑉) |
25 | | fvmptnn04if.c |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 = 𝑆) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐶) |
26 | 25 | eqcomd 2616 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 = 𝑆) → ⦋𝑁 / 𝑛⦌𝐶 = 𝑌) |
27 | 26 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ 𝑁 = 𝑆) → ⦋𝑁 / 𝑛⦌𝐶 = 𝑌) |
28 | 22 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ 𝑁 = 𝑆) → 𝑌 ∈ 𝑉) |
29 | 27, 28 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ 𝑁 = 𝑆) → ⦋𝑁 / 𝑛⦌𝐶 ∈ 𝑉) |
30 | | fvmptnn04if.d |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < 𝑁) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐷) |
31 | 30 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐷 = 𝑌) |
32 | 31 | ex 449 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 < 𝑁 → ⦋𝑁 / 𝑛⦌𝐷 = 𝑌)) |
33 | 32 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) → (𝑆 < 𝑁 → ⦋𝑁 / 𝑛⦌𝐷 = 𝑌)) |
34 | 33 | imp 444 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐷 = 𝑌) |
35 | 22 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ 𝑆 < 𝑁) → 𝑌 ∈ 𝑉) |
36 | 34, 35 | eqeltrd 2688 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐷 ∈ 𝑉) |
37 | | simplll 794 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → 𝜑) |
38 | | ancom 465 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑆 < 𝑁 ∧ 𝜑) ↔ (𝜑 ∧ ¬ 𝑆 < 𝑁)) |
39 | 38 | anbi2i 726 |
. . . . . . . . . . . 12
⊢ (((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ (¬ 𝑆 < 𝑁 ∧ 𝜑)) ↔ ((¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ (𝜑 ∧ ¬ 𝑆 < 𝑁))) |
40 | | ancom 465 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) ↔ ((¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁)) ∧ 𝜑)) |
41 | | anass 679 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) ↔ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) |
42 | 41 | bicomi 213 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁)) ↔ ((¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁)) |
43 | 42 | anbi1i 727 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁)) ∧ 𝜑) ↔ (((¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) ∧ 𝜑)) |
44 | | anass 679 |
. . . . . . . . . . . . 13
⊢ ((((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) ∧ 𝜑) ↔ ((¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ (¬ 𝑆 < 𝑁 ∧ 𝜑))) |
45 | 40, 43, 44 | 3bitri 285 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) ↔ ((¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ (¬ 𝑆 < 𝑁 ∧ 𝜑))) |
46 | | anass 679 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ 𝜑) ∧ ¬ 𝑆 < 𝑁) ↔ ((¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ (𝜑 ∧ ¬ 𝑆 < 𝑁))) |
47 | 39, 45, 46 | 3bitr4i 291 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) ↔ (((¬ 𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ 𝜑) ∧ ¬ 𝑆 < 𝑁)) |
48 | | an32 835 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ 𝜑) ↔ ((¬ 𝑁 = 0 ∧ 𝜑) ∧ ¬ 𝑁 = 𝑆)) |
49 | | ancom 465 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑁 = 0 ∧ 𝜑) ↔ (𝜑 ∧ ¬ 𝑁 = 0)) |
50 | 49 | anbi1i 727 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑁 = 0 ∧ 𝜑) ∧ ¬ 𝑁 = 𝑆) ↔ ((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆)) |
51 | 48, 50 | bitri 263 |
. . . . . . . . . . . 12
⊢ (((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ 𝜑) ↔ ((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆)) |
52 | 51 | anbi1i 727 |
. . . . . . . . . . 11
⊢ ((((¬
𝑁 = 0 ∧ ¬ 𝑁 = 𝑆) ∧ 𝜑) ∧ ¬ 𝑆 < 𝑁) ↔ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁)) |
53 | 47, 52 | bitri 263 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) ↔ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁)) |
54 | | df-ne 2782 |
. . . . . . . . . . . . 13
⊢ (𝑁 ≠ 0 ↔ ¬ 𝑁 = 0) |
55 | | elnnne0 11183 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0
∧ 𝑁 ≠
0)) |
56 | | nngt0 10926 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
57 | 55, 56 | sylbir 224 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑁 ≠ 0) → 0
< 𝑁) |
58 | 57 | expcom 450 |
. . . . . . . . . . . . 13
⊢ (𝑁 ≠ 0 → (𝑁 ∈ ℕ0
→ 0 < 𝑁)) |
59 | 54, 58 | sylbir 224 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 = 0 → (𝑁 ∈ ℕ0
→ 0 < 𝑁)) |
60 | 59 | adantr 480 |
. . . . . . . . . . 11
⊢ ((¬
𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁)) → (𝑁 ∈ ℕ0 → 0 <
𝑁)) |
61 | 1, 60 | mpan9 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 0 < 𝑁) |
62 | 53, 61 | sylbir 224 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → 0 < 𝑁) |
63 | 1 | nn0red 11229 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℝ) |
64 | | fvmptnn04if.s |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 ∈ ℕ) |
65 | 64 | nnred 10912 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑆 ∈ ℝ) |
66 | 63, 65 | lenltd 10062 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑁)) |
67 | 66 | biimprd 237 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (¬ 𝑆 < 𝑁 → 𝑁 ≤ 𝑆)) |
68 | 67 | adantld 482 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁) → 𝑁 ≤ 𝑆)) |
69 | 68 | adantld 482 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁)) → 𝑁 ≤ 𝑆)) |
70 | 69 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 𝑁 ≤ 𝑆) |
71 | | nesym 2838 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ≠ 𝑁 ↔ ¬ 𝑁 = 𝑆) |
72 | 71 | biimpri 217 |
. . . . . . . . . . . . 13
⊢ (¬
𝑁 = 𝑆 → 𝑆 ≠ 𝑁) |
73 | 72 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((¬
𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁) → 𝑆 ≠ 𝑁) |
74 | 73 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 𝑆 ≠ 𝑁) |
75 | 63 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 𝑁 ∈ ℝ) |
76 | 65 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 𝑆 ∈ ℝ) |
77 | 75, 76 | ltlend 10061 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → (𝑁 < 𝑆 ↔ (𝑁 ≤ 𝑆 ∧ 𝑆 ≠ 𝑁))) |
78 | 70, 74, 77 | mpbir2and 959 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (¬ 𝑁 = 0 ∧ (¬ 𝑁 = 𝑆 ∧ ¬ 𝑆 < 𝑁))) → 𝑁 < 𝑆) |
79 | 53, 78 | sylbir 224 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → 𝑁 < 𝑆) |
80 | | fvmptnn04if.b |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐵) |
81 | 80 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆) → ⦋𝑁 / 𝑛⦌𝐵 = 𝑌) |
82 | 37, 62, 79, 81 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐵 = 𝑌) |
83 | 22 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → 𝑌 ∈ 𝑉) |
84 | 82, 83 | eqeltrd 2688 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) ∧ ¬ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) |
85 | 36, 84 | ifclda 4070 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) → if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵) ∈ 𝑉) |
86 | 29, 85 | ifclda 4070 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 = 0) → if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)) ∈ 𝑉) |
87 | 24, 86 | ifclda 4070 |
. . . 4
⊢ (𝜑 → if(𝑁 = 0, ⦋𝑁 / 𝑛⦌𝐴, if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵))) ∈ 𝑉) |
88 | 20, 87 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → ⦋𝑁 / 𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) ∈ 𝑉) |
89 | | fvmptnn04if.g |
. . . 4
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) |
90 | 89 | fvmpts 6194 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ⦋𝑁 /
𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵))) ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) |
91 | 1, 88, 90 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) |
92 | 21 | eqcomd 2616 |
. . 3
⊢ ((𝜑 ∧ 𝑁 = 0) → ⦋𝑁 / 𝑛⦌𝐴 = 𝑌) |
93 | 34, 82 | ifeqda 4071 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 = 0) ∧ ¬ 𝑁 = 𝑆) → if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵) = 𝑌) |
94 | 27, 93 | ifeqda 4071 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 = 0) → if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵)) = 𝑌) |
95 | 92, 94 | ifeqda 4071 |
. 2
⊢ (𝜑 → if(𝑁 = 0, ⦋𝑁 / 𝑛⦌𝐴, if(𝑁 = 𝑆, ⦋𝑁 / 𝑛⦌𝐶, if(𝑆 < 𝑁, ⦋𝑁 / 𝑛⦌𝐷, ⦋𝑁 / 𝑛⦌𝐵))) = 𝑌) |
96 | 91, 20, 95 | 3eqtrd 2648 |
1
⊢ (𝜑 → (𝐺‘𝑁) = 𝑌) |