Theorem nnge1 12406

Description: A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.)

Assertion

Ref	Expression
nnge1	⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)

Proof of Theorem nnge1

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 5112	. 2 ⊢ (𝑥 = 1 → (1 ≤ 𝑥 ↔ 1 ≤ 1))
2		breq2 5112	. 2 ⊢ (𝑥 = 𝑦 → (1 ≤ 𝑥 ↔ 1 ≤ 𝑦))
3		breq2 5112	. 2 ⊢ (𝑥 = (𝑦 + 1) → (1 ≤ 𝑥 ↔ 1 ≤ (𝑦 + 1)))
4		breq2 5112	. 2 ⊢ (𝑥 = 𝐴 → (1 ≤ 𝑥 ↔ 1 ≤ 𝐴))
5		1le1 11984	. 2 ⊢ 1 ≤ 1
6		nnre 12382	. . 3 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
7		recn 11329	. . . . . 6 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
8	7	addridd 11549	. . . . 5 ⊢ (𝑦 ∈ ℝ → (𝑦 + 0) = 𝑦)
9	8	breq2d 5120	. . . 4 ⊢ (𝑦 ∈ ℝ → (1 ≤ (𝑦 + 0) ↔ 1 ≤ 𝑦))
10		0lt1 11878	. . . . . . . 8 ⊢ 0 < 1
11		0re 11349	. . . . . . . . 9 ⊢ 0 ∈ ℝ
12		1re 11347	. . . . . . . . 9 ⊢ 1 ∈ ℝ
13		axltadd 11422	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 < 1 → (𝑦 + 0) < (𝑦 + 1)))
14	11, 12, 13	mp3an12 1481	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → (0 < 1 → (𝑦 + 0) < (𝑦 + 1)))
15	10, 14	mpi 21	. . . . . . 7 ⊢ (𝑦 ∈ ℝ → (𝑦 + 0) < (𝑦 + 1))
16		readdcl 11322	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ ∧ 0 ∈ ℝ) → (𝑦 + 0) ∈ ℝ)
17	11, 16	mpan2 704	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → (𝑦 + 0) ∈ ℝ)
18		peano2re 11522	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈ ℝ)
19		lttr 11425	. . . . . . . . 9 ⊢ (((𝑦 + 0) ∈ ℝ ∧ (𝑦 + 1) ∈ ℝ ∧ 1 ∈ ℝ) → (((𝑦 + 0) < (𝑦 + 1) ∧ (𝑦 + 1) < 1) → (𝑦 + 0) < 1))
20	12, 19	mp3an3 1480	. . . . . . . 8 ⊢ (((𝑦 + 0) ∈ ℝ ∧ (𝑦 + 1) ∈ ℝ) → (((𝑦 + 0) < (𝑦 + 1) ∧ (𝑦 + 1) < 1) → (𝑦 + 0) < 1))
21	17, 18, 20	syl2anc 596	. . . . . . 7 ⊢ (𝑦 ∈ ℝ → (((𝑦 + 0) < (𝑦 + 1) ∧ (𝑦 + 1) < 1) → (𝑦 + 0) < 1))
22	15, 21	mpand 708	. . . . . 6 ⊢ (𝑦 ∈ ℝ → ((𝑦 + 1) < 1 → (𝑦 + 0) < 1))
23	22	con3d 153	. . . . 5 ⊢ (𝑦 ∈ ℝ → (¬ (𝑦 + 0) < 1 → ¬ (𝑦 + 1) < 1))
24		lenlt 11427	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ (𝑦 + 0) ∈ ℝ) → (1 ≤ (𝑦 + 0) ↔ ¬ (𝑦 + 0) < 1))
25	12, 17, 24	sylancr 599	. . . . 5 ⊢ (𝑦 ∈ ℝ → (1 ≤ (𝑦 + 0) ↔ ¬ (𝑦 + 0) < 1))
26		lenlt 11427	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ (𝑦 + 1) ∈ ℝ) → (1 ≤ (𝑦 + 1) ↔ ¬ (𝑦 + 1) < 1))
27	12, 18, 26	sylancr 599	. . . . 5 ⊢ (𝑦 ∈ ℝ → (1 ≤ (𝑦 + 1) ↔ ¬ (𝑦 + 1) < 1))
28	23, 25, 27	3imtr4d 297	. . . 4 ⊢ (𝑦 ∈ ℝ → (1 ≤ (𝑦 + 0) → 1 ≤ (𝑦 + 1)))
29	9, 28	sylbird 263	. . 3 ⊢ (𝑦 ∈ ℝ → (1 ≤ 𝑦 → 1 ≤ (𝑦 + 1)))
30	6, 29	syl 18	. 2 ⊢ (𝑦 ∈ ℕ → (1 ≤ 𝑦 → 1 ≤ (𝑦 + 1)))
31	1, 2, 3, 4, 5, 30	nnind 12393	1 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2147   class class class wbr 5108  (class class class)co 7451  ℝcr 11238  0cc0 11239  1c1 11240   + caddc 11242   < clt 11382   ≤ cle 11383  ℕcn 12375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-nn 12376

This theorem is used by:  nngt1ne1  12407  nnle1eq1  12408  nngt0  12409  nnnlt1  12410  nnrecgt0  12421  nnge1d  12426  elnnnn0c  12691  zle0orge1  12750  elnnz1  12762  zltp1le  12786  nn0ledivnn  13275  fzo1fzo0n0  13890  elfzom1elp1fzo  13907  fzo0sn0fzo1  13930  addmodlteq  14129  nnlesq  14389  digit1  14422  expnngt1  14426  faclbnd  14475  faclbnd3  14477  faclbnd4lem1  14478  faclbnd4lem4  14481  len0nnbi  14737  fstwrdne0  14742  divalglem1  16608  coprmgcdb  16868  isprm3  16902  pockthg  17128  infpn2  17135  setsstruct  17398  chfacfpmmulgsum2  23238  dscmet  24946  ovolunlem1a  25872  vitali  25989  plyeq0lem  26584  logtayllem  27044  leibpi  27327  vmalelog  27589  chtublem  27595  logfaclbnd  27606  bposlem1  27668  gausslemma2dlem1a  27749  dchrisum0lem1  27900  logdivbnd  27940  pntlemn  27984  ostth2lem3  28019  clwwisshclwwslem  30662  clwlknf1oclwwlknlem2  30730  clwlknf1oclwwlknlem3  30731  clwlknf1oclwwlkn  30732  nnmulge  33427  lmatfvlem  34558  eulerpartlems  35103  eulerpartlemb  35111  ballotlem2  35232  reprlt  35359  fz0n  36711  nndivlub  37461  knoppndvlem1  37593  knoppndvlem2  37594  knoppndvlem7  37599  knoppndvlem11  37603  knoppndvlem14  37606  lcmineqlem13  43357  aks4d1p7d1  43398  fzsplit1nn0  44031  pell1qrgaplem  44146  pellqrex  44152  monotoddzzfi  44215  jm2.23  44269  sumnnodd  46915  dvnmul  47226  wallispilem4  47351  wallispilem5  47352  wallispi  47353  wallispi2lem1  47354  stirlinglem5  47361  stirlinglem13  47369  dirkertrigeqlem1  47381  fouriersw  47514  etransclem24  47541  flmrecm1  48686  zplusmodne  48692  addmodne  48693  minusmod5ne  48698  iccpartigtl  48778  fmtnodvds  48902  lighneallem2  48964  gpg3kgrtriexlem3  49456  gpg3kgrtriexlem4  49457  gpg3kgrtriexlem6  49459  logbpw2m1  50010  blennnelnn  50019  blenpw2m1  50022  dignnld  50046  itcovalt2lem2lem1  50116