![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pntibndlem1 | Structured version Visualization version Unicode version |
Description: Lemma for pntibnd 24442. (Contributed by Mario Carneiro, 10-Apr-2016.) |
Ref | Expression |
---|---|
pntibnd.r |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
pntibndlem1.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
pntibndlem1.l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pntibndlem1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pntibndlem1.l |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 4nn 10758 |
. . . . . 6
![]() ![]() ![]() ![]() | |
3 | nnrp 11300 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | rpreccl 11315 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | mp2b 10 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | pntibndlem1.1 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 3nn 10757 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
8 | nnrp 11300 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | ax-mp 5 |
. . . . . 6
![]() ![]() ![]() ![]() |
10 | rpaddcl 11312 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 6, 9, 10 | sylancl 673 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | rpdivcl 11314 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 5, 11, 12 | sylancr 674 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 1, 13 | syl5eqel 2533 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 14 | rpred 11330 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 14 | rpgt0d 11333 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | rpcn 11299 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | 5, 17 | ax-mp 5 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 18 | div1i 10323 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | rpre 11297 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
21 | 5, 20 | mp1i 13 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | 3re 10671 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
23 | 22 | a1i 11 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | 11 | rpred 11330 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | 1lt4 10770 |
. . . . . . . . 9
![]() ![]() ![]() ![]() | |
26 | 4re 10674 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() | |
27 | 4pos 10693 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() | |
28 | recgt1 10490 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
29 | 26, 27, 28 | mp2an 683 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
30 | 25, 29 | mpbi 213 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 1lt3 10767 |
. . . . . . . 8
![]() ![]() ![]() ![]() | |
32 | 5, 20 | ax-mp 5 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 1re 9628 |
. . . . . . . . 9
![]() ![]() ![]() ![]() | |
34 | 32, 33, 22 | lttri 9746 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
35 | 30, 31, 34 | mp2an 683 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 35 | a1i 11 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | ltaddrp 11325 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
38 | 22, 6, 37 | sylancr 674 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
39 | 3cn 10672 |
. . . . . . . 8
![]() ![]() ![]() ![]() | |
40 | 6 | rpcnd 11332 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | addcom 9805 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
42 | 39, 40, 41 | sylancr 674 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
43 | 38, 42 | breqtrd 4398 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
44 | 21, 23, 24, 36, 43 | lttrd 9782 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
45 | 19, 44 | syl5eqbr 4407 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
46 | 33 | a1i 11 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
47 | 0lt1 10124 |
. . . . . 6
![]() ![]() ![]() ![]() | |
48 | 47 | a1i 11 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
49 | 11 | rpregt0d 11336 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
50 | ltdiv23 10485 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
51 | 21, 46, 48, 49, 50 | syl121anc 1276 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
52 | 45, 51 | mpbid 215 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
53 | 1, 52 | syl5eqbr 4407 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
54 | 0xr 9673 |
. . 3
![]() ![]() ![]() ![]() | |
55 | 33 | rexri 9679 |
. . 3
![]() ![]() ![]() ![]() |
56 | elioo2 11666 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
57 | 54, 55, 56 | mp2an 683 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
58 | 15, 16, 53, 57 | syl3anbrc 1193 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1672 ax-4 1685 ax-5 1761 ax-6 1808 ax-7 1854 ax-8 1892 ax-9 1899 ax-10 1918 ax-11 1923 ax-12 1936 ax-13 2091 ax-ext 2431 ax-sep 4496 ax-nul 4505 ax-pow 4553 ax-pr 4611 ax-un 6570 ax-cnex 9581 ax-resscn 9582 ax-1cn 9583 ax-icn 9584 ax-addcl 9585 ax-addrcl 9586 ax-mulcl 9587 ax-mulrcl 9588 ax-mulcom 9589 ax-addass 9590 ax-mulass 9591 ax-distr 9592 ax-i2m1 9593 ax-1ne0 9594 ax-1rid 9595 ax-rnegex 9596 ax-rrecex 9597 ax-cnre 9598 ax-pre-lttri 9599 ax-pre-lttrn 9600 ax-pre-ltadd 9601 ax-pre-mulgt0 9602 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 987 df-3an 988 df-tru 1450 df-ex 1667 df-nf 1671 df-sb 1801 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3014 df-sbc 3235 df-csb 3331 df-dif 3374 df-un 3376 df-in 3378 df-ss 3385 df-pss 3387 df-nul 3699 df-if 3849 df-pw 3920 df-sn 3936 df-pr 3938 df-tp 3940 df-op 3942 df-uni 4168 df-iun 4249 df-br 4374 df-opab 4433 df-mpt 4434 df-tr 4469 df-eprel 4722 df-id 4726 df-po 4732 df-so 4733 df-fr 4770 df-we 4772 df-xp 4817 df-rel 4818 df-cnv 4819 df-co 4820 df-dm 4821 df-rn 4822 df-res 4823 df-ima 4824 df-pred 5358 df-ord 5404 df-on 5405 df-lim 5406 df-suc 5407 df-iota 5524 df-fun 5562 df-fn 5563 df-f 5564 df-f1 5565 df-fo 5566 df-f1o 5567 df-fv 5568 df-riota 6237 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-om 6680 df-1st 6780 df-2nd 6781 df-wrecs 7014 df-recs 7076 df-rdg 7114 df-er 7349 df-en 7556 df-dom 7557 df-sdom 7558 df-pnf 9663 df-mnf 9664 df-xr 9665 df-ltxr 9666 df-le 9667 df-sub 9848 df-neg 9849 df-div 10258 df-nn 10598 df-2 10656 df-3 10657 df-4 10658 df-rp 11292 df-ioo 11628 |
This theorem is referenced by: pntibndlem2a 24439 pntibndlem2 24440 pntibnd 24442 |
Copyright terms: Public domain | W3C validator |