Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem uzind 4603

Description: Induction on the upper partition of ℤ that starts at an integer B. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction hypothesis.

Warning: The HTML proof page is 3/4 megabyte in size. An attempt to shorten it is on my to-do list.

**Hypotheses**
Ref	Expression
uzind.1	⊢ (x = B → (φ ↔ ψ))
uzind.2	⊢ (x = y → (φ ↔ χ))
uzind.3	⊢ (x = (y + 1) → (φ ↔ θ))
uzind.4	⊢ (x = A → (φ ↔ τ))
uzind.5	⊢ ψ
uzind.6	⊢ (((y ∈ ℤ ∧ B ∈ ℤ) ∧ B ≤ y) → (χ → θ))

**Assertion**
Ref	Expression
uzind	⊢ (((A ∈ ℤ ∧ B ∈ ℤ) ∧ B ≤ A) → τ)

Distinct variable group(s): x,A ψ,x χ,x θ,x τ,x φ,y x,y,B

**Proof of Theorem uzind**
Step	Hyp	Ref	Expression
1		leadd2t 4351	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ ((A − B) + 1) ∈ ℝ ∧ (B − 1) ∈ ℝ) → (1 ≤ ((A − B) + 1) ↔ ((B − 1) + 1) ≤ ((B − 1) + ((A − B) + 1))))
2		ax1re 4064	. . . . . . 7 ⊢ 1 ∈ ℝ
3	2	a1i 7	. . . . . 6 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → 1 ∈ ℝ)
4		resubclt 4173	. . . . . . . 8 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A − B) ∈ ℝ)
5	4, 2	jctir 241	. . . . . . 7 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A − B) ∈ ℝ ∧ 1 ∈ ℝ))
6		axaddrcl 4067	. . . . . . 7 ⊢ (((A − B) ∈ ℝ ∧ 1 ∈ ℝ) → ((A − B) + 1) ∈ ℝ)
7	5, 6	syl 12	. . . . . 6 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A − B) + 1) ∈ ℝ)
8		resubclt 4173	. . . . . . . 8 ⊢ ((B ∈ ℝ ∧ 1 ∈ ℝ) → (B − 1) ∈ ℝ)
9	2, 8	mpan2 519	. . . . . . 7 ⊢ (B ∈ ℝ → (B − 1) ∈ ℝ)
10	9	adantl 305	. . . . . 6 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (B − 1) ∈ ℝ)
11	1, 3, 7, 10	syl3anc 629	. . . . 5 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (1 ≤ ((A − B) + 1) ↔ ((B − 1) + 1) ≤ ((B − 1) + ((A − B) + 1))))
12		1cn 4101	. . . . . . . . 9 ⊢ 1 ∈ ℂ
13		npcant 4162	. . . . . . . . 9 ⊢ ((B ∈ ℂ ∧ 1 ∈ ℂ) → ((B − 1) + 1) = B)
14	12, 13	mpan2 519	. . . . . . . 8 ⊢ (B ∈ ℂ → ((B − 1) + 1) = B)
15	14	adantl 305	. . . . . . 7 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((B − 1) + 1) = B)
16		add12t 4125	. . . . . . . . 9 ⊢ (((B − 1) ∈ ℂ ∧ (A − B) ∈ ℂ ∧ 1 ∈ ℂ) → ((B − 1) + ((A − B) + 1)) = ((A − B) + ((B − 1) + 1)))
17		subclt 4140	. . . . . . . . . . 11 ⊢ ((B ∈ ℂ ∧ 1 ∈ ℂ) → (B − 1) ∈ ℂ)
18	12, 17	mpan2 519	. . . . . . . . . 10 ⊢ (B ∈ ℂ → (B − 1) ∈ ℂ)
19	18	adantl 305	. . . . . . . . 9 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (B − 1) ∈ ℂ)
20		subclt 4140	. . . . . . . . 9 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A − B) ∈ ℂ)
21	12	a1i 7	. . . . . . . . 9 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → 1 ∈ ℂ)
22	16, 19, 20, 21	syl3anc 629	. . . . . . . 8 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((B − 1) + ((A − B) + 1)) = ((A − B) + ((B − 1) + 1)))
23	14	opreq2d 3013	. . . . . . . . 9 ⊢ (B ∈ ℂ → ((A − B) + ((B − 1) + 1)) = ((A − B) + B))
24	23	adantl 305	. . . . . . . 8 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A − B) + ((B − 1) + 1)) = ((A − B) + B))
25		npcant 4162	. . . . . . . 8 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A − B) + B) = A)
26	22, 24, 25	3eqtrd 1132	. . . . . . 7 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((B − 1) + ((A − B) + 1)) = A)
27	15, 26	breq12d 2073	. . . . . 6 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (((B − 1) + 1) ≤ ((B − 1) + ((A − B) + 1)) ↔ B ≤ A))
28		recnt 4097	. . . . . 6 ⊢ (A ∈ ℝ → A ∈ ℂ)
29		recnt 4097	. . . . . 6 ⊢ (B ∈ ℝ → B ∈ ℂ)
30	27, 28, 29	syl2an 349	. . . . 5 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (((B − 1) + 1) ≤ ((B − 1) + ((A − B) + 1)) ↔ B ≤ A))
31	11, 30	bitr2d 407	. . . 4 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (B ≤ A ↔ 1 ≤ ((A − B) + 1)))
32		zret 4567	. . . 4 ⊢ (A ∈ ℤ → A ∈ ℝ)
33		zret 4567	. . . 4 ⊢ (B ∈ ℤ → B ∈ ℝ)
34	31, 32, 33	syl2an 349	. . 3 ⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (B ≤ A ↔ 1 ≤ ((A − B) + 1)))
35		zsubclt 4591	. . . . 5 ⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A − B) ∈ ℤ)
36		1z 4584	. . . . . 6 ⊢ 1 ∈ ℤ
37		zaddclt 4590	. . . . . 6 ⊢ (((A − B) ∈ ℤ ∧ 1 ∈ ℤ) → ((A − B) + 1) ∈ ℤ)
38	36, 37	mpan2 519	. . . . 5 ⊢ ((A − B) ∈ ℤ → ((A − B) + 1) ∈ ℤ)
39	35, 38	syl 12	. . . 4 ⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → ((A − B) + 1) ∈ ℤ)
40		elnnz1 4581	. . . . . . . 8 ⊢ (((A − B) + 1) ∈ ℕ ↔ (((A − B) + 1) ∈ ℤ ∧ 1 ≤ ((A − B) + 1)))
41		eleq1 1149	. . . . . . . . . 10 ⊢ (z = 1 → (z ∈ ℤ ↔ 1 ∈ ℤ))
42		oprex 3018	. . . . . . . . . . . . . . 15 ⊢ ((z − 1) + B) ∈ V
43	42	isseti 1352	. . . . . . . . . . . . . 14 ⊢ ∃x x = ((z − 1) + B)
44		ax-17 925	. . . . . . . . . . . . . . . 16 ⊢ ((z = 1 ∧ B ∈ ℤ) → ∀x(z = 1 ∧ B ∈ ℤ))
45	42	hbsbcv 1447	. . . . . . . . . . . . . . . . 17 ⊢ ([((z − 1) + B) / x]φ → ∀x[((z − 1) + B) / x]φ)
46		ax-17 925	. . . . . . . . . . . . . . . . 17 ⊢ (ψ → ∀xψ)
47	45, 46	hbbi 705	. . . . . . . . . . . . . . . 16 ⊢ (([((z − 1) + B) / x]φ ↔ ψ) → ∀x([((z − 1) + B) / x]φ ↔ ψ))
48	44, 47	hbim 702	. . . . . . . . . . . . . . 15 ⊢ (((z = 1 ∧ B ∈ ℤ) → ([((z − 1) + B) / x]φ ↔ ψ)) → ∀x((z = 1 ∧ B ∈ ℤ) → ([((z − 1) + B) / x]φ ↔ ψ)))
49		sbceq1 1443	. . . . . . . . . . . . . . . . . 18 ⊢ (x = ((z − 1) + B) → (φ ↔ [((z − 1) + B) / x]φ))
50	49	adantr 306	. . . . . . . . . . . . . . . . 17 ⊢ ((x = ((z − 1) + B) ∧ (z = 1 ∧ B ∈ ℤ)) → (φ ↔ [((z − 1) + B) / x]φ))
51		cleqtr 1118	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x = ((z − 1) + B) ∧ ((z − 1) + B) = B) → x = B)
52		opreq1 3006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z = 1 → (z − 1) = (1 − 1))
53	52	opreq1d 3012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z = 1 → ((z − 1) + B) = ((1 − 1) + B))
54		zcnt 4568	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (B ∈ ℤ → B ∈ ℂ)
55		addid2t 4132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (B ∈ ℂ → (0 + B) = B)
56	54, 55	syl 12	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (B ∈ ℤ → (0 + B) = B)
57	12	subid 4155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − 1) = 0
58	57	opreq1i 3009	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 − 1) + B) = (0 + B)
59	56, 58	syl5eq 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ (B ∈ ℤ → ((1 − 1) + B) = B)
60	53, 59	sylan9eq 1144	. . . . . . . . . . . . . . . . . . 19 ⊢ ((z = 1 ∧ B ∈ ℤ) → ((z − 1) + B) = B)
61	51, 60	sylan2 346	. . . . . . . . . . . . . . . . . 18 ⊢ ((x = ((z − 1) + B) ∧ (z = 1 ∧ B ∈ ℤ)) → x = B)
62		uzind.1	. . . . . . . . . . . . . . . . . 18 ⊢ (x = B → (φ ↔ ψ))
63	61, 62	syl 12	. . . . . . . . . . . . . . . . 17 ⊢ ((x = ((z − 1) + B) ∧ (z = 1 ∧ B ∈ ℤ)) → (φ ↔ ψ))
64	50, 63	bitr3d 408	. . . . . . . . . . . . . . . 16 ⊢ ((x = ((z − 1) + B) ∧ (z = 1 ∧ B ∈ ℤ)) → ([((z − 1) + B) / x]φ ↔ ψ))
65	64	exp 291	. . . . . . . . . . . . . . 15 ⊢ (x = ((z − 1) + B) → ((z = 1 ∧ B ∈ ℤ) → ([((z − 1) + B) / x]φ ↔ ψ)))
66	48, 65	19.23ai 746	. . . . . . . . . . . . . 14 ⊢ (∃x x = ((z − 1) + B) → ((z = 1 ∧ B ∈ ℤ) → ([((z − 1) + B) / x]φ ↔ ψ)))
67	43, 66	ax-mp 6	. . . . . . . . . . . . 13 ⊢ ((z = 1 ∧ B ∈ ℤ) → ([((z − 1) + B) / x]φ ↔ ψ))
68	67	exp 291	. . . . . . . . . . . 12 ⊢ (z = 1 → (B ∈ ℤ → ([((z − 1) + B) / x]φ ↔ ψ)))
69	68	adantld 307	. . . . . . . . . . 11 ⊢ (z = 1 → ((A ∈ ℤ ∧ B ∈ ℤ) → ([((z − 1) + B) / x]φ ↔ ψ)))
70	69	pm5.74d 444	. . . . . . . . . 10 ⊢ (z = 1 → (((A ∈ ℤ ∧ B ∈ ℤ) → [((z − 1) + B) / x]φ) ↔ ((A ∈ ℤ ∧ B ∈ ℤ) → ψ)))
71	41, 70	imbi12d 474	. . . . . . . . 9 ⊢ (z = 1 → ((z ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → [((z − 1) + B) / x]φ)) ↔ (1 ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → ψ))))
72		eleq1 1149	. . . . . . . . . 10 ⊢ (z = w → (z ∈ ℤ ↔ w ∈ ℤ))
73		oprex 3018	. . . . . . . . . . . . 13 ⊢ ((w − 1) + B) ∈ V
74	73	isseti 1352	. . . . . . . . . . . 12 ⊢ ∃y y = ((w − 1) + B)
75		eeanv 980	. . . . . . . . . . . . 13 ⊢ (∃x∃y(x = ((z − 1) + B) ∧ y = ((w − 1) + B)) ↔ (∃x x = ((z − 1) + B) ∧ ∃y y = ((w − 1) + B)))
76		ax-17 925	. . . . . . . . . . . . . . 15 ⊢ (z = w → ∀x z = w)
77		ax-17 925	. . . . . . . . . . . . . . . 16 ⊢ ([((w − 1) + B) / y]χ → ∀x[((w − 1) + B) / y]χ)
78	45, 77	hbbi 705	. . . . . . . . . . . . . . 15 ⊢ (([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ) → ∀x([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ))
79	76, 78	hbim 702	. . . . . . . . . . . . . 14 ⊢ ((z = w → ([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ)) → ∀x(z = w → ([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ)))
80		ax-17 925	. . . . . . . . . . . . . . . 16 ⊢ (z = w → ∀y z = w)
81		ax-17 925	. . . . . . . . . . . . . . . . 17 ⊢ ([((z − 1) + B) / x]φ → ∀y[((z − 1) + B) / x]φ)
82	73	hbsbcv 1447	. . . . . . . . . . . . . . . . 17 ⊢ ([((w − 1) + B) / y]χ → ∀y[((w − 1) + B) / y]χ)
83	81, 82	hbbi 705	. . . . . . . . . . . . . . . 16 ⊢ (([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ) → ∀y([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ))
84	80, 83	hbim 702	. . . . . . . . . . . . . . 15 ⊢ ((z = w → ([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ)) → ∀y(z = w → ([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ)))
85		cleq12 1113	. . . . . . . . . . . . . . . . . 18 ⊢ ((x = ((z − 1) + B) ∧ y = ((w − 1) + B)) → (x = y ↔ ((z − 1) + B) = ((w − 1) + B)))
86		opreq1 3006	. . . . . . . . . . . . . . . . . . 19 ⊢ (z = w → (z − 1) = (w − 1))
87	86	opreq1d 3012	. . . . . . . . . . . . . . . . . 18 ⊢ (z = w → ((z − 1) + B) = ((w − 1) + B))
88	85, 87	syl5bir 184	. . . . . . . . . . . . . . . . 17 ⊢ ((x = ((z − 1) + B) ∧ y = ((w − 1) + B)) → (z = w → x = y))
89		uzind.2	. . . . . . . . . . . . . . . . 17 ⊢ (x = y → (φ ↔ χ))
90	88, 89	syl6 23	. . . . . . . . . . . . . . . 16 ⊢ ((x = ((z − 1) + B) ∧ y = ((w − 1) + B)) → (z = w → (φ ↔ χ)))
91		sbceq1 1443	. . . . . . . . . . . . . . . . 17 ⊢ (y = ((w − 1) + B) → (χ ↔ [((w − 1) + B) / y]χ))
92	49, 91	bi2bian9 480	. . . . . . . . . . . . . . . 16 ⊢ ((x = ((z − 1) + B) ∧ y = ((w − 1) + B)) → ((φ ↔ χ) ↔ ([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ)))
93	90, 92	sylibd 177	. . . . . . . . . . . . . . 15 ⊢ ((x = ((z − 1) + B) ∧ y = ((w − 1) + B)) → (z = w → ([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ)))
94	84, 93	19.23ai 746	. . . . . . . . . . . . . 14 ⊢ (∃y(x = ((z − 1) + B) ∧ y = ((w − 1) + B)) → (z = w → ([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ)))
95	79, 94	19.23ai 746	. . . . . . . . . . . . 13 ⊢ (∃x∃y(x = ((z − 1) + B) ∧ y = ((w − 1) + B)) → (z = w → ([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ)))
96	75, 95	sylbir 176	. . . . . . . . . . . 12 ⊢ ((∃x x = ((z − 1) + B) ∧ ∃y y = ((w − 1) + B)) → (z = w → ([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ)))
97	43, 74, 96	mp2an 520	. . . . . . . . . . 11 ⊢ (z = w → ([((z − 1) + B) / x]φ ↔ [((w − 1) + B) / y]χ))
98	97	imbi2d 464	. . . . . . . . . 10 ⊢ (z = w → (((A ∈ ℤ ∧ B ∈ ℤ) → [((z − 1) + B) / x]φ) ↔ ((A ∈ ℤ ∧ B ∈ ℤ) → [((w − 1) + B) / y]χ)))
99	72, 98	imbi12d 474	. . . . . . . . 9 ⊢ (z = w → ((z ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → [((z − 1) + B) / x]φ)) ↔ (w ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → [((w − 1) + B) / y]χ))))
100		eleq1 1149	. . . . . . . . . . 11 ⊢ (z = (w + 1) → (z ∈ ℤ ↔ (w + 1) ∈ ℤ))
101		oprex 3018	. . . . . . . . . . . . . 14 ⊢ ((((z − 1) + B) − 1) + 1) ∈ V
102	101	isseti 1352	. . . . . . . . . . . . 13 ⊢ ∃x x = ((((z − 1) + B) − 1) + 1)
103		oprex 3018	. . . . . . . . . . . . . 14 ⊢ ((((w + 1) − 1) + B) − 1) ∈ V
104	103	isseti 1352	. . . . . . . . . . . . 13 ⊢ ∃y y = ((((w + 1) − 1) + B) − 1)
105		eeanv 980	. . . . . . . . . . . . . 14 ⊢ (∃x∃y(x = ((((z − 1) + B) − 1) + 1) ∧ y = ((((w + 1) − 1) + B) − 1)) ↔ (∃x x = ((((z − 1) + B) − 1) + 1) ∧ ∃y y = ((((w + 1) − 1) + B) − 1)))
106		ax-17 925	. . . . . . . . . . . . . . . 16 ⊢ (z = (w + 1) → ∀x z = (w + 1))
107	101	hbsbcv 1447	. . . . . . . . . . . . . . . . 17 ⊢ ([((((z − 1) + B) − 1) + 1) / x]φ → ∀x[((((z − 1) + B) − 1) + 1) / x]φ)
108		ax-17 925	. . . . . . . . . . . . . . . . 17 ⊢ ([((((w + 1) − 1) + B) − 1) / y]θ → ∀x[((((w + 1) − 1) + B) − 1) / y]θ)
109	107, 108	hbbi 705	. . . . . . . . . . . . . . . 16 ⊢ (([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ) → ∀x([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ))
110	106, 109	hbim 702	. . . . . . . . . . . . . . 15 ⊢ ((z = (w + 1) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ)) → ∀x(z = (w + 1) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ)))
111		ax-17 925	. . . . . . . . . . . . . . . . 17 ⊢ (z = (w + 1) → ∀y z = (w + 1))
112		ax-17 925	. . . . . . . . . . . . . . . . . 18 ⊢ ([((((z − 1) + B) − 1) + 1) / x]φ → ∀y[((((z − 1) + B) − 1) + 1) / x]φ)
113	103	hbsbcv 1447	. . . . . . . . . . . . . . . . . 18 ⊢ ([((((w + 1) − 1) + B) − 1) / y]θ → ∀y[((((w + 1) − 1) + B) − 1) / y]θ)
114	112, 113	hbbi 705	. . . . . . . . . . . . . . . . 17 ⊢ (([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ) → ∀y([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ))
115	111, 114	hbim 702	. . . . . . . . . . . . . . . 16 ⊢ ((z = (w + 1) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ)) → ∀y(z = (w + 1) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ)))
116		cleq12 1113	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((x = ((((z − 1) + B) − 1) + 1) ∧ (y + 1) = (((((w + 1) − 1) + B) − 1) + 1)) → (x = (y + 1) ↔ ((((z − 1) + B) − 1) + 1) = (((((w + 1) − 1) + B) − 1) + 1)))
117		opreq1 3006	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = ((((w + 1) − 1) + B) − 1) → (y + 1) = (((((w + 1) − 1) + B) − 1) + 1))
118	116, 117	sylan2 346	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x = ((((z − 1) + B) − 1) + 1) ∧ y = ((((w + 1) − 1) + B) − 1)) → (x = (y + 1) ↔ ((((z − 1) + B) − 1) + 1) = (((((w + 1) − 1) + B) − 1) + 1)))
119		opreq1 3006	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z = (w + 1) → (z − 1) = ((w + 1) − 1))
120	119	opreq1d 3012	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z = (w + 1) → ((z − 1) + B) = (((w + 1) − 1) + B))
121	120	opreq1d 3012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z = (w + 1) → (((z − 1) + B) − 1) = ((((w + 1) − 1) + B) − 1))
122	121	opreq1d 3012	. . . . . . . . . . . . . . . . . . 19 ⊢ (z = (w + 1) → ((((z − 1) + B) − 1) + 1) = (((((w + 1) − 1) + B) − 1) + 1))
123	118, 122	syl5bir 184	. . . . . . . . . . . . . . . . . 18 ⊢ ((x = ((((z − 1) + B) − 1) + 1) ∧ y = ((((w + 1) − 1) + B) − 1)) → (z = (w + 1) → x = (y + 1)))
124		uzind.3	. . . . . . . . . . . . . . . . . 18 ⊢ (x = (y + 1) → (φ ↔ θ))
125	123, 124	syl6 23	. . . . . . . . . . . . . . . . 17 ⊢ ((x = ((((z − 1) + B) − 1) + 1) ∧ y = ((((w + 1) − 1) + B) − 1)) → (z = (w + 1) → (φ ↔ θ)))
126		sbceq1 1443	. . . . . . . . . . . . . . . . . 18 ⊢ (x = ((((z − 1) + B) − 1) + 1) → (φ ↔ [((((z − 1) + B) − 1) + 1) / x]φ))
127		sbceq1 1443	. . . . . . . . . . . . . . . . . 18 ⊢ (y = ((((w + 1) − 1) + B) − 1) → (θ ↔ [((((w + 1) − 1) + B) − 1) / y]θ))
128	126, 127	bi2bian9 480	. . . . . . . . . . . . . . . . 17 ⊢ ((x = ((((z − 1) + B) − 1) + 1) ∧ y = ((((w + 1) − 1) + B) − 1)) → ((φ ↔ θ) ↔ ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ)))
129	125, 128	sylibd 177	. . . . . . . . . . . . . . . 16 ⊢ ((x = ((((z − 1) + B) − 1) + 1) ∧ y = ((((w + 1) − 1) + B) − 1)) → (z = (w + 1) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ)))
130	115, 129	19.23ai 746	. . . . . . . . . . . . . . 15 ⊢ (∃y(x = ((((z − 1) + B) − 1) + 1) ∧ y = ((((w + 1) − 1) + B) − 1)) → (z = (w + 1) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ)))
131	110, 130	19.23ai 746	. . . . . . . . . . . . . 14 ⊢ (∃x∃y(x = ((((z − 1) + B) − 1) + 1) ∧ y = ((((w + 1) − 1) + B) − 1)) → (z = (w + 1) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ)))
132	105, 131	sylbir 176	. . . . . . . . . . . . 13 ⊢ ((∃x x = ((((z − 1) + B) − 1) + 1) ∧ ∃y y = ((((w + 1) − 1) + B) − 1)) → (z = (w + 1) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ)))
133	102, 104, 132	mp2an 520	. . . . . . . . . . . 12 ⊢ (z = (w + 1) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((((w + 1) − 1) + B) − 1) / y]θ))
134	133	imbi2d 464	. . . . . . . . . . 11 ⊢ (z = (w + 1) → (((A ∈ ℤ ∧ B ∈ ℤ) → [((((z − 1) + B) − 1) + 1) / x]φ) ↔ ((A ∈ ℤ ∧ B ∈ ℤ) → [((((w + 1) − 1) + B) − 1) / y]θ)))
135	100, 134	imbi12d 474	. . . . . . . . . 10 ⊢ (z = (w + 1) → ((z ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → [((((z − 1) + B) − 1) + 1) / x]φ)) ↔ ((w + 1) ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → [((((w + 1) − 1) + B) − 1) / y]θ))))
136		axaddcl 4066	. . . . . . . . . . . . . . . . . 18 ⊢ (((z − 1) ∈ ℂ ∧ B ∈ ℂ) → ((z − 1) + B) ∈ ℂ)
137		subclt 4140	. . . . . . . . . . . . . . . . . . 19 ⊢ ((z ∈ ℂ ∧ 1 ∈ ℂ) → (z − 1) ∈ ℂ)
138	12, 137	mpan2 519	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ ℂ → (z − 1) ∈ ℂ)
139	136, 138	sylan 343	. . . . . . . . . . . . . . . . 17 ⊢ ((z ∈ ℂ ∧ B ∈ ℂ) → ((z − 1) + B) ∈ ℂ)
140		npcant 4162	. . . . . . . . . . . . . . . . . 18 ⊢ ((((z − 1) + B) ∈ ℂ ∧ 1 ∈ ℂ) → ((((z − 1) + B) − 1) + 1) = ((z − 1) + B))
141	12, 140	mpan2 519	. . . . . . . . . . . . . . . . 17 ⊢ (((z − 1) + B) ∈ ℂ → ((((z − 1) + B) − 1) + 1) = ((z − 1) + B))
142	139, 141	syl 12	. . . . . . . . . . . . . . . 16 ⊢ ((z ∈ ℂ ∧ B ∈ ℂ) → ((((z − 1) + B) − 1) + 1) = ((z − 1) + B))
143		zcnt 4568	. . . . . . . . . . . . . . . 16 ⊢ (z ∈ ℤ → z ∈ ℂ)
144	142, 143, 54	syl2an 349	. . . . . . . . . . . . . . 15 ⊢ ((z ∈ ℤ ∧ B ∈ ℤ) → ((((z − 1) + B) − 1) + 1) = ((z − 1) + B))
145	144	exp 291	. . . . . . . . . . . . . 14 ⊢ (z ∈ ℤ → (B ∈ ℤ → ((((z − 1) + B) − 1) + 1) = ((z − 1) + B)))
146	145	adantld 307	. . . . . . . . . . . . 13 ⊢ (z ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → ((((z − 1) + B) − 1) + 1) = ((z − 1) + B)))
147		dfsbcq 1442	. . . . . . . . . . . . 13 ⊢ (((((z − 1) + B) − 1) + 1) = ((z − 1) + B) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((z − 1) + B) / x]φ))
148	146, 147	syl6 23	. . . . . . . . . . . 12 ⊢ (z ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → ([((((z − 1) + B) − 1) + 1) / x]φ ↔ [((z − 1) + B) / x]φ)))
149	148	pm5.74d 444	. . . . . . . . . . 11 ⊢ (z ∈ ℤ → (((A ∈ ℤ ∧ B ∈ ℤ) → [((((z − 1) + B) − 1) + 1) / x]φ) ↔ ((A ∈ ℤ ∧ B ∈ ℤ) → [((z − 1) + B) / x]φ)))
150	149	pm5.74i 443	. . . . . . . . . 10 ⊢ ((z ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → [((((z − 1) + B) − 1) + 1) / x]φ)) ↔ (z ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → [((z − 1) + B) / x]φ)))
151	135, 150	syl5bbr 412	. . . . . . . . 9 ⊢ (z = (w + 1) → ((z ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → [((z − 1) + B) / x]φ)) ↔ ((w + 1) ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → [((((w + 1) − 1) + B) − 1) / y]θ))))
152		eleq1 1149	. . . . . . . . . 10 ⊢ (z = ((A − B) + 1) → (z ∈ ℤ ↔ ((A − B) + 1) ∈ ℤ))
153		ax-17 925	. . . . . . . . . . . . . . 15 ⊢ ((z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ)) → ∀x(z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ)))
154		ax-17 925	. . . . . . . . . . . . . . . 16 ⊢ (τ → ∀xτ)
155	45, 154	hbbi 705	. . . . . . . . . . . . . . 15 ⊢ (([((z − 1) + B) / x]φ ↔ τ) → ∀x([((z − 1) + B) / x]φ ↔ τ))
156	153, 155	hbim 702	. . . . . . . . . . . . . 14 ⊢ (((z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ)) → ([((z − 1) + B) / x]φ ↔ τ)) → ∀x((z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ)) → ([((z − 1) + B) / x]φ ↔ τ)))
157	49	adantr 306	. . . . . . . . . . . . . . . 16 ⊢ ((x = ((z − 1) + B) ∧ (z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ))) → (φ ↔ [((z − 1) + B) / x]φ))
158		cleqtr 1118	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((x = ((z − 1) + B) ∧ ((z − 1) + B) = ((((A − B) + 1) − 1) + B)) → x = ((((A − B) + 1) − 1) + B))
159		opreq1 3006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z = ((A − B) + 1) → (z − 1) = (((A − B) + 1) − 1))
160	159	opreq1d 3012	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z = ((A − B) + 1) → ((z − 1) + B) = ((((A − B) + 1) − 1) + B))
161	158, 160	sylan2 346	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x = ((z − 1) + B) ∧ z = ((A − B) + 1)) → x = ((((A − B) + 1) − 1) + B))
162		add23t 4126	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((A − B) ∈ ℂ ∧ 1 ∈ ℂ ∧ B ∈ ℂ) → (((A − B) + 1) + B) = (((A − B) + B) + 1))
163		pm3.27 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → B ∈ ℂ)
164	162, 20, 21, 163	syl3anc 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (((A − B) + 1) + B) = (((A − B) + B) + 1))
165	25	opreq1d 3012	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (((A − B) + B) + 1) = (A + 1))
166	164, 165	eqtrd 1128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (((A − B) + 1) + B) = (A + 1))
167	166	opreq1d 3012	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((((A − B) + 1) + B) − 1) = ((A + 1) − 1))
168		addsubt 4151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((A − B) + 1) ∈ ℂ ∧ B ∈ ℂ ∧ 1 ∈ ℂ) → ((((A − B) + 1) + B) − 1) = ((((A − B) + 1) − 1) + B))
169		axaddcl 4066	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((A − B) ∈ ℂ ∧ 1 ∈ ℂ) → ((A − B) + 1) ∈ ℂ)
170	12, 169	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((A − B) ∈ ℂ → ((A − B) + 1) ∈ ℂ)
171	20, 170	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A − B) + 1) ∈ ℂ)
172	168, 171, 163, 21	syl3anc 629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((((A − B) + 1) + B) − 1) = ((((A − B) + 1) − 1) + B))
173		pncant 4161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((A ∈ ℂ ∧ 1 ∈ ℂ) → ((A + 1) − 1) = A)
174	12, 173	mpan2 519	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (A ∈ ℂ → ((A + 1) − 1) = A)
175	174	adantr 306	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A + 1) − 1) = A)
176	167, 172, 175	3eqtr3d 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((((A − B) + 1) − 1) + B) = A)
177		zcnt 4568	. . . . . . . . . . . . . . . . . . . 20 ⊢ (A ∈ ℤ → A ∈ ℂ)
178	176, 177, 54	syl2an 349	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → ((((A − B) + 1) − 1) + B) = A)
179	161, 178	sylan9eq 1144	. . . . . . . . . . . . . . . . . 18 ⊢ (((x = ((z − 1) + B) ∧ z = ((A − B) + 1)) ∧ (A ∈ ℤ ∧ B ∈ ℤ)) → x = A)
180	179	anasss 337	. . . . . . . . . . . . . . . . 17 ⊢ ((x = ((z − 1) + B) ∧ (z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ))) → x = A)
181		uzind.4	. . . . . . . . . . . . . . . . 17 ⊢ (x = A → (φ ↔ τ))
182	180, 181	syl 12	. . . . . . . . . . . . . . . 16 ⊢ ((x = ((z − 1) + B) ∧ (z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ))) → (φ ↔ τ))
183	157, 182	bitr3d 408	. . . . . . . . . . . . . . 15 ⊢ ((x = ((z − 1) + B) ∧ (z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ))) → ([((z − 1) + B) / x]φ ↔ τ))
184	183	exp 291	. . . . . . . . . . . . . 14 ⊢ (x = ((z − 1) + B) → ((z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ)) → ([((z − 1) + B) / x]φ ↔ τ)))
185	156, 184	19.23ai 746	. . . . . . . . . . . . 13 ⊢ (∃x x = ((z − 1) + B) → ((z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ)) → ([((z − 1) + B) / x]φ ↔ τ)))
186	43, 185	ax-mp 6	. . . . . . . . . . . 12 ⊢ ((z = ((A − B) + 1) ∧ (A ∈ ℤ ∧ B ∈ ℤ)) → ([((z − 1) + B) / x]φ ↔ τ))
187	186	exp 291	. . . . . . . . . . 11 ⊢ (z = ((A − B) + 1) → ((A ∈ ℤ ∧ B ∈ ℤ) → ([((z − 1) + B) / x]φ ↔ τ)))
188	187	pm5.74d 444	. . . . . . . . . 10 ⊢ (z = ((A − B) + 1) → (((A ∈ ℤ ∧ B ∈ ℤ) → [((z − 1) + B) / x]φ) ↔ ((A ∈ ℤ ∧ B ∈ ℤ) → τ)))
189	152, 188	imbi12d 474	. . . . . . . . 9 ⊢ (z = ((A − B) + 1) → ((z ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → [((z − 1) + B) / x]φ)) ↔ (((A − B) + 1) ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → τ))))
190		uzind.5	. . . . . . . . . . 11 ⊢ ψ
191	190	a1i 7	. . . . . . . . . 10 ⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → ψ)
192	191	a1i 7	. . . . . . . . 9 ⊢ (1 ∈ ℤ → ((A ∈ ℤ ∧ B ∈ ℤ) → ψ))
193		nnzt 4579	. . . . . . . . . . 11 ⊢ (w ∈ ℕ → w ∈ ℤ)
194	193	a1d 14	. . . . . . . . . 10 ⊢ (w ∈ ℕ → ((w + 1) ∈ ℤ → w ∈ ℤ))
195		ax-17 925	. . . . . . . . . . . . . . . . 17 ⊢ ((w ∈ ℕ ∧ B ∈ ℤ) → ∀y(w ∈ ℕ ∧ B ∈ ℤ))
196	73	hbsbcv 1447	. . . . . . . . . . . . . . . . . 18 ⊢ ([((w − 1) + B) / y]θ → ∀y[((w − 1) + B) / y]θ)
197	82, 196	hbim 702	. . . . . . . . . . . . . . . . 17 ⊢ (([((w − 1) + B) / y]χ → [((w − 1) + B) / y]θ) → ∀y([((w − 1) + B) / y]χ → [((w − 1) + B) / y]θ))
198	195, 197	hbim 702	. . . . . . . . . . . . . . . 16 ⊢ (((w ∈ ℕ ∧ B ∈ ℤ) → ([((w − 1) + B) / y]χ → [((w − 1) + B) / y]θ)) → ∀y((w ∈ ℕ ∧ B ∈ ℤ) → ([((w − 1) + B) / y]χ → [((w − 1) + B) / y]θ)))
199		uzind.6	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ ℤ ∧ B ∈ ℤ) ∧ B ≤ y) → (χ → θ))
200		eleq1 1149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = ((w − 1) + B) → (y ∈ ℤ ↔ ((w − 1) + B) ∈ ℤ))
201	200	anbi1d 469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = ((w − 1) + B) → ((y ∈ ℤ ∧ B ∈ ℤ) ↔ (((w − 1) + B) ∈ ℤ ∧ B ∈ ℤ)))
202		breq2 2066	. . . . . . . . . . . . . . . . . . . 20 ⊢ (