Step | Hyp | Ref
| Expression |
1 | | cqp 34632 |
. 2
class
Qp |
2 | | vp |
. . 3
setvar π |
3 | | cprime 16607 |
. . 3
class
β |
4 | | vb |
. . . 4
setvar π |
5 | | vh |
. . . . . . . . . 10
setvar β |
6 | 5 | cv 1540 |
. . . . . . . . 9
class β |
7 | 6 | ccnv 5675 |
. . . . . . . 8
class β‘β |
8 | | cz 12557 |
. . . . . . . . 9
class
β€ |
9 | | cc0 11109 |
. . . . . . . . . 10
class
0 |
10 | 9 | csn 4628 |
. . . . . . . . 9
class
{0} |
11 | 8, 10 | cdif 3945 |
. . . . . . . 8
class (β€
β {0}) |
12 | 7, 11 | cima 5679 |
. . . . . . 7
class (β‘β β (β€ β
{0})) |
13 | | vx |
. . . . . . . 8
setvar π₯ |
14 | 13 | cv 1540 |
. . . . . . 7
class π₯ |
15 | 12, 14 | wss 3948 |
. . . . . 6
wff (β‘β β (β€ β {0})) β π₯ |
16 | | cuz 12821 |
. . . . . . 7
class
β€β₯ |
17 | 16 | crn 5677 |
. . . . . 6
class ran
β€β₯ |
18 | 15, 13, 17 | wrex 3070 |
. . . . 5
wff
βπ₯ β ran
β€β₯(β‘β β (β€ β {0}))
β π₯ |
19 | 2 | cv 1540 |
. . . . . . . 8
class π |
20 | | c1 11110 |
. . . . . . . 8
class
1 |
21 | | cmin 11443 |
. . . . . . . 8
class
β |
22 | 19, 20, 21 | co 7408 |
. . . . . . 7
class (π β 1) |
23 | | cfz 13483 |
. . . . . . 7
class
... |
24 | 9, 22, 23 | co 7408 |
. . . . . 6
class
(0...(π β
1)) |
25 | | cmap 8819 |
. . . . . 6
class
βm |
26 | 8, 24, 25 | co 7408 |
. . . . 5
class (β€
βm (0...(π
β 1))) |
27 | 18, 5, 26 | crab 3432 |
. . . 4
class {β β (β€
βm (0...(π
β 1))) β£ βπ₯ β ran β€β₯(β‘β β (β€ β {0})) β π₯} |
28 | | cnx 17125 |
. . . . . . . . 9
class
ndx |
29 | | cbs 17143 |
. . . . . . . . 9
class
Base |
30 | 28, 29 | cfv 6543 |
. . . . . . . 8
class
(Baseβndx) |
31 | 4 | cv 1540 |
. . . . . . . 8
class π |
32 | 30, 31 | cop 4634 |
. . . . . . 7
class
β¨(Baseβndx), πβ© |
33 | | cplusg 17196 |
. . . . . . . . 9
class
+g |
34 | 28, 33 | cfv 6543 |
. . . . . . . 8
class
(+gβndx) |
35 | | vf |
. . . . . . . . 9
setvar π |
36 | | vg |
. . . . . . . . 9
setvar π |
37 | 35 | cv 1540 |
. . . . . . . . . . 11
class π |
38 | 36 | cv 1540 |
. . . . . . . . . . 11
class π |
39 | | caddc 11112 |
. . . . . . . . . . . 12
class
+ |
40 | 39 | cof 7667 |
. . . . . . . . . . 11
class
βf + |
41 | 37, 38, 40 | co 7408 |
. . . . . . . . . 10
class (π βf + π) |
42 | | crqp 34631 |
. . . . . . . . . . 11
class
/Qp |
43 | 19, 42 | cfv 6543 |
. . . . . . . . . 10
class
(/Qpβπ) |
44 | 41, 43 | cfv 6543 |
. . . . . . . . 9
class
((/Qpβπ)β(π βf + π)) |
45 | 35, 36, 31, 31, 44 | cmpo 7410 |
. . . . . . . 8
class (π β π, π β π β¦ ((/Qpβπ)β(π βf + π))) |
46 | 34, 45 | cop 4634 |
. . . . . . 7
class
β¨(+gβndx), (π β π, π β π β¦ ((/Qpβπ)β(π βf + π)))β© |
47 | | cmulr 17197 |
. . . . . . . . 9
class
.r |
48 | 28, 47 | cfv 6543 |
. . . . . . . 8
class
(.rβndx) |
49 | | vn |
. . . . . . . . . . 11
setvar π |
50 | | vk |
. . . . . . . . . . . . . . 15
setvar π |
51 | 50 | cv 1540 |
. . . . . . . . . . . . . 14
class π |
52 | 51, 37 | cfv 6543 |
. . . . . . . . . . . . 13
class (πβπ) |
53 | 49 | cv 1540 |
. . . . . . . . . . . . . . 15
class π |
54 | 53, 51, 21 | co 7408 |
. . . . . . . . . . . . . 14
class (π β π) |
55 | 54, 38 | cfv 6543 |
. . . . . . . . . . . . 13
class (πβ(π β π)) |
56 | | cmul 11114 |
. . . . . . . . . . . . 13
class
Β· |
57 | 52, 55, 56 | co 7408 |
. . . . . . . . . . . 12
class ((πβπ) Β· (πβ(π β π))) |
58 | 8, 57, 50 | csu 15631 |
. . . . . . . . . . 11
class
Ξ£π β
β€ ((πβπ) Β· (πβ(π β π))) |
59 | 49, 8, 58 | cmpt 5231 |
. . . . . . . . . 10
class (π β β€ β¦
Ξ£π β β€
((πβπ) Β· (πβ(π β π)))) |
60 | 59, 43 | cfv 6543 |
. . . . . . . . 9
class
((/Qpβπ)β(π β β€ β¦ Ξ£π β β€ ((πβπ) Β· (πβ(π β π))))) |
61 | 35, 36, 31, 31, 60 | cmpo 7410 |
. . . . . . . 8
class (π β π, π β π β¦ ((/Qpβπ)β(π β β€ β¦ Ξ£π β β€ ((πβπ) Β· (πβ(π β π)))))) |
62 | 48, 61 | cop 4634 |
. . . . . . 7
class
β¨(.rβndx), (π β π, π β π β¦ ((/Qpβπ)β(π β β€ β¦ Ξ£π β β€ ((πβπ) Β· (πβ(π β π))))))β© |
63 | 32, 46, 62 | ctp 4632 |
. . . . . 6
class
{β¨(Baseβndx), πβ©, β¨(+gβndx),
(π β π, π β π β¦ ((/Qpβπ)β(π βf + π)))β©, β¨(.rβndx),
(π β π, π β π β¦ ((/Qpβπ)β(π β β€ β¦ Ξ£π β β€ ((πβπ) Β· (πβ(π β π))))))β©} |
64 | | cple 17203 |
. . . . . . . . 9
class
le |
65 | 28, 64 | cfv 6543 |
. . . . . . . 8
class
(leβndx) |
66 | 37, 38 | cpr 4630 |
. . . . . . . . . . 11
class {π, π} |
67 | 66, 31 | wss 3948 |
. . . . . . . . . 10
wff {π, π} β π |
68 | 51 | cneg 11444 |
. . . . . . . . . . . . . 14
class -π |
69 | 68, 37 | cfv 6543 |
. . . . . . . . . . . . 13
class (πβ-π) |
70 | 19, 20, 39 | co 7408 |
. . . . . . . . . . . . . 14
class (π + 1) |
71 | | cexp 14026 |
. . . . . . . . . . . . . 14
class
β |
72 | 70, 68, 71 | co 7408 |
. . . . . . . . . . . . 13
class ((π + 1)β-π) |
73 | 69, 72, 56 | co 7408 |
. . . . . . . . . . . 12
class ((πβ-π) Β· ((π + 1)β-π)) |
74 | 8, 73, 50 | csu 15631 |
. . . . . . . . . . 11
class
Ξ£π β
β€ ((πβ-π) Β· ((π + 1)β-π)) |
75 | 68, 38 | cfv 6543 |
. . . . . . . . . . . . 13
class (πβ-π) |
76 | 75, 72, 56 | co 7408 |
. . . . . . . . . . . 12
class ((πβ-π) Β· ((π + 1)β-π)) |
77 | 8, 76, 50 | csu 15631 |
. . . . . . . . . . 11
class
Ξ£π β
β€ ((πβ-π) Β· ((π + 1)β-π)) |
78 | | clt 11247 |
. . . . . . . . . . 11
class
< |
79 | 74, 77, 78 | wbr 5148 |
. . . . . . . . . 10
wff
Ξ£π β
β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) |
80 | 67, 79 | wa 396 |
. . . . . . . . 9
wff ({π, π} β π β§ Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π))) |
81 | 80, 35, 36 | copab 5210 |
. . . . . . . 8
class
{β¨π, πβ© β£ ({π, π} β π β§ Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)))} |
82 | 65, 81 | cop 4634 |
. . . . . . 7
class
β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)))}β© |
83 | 82 | csn 4628 |
. . . . . 6
class
{β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)))}β©} |
84 | 63, 83 | cun 3946 |
. . . . 5
class
({β¨(Baseβndx), πβ©, β¨(+gβndx),
(π β π, π β π β¦ ((/Qpβπ)β(π βf + π)))β©, β¨(.rβndx),
(π β π, π β π β¦ ((/Qpβπ)β(π β β€ β¦ Ξ£π β β€ ((πβπ) Β· (πβ(π β π))))))β©} βͺ {β¨(leβndx),
{β¨π, πβ© β£ ({π, π} β π β§ Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)))}β©}) |
85 | 8, 10 | cxp 5674 |
. . . . . . . 8
class (β€
Γ {0}) |
86 | 37, 85 | wceq 1541 |
. . . . . . 7
wff π = (β€ Γ
{0}) |
87 | 37 | ccnv 5675 |
. . . . . . . . . . 11
class β‘π |
88 | 87, 11 | cima 5679 |
. . . . . . . . . 10
class (β‘π β (β€ β
{0})) |
89 | | cr 11108 |
. . . . . . . . . 10
class
β |
90 | 88, 89, 78 | cinf 9435 |
. . . . . . . . 9
class
inf((β‘π β (β€ β {0})), β,
< ) |
91 | 90 | cneg 11444 |
. . . . . . . 8
class
-inf((β‘π β (β€ β {0})), β,
< ) |
92 | 19, 91, 71 | co 7408 |
. . . . . . 7
class (πβ-inf((β‘π β (β€ β {0})), β,
< )) |
93 | 86, 9, 92 | cif 4528 |
. . . . . 6
class if(π = (β€ Γ {0}), 0,
(πβ-inf((β‘π β (β€ β {0})), β,
< ))) |
94 | 35, 31, 93 | cmpt 5231 |
. . . . 5
class (π β π β¦ if(π = (β€ Γ {0}), 0, (πβ-inf((β‘π β (β€ β {0})), β,
< )))) |
95 | | ctng 24086 |
. . . . 5
class
toNrmGrp |
96 | 84, 94, 95 | co 7408 |
. . . 4
class
(({β¨(Baseβndx), πβ©, β¨(+gβndx),
(π β π, π β π β¦ ((/Qpβπ)β(π βf + π)))β©, β¨(.rβndx),
(π β π, π β π β¦ ((/Qpβπ)β(π β β€ β¦ Ξ£π β β€ ((πβπ) Β· (πβ(π β π))))))β©} βͺ {β¨(leβndx),
{β¨π, πβ© β£ ({π, π} β π β§ Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)))}β©}) toNrmGrp (π β π β¦ if(π = (β€ Γ {0}), 0, (πβ-inf((β‘π β (β€ β {0})), β,
< ))))) |
97 | 4, 27, 96 | csb 3893 |
. . 3
class
β¦{β
β (β€ βm (0...(π β 1))) β£ βπ₯ β ran
β€β₯(β‘β β (β€ β {0}))
β π₯} / πβ¦(({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π β π, π β π β¦ ((/Qpβπ)β(π βf + π)))β©, β¨(.rβndx),
(π β π, π β π β¦ ((/Qpβπ)β(π β β€ β¦ Ξ£π β β€ ((πβπ) Β· (πβ(π β π))))))β©} βͺ {β¨(leβndx),
{β¨π, πβ© β£ ({π, π} β π β§ Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)))}β©}) toNrmGrp (π β π β¦ if(π = (β€ Γ {0}), 0, (πβ-inf((β‘π β (β€ β {0})), β,
< ))))) |
98 | 2, 3, 97 | cmpt 5231 |
. 2
class (π β β β¦
β¦{β β
(β€ βm (0...(π β 1))) β£ βπ₯ β ran
β€β₯(β‘β β (β€ β {0}))
β π₯} / πβ¦(({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π β π, π β π β¦ ((/Qpβπ)β(π βf + π)))β©, β¨(.rβndx),
(π β π, π β π β¦ ((/Qpβπ)β(π β β€ β¦ Ξ£π β β€ ((πβπ) Β· (πβ(π β π))))))β©} βͺ {β¨(leβndx),
{β¨π, πβ© β£ ({π, π} β π β§ Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)))}β©}) toNrmGrp (π β π β¦ if(π = (β€ Γ {0}), 0, (πβ-inf((β‘π β (β€ β {0})), β,
< )))))) |
99 | 1, 98 | wceq 1541 |
1
wff Qp = (π β β β¦
β¦{β β
(β€ βm (0...(π β 1))) β£ βπ₯ β ran
β€β₯(β‘β β (β€ β {0}))
β π₯} / πβ¦(({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π β π, π β π β¦ ((/Qpβπ)β(π βf + π)))β©, β¨(.rβndx),
(π β π, π β π β¦ ((/Qpβπ)β(π β β€ β¦ Ξ£π β β€ ((πβπ) Β· (πβ(π β π))))))β©} βͺ {β¨(leβndx),
{β¨π, πβ© β£ ({π, π} β π β§ Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)) < Ξ£π β β€ ((πβ-π) Β· ((π + 1)β-π)))}β©}) toNrmGrp (π β π β¦ if(π = (β€ Γ {0}), 0, (πβ-inf((β‘π β (β€ β {0})), β,
< )))))) |