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	⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
	uzind.2	⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) )
	uzind.3	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
	uzind.4	⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
	uzind.5	⊢ ( 𝑀 ∈ ℤ → 𝜓 )
	uzind.6	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) → ( 𝜒 → 𝜃 ) )
Assertion	uzind	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		uzind.1	⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
2		uzind.2	⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) )
3		uzind.3	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4		uzind.4	⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
5		uzind.5	⊢ ( 𝑀 ∈ ℤ → 𝜓 )
6		uzind.6	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) → ( 𝜒 → 𝜃 ) )
7		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
8	7	leidd	⊢ ( 𝑀 ∈ ℤ → 𝑀 ≤ 𝑀 )
9	8 5	jca	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ≤ 𝑀 ∧ 𝜓 ) )
10	9	ancli	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑀 ∧ 𝜓 ) ) )
11		breq2	⊢ ( 𝑗 = 𝑀 → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑀 ) )
12	11 1	anbi12d	⊢ ( 𝑗 = 𝑀 → ( ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤ 𝑀 ∧ 𝜓 ) ) )
13	12	elrab	⊢ ( 𝑀 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑀 ∧ 𝜓 ) ) )
14	10 13	sylibr	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } )
15		peano2z	⊢ ( 𝑘 ∈ ℤ → ( 𝑘 + 1 ) ∈ ℤ )
16	15	a1i	⊢ ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ℤ → ( 𝑘 + 1 ) ∈ ℤ ) )
17	16	adantrd	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) → ( 𝑘 + 1 ) ∈ ℤ ) )
18		zre	⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
19		ltp1	⊢ ( 𝑘 ∈ ℝ → 𝑘 < ( 𝑘 + 1 ) )
20	19	adantl	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → 𝑘 < ( 𝑘 + 1 ) )
21		peano2re	⊢ ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ )
22	21	ancli	⊢ ( 𝑘 ∈ ℝ → ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) )
23		lelttr	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 < ( 𝑘 + 1 ) ) → 𝑀 < ( 𝑘 + 1 ) ) )
24	23	3expb	⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 < ( 𝑘 + 1 ) ) → 𝑀 < ( 𝑘 + 1 ) ) )
25	22 24	sylan2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 < ( 𝑘 + 1 ) ) → 𝑀 < ( 𝑘 + 1 ) ) )
26	20 25	mpan2d	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑀 ≤ 𝑘 → 𝑀 < ( 𝑘 + 1 ) ) )
27		ltle	⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( 𝑀 < ( 𝑘 + 1 ) → 𝑀 ≤ ( 𝑘 + 1 ) ) )
28	21 27	sylan2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑀 < ( 𝑘 + 1 ) → 𝑀 ≤ ( 𝑘 + 1 ) ) )
29	26 28	syld	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑀 ≤ 𝑘 → 𝑀 ≤ ( 𝑘 + 1 ) ) )
30	7 18 29	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀 ≤ 𝑘 → 𝑀 ≤ ( 𝑘 + 1 ) ) )
31	30	adantrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) → 𝑀 ≤ ( 𝑘 + 1 ) ) )
32	31	expimpd	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) → 𝑀 ≤ ( 𝑘 + 1 ) ) )
33	6	3exp	⊢ ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ℤ → ( 𝑀 ≤ 𝑘 → ( 𝜒 → 𝜃 ) ) ) )
34	33	imp4d	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) → 𝜃 ) )
35	32 34	jcad	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) → ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) )
36	17 35	jcad	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) → ( ( 𝑘 + 1 ) ∈ ℤ ∧ ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) ) )
37		breq2	⊢ ( 𝑗 = 𝑘 → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑘 ) )
38	37 2	anbi12d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) )
39	38	elrab	⊢ ( 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ↔ ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) )
40		breq2	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ ( 𝑘 + 1 ) ) )
41	40 3	anbi12d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) )
42	41	elrab	⊢ ( ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ↔ ( ( 𝑘 + 1 ) ∈ ℤ ∧ ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) )
43	36 39 42	3imtr4g	⊢ ( 𝑀 ∈ ℤ → ( 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } → ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) )
44	43	ralrimiv	⊢ ( 𝑀 ∈ ℤ → ∀ 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } )
45		peano5uzti	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) → { 𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤 } ⊆ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) )
46	14 44 45	mp2and	⊢ ( 𝑀 ∈ ℤ → { 𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤 } ⊆ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } )
47	46	sseld	⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ { 𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤 } → 𝑁 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) )
48		breq2	⊢ ( 𝑤 = 𝑁 → ( 𝑀 ≤ 𝑤 ↔ 𝑀 ≤ 𝑁 ) )
49	48	elrab	⊢ ( 𝑁 ∈ { 𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤 } ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
50		breq2	⊢ ( 𝑗 = 𝑁 → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑁 ) )
51	50 4	anbi12d	⊢ ( 𝑗 = 𝑁 → ( ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤ 𝑁 ∧ 𝜏 ) ) )
52	51	elrab	⊢ ( 𝑁 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑀 ≤ 𝑁 ∧ 𝜏 ) ) )
53	47 49 52	3imtr3g	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑁 ∈ ℤ ∧ ( 𝑀 ≤ 𝑁 ∧ 𝜏 ) ) ) )
54	53	3impib	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑁 ∈ ℤ ∧ ( 𝑀 ≤ 𝑁 ∧ 𝜏 ) ) )
55	54	simprrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜏 )

Metamath Proof Explorer

Theorem uzind

Proof