uzind

Description: Induction on the upper integers that start at M . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 5-Jul-2005)

	Ref	Expression
Hypotheses	uzind.1	$⊢ j = M \to (φ \leftrightarrow ψ)$
	uzind.2	$⊢ j = k \to (φ \leftrightarrow χ)$
	uzind.3	$⊢ j = k + 1 \to (φ \leftrightarrow θ)$
	uzind.4	$⊢ j = N \to (φ \leftrightarrow τ)$
	uzind.5	$⊢ M \in ℤ \to ψ$
	uzind.6	$⊢ (M \in ℤ \land k \in ℤ \land M \leq k) \to (χ \to θ)$
Assertion	uzind	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to τ$

Proof

Step	Hyp	Ref	Expression
1		uzind.1	$⊢ j = M \to (φ \leftrightarrow ψ)$
2		uzind.2	$⊢ j = k \to (φ \leftrightarrow χ)$
3		uzind.3	$⊢ j = k + 1 \to (φ \leftrightarrow θ)$
4		uzind.4	$⊢ j = N \to (φ \leftrightarrow τ)$
5		uzind.5	$⊢ M \in ℤ \to ψ$
6		uzind.6	$⊢ (M \in ℤ \land k \in ℤ \land M \leq k) \to (χ \to θ)$
7		zre	$⊢ M \in ℤ \to M \in ℝ$
8	7	leidd	$⊢ M \in ℤ \to M \leq M$
9	8 5	jca	$⊢ M \in ℤ \to (M \leq M \land ψ)$
10	9	ancli	$⊢ M \in ℤ \to (M \in ℤ \land (M \leq M \land ψ))$
11		breq2	$⊢ j = M \to (M \leq j \leftrightarrow M \leq M)$
12	11 1	anbi12d	$⊢ j = M \to ((M \leq j \land φ) \leftrightarrow (M \leq M \land ψ))$
13	12	elrab	$⊢ M \in \{j \in ℤ \| (M \leq j \land φ)\} \leftrightarrow (M \in ℤ \land (M \leq M \land ψ))$
14	10 13	sylibr	$⊢ M \in ℤ \to M \in \{j \in ℤ \| (M \leq j \land φ)\}$
15		peano2z	$⊢ k \in ℤ \to k + 1 \in ℤ$
16	15	a1i	$⊢ M \in ℤ \to (k \in ℤ \to k + 1 \in ℤ)$
17	16	adantrd	$⊢ M \in ℤ \to ((k \in ℤ \land (M \leq k \land χ)) \to k + 1 \in ℤ)$
18		zre	$⊢ k \in ℤ \to k \in ℝ$
19		ltp1	$⊢ k \in ℝ \to k < k + 1$
20	19	adantl	$⊢ (M \in ℝ \land k \in ℝ) \to k < k + 1$
21		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
22	21	ancli	$⊢ k \in ℝ \to (k \in ℝ \land k + 1 \in ℝ)$
23		lelttr	$⊢ (M \in ℝ \land k \in ℝ \land k + 1 \in ℝ) \to ((M \leq k \land k < k + 1) \to M < k + 1)$
24	23	3expb	$⊢ (M \in ℝ \land (k \in ℝ \land k + 1 \in ℝ)) \to ((M \leq k \land k < k + 1) \to M < k + 1)$
25	22 24	sylan2	$⊢ (M \in ℝ \land k \in ℝ) \to ((M \leq k \land k < k + 1) \to M < k + 1)$
26	20 25	mpan2d	$⊢ (M \in ℝ \land k \in ℝ) \to (M \leq k \to M < k + 1)$
27		ltle	$⊢ (M \in ℝ \land k + 1 \in ℝ) \to (M < k + 1 \to M \leq k + 1)$
28	21 27	sylan2	$⊢ (M \in ℝ \land k \in ℝ) \to (M < k + 1 \to M \leq k + 1)$
29	26 28	syld	$⊢ (M \in ℝ \land k \in ℝ) \to (M \leq k \to M \leq k + 1)$
30	7 18 29	syl2an	$⊢ (M \in ℤ \land k \in ℤ) \to (M \leq k \to M \leq k + 1)$
31	30	adantrd	$⊢ (M \in ℤ \land k \in ℤ) \to ((M \leq k \land χ) \to M \leq k + 1)$
32	31	expimpd	$⊢ M \in ℤ \to ((k \in ℤ \land (M \leq k \land χ)) \to M \leq k + 1)$
33	6	3exp	$⊢ M \in ℤ \to (k \in ℤ \to (M \leq k \to (χ \to θ)))$
34	33	imp4d	$⊢ M \in ℤ \to ((k \in ℤ \land (M \leq k \land χ)) \to θ)$
35	32 34	jcad	$⊢ M \in ℤ \to ((k \in ℤ \land (M \leq k \land χ)) \to (M \leq k + 1 \land θ))$
36	17 35	jcad	$⊢ M \in ℤ \to ((k \in ℤ \land (M \leq k \land χ)) \to (k + 1 \in ℤ \land (M \leq k + 1 \land θ)))$
37		breq2	$⊢ j = k \to (M \leq j \leftrightarrow M \leq k)$
38	37 2	anbi12d	$⊢ j = k \to ((M \leq j \land φ) \leftrightarrow (M \leq k \land χ))$
39	38	elrab	$⊢ k \in \{j \in ℤ \| (M \leq j \land φ)\} \leftrightarrow (k \in ℤ \land (M \leq k \land χ))$
40		breq2	$⊢ j = k + 1 \to (M \leq j \leftrightarrow M \leq k + 1)$
41	40 3	anbi12d	$⊢ j = k + 1 \to ((M \leq j \land φ) \leftrightarrow (M \leq k + 1 \land θ))$
42	41	elrab	$⊢ k + 1 \in \{j \in ℤ \| (M \leq j \land φ)\} \leftrightarrow (k + 1 \in ℤ \land (M \leq k + 1 \land θ))$
43	36 39 42	3imtr4g	$⊢ M \in ℤ \to (k \in \{j \in ℤ \| (M \leq j \land φ)\} \to k + 1 \in \{j \in ℤ \| (M \leq j \land φ)\})$
44	43	ralrimiv	$⊢ M \in ℤ \to \forall k \in \{j \in ℤ \| (M \leq j \land φ)\} k + 1 \in \{j \in ℤ \| (M \leq j \land φ)\}$
45		peano5uzti	$⊢ M \in ℤ \to ((M \in \{j \in ℤ \| (M \leq j \land φ)\} \land \forall k \in \{j \in ℤ \| (M \leq j \land φ)\} k + 1 \in \{j \in ℤ \| (M \leq j \land φ)\}) \to \{w \in ℤ \| M \leq w\} \subseteq \{j \in ℤ \| (M \leq j \land φ)\})$
46	14 44 45	mp2and	$⊢ M \in ℤ \to \{w \in ℤ \| M \leq w\} \subseteq \{j \in ℤ \| (M \leq j \land φ)\}$
47	46	sseld	$⊢ M \in ℤ \to (N \in \{w \in ℤ \| M \leq w\} \to N \in \{j \in ℤ \| (M \leq j \land φ)\})$
48		breq2	$⊢ w = N \to (M \leq w \leftrightarrow M \leq N)$
49	48	elrab	$⊢ N \in \{w \in ℤ \| M \leq w\} \leftrightarrow (N \in ℤ \land M \leq N)$
50		breq2	$⊢ j = N \to (M \leq j \leftrightarrow M \leq N)$
51	50 4	anbi12d	$⊢ j = N \to ((M \leq j \land φ) \leftrightarrow (M \leq N \land τ))$
52	51	elrab	$⊢ N \in \{j \in ℤ \| (M \leq j \land φ)\} \leftrightarrow (N \in ℤ \land (M \leq N \land τ))$
53	47 49 52	3imtr3g	$⊢ M \in ℤ \to ((N \in ℤ \land M \leq N) \to (N \in ℤ \land (M \leq N \land τ)))$
54	53	3impib	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to (N \in ℤ \land (M \leq N \land τ))$
55	54	simprrd	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to τ$

Metamath Proof Explorer

Theorem uzind

Proof