Theorem nnge1

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

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

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑥 = 1 → ( 1 ≤ 𝑥 ↔ 1 ≤ 1 ) )
2		breq2	⊢ ( 𝑥 = 𝑦 → ( 1 ≤ 𝑥 ↔ 1 ≤ 𝑦 ) )
3		breq2	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 1 ≤ 𝑥 ↔ 1 ≤ ( 𝑦 + 1 ) ) )
4		breq2	⊢ ( 𝑥 = 𝐴 → ( 1 ≤ 𝑥 ↔ 1 ≤ 𝐴 ) )
5		1le1	⊢ 1 ≤ 1
6		nnre	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
7		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
8	7	addridd	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 0 ) = 𝑦 )
9	8	breq2d	⊢ ( 𝑦 ∈ ℝ → ( 1 ≤ ( 𝑦 + 0 ) ↔ 1 ≤ 𝑦 ) )
10		0lt1	⊢ 0 < 1
11		0re	⊢ 0 ∈ ℝ
12		1re	⊢ 1 ∈ ℝ
13		axltadd	⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 < 1 → ( 𝑦 + 0 ) < ( 𝑦 + 1 ) ) )
14	11 12 13	mp3an12	⊢ ( 𝑦 ∈ ℝ → ( 0 < 1 → ( 𝑦 + 0 ) < ( 𝑦 + 1 ) ) )
15	10 14	mpi	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 0 ) < ( 𝑦 + 1 ) )
16		readdcl	⊢ ( ( 𝑦 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑦 + 0 ) ∈ ℝ )
17	11 16	mpan2	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 0 ) ∈ ℝ )
18		peano2re	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 1 ) ∈ ℝ )
19		lttr	⊢ ( ( ( 𝑦 + 0 ) ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( 𝑦 + 0 ) < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) < 1 ) → ( 𝑦 + 0 ) < 1 ) )
20	12 19	mp3an3	⊢ ( ( ( 𝑦 + 0 ) ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ) → ( ( ( 𝑦 + 0 ) < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) < 1 ) → ( 𝑦 + 0 ) < 1 ) )
21	17 18 20	syl2anc	⊢ ( 𝑦 ∈ ℝ → ( ( ( 𝑦 + 0 ) < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) < 1 ) → ( 𝑦 + 0 ) < 1 ) )
22	15 21	mpand	⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 + 1 ) < 1 → ( 𝑦 + 0 ) < 1 ) )
23	22	con3d	⊢ ( 𝑦 ∈ ℝ → ( ¬ ( 𝑦 + 0 ) < 1 → ¬ ( 𝑦 + 1 ) < 1 ) )
24		lenlt	⊢ ( ( 1 ∈ ℝ ∧ ( 𝑦 + 0 ) ∈ ℝ ) → ( 1 ≤ ( 𝑦 + 0 ) ↔ ¬ ( 𝑦 + 0 ) < 1 ) )
25	12 17 24	sylancr	⊢ ( 𝑦 ∈ ℝ → ( 1 ≤ ( 𝑦 + 0 ) ↔ ¬ ( 𝑦 + 0 ) < 1 ) )
26		lenlt	⊢ ( ( 1 ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ) → ( 1 ≤ ( 𝑦 + 1 ) ↔ ¬ ( 𝑦 + 1 ) < 1 ) )
27	12 18 26	sylancr	⊢ ( 𝑦 ∈ ℝ → ( 1 ≤ ( 𝑦 + 1 ) ↔ ¬ ( 𝑦 + 1 ) < 1 ) )
28	23 25 27	3imtr4d	⊢ ( 𝑦 ∈ ℝ → ( 1 ≤ ( 𝑦 + 0 ) → 1 ≤ ( 𝑦 + 1 ) ) )
29	9 28	sylbird	⊢ ( 𝑦 ∈ ℝ → ( 1 ≤ 𝑦 → 1 ≤ ( 𝑦 + 1 ) ) )
30	6 29	syl	⊢ ( 𝑦 ∈ ℕ → ( 1 ≤ 𝑦 → 1 ≤ ( 𝑦 + 1 ) ) )
31	1 2 3 4 5 30	nnind	⊢ ( 𝐴 ∈ ℕ → 1 ≤ 𝐴 )