Theorem 2nn0ind

Description: Induction on nonnegative integers with two base cases, for use with Lucas-type sequences. (Contributed by Stefan O'Rear, 1-Oct-2014)

	Ref	Expression
Hypotheses	2nn0ind.1	⊢ 𝜓
	2nn0ind.2	⊢ 𝜒
	2nn0ind.3	⊢ ( 𝑦 ∈ ℕ → ( ( 𝜃 ∧ 𝜏 ) → 𝜂 ) )
	2nn0ind.4	⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
	2nn0ind.5	⊢ ( 𝑥 = 1 → ( 𝜑 ↔ 𝜒 ) )
	2nn0ind.6	⊢ ( 𝑥 = ( 𝑦 − 1 ) → ( 𝜑 ↔ 𝜃 ) )
	2nn0ind.7	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜏 ) )
	2nn0ind.8	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜂 ) )
	2nn0ind.9	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜌 ) )
Assertion	2nn0ind	⊢ ( 𝐴 ∈ ℕ0 → 𝜌 )

Proof

Step	Hyp	Ref	Expression
1		2nn0ind.1	⊢ 𝜓
2		2nn0ind.2	⊢ 𝜒
3		2nn0ind.3	⊢ ( 𝑦 ∈ ℕ → ( ( 𝜃 ∧ 𝜏 ) → 𝜂 ) )
4		2nn0ind.4	⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) )
5		2nn0ind.5	⊢ ( 𝑥 = 1 → ( 𝜑 ↔ 𝜒 ) )
6		2nn0ind.6	⊢ ( 𝑥 = ( 𝑦 − 1 ) → ( 𝜑 ↔ 𝜃 ) )
7		2nn0ind.7	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜏 ) )
8		2nn0ind.8	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜂 ) )
9		2nn0ind.9	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜌 ) )
10		nn0p1nn	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 + 1 ) ∈ ℕ )
11		oveq1	⊢ ( 𝑎 = 1 → ( 𝑎 − 1 ) = ( 1 − 1 ) )
12	11	sbceq1d	⊢ ( 𝑎 = 1 → ( [ ( 𝑎 − 1 ) / 𝑥 ] 𝜑 ↔ [ ( 1 − 1 ) / 𝑥 ] 𝜑 ) )
13		dfsbcq	⊢ ( 𝑎 = 1 → ( [ 𝑎 / 𝑥 ] 𝜑 ↔ [ 1 / 𝑥 ] 𝜑 ) )
14	12 13	anbi12d	⊢ ( 𝑎 = 1 → ( ( [ ( 𝑎 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] 𝜑 ) ↔ ( [ ( 1 − 1 ) / 𝑥 ] 𝜑 ∧ [ 1 / 𝑥 ] 𝜑 ) ) )
15		oveq1	⊢ ( 𝑎 = 𝑦 → ( 𝑎 − 1 ) = ( 𝑦 − 1 ) )
16	15	sbceq1d	⊢ ( 𝑎 = 𝑦 → ( [ ( 𝑎 − 1 ) / 𝑥 ] 𝜑 ↔ [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ) )
17		dfsbcq	⊢ ( 𝑎 = 𝑦 → ( [ 𝑎 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
18	16 17	anbi12d	⊢ ( 𝑎 = 𝑦 → ( ( [ ( 𝑎 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] 𝜑 ) ↔ ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
19		oveq1	⊢ ( 𝑎 = ( 𝑦 + 1 ) → ( 𝑎 − 1 ) = ( ( 𝑦 + 1 ) − 1 ) )
20	19	sbceq1d	⊢ ( 𝑎 = ( 𝑦 + 1 ) → ( [ ( 𝑎 − 1 ) / 𝑥 ] 𝜑 ↔ [ ( ( 𝑦 + 1 ) − 1 ) / 𝑥 ] 𝜑 ) )
21		dfsbcq	⊢ ( 𝑎 = ( 𝑦 + 1 ) → ( [ 𝑎 / 𝑥 ] 𝜑 ↔ [ ( 𝑦 + 1 ) / 𝑥 ] 𝜑 ) )
22	20 21	anbi12d	⊢ ( 𝑎 = ( 𝑦 + 1 ) → ( ( [ ( 𝑎 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] 𝜑 ) ↔ ( [ ( ( 𝑦 + 1 ) − 1 ) / 𝑥 ] 𝜑 ∧ [ ( 𝑦 + 1 ) / 𝑥 ] 𝜑 ) ) )
23		oveq1	⊢ ( 𝑎 = ( 𝐴 + 1 ) → ( 𝑎 − 1 ) = ( ( 𝐴 + 1 ) − 1 ) )
24	23	sbceq1d	⊢ ( 𝑎 = ( 𝐴 + 1 ) → ( [ ( 𝑎 − 1 ) / 𝑥 ] 𝜑 ↔ [ ( ( 𝐴 + 1 ) − 1 ) / 𝑥 ] 𝜑 ) )
25		dfsbcq	⊢ ( 𝑎 = ( 𝐴 + 1 ) → ( [ 𝑎 / 𝑥 ] 𝜑 ↔ [ ( 𝐴 + 1 ) / 𝑥 ] 𝜑 ) )
26	24 25	anbi12d	⊢ ( 𝑎 = ( 𝐴 + 1 ) → ( ( [ ( 𝑎 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] 𝜑 ) ↔ ( [ ( ( 𝐴 + 1 ) − 1 ) / 𝑥 ] 𝜑 ∧ [ ( 𝐴 + 1 ) / 𝑥 ] 𝜑 ) ) )
27		ovex	⊢ ( 1 − 1 ) ∈ V
28		1m1e0	⊢ ( 1 − 1 ) = 0
29	28	eqeq2i	⊢ ( 𝑥 = ( 1 − 1 ) ↔ 𝑥 = 0 )
30	29 4	sylbi	⊢ ( 𝑥 = ( 1 − 1 ) → ( 𝜑 ↔ 𝜓 ) )
31	27 30	sbcie	⊢ ( [ ( 1 − 1 ) / 𝑥 ] 𝜑 ↔ 𝜓 )
32	1 31	mpbir	⊢ [ ( 1 − 1 ) / 𝑥 ] 𝜑
33		1ex	⊢ 1 ∈ V
34	33 5	sbcie	⊢ ( [ 1 / 𝑥 ] 𝜑 ↔ 𝜒 )
35	2 34	mpbir	⊢ [ 1 / 𝑥 ] 𝜑
36	32 35	pm3.2i	⊢ ( [ ( 1 − 1 ) / 𝑥 ] 𝜑 ∧ [ 1 / 𝑥 ] 𝜑 )
37		simprr	⊢ ( ( 𝑦 ∈ ℕ ∧ ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → [ 𝑦 / 𝑥 ] 𝜑 )
38		nncn	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
39		ax-1cn	⊢ 1 ∈ ℂ
40		pncan	⊢ ( ( 𝑦 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑦 + 1 ) − 1 ) = 𝑦 )
41	38 39 40	sylancl	⊢ ( 𝑦 ∈ ℕ → ( ( 𝑦 + 1 ) − 1 ) = 𝑦 )
42	41	adantr	⊢ ( ( 𝑦 ∈ ℕ ∧ ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → ( ( 𝑦 + 1 ) − 1 ) = 𝑦 )
43	42	sbceq1d	⊢ ( ( 𝑦 ∈ ℕ ∧ ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → ( [ ( ( 𝑦 + 1 ) − 1 ) / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
44	37 43	mpbird	⊢ ( ( 𝑦 ∈ ℕ ∧ ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → [ ( ( 𝑦 + 1 ) − 1 ) / 𝑥 ] 𝜑 )
45		ovex	⊢ ( 𝑦 − 1 ) ∈ V
46	45 6	sbcie	⊢ ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ↔ 𝜃 )
47		vex	⊢ 𝑦 ∈ V
48	47 7	sbcie	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜏 )
49	46 48	anbi12i	⊢ ( ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜃 ∧ 𝜏 ) )
50		ovex	⊢ ( 𝑦 + 1 ) ∈ V
51	50 8	sbcie	⊢ ( [ ( 𝑦 + 1 ) / 𝑥 ] 𝜑 ↔ 𝜂 )
52	3 49 51	3imtr4g	⊢ ( 𝑦 ∈ ℕ → ( ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → [ ( 𝑦 + 1 ) / 𝑥 ] 𝜑 ) )
53	52	imp	⊢ ( ( 𝑦 ∈ ℕ ∧ ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → [ ( 𝑦 + 1 ) / 𝑥 ] 𝜑 )
54	44 53	jca	⊢ ( ( 𝑦 ∈ ℕ ∧ ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) → ( [ ( ( 𝑦 + 1 ) − 1 ) / 𝑥 ] 𝜑 ∧ [ ( 𝑦 + 1 ) / 𝑥 ] 𝜑 ) )
55	54	ex	⊢ ( 𝑦 ∈ ℕ → ( ( [ ( 𝑦 − 1 ) / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ( [ ( ( 𝑦 + 1 ) − 1 ) / 𝑥 ] 𝜑 ∧ [ ( 𝑦 + 1 ) / 𝑥 ] 𝜑 ) ) )
56	14 18 22 26 36 55	nnind	⊢ ( ( 𝐴 + 1 ) ∈ ℕ → ( [ ( ( 𝐴 + 1 ) − 1 ) / 𝑥 ] 𝜑 ∧ [ ( 𝐴 + 1 ) / 𝑥 ] 𝜑 ) )
57	10 56	syl	⊢ ( 𝐴 ∈ ℕ0 → ( [ ( ( 𝐴 + 1 ) − 1 ) / 𝑥 ] 𝜑 ∧ [ ( 𝐴 + 1 ) / 𝑥 ] 𝜑 ) )
58		nn0cn	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ )
59		pncan	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
60	58 39 59	sylancl	⊢ ( 𝐴 ∈ ℕ0 → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
61	60	sbceq1d	⊢ ( 𝐴 ∈ ℕ0 → ( [ ( ( 𝐴 + 1 ) − 1 ) / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
62	61	biimpa	⊢ ( ( 𝐴 ∈ ℕ0 ∧ [ ( ( 𝐴 + 1 ) − 1 ) / 𝑥 ] 𝜑 ) → [ 𝐴 / 𝑥 ] 𝜑 )
63	62	adantrr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( [ ( ( 𝐴 + 1 ) − 1 ) / 𝑥 ] 𝜑 ∧ [ ( 𝐴 + 1 ) / 𝑥 ] 𝜑 ) ) → [ 𝐴 / 𝑥 ] 𝜑 )
64	57 63	mpdan	⊢ ( 𝐴 ∈ ℕ0 → [ 𝐴 / 𝑥 ] 𝜑 )
65	9	sbcieg	⊢ ( 𝐴 ∈ ℕ0 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜌 ) )
66	64 65	mpbid	⊢ ( 𝐴 ∈ ℕ0 → 𝜌 )