Theorem bezoutlemmain 11526

Description: Lemma for Bézout's identity. This is the main result which we prove by induction and which represents the application of the Extended Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.)

Hypotheses

Ref	Expression
bezout.is-bezout	⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))
bezout.sub-gcd	⊢ (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))
bezout.a	⊢ (𝜃 → 𝐴 ∈ ℕ0)
bezout.b	⊢ (𝜃 → 𝐵 ∈ ℕ0)

Assertion

Ref	Expression
bezoutlemmain	⊢ (𝜃 → ∀𝑥 ∈ ℕ0 ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))

Distinct variable groups:   𝜑,𝑠,𝑡,𝑥,𝑦,𝑧   𝜓,𝑠,𝑡,𝑧   𝑠,𝑟,𝑡,𝑥,𝑦,𝑧,𝜃   𝐴,𝑟,𝑠,𝑡   𝐵,𝑟,𝑠,𝑡

Allowed substitution hints:   𝜑(𝑟)   𝜓(𝑥,𝑦,𝑟)   𝐴(𝑥,𝑦,𝑧)   𝐵(𝑥,𝑦,𝑧)

Proof of Theorem bezoutlemmain

Dummy variables 𝑎 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbequ 1792	. . . . . . 7 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑟]𝜑 ↔ [𝑧 / 𝑟]𝜑))
2	1	anbi2d 457	. . . . . 6 ⊢ (𝑤 = 𝑧 → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) ↔ (𝜃 ∧ [𝑧 / 𝑟]𝜑)))
3		sbequ 1792	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
4	3	anbi1d 458	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
5	4	rexbidv 2410	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
6	5	imbi2d 229	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
7	6	ralbidv 2409	. . . . . 6 ⊢ (𝑤 = 𝑧 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
8	2, 7	imbi12d 233	. . . . 5 ⊢ (𝑤 = 𝑧 → (((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))))
9		sbequ 1792	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑟]𝜑 ↔ [𝑥 / 𝑟]𝜑))
10	9	anbi2d 457	. . . . . 6 ⊢ (𝑤 = 𝑥 → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) ↔ (𝜃 ∧ [𝑥 / 𝑟]𝜑)))
11		sbequ12r 1726	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜓 ↔ 𝜓))
12	11	anbi1d 458	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ (𝜓 ∧ 𝜑)))
13	12	rexbidv 2410	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))
14	13	imbi2d 229	. . . . . . 7 ⊢ (𝑤 = 𝑥 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
15	14	ralbidv 2409	. . . . . 6 ⊢ (𝑤 = 𝑥 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
16	10, 15	imbi12d 233	. . . . 5 ⊢ (𝑤 = 𝑥 → (((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [𝑥 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))))
17		nfv 1489	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑤 ∈ ℕ0
18		nfcv 2253	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(0...(𝑤 − 1))
19		nfv 1489	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝜃 ∧ [𝑧 / 𝑟]𝜑)
20		nfra1 2438	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
21	19, 20	nfim 1532	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
22	18, 21	nfralxy 2443	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
23	17, 22	nfan 1525	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
24		nfv 1489	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜃 ∧ [𝑤 / 𝑟]𝜑)
25	23, 24	nfan 1525	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
26		nfv 1489	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑤 = 0
27	25, 26	nfan 1525	. . . . . . . 8 ⊢ Ⅎ𝑦(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0)
28		simplr 502	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑦 ∈ ℕ0)
29		nfv 1489	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))
30		breq2 3897	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑦 → (𝑧 ∥ 𝑟 ↔ 𝑧 ∥ 𝑦))
31	30	imbi1d 230	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑦 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
32	31	ralbidv 2409	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑦 → (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
33	29, 32	sbie 1745	. . . . . . . . . . . . 13 ⊢ ([𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
34		nn0z 8972	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∈ ℤ)
35		dvds0 11350	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℤ → 𝑧 ∥ 0)
36	34, 35	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∥ 0)
37	36	biantrurd 301	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℕ0 → (𝑧 ∥ 𝑦 ↔ (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
38	37	biimpd 143	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℕ0 → (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
39	33, 38	mprgbir 2462	. . . . . . . . . . . 12 ⊢ [𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))
40		nfv 1489	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟 𝑤 = 0
41		dfsbcq2 2879	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 0 → ([𝑤 / 𝑥]𝜓 ↔ [0 / 𝑥]𝜓))
42		bezout.sub-gcd	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))
43	42	sbcbii 2934	. . . . . . . . . . . . . . 15 ⊢ ([0 / 𝑥]𝜓 ↔ [0 / 𝑥]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))
44		c0ex 7678	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ V
45		breq2 3897	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑧 ∥ 𝑥 ↔ 𝑧 ∥ 0))
46	45	anbi1d 458	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → ((𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦) ↔ (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
47	46	imbi2d 229	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
48	47	ralbidv 2409	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
49	44, 48	sbcie 2909	. . . . . . . . . . . . . . 15 ⊢ ([0 / 𝑥]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
50	43, 49	bitri 183	. . . . . . . . . . . . . 14 ⊢ ([0 / 𝑥]𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
51	41, 50	syl6bb 195	. . . . . . . . . . . . 13 ⊢ (𝑤 = 0 → ([𝑤 / 𝑥]𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
52	40, 51	sbbid 1798	. . . . . . . . . . . 12 ⊢ (𝑤 = 0 → ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ↔ [𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
53	39, 52	mpbiri 167	. . . . . . . . . . 11 ⊢ (𝑤 = 0 → [𝑦 / 𝑟][𝑤 / 𝑥]𝜓)
54	53	ad3antlr 482	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟][𝑤 / 𝑥]𝜓)
55		simpr 109	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟]𝜑)
56		nfs1v 1888	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟[𝑦 / 𝑟][𝑤 / 𝑥]𝜓
57		nfs1v 1888	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟[𝑦 / 𝑟]𝜑
58	56, 57	nfan 1525	. . . . . . . . . . 11 ⊢ Ⅎ𝑟([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)
59		sbequ12 1725	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑦 → ([𝑤 / 𝑥]𝜓 ↔ [𝑦 / 𝑟][𝑤 / 𝑥]𝜓))
60		sbequ12 1725	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑟]𝜑))
61	59, 60	anbi12d 462	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑦 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)))
62	58, 61	rspce 2753	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ0 ∧ ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
63	28, 54, 55, 62	syl12anc 1195	. . . . . . . . 9 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
64	63	exp31 359	. . . . . . . 8 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) → (𝑦 ∈ ℕ0 → ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))))
65	27, 64	ralrimi 2475	. . . . . . 7 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
66		nfv 1489	. . . . . . . . . 10 ⊢ Ⅎ𝑦0 < 𝑤
67	25, 66	nfan 1525	. . . . . . . . 9 ⊢ Ⅎ𝑦(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
68		bezout.is-bezout	. . . . . . . . . . 11 ⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))
69		simplrl 507	. . . . . . . . . . . . 13 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝜃)
70		bezout.a	. . . . . . . . . . . . 13 ⊢ (𝜃 → 𝐴 ∈ ℕ0)
71	69, 70	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝐴 ∈ ℕ0)
72	71	ad2antrr 477	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝐴 ∈ ℕ0)
73		bezout.b	. . . . . . . . . . . . 13 ⊢ (𝜃 → 𝐵 ∈ ℕ0)
74	69, 73	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝐵 ∈ ℕ0)
75	74	ad2antrr 477	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝐵 ∈ ℕ0)
76		simplll 505	. . . . . . . . . . . . 13 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝑤 ∈ ℕ0)
77		simpr 109	. . . . . . . . . . . . 13 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 0 < 𝑤)
78		elnnnn0b 8919	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ℕ ↔ (𝑤 ∈ ℕ0 ∧ 0 < 𝑤))
79	76, 77, 78	sylanbrc 411	. . . . . . . . . . . 12 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝑤 ∈ ℕ)
80	79	ad2antrr 477	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑤 ∈ ℕ)
81		simpr 109	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟]𝜑)
82		simplr 502	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑦 ∈ ℕ0)
83		simplrr 508	. . . . . . . . . . . . 13 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → [𝑤 / 𝑟]𝜑)
84		sbsbc 2880	. . . . . . . . . . . . 13 ⊢ ([𝑤 / 𝑟]𝜑 ↔ [𝑤 / 𝑟]𝜑)
85	83, 84	sylib 121	. . . . . . . . . . . 12 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → [𝑤 / 𝑟]𝜑)
86	85	ad2antrr 477	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑤 / 𝑟]𝜑)
87		breq1 3896	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑟 ↔ 𝑎 ∥ 𝑟))
88		breq1 3896	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑥 ↔ 𝑎 ∥ 𝑥))
89		breq1 3896	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑦 ↔ 𝑎 ∥ 𝑦))
90	88, 89	anbi12d 462	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → ((𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦) ↔ (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))
91	87, 90	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦))))
92	91	cbvralv 2626	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑎 ∈ ℕ0 (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))
93	42, 92	bitri 183	. . . . . . . . . . 11 ⊢ (𝜓 ↔ ∀𝑎 ∈ ℕ0 (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))
94	69	ad3antrrr 481	. . . . . . . . . . . . 13 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝜃)
95		simpr 109	. . . . . . . . . . . . 13 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → [(𝑦 mod 𝑤) / 𝑟]𝜑)
96	94, 95	jca 302	. . . . . . . . . . . 12 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → (𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑))
97	83	ad3antrrr 481	. . . . . . . . . . . 12 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → [𝑤 / 𝑟]𝜑)
98		dfsbcq2 2879	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑦 mod 𝑤) → ([𝑧 / 𝑟]𝜑 ↔ [(𝑦 mod 𝑤) / 𝑟]𝜑))
99	98	anbi2d 457	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑦 mod 𝑤) → ((𝜃 ∧ [𝑧 / 𝑟]𝜑) ↔ (𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑)))
100		sbsbc 2880	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
101		sbsbc 2880	. . . . . . . . . . . . . . . . . . . 20 ⊢ ([𝑤 / 𝑦]𝜓 ↔ [𝑤 / 𝑦]𝜓)
102	101	sbcbii 2934	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
103	100, 102	bitri 183	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
104	103	anbi1i 451	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))
105		dfsbcq 2878	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑦 mod 𝑤) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓))
106	105	anbi1d 458	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
107	104, 106	syl5bb 191	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
108	107	rexbidv 2410	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑦 mod 𝑤) → (∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
109	108	imbi2d 229	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)) ↔ ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
110	99, 109	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑦 mod 𝑤) → (((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))))
111		simpll 501	. . . . . . . . . . . . . 14 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → (((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤))
112		simpr 109	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
113	112	ad3antrrr 481	. . . . . . . . . . . . . . 15 ⊢ (((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
114		nfv 1489	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦[𝑤 / 𝑟]𝜑
115		nfcv 2253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦ℕ0
116		nfs1v 1888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜓
117	116	nfsbxy 1891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜓
118		nfv 1489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦𝜑
119	117, 118	nfan 1525	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)
120	115, 119	nfrexxy 2444	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)
121	114, 120	nfim 1532	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))
122		sbequ 1792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → ([𝑦 / 𝑟]𝜑 ↔ [𝑤 / 𝑟]𝜑))
123		nfv 1489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥 𝑦 = 𝑤
124		sbequ12 1725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑦]𝜓))
125	123, 124	sbbid 1798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓))
126	125	anbi1d 458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑤 → (([𝑧 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
127	126	rexbidv 2410	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → (∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
128	122, 127	imbi12d 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑤 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
129	121, 128	rspc 2752	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ0 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
130	129	imim2d 54	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℕ0 → (((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))))
131	130	ralimdv 2472	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℕ0 → (∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))))
132	131	ad4antr 483	. . . . . . . . . . . . . . 15 ⊢ (((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → (∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))))
133	113, 132	mpd 13	. . . . . . . . . . . . . 14 ⊢ (((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
134	111, 133	sylan 279	. . . . . . . . . . . . 13 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
135		simpllr 506	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑦 ∈ ℕ0)
136	135	nn0zd 9069	. . . . . . . . . . . . . 14 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑦 ∈ ℤ)
137	79	ad3antrrr 481	. . . . . . . . . . . . . 14 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑤 ∈ ℕ)
138		zmodfz 10006	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℤ ∧ 𝑤 ∈ ℕ) → (𝑦 mod 𝑤) ∈ (0...(𝑤 − 1)))
139	136, 137, 138	syl2anc 406	. . . . . . . . . . . . 13 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → (𝑦 mod 𝑤) ∈ (0...(𝑤 − 1)))
140	110, 134, 139	rspcdva 2763	. . . . . . . . . . . 12 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ((𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
141	96, 97, 140	mp2d 47	. . . . . . . . . . 11 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))
142		nfv 1489	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ ℕ0
143		nfcv 2253	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(0...(𝑤 − 1))
144		nfv 1489	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝜃 ∧ [𝑧 / 𝑟]𝜑)
145		nfcv 2253	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥ℕ0
146		nfv 1489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝜑
147	146	nfsbxy 1891	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥[𝑦 / 𝑟]𝜑
148		nfs1v 1888	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜓
149	148, 146	nfan 1525	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥([𝑧 / 𝑥]𝜓 ∧ 𝜑)
150	145, 149	nfrexxy 2444	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)
151	147, 150	nfim 1532	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
152	145, 151	nfralxy 2443	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
153	144, 152	nfim 1532	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
154	143, 153	nfralxy 2443	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
155	142, 154	nfan 1525	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
156		nfv 1489	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝜃 ∧ [𝑤 / 𝑟]𝜑)
157	155, 156	nfan 1525	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
158		nfv 1489	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥0 < 𝑤
159	157, 158	nfan 1525	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
160		nfv 1489	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑦 ∈ ℕ0
161	159, 160	nfan 1525	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0)
162	161, 147	nfan 1525	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑)
163		nfv 1489	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟 𝑤 ∈ ℕ0
164		nfcv 2253	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟(0...(𝑤 − 1))
165		nfv 1489	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟𝜃
166		nfs1v 1888	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟[𝑧 / 𝑟]𝜑
167	165, 166	nfan 1525	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟(𝜃 ∧ [𝑧 / 𝑟]𝜑)
168		nfcv 2253	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟ℕ0
169		nfre1 2448	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑟∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)
170	57, 169	nfim 1532	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
171	168, 170	nfralxy 2443	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
172	167, 171	nfim 1532	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
173	164, 172	nfralxy 2443	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
174	163, 173	nfan 1525	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
175		nfs1v 1888	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟[𝑤 / 𝑟]𝜑
176	165, 175	nfan 1525	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟(𝜃 ∧ [𝑤 / 𝑟]𝜑)
177	174, 176	nfan 1525	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
178		nfv 1489	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟0 < 𝑤
179	177, 178	nfan 1525	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
180		nfv 1489	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟 𝑦 ∈ ℕ0
181	179, 180	nfan 1525	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0)
182	181, 57	nfan 1525	. . . . . . . . . . 11 ⊢ Ⅎ𝑟(((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑)
183	68, 72, 75, 80, 81, 82, 86, 93, 141, 162, 182	bezoutlemstep 11525	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
184	183	exp31 359	. . . . . . . . 9 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → (𝑦 ∈ ℕ0 → ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))))
185	67, 184	ralrimi 2475	. . . . . . . 8 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
186		sbsbc 2880	. . . . . . . . . . . 12 ⊢ ([𝑤 / 𝑥]𝜓 ↔ [𝑤 / 𝑥]𝜓)
187	186	anbi1i 451	. . . . . . . . . . 11 ⊢ (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
188	187	rexbii 2414	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
189	188	imbi2i 225	. . . . . . . . 9 ⊢ (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
190	189	ralbii 2413	. . . . . . . 8 ⊢ (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
191	185, 190	sylibr 133	. . . . . . 7 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
192		nn0nlt0 8901	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ0 → ¬ 𝑤 < 0)
193		nn0z 8972	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℕ0 → 𝑤 ∈ ℤ)
194		ztri3or0 8994	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℤ → (𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤))
195	193, 194	syl 14	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℕ0 → (𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤))
196		3orass 946	. . . . . . . . . . 11 ⊢ ((𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤) ↔ (𝑤 < 0 ∨ (𝑤 = 0 ∨ 0 < 𝑤)))
197	195, 196	sylib 121	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℕ0 → (𝑤 < 0 ∨ (𝑤 = 0 ∨ 0 < 𝑤)))
198	197	orcomd 701	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ0 → ((𝑤 = 0 ∨ 0 < 𝑤) ∨ 𝑤 < 0))
199	192, 198	ecased 1308	. . . . . . . 8 ⊢ (𝑤 ∈ ℕ0 → (𝑤 = 0 ∨ 0 < 𝑤))
200	199	ad2antrr 477	. . . . . . 7 ⊢ (((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) → (𝑤 = 0 ∨ 0 < 𝑤))
201	65, 191, 200	mpjaodan 770	. . . . . 6 ⊢ (((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
202	201	exp31 359	. . . . 5 ⊢ (𝑤 ∈ ℕ0 → (∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))))
203	8, 16, 202	nn0sinds 10104	. . . 4 ⊢ (𝑥 ∈ ℕ0 → ((𝜃 ∧ [𝑥 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
204	203	expd 256	. . 3 ⊢ (𝑥 ∈ ℕ0 → (𝜃 → ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))))
205	204	impcom 124	. 2 ⊢ ((𝜃 ∧ 𝑥 ∈ ℕ0) → ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
206	205	ralrimiva 2477	1 ⊢ (𝜃 → ∀𝑥 ∈ ℕ0 ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 680   ∨ w3o 942   = wceq 1312   ∈ wcel 1461  [wsb 1716  ∀wral 2388  ∃wrex 2389  [wsbc 2876   class class class wbr 3893  (class class class)co 5726  0cc0 7541  1c1 7542   + caddc 7544   · cmul 7546   < clt 7718   − cmin 7850  ℕcn 8624  ℕ₀cn0 8875  ℤcz 8952  ...cfz 9677   mod cmo 9982   ∥ cdvds 11335

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-coll 4001  ax-sep 4004  ax-nul 4012  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410  ax-iinf 4460  ax-cnex 7630  ax-resscn 7631  ax-1cn 7632  ax-1re 7633  ax-icn 7634  ax-addcl 7635  ax-addrcl 7636  ax-mulcl 7637  ax-mulrcl 7638  ax-addcom 7639  ax-mulcom 7640  ax-addass 7641  ax-mulass 7642  ax-distr 7643  ax-i2m1 7644  ax-0lt1 7645  ax-1rid 7646  ax-0id 7647  ax-rnegex 7648  ax-precex 7649  ax-cnre 7650  ax-pre-ltirr 7651  ax-pre-ltwlin 7652  ax-pre-lttrn 7653  ax-pre-apti 7654  ax-pre-ltadd 7655  ax-pre-mulgt0 7656  ax-pre-mulext 7657  ax-arch 7658

This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 944  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-nel 2376  df-ral 2393  df-rex 2394  df-reu 2395  df-rmo 2396  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-if 3439  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-tr 3985  df-id 4173  df-po 4176  df-iso 4177  df-iord 4246  df-on 4248  df-ilim 4249  df-suc 4251  df-iom 4463  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-fv 5087  df-riota 5682  df-ov 5729  df-oprab 5730  df-mpo 5731  df-1st 5990  df-2nd 5991  df-recs 6154  df-frec 6240  df-pnf 7720  df-mnf 7721  df-xr 7722  df-ltxr 7723  df-le 7724  df-sub 7852  df-neg 7853  df-reap 8249  df-ap 8256  df-div 8340  df-inn 8625  df-2 8683  df-n0 8876  df-z 8953  df-uz 9223  df-q 9308  df-rp 9338  df-fz 9678  df-fl 9930  df-mod 9983  df-seqfrec 10106  df-exp 10180  df-cj 10501  df-re 10502  df-im 10503  df-rsqrt 10656  df-abs 10657  df-dvds 11336

This theorem is referenced by:  bezoutlemex  11529