Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nn0addge2i | Structured version Visualization version GIF version |
Description: A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.) |
Ref | Expression |
---|---|
nn0addge1i.1 | ⊢ 𝐴 ∈ ℝ |
nn0addge1i.2 | ⊢ 𝑁 ∈ ℕ0 |
Ref | Expression |
---|---|
nn0addge2i | ⊢ 𝐴 ≤ (𝑁 + 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0addge1i.1 | . 2 ⊢ 𝐴 ∈ ℝ | |
2 | nn0addge1i.2 | . 2 ⊢ 𝑁 ∈ ℕ0 | |
3 | nn0addge2 11971 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → 𝐴 ≤ (𝑁 + 𝐴)) | |
4 | 1, 2, 3 | mp2an 692 | 1 ⊢ 𝐴 ≤ (𝑁 + 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2112 class class class wbr 5030 (class class class)co 7148 ℝcr 10564 + caddc 10568 ≤ cle 10704 ℕ0cn0 11924 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7457 ax-resscn 10622 ax-1cn 10623 ax-icn 10624 ax-addcl 10625 ax-addrcl 10626 ax-mulcl 10627 ax-mulrcl 10628 ax-mulcom 10629 ax-addass 10630 ax-mulass 10631 ax-distr 10632 ax-i2m1 10633 ax-1ne0 10634 ax-1rid 10635 ax-rnegex 10636 ax-rrecex 10637 ax-cnre 10638 ax-pre-lttri 10639 ax-pre-lttrn 10640 ax-pre-ltadd 10641 ax-pre-mulgt0 10642 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-nel 3057 df-ral 3076 df-rex 3077 df-reu 3078 df-rab 3080 df-v 3412 df-sbc 3698 df-csb 3807 df-dif 3862 df-un 3864 df-in 3866 df-ss 3876 df-pss 3878 df-nul 4227 df-if 4419 df-pw 4494 df-sn 4521 df-pr 4523 df-tp 4525 df-op 4527 df-uni 4797 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5428 df-eprel 5433 df-po 5441 df-so 5442 df-fr 5481 df-we 5483 df-xp 5528 df-rel 5529 df-cnv 5530 df-co 5531 df-dm 5532 df-rn 5533 df-res 5534 df-ima 5535 df-pred 6124 df-ord 6170 df-on 6171 df-lim 6172 df-suc 6173 df-iota 6292 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-riota 7106 df-ov 7151 df-oprab 7152 df-mpo 7153 df-om 7578 df-wrecs 7955 df-recs 8016 df-rdg 8054 df-er 8297 df-en 8526 df-dom 8527 df-sdom 8528 df-pnf 10705 df-mnf 10706 df-xr 10707 df-ltxr 10708 df-le 10709 df-sub 10900 df-neg 10901 df-nn 11665 df-n0 11925 |
This theorem is referenced by: nn0opthlem2 13669 divsqrtsumlem 25654 aks4d1p1p7 39630 |
Copyright terms: Public domain | W3C validator |