Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > prmgaplem6 | Structured version Visualization version Unicode version | ||
| Description: Lemma for prmgap 15022: for each positive integer there is a greater prime closest to this integer, i.e. there is a greater prime and no other prime is between this prime and the integer. (Contributed by AV, 10-Aug-2020.) |
| Ref | Expression |
|---|---|
| prmgaplem6 |
          ![/\](wedge.gif "/\"){kind=small}
     ..^  |
,,
are mutually distinct and distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prmunb 14851 |
. 2
| |
| 2 | eqid 2450 |
. . . . 5
   
| |
| 3 | 2 | prmgaplem4 15017 |
. . . 4
|
| 4 | breq2 4405 |
. . . . . . . . 9
| |
| 5 | breq1 4404 |
. . . . . . . . 9
| |
| 6 | 4, 5 | anbi12d 716 |
. . . . . . . 8
|
| 7 | 6 | elrab 3195 |
. . . . . . 7
|
| 8 | simplrl 769 |
. . . . . . . . . 10
| |
| 9 | simprrl 773 |
. . . . . . . . . . 11
| |
| 10 | 9 | adantr 467 |
. . . . . . . . . 10
|
| 11 | simpll 759 |
. . . . . . . . . . . . . . . . . 18
..^
| |
| 12 | elfzo2 11920 |
. . . . . . . . . . . . . . . . . . . 20
..^    | |
| 13 | eluz2 11162 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 14 | nnz 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
| |
| 15 | prmz 14619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
| |
| 16 | zltp1le 10983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
| |
| 17 | 14, 15, 16 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 18 | 17 | exbiri 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 19 | 18 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 20 | 19 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 21 | 20 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 22 | 21 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 23 | 22 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 24 | 23 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 25 | 24 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 26 | prmnn 14618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
| |
| 27 | 26 | nnred 10621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 |
| 28 | 27 | ad2antrl 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
| 29 | prmnn 14618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
| |
| 30 | 29 | nnred 10621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
| 31 | 30 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
| 32 | 31 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
| 33 | prmnn 14618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
| |
| 34 | 33 | nnred 10621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
| 35 | 34 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
| 36 | ltleletr 9723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
| |
| 37 | 28, 32, 35, 36 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
| 38 | 37 | exp4b 611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 39 | 38 | 3ad2ant2 1029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 40 | 39 | expdcom 441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 41 | 40 | com45 92 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 42 | 41 | com14 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 43 | 42 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 44 | 43 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 45 | 44 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 46 | 45 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 47 | 46 | adantld 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 48 | 47 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 49 | 25, 48 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 50 | 49 | exp41 614 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 51 | 50 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 52 | 13, 51 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 53 | 52 | 3imp 1201 |
. . . . . . . . . . . . . . . . . . . 20
|
| 54 | 12, 53 | sylbi 199 |
. . . . . . . . . . . . . . . . . . 19
..^
|
| 55 | 54 | impcom 432 |
. . . . . . . . . . . . . . . . . 18
..^
|
| 56 | breq2 4405 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 57 | breq1 4404 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 58 | 56, 57 | anbi12d 716 |
. . . . . . . . . . . . . . . . . . 19
|
| 59 | 58 | elrab 3195 |
. . . . . . . . . . . . . . . . . 18
|
| 60 | 11, 55, 59 | sylanbrc 669 |
. . . . . . . . . . . . . . . . 17
..^
|
| 61 | elfzolt2 11926 |
. . . . . . . . . . . . . . . . . 18
..^
| |
| 62 | 30 | ad2antrl 733 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 63 | ltnle 9710 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 64 | 63 | biimpd 211 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 65 | 27, 62, 64 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . 20
|
| 66 | 65 | imp 431 |
. . . . . . . . . . . . . . . . . . 19
|
| 67 | 66 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . 18
|
| 68 | 61, 67 | sylan2 477 |
. . . . . . . . . . . . . . . . 17
..^
|
| 69 | 60, 68 | embantd 56 |
. . . . . . . . . . . . . . . 16
..^
|
| 70 | 69 | ex 436 |
. . . . . . . . . . . . . . 15
..^
|
| 71 | 70 | com23 81 |
. . . . . . . . . . . . . 14
..^
|
| 72 | 71 | ex 436 |
. . . . . . . . . . . . 13
..^
|
| 73 | df-nel 2624 |
. . . . . . . . . . . . . 14
| |
| 74 | ax-1 6 |
. . . . . . . . . . . . . . . 16
..^
| |
| 75 | 74 | a1d 26 |
. . . . . . . . . . . . . . 15
..^
|
| 76 | 75 | a1d 26 |
. . . . . . . . . . . . . 14
..^
|
| 77 | 73, 76 | sylbir 217 |
. . . . . . . . . . . . 13
..^
|
| 78 | 72, 77 | pm2.61i 168 |
. . . . . . . . . . . 12
..^
|
| 79 | 78 | ralimdv2 2794 |
. . . . . . . . . . 11
..^ |
| 80 | 79 | imp 431 |
. . . . . . . . . 10
..^ |
| 81 | 8, 10, 80 | jca32 538 |
. . . . . . . . 9
..^ |
| 82 | 81 | ex 436 |
. . . . . . . 8
..^ |
| 83 | 82 | ex 436 |
. . . . . . 7
..^ |
| 84 | 7, 83 | syl5bi 221 |
. . . . . 6
..^ |
| 85 | 84 | impd 433 |
. . . . 5
..^ |
| 86 | 85 | reximdv2 2857 |
. . . 4
..^ |
| 87 | 3, 86 | mpd 15 |
. . 3
..^ |
| 88 | 87 | rexlimdv3a 2880 |
. 2
..^ |
| 89 | 1, 88 | mpd 15 |
1
..^ |
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 188 wa 371 w3a 984 wceq 1443 wcel 1886 wnel 2622 wral 2736 wrex 2737 crab 2740 class class class wbr 4401
cfv 5581
(class class class)co 6288 cr 9535 c1 9537 caddc 9539 clt 9672 cle 9673 cn 10606 cz 10934 cuz 11156 ..^cfzo 11912
cprime 14615 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614 |
| This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-2o 7180 df-oadd 7183 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-sup 7953 df-inf 7954 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-n0 10867 df-z 10935 df-uz 11157 df-rp 11300 df-fz 11782 df-fzo 11913 df-seq 12211 df-exp 12270 df-fac 12457 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292 df-dvds 14299 df-prm 14616 |
| This theorem is referenced by: prmgaplem7 15020 |
| Copyright terms: Public domain | W3C validator |