uzindd

Description: Induction on the upper integers that start at M . The first four hypotheses give us the substitution instances we need; the following two are the basis and the induction step, a deduction version. (Contributed by metakunt, 8-Jun-2024)

	Ref	Expression
Hypotheses	uzindd.1	⊢ ( 𝑗 = 𝑀 → ( 𝜓 ↔ 𝜒 ) )
	uzindd.2	⊢ ( 𝑗 = 𝑘 → ( 𝜓 ↔ 𝜃 ) )
	uzindd.3	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜓 ↔ 𝜏 ) )
	uzindd.4	⊢ ( 𝑗 = 𝑁 → ( 𝜓 ↔ 𝜂 ) )
	uzindd.5	⊢ ( 𝜑 → 𝜒 )
	uzindd.6	⊢ ( ( 𝜑 ∧ 𝜃 ∧ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) → 𝜏 )
	uzindd.7	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	uzindd.8	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	uzindd.9	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
Assertion	uzindd	⊢ ( 𝜑 → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		uzindd.1	⊢ ( 𝑗 = 𝑀 → ( 𝜓 ↔ 𝜒 ) )
2		uzindd.2	⊢ ( 𝑗 = 𝑘 → ( 𝜓 ↔ 𝜃 ) )
3		uzindd.3	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜓 ↔ 𝜏 ) )
4		uzindd.4	⊢ ( 𝑗 = 𝑁 → ( 𝜓 ↔ 𝜂 ) )
5		uzindd.5	⊢ ( 𝜑 → 𝜒 )
6		uzindd.6	⊢ ( ( 𝜑 ∧ 𝜃 ∧ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) → 𝜏 )
7		uzindd.7	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8		uzindd.8	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
9		uzindd.9	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
10	7 8 9	3jca	⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
11	1	imbi2d	⊢ ( 𝑗 = 𝑀 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) )
12	2	imbi2d	⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜃 ) ) )
13	3	imbi2d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜏 ) ) )
14	4	imbi2d	⊢ ( 𝑗 = 𝑁 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜂 ) ) )
15	5	adantr	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → 𝜒 )
16	15	expcom	⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → 𝜒 ) )
17		3anass	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) )
18		ancom	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) ↔ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑀 ∈ ℤ ) )
19	17 18	bitri	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ↔ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑀 ∈ ℤ ) )
20	6	ad4ant123	⊢ ( ( ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) ∧ 𝑀 ∈ ℤ ) → 𝜏 )
21	20	anasss	⊢ ( ( ( 𝜑 ∧ 𝜃 ) ∧ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑀 ∈ ℤ ) ) → 𝜏 )
22	19 21	sylan2b	⊢ ( ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) → 𝜏 )
23	22	3impa	⊢ ( ( 𝜑 ∧ 𝜃 ∧ ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) → 𝜏 )
24	23	3com23	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ∧ 𝜃 ) → 𝜏 )
25	24	3expia	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) → ( 𝜃 → 𝜏 ) )
26	25	expcom	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) → ( 𝜑 → ( 𝜃 → 𝜏 ) ) )
27	26	a2d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) → ( ( 𝜑 → 𝜃 ) → ( 𝜑 → 𝜏 ) ) )
28	11 12 13 14 16 27	uzind	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝜑 → 𝜂 ) )
29	10 28	mpcom	⊢ ( 𝜑 → 𝜂 )

Metamath Proof Explorer

Theorem uzindd

Proof