Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > bdnthALT | Unicode version |
Description: Alternate proof of bdnth 12959 not using bdfal 12958. Then, bdfal 12958 can be proved from this theorem, using fal 1323. The total number of proof steps would be 17 (for bdnthALT 12960) + 3 = 20, which is more than 8 (for bdfal 12958) + 9 (for bdnth 12959) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
bdnth.1 |
Ref | Expression |
---|---|
bdnthALT | BOUNDED |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bdtru 12957 | . . 3 BOUNDED | |
2 | 1 | ax-bdn 12942 | . 2 BOUNDED |
3 | notnot 603 | . . . 4 | |
4 | 3 | mptru 1325 | . . 3 |
5 | bdnth.1 | . . 3 | |
6 | 4, 5 | 2false 675 | . 2 |
7 | 2, 6 | bd0 12949 | 1 BOUNDED |
Colors of variables: wff set class |
Syntax hints: wn 3 wtru 1317 BOUNDED wbd 12937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 588 ax-in2 589 ax-bd0 12938 ax-bdim 12939 ax-bdn 12942 ax-bdeq 12945 |
This theorem depends on definitions: df-bi 116 df-tru 1319 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |