Step | Hyp | Ref
| Expression |
1 | | wph |
. 2
wff π |
2 | | cc0 7811 |
. . . . . 6
class
0 |
3 | | vx |
. . . . . . 7
setvar π₯ |
4 | 3 | cv 1352 |
. . . . . 6
class π₯ |
5 | | cltrr 7815 |
. . . . . 6
class
<β |
6 | 2, 4, 5 | wbr 4004 |
. . . . 5
wff 0
<β π₯ |
7 | | vj |
. . . . . . . . . 10
setvar π |
8 | 7 | cv 1352 |
. . . . . . . . 9
class π |
9 | | vk |
. . . . . . . . . 10
setvar π |
10 | 9 | cv 1352 |
. . . . . . . . 9
class π |
11 | 8, 10, 5 | wbr 4004 |
. . . . . . . 8
wff π <β π |
12 | | cF |
. . . . . . . . . . 11
class πΉ |
13 | 10, 12 | cfv 5217 |
. . . . . . . . . 10
class (πΉβπ) |
14 | | vy |
. . . . . . . . . . . 12
setvar π¦ |
15 | 14 | cv 1352 |
. . . . . . . . . . 11
class π¦ |
16 | | caddc 7814 |
. . . . . . . . . . 11
class
+ |
17 | 15, 4, 16 | co 5875 |
. . . . . . . . . 10
class (π¦ + π₯) |
18 | 13, 17, 5 | wbr 4004 |
. . . . . . . . 9
wff (πΉβπ) <β (π¦ + π₯) |
19 | 13, 4, 16 | co 5875 |
. . . . . . . . . 10
class ((πΉβπ) + π₯) |
20 | 15, 19, 5 | wbr 4004 |
. . . . . . . . 9
wff π¦ <β ((πΉβπ) + π₯) |
21 | 18, 20 | wa 104 |
. . . . . . . 8
wff ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯)) |
22 | 11, 21 | wi 4 |
. . . . . . 7
wff (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯))) |
23 | | cN |
. . . . . . 7
class π |
24 | 22, 9, 23 | wral 2455 |
. . . . . 6
wff
βπ β
π (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯))) |
25 | 24, 7, 23 | wrex 2456 |
. . . . 5
wff
βπ β
π βπ β π (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯))) |
26 | 6, 25 | wi 4 |
. . . 4
wff (0
<β π₯
β βπ β
π βπ β π (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯)))) |
27 | | cr 7810 |
. . . 4
class
β |
28 | 26, 3, 27 | wral 2455 |
. . 3
wff
βπ₯ β
β (0 <β π₯ β βπ β π βπ β π (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯)))) |
29 | 28, 14, 27 | wrex 2456 |
. 2
wff
βπ¦ β
β βπ₯ β
β (0 <β π₯ β βπ β π βπ β π (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯)))) |
30 | 1, 29 | wi 4 |
1
wff (π β βπ¦ β β βπ₯ β β (0 <β
π₯ β βπ β π βπ β π (π <β π β ((πΉβπ) <β (π¦ + π₯) β§ π¦ <β ((πΉβπ) + π₯))))) |