peano5uzi

Description: Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005) (Revised by Mario Carneiro, 3-May-2014)

		Ref	Expression
	Hypothesis	peano5uzi.1	$⊢ N \in ℤ$
	Assertion	peano5uzi	$⊢ (N \in A \land \forall x \in A x + 1 \in A) \to \{k \in ℤ \| N \leq k\} \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		peano5uzi.1	$⊢ N \in ℤ$
2		breq2	$⊢ k = n \to (N \leq k \leftrightarrow N \leq n)$
3	2	elrab	$⊢ n \in \{k \in ℤ \| N \leq k\} \leftrightarrow (n \in ℤ \land N \leq n)$
4		zcn	$⊢ n \in ℤ \to n \in ℂ$
5	4	ad2antrl	$⊢ ((N \in A \land \forall x \in A x + 1 \in A) \land (n \in ℤ \land N \leq n)) \to n \in ℂ$
6		zcn	$⊢ N \in ℤ \to N \in ℂ$
7	1 6	ax-mp	$⊢ N \in ℂ$
8		ax-1cn	$⊢ 1 \in ℂ$
9	7 8	subcli	$⊢ N - 1 \in ℂ$
10		npcan	$⊢ (n \in ℂ \land N - 1 \in ℂ) \to (n - (N - 1)) + N - 1 = n$
11	5 9 10	sylancl	$⊢ ((N \in A \land \forall x \in A x + 1 \in A) \land (n \in ℤ \land N \leq n)) \to (n - (N - 1)) + N - 1 = n$
12		subsub	$⊢ (n \in ℂ \land N \in ℂ \land 1 \in ℂ) \to n - (N - 1) = n - N + 1$
13	7 8 12	mp3an23	$⊢ n \in ℂ \to n - (N - 1) = n - N + 1$
14	5 13	syl	$⊢ ((N \in A \land \forall x \in A x + 1 \in A) \land (n \in ℤ \land N \leq n)) \to n - (N - 1) = n - N + 1$
15		znn0sub	$⊢ (N \in ℤ \land n \in ℤ) \to (N \leq n \leftrightarrow n - N \in ℕ_{0})$
16	1 15	mpan	$⊢ n \in ℤ \to (N \leq n \leftrightarrow n - N \in ℕ_{0})$
17	16	biimpa	$⊢ (n \in ℤ \land N \leq n) \to n - N \in ℕ_{0}$
18	17	adantl	$⊢ ((N \in A \land \forall x \in A x + 1 \in A) \land (n \in ℤ \land N \leq n)) \to n - N \in ℕ_{0}$
19		nn0p1nn	$⊢ n - N \in ℕ_{0} \to n - N + 1 \in ℕ$
20	18 19	syl	$⊢ ((N \in A \land \forall x \in A x + 1 \in A) \land (n \in ℤ \land N \leq n)) \to n - N + 1 \in ℕ$
21	14 20	eqeltrd	$⊢ ((N \in A \land \forall x \in A x + 1 \in A) \land (n \in ℤ \land N \leq n)) \to n - (N - 1) \in ℕ$
22		simpl	$⊢ ((N \in A \land \forall x \in A x + 1 \in A) \land (n \in ℤ \land N \leq n)) \to (N \in A \land \forall x \in A x + 1 \in A)$
23		oveq1	$⊢ k = 1 \to k + N - 1 = 1 + N - 1$
24	23	eleq1d	$⊢ k = 1 \to (k + N - 1 \in A \leftrightarrow 1 + N - 1 \in A)$
25	24	imbi2d	$⊢ k = 1 \to (((N \in A \land \forall x \in A x + 1 \in A) \to k + N - 1 \in A) \leftrightarrow ((N \in A \land \forall x \in A x + 1 \in A) \to 1 + N - 1 \in A))$
26		oveq1	$⊢ k = n \to k + N - 1 = n + N - 1$
27	26	eleq1d	$⊢ k = n \to (k + N - 1 \in A \leftrightarrow n + N - 1 \in A)$
28	27	imbi2d	$⊢ k = n \to (((N \in A \land \forall x \in A x + 1 \in A) \to k + N - 1 \in A) \leftrightarrow ((N \in A \land \forall x \in A x + 1 \in A) \to n + N - 1 \in A))$
29		oveq1	$⊢ k = n + 1 \to k + N - 1 = n + 1 + (N - 1)$
30	29	eleq1d	$⊢ k = n + 1 \to (k + N - 1 \in A \leftrightarrow n + 1 + (N - 1) \in A)$
31	30	imbi2d	$⊢ k = n + 1 \to (((N \in A \land \forall x \in A x + 1 \in A) \to k + N - 1 \in A) \leftrightarrow ((N \in A \land \forall x \in A x + 1 \in A) \to n + 1 + (N - 1) \in A))$
32		oveq1	$⊢ k = n - (N - 1) \to k + N - 1 = (n - (N - 1)) + N - 1$
33	32	eleq1d	$⊢ k = n - (N - 1) \to (k + N - 1 \in A \leftrightarrow (n - (N - 1)) + N - 1 \in A)$
34	33	imbi2d	$⊢ k = n - (N - 1) \to (((N \in A \land \forall x \in A x + 1 \in A) \to k + N - 1 \in A) \leftrightarrow ((N \in A \land \forall x \in A x + 1 \in A) \to (n - (N - 1)) + N - 1 \in A))$
35	8 7	pncan3i	$⊢ 1 + N - 1 = N$
36		simpl	$⊢ (N \in A \land \forall x \in A x + 1 \in A) \to N \in A$
37	35 36	eqeltrid	$⊢ (N \in A \land \forall x \in A x + 1 \in A) \to 1 + N - 1 \in A$
38		oveq1	$⊢ x = n + N - 1 \to x + 1 = n + (N - 1) + 1$
39	38	eleq1d	$⊢ x = n + N - 1 \to (x + 1 \in A \leftrightarrow n + (N - 1) + 1 \in A)$
40	39	rspccv	$⊢ \forall x \in A x + 1 \in A \to (n + N - 1 \in A \to n + (N - 1) + 1 \in A)$
41	40	ad2antll	$⊢ (n \in ℕ \land (N \in A \land \forall x \in A x + 1 \in A)) \to (n + N - 1 \in A \to n + (N - 1) + 1 \in A)$
42		nncn	$⊢ n \in ℕ \to n \in ℂ$
43	42	adantr	$⊢ (n \in ℕ \land (N \in A \land \forall x \in A x + 1 \in A)) \to n \in ℂ$
44		add32	$⊢ (n \in ℂ \land N - 1 \in ℂ \land 1 \in ℂ) \to n + (N - 1) + 1 = n + 1 + (N - 1)$
45	9 8 44	mp3an23	$⊢ n \in ℂ \to n + (N - 1) + 1 = n + 1 + (N - 1)$
46	43 45	syl	$⊢ (n \in ℕ \land (N \in A \land \forall x \in A x + 1 \in A)) \to n + (N - 1) + 1 = n + 1 + (N - 1)$
47	46	eleq1d	$⊢ (n \in ℕ \land (N \in A \land \forall x \in A x + 1 \in A)) \to (n + (N - 1) + 1 \in A \leftrightarrow n + 1 + (N - 1) \in A)$
48	41 47	sylibd	$⊢ (n \in ℕ \land (N \in A \land \forall x \in A x + 1 \in A)) \to (n + N - 1 \in A \to n + 1 + (N - 1) \in A)$
49	48	ex	$⊢ n \in ℕ \to ((N \in A \land \forall x \in A x + 1 \in A) \to (n + N - 1 \in A \to n + 1 + (N - 1) \in A))$
50	49	a2d	$⊢ n \in ℕ \to (((N \in A \land \forall x \in A x + 1 \in A) \to n + N - 1 \in A) \to ((N \in A \land \forall x \in A x + 1 \in A) \to n + 1 + (N - 1) \in A))$
51	25 28 31 34 37 50	nnind	$⊢ n - (N - 1) \in ℕ \to ((N \in A \land \forall x \in A x + 1 \in A) \to (n - (N - 1)) + N - 1 \in A)$
52	21 22 51	sylc	$⊢ ((N \in A \land \forall x \in A x + 1 \in A) \land (n \in ℤ \land N \leq n)) \to (n - (N - 1)) + N - 1 \in A$
53	11 52	eqeltrrd	$⊢ ((N \in A \land \forall x \in A x + 1 \in A) \land (n \in ℤ \land N \leq n)) \to n \in A$
54	53	ex	$⊢ (N \in A \land \forall x \in A x + 1 \in A) \to ((n \in ℤ \land N \leq n) \to n \in A)$
55	3 54	biimtrid	$⊢ (N \in A \land \forall x \in A x + 1 \in A) \to (n \in \{k \in ℤ \| N \leq k\} \to n \in A)$
56	55	ssrdv	$⊢ (N \in A \land \forall x \in A x + 1 \in A) \to \{k \in ℤ \| N \leq k\} \subseteq A$

Metamath Proof Explorer

Theorem peano5uzi

Proof