Theorem bezoutlemmain 11931

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 1828	. . . . . . 7 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑟]𝜑 ↔ [𝑧 / 𝑟]𝜑))
2	1	anbi2d 460	. . . . . 6 ⊢ (𝑤 = 𝑧 → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) ↔ (𝜃 ∧ [𝑧 / 𝑟]𝜑)))
3		sbequ 1828	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
4	3	anbi1d 461	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
5	4	rexbidv 2467	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
6	5	imbi2d 229	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
7	6	ralbidv 2466	. . . . . 6 ⊢ (𝑤 = 𝑧 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
8	2, 7	imbi12d 233	. . . . 5 ⊢ (𝑤 = 𝑧 → (((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))))
9		sbequ 1828	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑟]𝜑 ↔ [𝑥 / 𝑟]𝜑))
10	9	anbi2d 460	. . . . . 6 ⊢ (𝑤 = 𝑥 → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) ↔ (𝜃 ∧ [𝑥 / 𝑟]𝜑)))
11		sbequ12r 1760	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜓 ↔ 𝜓))
12	11	anbi1d 461	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ (𝜓 ∧ 𝜑)))
13	12	rexbidv 2467	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))
14	13	imbi2d 229	. . . . . . 7 ⊢ (𝑤 = 𝑥 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
15	14	ralbidv 2466	. . . . . 6 ⊢ (𝑤 = 𝑥 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
16	10, 15	imbi12d 233	. . . . 5 ⊢ (𝑤 = 𝑥 → (((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [𝑥 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))))
17		nfv 1516	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑤 ∈ ℕ0
18		nfcv 2308	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(0...(𝑤 − 1))
19		nfv 1516	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝜃 ∧ [𝑧 / 𝑟]𝜑)
20		nfra1 2497	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
21	19, 20	nfim 1560	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
22	18, 21	nfralxy 2504	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
23	17, 22	nfan 1553	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
24		nfv 1516	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜃 ∧ [𝑤 / 𝑟]𝜑)
25	23, 24	nfan 1553	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
26		nfv 1516	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑤 = 0
27	25, 26	nfan 1553	. . . . . . . 8 ⊢ Ⅎ𝑦(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0)
28		simplr 520	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑦 ∈ ℕ0)
29		nfv 1516	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))
30		breq2 3986	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑦 → (𝑧 ∥ 𝑟 ↔ 𝑧 ∥ 𝑦))
31	30	imbi1d 230	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑦 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
32	31	ralbidv 2466	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑦 → (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
33	29, 32	sbie 1779	. . . . . . . . . . . . 13 ⊢ ([𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
34		nn0z 9211	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∈ ℤ)
35		dvds0 11746	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℤ → 𝑧 ∥ 0)
36	34, 35	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∥ 0)
37	36	biantrurd 303	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℕ0 → (𝑧 ∥ 𝑦 ↔ (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
38	37	biimpd 143	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℕ0 → (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
39	33, 38	mprgbir 2524	. . . . . . . . . . . 12 ⊢ [𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))
40		nfv 1516	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟 𝑤 = 0
41		dfsbcq2 2954	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 0 → ([𝑤 / 𝑥]𝜓 ↔ [0 / 𝑥]𝜓))
42		bezout.sub-gcd	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))
43	42	sbcbii 3010	. . . . . . . . . . . . . . 15 ⊢ ([0 / 𝑥]𝜓 ↔ [0 / 𝑥]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))
44		c0ex 7893	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ V
45		breq2 3986	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑧 ∥ 𝑥 ↔ 𝑧 ∥ 0))
46	45	anbi1d 461	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → ((𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦) ↔ (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
47	46	imbi2d 229	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
48	47	ralbidv 2466	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
49	44, 48	sbcie 2985	. . . . . . . . . . . . . . 15 ⊢ ([0 / 𝑥]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
50	43, 49	bitri 183	. . . . . . . . . . . . . 14 ⊢ ([0 / 𝑥]𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
51	41, 50	bitrdi 195	. . . . . . . . . . . . 13 ⊢ (𝑤 = 0 → ([𝑤 / 𝑥]𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
52	40, 51	sbbid 1834	. . . . . . . . . . . 12 ⊢ (𝑤 = 0 → ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ↔ [𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
53	39, 52	mpbiri 167	. . . . . . . . . . 11 ⊢ (𝑤 = 0 → [𝑦 / 𝑟][𝑤 / 𝑥]𝜓)
54	53	ad3antlr 485	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟][𝑤 / 𝑥]𝜓)
55		simpr 109	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟]𝜑)
56		nfs1v 1927	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟[𝑦 / 𝑟][𝑤 / 𝑥]𝜓
57		nfs1v 1927	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟[𝑦 / 𝑟]𝜑
58	56, 57	nfan 1553	. . . . . . . . . . 11 ⊢ Ⅎ𝑟([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)
59		sbequ12 1759	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑦 → ([𝑤 / 𝑥]𝜓 ↔ [𝑦 / 𝑟][𝑤 / 𝑥]𝜓))
60		sbequ12 1759	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑟]𝜑))
61	59, 60	anbi12d 465	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑦 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)))
62	58, 61	rspce 2825	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ0 ∧ ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
63	28, 54, 55, 62	syl12anc 1226	. . . . . . . . 9 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
64	63	exp31 362	. . . . . . . 8 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) → (𝑦 ∈ ℕ0 → ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))))
65	27, 64	ralrimi 2537	. . . . . . 7 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
66		nfv 1516	. . . . . . . . . 10 ⊢ Ⅎ𝑦0 < 𝑤
67	25, 66	nfan 1553	. . . . . . . . 9 ⊢ Ⅎ𝑦(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
68		bezout.is-bezout	. . . . . . . . . . 11 ⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))
69		simplrl 525	. . . . . . . . . . . . 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 480	. . . . . . . . . . 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 480	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝐵 ∈ ℕ0)
76		simplll 523	. . . . . . . . . . . . 13 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝑤 ∈ ℕ0)
77		simpr 109	. . . . . . . . . . . . 13 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 0 < 𝑤)
78		elnnnn0b 9158	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ℕ ↔ (𝑤 ∈ ℕ0 ∧ 0 < 𝑤))
79	76, 77, 78	sylanbrc 414	. . . . . . . . . . . 12 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝑤 ∈ ℕ)
80	79	ad2antrr 480	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑤 ∈ ℕ)
81		simpr 109	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟]𝜑)
82		simplr 520	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑦 ∈ ℕ0)
83		simplrr 526	. . . . . . . . . . . . 13 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → [𝑤 / 𝑟]𝜑)
84		sbsbc 2955	. . . . . . . . . . . . 13 ⊢ ([𝑤 / 𝑟]𝜑 ↔ [𝑤 / 𝑟]𝜑)
85	83, 84	sylib 121	. . . . . . . . . . . 12 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → [𝑤 / 𝑟]𝜑)
86	85	ad2antrr 480	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑤 / 𝑟]𝜑)
87		breq1 3985	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑟 ↔ 𝑎 ∥ 𝑟))
88		breq1 3985	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑥 ↔ 𝑎 ∥ 𝑥))
89		breq1 3985	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑦 ↔ 𝑎 ∥ 𝑦))
90	88, 89	anbi12d 465	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → ((𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦) ↔ (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))
91	87, 90	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦))))
92	91	cbvralv 2692	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑎 ∈ ℕ0 (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))
93	42, 92	bitri 183	. . . . . . . . . . 11 ⊢ (𝜓 ↔ ∀𝑎 ∈ ℕ0 (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))
94	69	ad3antrrr 484	. . . . . . . . . . . . 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 304	. . . . . . . . . . . 12 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → (𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑))
97	83	ad3antrrr 484	. . . . . . . . . . . 12 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → [𝑤 / 𝑟]𝜑)
98		dfsbcq2 2954	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑦 mod 𝑤) → ([𝑧 / 𝑟]𝜑 ↔ [(𝑦 mod 𝑤) / 𝑟]𝜑))
99	98	anbi2d 460	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑦 mod 𝑤) → ((𝜃 ∧ [𝑧 / 𝑟]𝜑) ↔ (𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑)))
100		sbsbc 2955	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
101		sbsbc 2955	. . . . . . . . . . . . . . . . . . . 20 ⊢ ([𝑤 / 𝑦]𝜓 ↔ [𝑤 / 𝑦]𝜓)
102	101	sbcbii 3010	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
103	100, 102	bitri 183	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
104	103	anbi1i 454	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))
105		dfsbcq 2953	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑦 mod 𝑤) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓))
106	105	anbi1d 461	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
107	104, 106	syl5bb 191	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
108	107	rexbidv 2467	. . . . . . . . . . . . . . 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 519	. . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ (((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
114		nfv 1516	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦[𝑤 / 𝑟]𝜑
115		nfcv 2308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦ℕ0
116		nfs1v 1927	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜓
117	116	nfsbxy 1930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜓
118		nfv 1516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦𝜑
119	117, 118	nfan 1553	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)
120	115, 119	nfrexxy 2505	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)
121	114, 120	nfim 1560	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))
122		sbequ 1828	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → ([𝑦 / 𝑟]𝜑 ↔ [𝑤 / 𝑟]𝜑))
123		nfv 1516	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥 𝑦 = 𝑤
124		sbequ12 1759	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑦]𝜓))
125	123, 124	sbbid 1834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓))
126	125	anbi1d 461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑤 → (([𝑧 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
127	126	rexbidv 2467	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → (∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
128	122, 127	imbi12d 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑤 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
129	121, 128	rspc 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ0 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
130	129	imim2d 54	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℕ0 → (((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))))
131	130	ralimdv 2534	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℕ0 → (∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))))
132	131	ad4antr 486	. . . . . . . . . . . . . . 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 281	. . . . . . . . . . . . 13 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
135		simpllr 524	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑦 ∈ ℕ0)
136	135	nn0zd 9311	. . . . . . . . . . . . . 14 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑦 ∈ ℤ)
137	79	ad3antrrr 484	. . . . . . . . . . . . . 14 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑤 ∈ ℕ)
138		zmodfz 10281	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℤ ∧ 𝑤 ∈ ℕ) → (𝑦 mod 𝑤) ∈ (0...(𝑤 − 1)))
139	136, 137, 138	syl2anc 409	. . . . . . . . . . . . 13 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → (𝑦 mod 𝑤) ∈ (0...(𝑤 − 1)))
140	110, 134, 139	rspcdva 2835	. . . . . . . . . . . 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 1516	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ ℕ0
143		nfcv 2308	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(0...(𝑤 − 1))
144		nfv 1516	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝜃 ∧ [𝑧 / 𝑟]𝜑)
145		nfcv 2308	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥ℕ0
146		nfv 1516	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝜑
147	146	nfsbxy 1930	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥[𝑦 / 𝑟]𝜑
148		nfs1v 1927	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜓
149	148, 146	nfan 1553	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥([𝑧 / 𝑥]𝜓 ∧ 𝜑)
150	145, 149	nfrexxy 2505	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)
151	147, 150	nfim 1560	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
152	145, 151	nfralxy 2504	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
153	144, 152	nfim 1560	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
154	143, 153	nfralxy 2504	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
155	142, 154	nfan 1553	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
156		nfv 1516	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝜃 ∧ [𝑤 / 𝑟]𝜑)
157	155, 156	nfan 1553	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
158		nfv 1516	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥0 < 𝑤
159	157, 158	nfan 1553	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
160		nfv 1516	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑦 ∈ ℕ0
161	159, 160	nfan 1553	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0)
162	161, 147	nfan 1553	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑)
163		nfv 1516	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟 𝑤 ∈ ℕ0
164		nfcv 2308	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟(0...(𝑤 − 1))
165		nfv 1516	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟𝜃
166		nfs1v 1927	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟[𝑧 / 𝑟]𝜑
167	165, 166	nfan 1553	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟(𝜃 ∧ [𝑧 / 𝑟]𝜑)
168		nfcv 2308	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟ℕ0
169		nfre1 2509	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑟∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)
170	57, 169	nfim 1560	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
171	168, 170	nfralxy 2504	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
172	167, 171	nfim 1560	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
173	164, 172	nfralxy 2504	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
174	163, 173	nfan 1553	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
175		nfs1v 1927	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟[𝑤 / 𝑟]𝜑
176	165, 175	nfan 1553	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟(𝜃 ∧ [𝑤 / 𝑟]𝜑)
177	174, 176	nfan 1553	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
178		nfv 1516	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟0 < 𝑤
179	177, 178	nfan 1553	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
180		nfv 1516	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟 𝑦 ∈ ℕ0
181	179, 180	nfan 1553	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0)
182	181, 57	nfan 1553	. . . . . . . . . . 11 ⊢ Ⅎ𝑟(((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑)
183	68, 72, 75, 80, 81, 82, 86, 93, 141, 162, 182	bezoutlemstep 11930	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
184	183	exp31 362	. . . . . . . . 9 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → (𝑦 ∈ ℕ0 → ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))))
185	67, 184	ralrimi 2537	. . . . . . . 8 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
186		sbsbc 2955	. . . . . . . . . . . 12 ⊢ ([𝑤 / 𝑥]𝜓 ↔ [𝑤 / 𝑥]𝜓)
187	186	anbi1i 454	. . . . . . . . . . 11 ⊢ (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
188	187	rexbii 2473	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
189	188	imbi2i 225	. . . . . . . . 9 ⊢ (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
190	189	ralbii 2472	. . . . . . . 8 ⊢ (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
191	185, 190	sylibr 133	. . . . . . 7 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
192		nn0nlt0 9140	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ0 → ¬ 𝑤 < 0)
193		nn0z 9211	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℕ0 → 𝑤 ∈ ℤ)
194		ztri3or0 9233	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℤ → (𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤))
195	193, 194	syl 14	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℕ0 → (𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤))
196		3orass 971	. . . . . . . . . . 11 ⊢ ((𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤) ↔ (𝑤 < 0 ∨ (𝑤 = 0 ∨ 0 < 𝑤)))
197	195, 196	sylib 121	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℕ0 → (𝑤 < 0 ∨ (𝑤 = 0 ∨ 0 < 𝑤)))
198	197	orcomd 719	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ0 → ((𝑤 = 0 ∨ 0 < 𝑤) ∨ 𝑤 < 0))
199	192, 198	ecased 1339	. . . . . . . 8 ⊢ (𝑤 ∈ ℕ0 → (𝑤 = 0 ∨ 0 < 𝑤))
200	199	ad2antrr 480	. . . . . . 7 ⊢ (((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) → (𝑤 = 0 ∨ 0 < 𝑤))
201	65, 191, 200	mpjaodan 788	. . . . . 6 ⊢ (((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
202	201	exp31 362	. . . . 5 ⊢ (𝑤 ∈ ℕ0 → (∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))))
203	8, 16, 202	nn0sinds 10379	. . . 4 ⊢ (𝑥 ∈ ℕ0 → ((𝜃 ∧ [𝑥 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
204	203	expd 256	. . 3 ⊢ (𝑥 ∈ ℕ0 → (𝜃 → ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))))
205	204	impcom 124	. 2 ⊢ ((𝜃 ∧ 𝑥 ∈ ℕ0) → ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
206	205	ralrimiva 2539	1 ⊢ (𝜃 → ∀𝑥 ∈ ℕ0 ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   ∨ w3o 967   = wceq 1343  [wsb 1750   ∈ wcel 2136  ∀wral 2444  ∃wrex 2445  [wsbc 2951   class class class wbr 3982  (class class class)co 5842  0cc0 7753  1c1 7754   + caddc 7756   · cmul 7758   < clt 7933   − cmin 8069  ℕcn 8857  ℕ₀cn0 9114  ℤcz 9191  ...cfz 9944   mod cmo 10257   ∥ cdvds 11727

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-coll 4097  ax-sep 4100  ax-nul 4108  ax-pow 4153  ax-pr 4187  ax-un 4411  ax-setind 4514  ax-iinf 4565  ax-cnex 7844  ax-resscn 7845  ax-1cn 7846  ax-1re 7847  ax-icn 7848  ax-addcl 7849  ax-addrcl 7850  ax-mulcl 7851  ax-mulrcl 7852  ax-addcom 7853  ax-mulcom 7854  ax-addass 7855  ax-mulass 7856  ax-distr 7857  ax-i2m1 7858  ax-0lt1 7859  ax-1rid 7860  ax-0id 7861  ax-rnegex 7862  ax-precex 7863  ax-cnre 7864  ax-pre-ltirr 7865  ax-pre-ltwlin 7866  ax-pre-lttrn 7867  ax-pre-apti 7868  ax-pre-ltadd 7869  ax-pre-mulgt0 7870  ax-pre-mulext 7871  ax-arch 7872

This theorem depends on definitions:  df-bi 116  df-dc 825  df-3or 969  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ne 2337  df-nel 2432  df-ral 2449  df-rex 2450  df-reu 2451  df-rmo 2452  df-rab 2453  df-v 2728  df-sbc 2952  df-csb 3046  df-dif 3118  df-un 3120  df-in 3122  df-ss 3129  df-nul 3410  df-if 3521  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-int 3825  df-iun 3868  df-br 3983  df-opab 4044  df-mpt 4045  df-tr 4081  df-id 4271  df-po 4274  df-iso 4275  df-iord 4344  df-on 4346  df-ilim 4347  df-suc 4349  df-iom 4568  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-rn 4615  df-res 4616  df-ima 4617  df-iota 5153  df-fun 5190  df-fn 5191  df-f 5192  df-f1 5193  df-fo 5194  df-f1o 5195  df-fv 5196  df-riota 5798  df-ov 5845  df-oprab 5846  df-mpo 5847  df-1st 6108  df-2nd 6109  df-recs 6273  df-frec 6359  df-pnf 7935  df-mnf 7936  df-xr 7937  df-ltxr 7938  df-le 7939  df-sub 8071  df-neg 8072  df-reap 8473  df-ap 8480  df-div 8569  df-inn 8858  df-2 8916  df-n0 9115  df-z 9192  df-uz 9467  df-q 9558  df-rp 9590  df-fz 9945  df-fl 10205  df-mod 10258  df-seqfrec 10381  df-exp 10455  df-cj 10784  df-re 10785  df-im 10786  df-rsqrt 10940  df-abs 10941  df-dvds 11728

This theorem is referenced by:  bezoutlemex  11934