Theorem nnge1 8937

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 4006	. 2 ⊢ (𝑥 = 1 → (1 ≤ 𝑥 ↔ 1 ≤ 1))
2		breq2 4006	. 2 ⊢ (𝑥 = 𝑦 → (1 ≤ 𝑥 ↔ 1 ≤ 𝑦))
3		breq2 4006	. 2 ⊢ (𝑥 = (𝑦 + 1) → (1 ≤ 𝑥 ↔ 1 ≤ (𝑦 + 1)))
4		breq2 4006	. 2 ⊢ (𝑥 = 𝐴 → (1 ≤ 𝑥 ↔ 1 ≤ 𝐴))
5		1le1 8524	. 2 ⊢ 1 ≤ 1
6		nnre 8921	. . 3 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
7		recn 7940	. . . . . 6 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
8	7	addid1d 8101	. . . . 5 ⊢ (𝑦 ∈ ℝ → (𝑦 + 0) = 𝑦)
9	8	breq2d 4014	. . . 4 ⊢ (𝑦 ∈ ℝ → (1 ≤ (𝑦 + 0) ↔ 1 ≤ 𝑦))
10		0lt1 8079	. . . . . . . 8 ⊢ 0 < 1
11		0re 7953	. . . . . . . . 9 ⊢ 0 ∈ ℝ
12		1re 7952	. . . . . . . . 9 ⊢ 1 ∈ ℝ
13		axltadd 8022	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 < 1 → (𝑦 + 0) < (𝑦 + 1)))
14	11, 12, 13	mp3an12 1327	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → (0 < 1 → (𝑦 + 0) < (𝑦 + 1)))
15	10, 14	mpi 15	. . . . . . 7 ⊢ (𝑦 ∈ ℝ → (𝑦 + 0) < (𝑦 + 1))
16		readdcl 7933	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ ∧ 0 ∈ ℝ) → (𝑦 + 0) ∈ ℝ)
17	11, 16	mpan2 425	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → (𝑦 + 0) ∈ ℝ)
18		peano2re 8088	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈ ℝ)
19		lttr 8026	. . . . . . . . 9 ⊢ (((𝑦 + 0) ∈ ℝ ∧ (𝑦 + 1) ∈ ℝ ∧ 1 ∈ ℝ) → (((𝑦 + 0) < (𝑦 + 1) ∧ (𝑦 + 1) < 1) → (𝑦 + 0) < 1))
20	12, 19	mp3an3 1326	. . . . . . . 8 ⊢ (((𝑦 + 0) ∈ ℝ ∧ (𝑦 + 1) ∈ ℝ) → (((𝑦 + 0) < (𝑦 + 1) ∧ (𝑦 + 1) < 1) → (𝑦 + 0) < 1))
21	17, 18, 20	syl2anc 411	. . . . . . 7 ⊢ (𝑦 ∈ ℝ → (((𝑦 + 0) < (𝑦 + 1) ∧ (𝑦 + 1) < 1) → (𝑦 + 0) < 1))
22	15, 21	mpand 429	. . . . . 6 ⊢ (𝑦 ∈ ℝ → ((𝑦 + 1) < 1 → (𝑦 + 0) < 1))
23	22	con3d 631	. . . . 5 ⊢ (𝑦 ∈ ℝ → (¬ (𝑦 + 0) < 1 → ¬ (𝑦 + 1) < 1))
24		lenlt 8028	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ (𝑦 + 0) ∈ ℝ) → (1 ≤ (𝑦 + 0) ↔ ¬ (𝑦 + 0) < 1))
25	12, 17, 24	sylancr 414	. . . . 5 ⊢ (𝑦 ∈ ℝ → (1 ≤ (𝑦 + 0) ↔ ¬ (𝑦 + 0) < 1))
26		lenlt 8028	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ (𝑦 + 1) ∈ ℝ) → (1 ≤ (𝑦 + 1) ↔ ¬ (𝑦 + 1) < 1))
27	12, 18, 26	sylancr 414	. . . . 5 ⊢ (𝑦 ∈ ℝ → (1 ≤ (𝑦 + 1) ↔ ¬ (𝑦 + 1) < 1))
28	23, 25, 27	3imtr4d 203	. . . 4 ⊢ (𝑦 ∈ ℝ → (1 ≤ (𝑦 + 0) → 1 ≤ (𝑦 + 1)))
29	9, 28	sylbird 170	. . 3 ⊢ (𝑦 ∈ ℝ → (1 ≤ 𝑦 → 1 ≤ (𝑦 + 1)))
30	6, 29	syl 14	. 2 ⊢ (𝑦 ∈ ℕ → (1 ≤ 𝑦 → 1 ≤ (𝑦 + 1)))
31	1, 2, 3, 4, 5, 30	nnind 8930	1 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2148   class class class wbr 4002  (class class class)co 5871  ℝcr 7806  0cc0 7807  1c1 7808   + caddc 7810   < clt 7987   ≤ cle 7988  ℕcn 8914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4120  ax-pow 4173  ax-pr 4208  ax-un 4432  ax-setind 4535  ax-cnex 7898  ax-resscn 7899  ax-1re 7901  ax-addrcl 7904  ax-0lt1 7913  ax-0id 7915  ax-rnegex 7916  ax-pre-ltirr 7919  ax-pre-lttrn 7921  ax-pre-ltadd 7923

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-br 4003  df-opab 4064  df-xp 4631  df-cnv 4633  df-iota 5176  df-fv 5222  df-ov 5874  df-pnf 7989  df-mnf 7990  df-xr 7991  df-ltxr 7992  df-le 7993  df-inn 8915

This theorem is referenced by:  nnle1eq1  8938  nngt0  8939  nnnlt1  8940  nnrecgt0  8952  nnge1d  8957  elnnnn0c  9216  elnnz1  9271  zltp1le  9302  nn0ledivnn  9762  elfz1b  10084  fzo1fzo0n0  10177  elfzom1elp1fzo  10196  fzo0sn0fzo1  10215  nnlesq  10617  faclbnd  10713  faclbnd3  10715  cvgratz  11532  coprmgcdb  12079  isprm3  12109  pw2dvds  12157  pockthg  12346  oddennn  12384