Theorem bezoutlemmain 11916

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 1827	. . . . . . 7 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑟]𝜑 ↔ [𝑧 / 𝑟]𝜑))
2	1	anbi2d 460	. . . . . 6 ⊢ (𝑤 = 𝑧 → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) ↔ (𝜃 ∧ [𝑧 / 𝑟]𝜑)))
3		sbequ 1827	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
4	3	anbi1d 461	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
5	4	rexbidv 2465	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
6	5	imbi2d 229	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
7	6	ralbidv 2464	. . . . . 6 ⊢ (𝑤 = 𝑧 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
8	2, 7	imbi12d 233	. . . . 5 ⊢ (𝑤 = 𝑧 → (((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))))
9		sbequ 1827	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑟]𝜑 ↔ [𝑥 / 𝑟]𝜑))
10	9	anbi2d 460	. . . . . 6 ⊢ (𝑤 = 𝑥 → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) ↔ (𝜃 ∧ [𝑥 / 𝑟]𝜑)))
11		sbequ12r 1759	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜓 ↔ 𝜓))
12	11	anbi1d 461	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ (𝜓 ∧ 𝜑)))
13	12	rexbidv 2465	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))
14	13	imbi2d 229	. . . . . . 7 ⊢ (𝑤 = 𝑥 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
15	14	ralbidv 2464	. . . . . 6 ⊢ (𝑤 = 𝑥 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
16	10, 15	imbi12d 233	. . . . 5 ⊢ (𝑤 = 𝑥 → (((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [𝑥 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))))
17		nfv 1515	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑤 ∈ ℕ0
18		nfcv 2306	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(0...(𝑤 − 1))
19		nfv 1515	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝜃 ∧ [𝑧 / 𝑟]𝜑)
20		nfra1 2495	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
21	19, 20	nfim 1559	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
22	18, 21	nfralxy 2502	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
23	17, 22	nfan 1552	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
24		nfv 1515	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜃 ∧ [𝑤 / 𝑟]𝜑)
25	23, 24	nfan 1552	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
26		nfv 1515	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑤 = 0
27	25, 26	nfan 1552	. . . . . . . 8 ⊢ Ⅎ𝑦(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0)
28		simplr 520	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑦 ∈ ℕ0)
29		nfv 1515	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))
30		breq2 3980	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑦 → (𝑧 ∥ 𝑟 ↔ 𝑧 ∥ 𝑦))
31	30	imbi1d 230	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑦 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
32	31	ralbidv 2464	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑦 → (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
33	29, 32	sbie 1778	. . . . . . . . . . . . 13 ⊢ ([𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
34		nn0z 9202	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∈ ℤ)
35		dvds0 11732	. . . . . . . . . . . . . . . 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 2522	. . . . . . . . . . . 12 ⊢ [𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))
40		nfv 1515	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟 𝑤 = 0
41		dfsbcq2 2949	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 0 → ([𝑤 / 𝑥]𝜓 ↔ [0 / 𝑥]𝜓))
42		bezout.sub-gcd	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))
43	42	sbcbii 3005	. . . . . . . . . . . . . . 15 ⊢ ([0 / 𝑥]𝜓 ↔ [0 / 𝑥]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))
44		c0ex 7884	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ V
45		breq2 3980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑧 ∥ 𝑥 ↔ 𝑧 ∥ 0))
46	45	anbi1d 461	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → ((𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦) ↔ (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
47	46	imbi2d 229	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
48	47	ralbidv 2464	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
49	44, 48	sbcie 2980	. . . . . . . . . . . . . . 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 1833	. . . . . . . . . . . 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 1926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟[𝑦 / 𝑟][𝑤 / 𝑥]𝜓
57		nfs1v 1926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟[𝑦 / 𝑟]𝜑
58	56, 57	nfan 1552	. . . . . . . . . . 11 ⊢ Ⅎ𝑟([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)
59		sbequ12 1758	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑦 → ([𝑤 / 𝑥]𝜓 ↔ [𝑦 / 𝑟][𝑤 / 𝑥]𝜓))
60		sbequ12 1758	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑟]𝜑))
61	59, 60	anbi12d 465	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑦 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)))
62	58, 61	rspce 2820	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ0 ∧ ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
63	28, 54, 55, 62	syl12anc 1225	. . . . . . . . 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 2535	. . . . . . 7 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
66		nfv 1515	. . . . . . . . . 10 ⊢ Ⅎ𝑦0 < 𝑤
67	25, 66	nfan 1552	. . . . . . . . 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 9149	. . . . . . . . . . . . 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 2950	. . . . . . . . . . . . 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 3979	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑟 ↔ 𝑎 ∥ 𝑟))
88		breq1 3979	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑥 ↔ 𝑎 ∥ 𝑥))
89		breq1 3979	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑦 ↔ 𝑎 ∥ 𝑦))
90	88, 89	anbi12d 465	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → ((𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦) ↔ (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))
91	87, 90	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦))))
92	91	cbvralv 2689	. . . . . . . . . . . 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 2949	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑦 mod 𝑤) → ([𝑧 / 𝑟]𝜑 ↔ [(𝑦 mod 𝑤) / 𝑟]𝜑))
99	98	anbi2d 460	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑦 mod 𝑤) → ((𝜃 ∧ [𝑧 / 𝑟]𝜑) ↔ (𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑)))
100		sbsbc 2950	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
101		sbsbc 2950	. . . . . . . . . . . . . . . . . . . 20 ⊢ ([𝑤 / 𝑦]𝜓 ↔ [𝑤 / 𝑦]𝜓)
102	101	sbcbii 3005	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
103	100, 102	bitri 183	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
104	103	anbi1i 454	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))
105		dfsbcq 2948	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑦 mod 𝑤) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓))
106	105	anbi1d 461	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
107	104, 106	syl5bb 191	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
108	107	rexbidv 2465	. . . . . . . . . . . . . . 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 1515	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦[𝑤 / 𝑟]𝜑
115		nfcv 2306	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦ℕ0
116		nfs1v 1926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜓
117	116	nfsbxy 1929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜓
118		nfv 1515	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦𝜑
119	117, 118	nfan 1552	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)
120	115, 119	nfrexxy 2503	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)
121	114, 120	nfim 1559	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))
122		sbequ 1827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → ([𝑦 / 𝑟]𝜑 ↔ [𝑤 / 𝑟]𝜑))
123		nfv 1515	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥 𝑦 = 𝑤
124		sbequ12 1758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑦]𝜓))
125	123, 124	sbbid 1833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓))
126	125	anbi1d 461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑤 → (([𝑧 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
127	126	rexbidv 2465	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → (∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
128	122, 127	imbi12d 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑤 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
129	121, 128	rspc 2819	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ0 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
130	129	imim2d 54	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℕ0 → (((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))))
131	130	ralimdv 2532	. . . . . . . . . . . . . . . 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 9302	. . . . . . . . . . . . . 14 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑦 ∈ ℤ)
137	79	ad3antrrr 484	. . . . . . . . . . . . . 14 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑤 ∈ ℕ)
138		zmodfz 10271	. . . . . . . . . . . . . 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 2830	. . . . . . . . . . . 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 1515	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ ℕ0
143		nfcv 2306	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(0...(𝑤 − 1))
144		nfv 1515	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝜃 ∧ [𝑧 / 𝑟]𝜑)
145		nfcv 2306	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥ℕ0
146		nfv 1515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝜑
147	146	nfsbxy 1929	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥[𝑦 / 𝑟]𝜑
148		nfs1v 1926	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜓
149	148, 146	nfan 1552	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥([𝑧 / 𝑥]𝜓 ∧ 𝜑)
150	145, 149	nfrexxy 2503	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)
151	147, 150	nfim 1559	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
152	145, 151	nfralxy 2502	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
153	144, 152	nfim 1559	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
154	143, 153	nfralxy 2502	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
155	142, 154	nfan 1552	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
156		nfv 1515	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝜃 ∧ [𝑤 / 𝑟]𝜑)
157	155, 156	nfan 1552	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
158		nfv 1515	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥0 < 𝑤
159	157, 158	nfan 1552	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
160		nfv 1515	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑦 ∈ ℕ0
161	159, 160	nfan 1552	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0)
162	161, 147	nfan 1552	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑)
163		nfv 1515	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟 𝑤 ∈ ℕ0
164		nfcv 2306	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟(0...(𝑤 − 1))
165		nfv 1515	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟𝜃
166		nfs1v 1926	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟[𝑧 / 𝑟]𝜑
167	165, 166	nfan 1552	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟(𝜃 ∧ [𝑧 / 𝑟]𝜑)
168		nfcv 2306	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟ℕ0
169		nfre1 2507	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑟∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)
170	57, 169	nfim 1559	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
171	168, 170	nfralxy 2502	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
172	167, 171	nfim 1559	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
173	164, 172	nfralxy 2502	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
174	163, 173	nfan 1552	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
175		nfs1v 1926	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟[𝑤 / 𝑟]𝜑
176	165, 175	nfan 1552	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟(𝜃 ∧ [𝑤 / 𝑟]𝜑)
177	174, 176	nfan 1552	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
178		nfv 1515	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟0 < 𝑤
179	177, 178	nfan 1552	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
180		nfv 1515	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟 𝑦 ∈ ℕ0
181	179, 180	nfan 1552	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0)
182	181, 57	nfan 1552	. . . . . . . . . . 11 ⊢ Ⅎ𝑟(((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑)
183	68, 72, 75, 80, 81, 82, 86, 93, 141, 162, 182	bezoutlemstep 11915	. . . . . . . . . 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 2535	. . . . . . . 8 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
186		sbsbc 2950	. . . . . . . . . . . 12 ⊢ ([𝑤 / 𝑥]𝜓 ↔ [𝑤 / 𝑥]𝜓)
187	186	anbi1i 454	. . . . . . . . . . 11 ⊢ (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
188	187	rexbii 2471	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
189	188	imbi2i 225	. . . . . . . . 9 ⊢ (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
190	189	ralbii 2470	. . . . . . . 8 ⊢ (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
191	185, 190	sylibr 133	. . . . . . 7 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
192		nn0nlt0 9131	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ0 → ¬ 𝑤 < 0)
193		nn0z 9202	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℕ0 → 𝑤 ∈ ℤ)
194		ztri3or0 9224	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℤ → (𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤))
195	193, 194	syl 14	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℕ0 → (𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤))
196		3orass 970	. . . . . . . . . . 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 1338	. . . . . . . 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 10369	. . . 4 ⊢ (𝑥 ∈ ℕ0 → ((𝜃 ∧ [𝑥 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
204	203	expd 256	. . 3 ⊢ (𝑥 ∈ ℕ0 → (𝜃 → ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))))
205	204	impcom 124	. 2 ⊢ ((𝜃 ∧ 𝑥 ∈ ℕ0) → ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
206	205	ralrimiva 2537	1 ⊢ (𝜃 → ∀𝑥 ∈ ℕ0 ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   ∨ w3o 966   = wceq 1342  [wsb 1749   ∈ wcel 2135  ∀wral 2442  ∃wrex 2443  [wsbc 2946   class class class wbr 3976  (class class class)co 5836  0cc0 7744  1c1 7745   + caddc 7747   · cmul 7749   < clt 7924   − cmin 8060  ℕcn 8848  ℕ₀cn0 9105  ℤcz 9182  ...cfz 9935   mod cmo 10247   ∥ cdvds 11713

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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-coll 4091  ax-sep 4094  ax-nul 4102  ax-pow 4147  ax-pr 4181  ax-un 4405  ax-setind 4508  ax-iinf 4559  ax-cnex 7835  ax-resscn 7836  ax-1cn 7837  ax-1re 7838  ax-icn 7839  ax-addcl 7840  ax-addrcl 7841  ax-mulcl 7842  ax-mulrcl 7843  ax-addcom 7844  ax-mulcom 7845  ax-addass 7846  ax-mulass 7847  ax-distr 7848  ax-i2m1 7849  ax-0lt1 7850  ax-1rid 7851  ax-0id 7852  ax-rnegex 7853  ax-precex 7854  ax-cnre 7855  ax-pre-ltirr 7856  ax-pre-ltwlin 7857  ax-pre-lttrn 7858  ax-pre-apti 7859  ax-pre-ltadd 7860  ax-pre-mulgt0 7861  ax-pre-mulext 7862  ax-arch 7863

This theorem depends on definitions:  df-bi 116  df-dc 825  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-reu 2449  df-rmo 2450  df-rab 2451  df-v 2723  df-sbc 2947  df-csb 3041  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-nul 3405  df-if 3516  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-int 3819  df-iun 3862  df-br 3977  df-opab 4038  df-mpt 4039  df-tr 4075  df-id 4265  df-po 4268  df-iso 4269  df-iord 4338  df-on 4340  df-ilim 4341  df-suc 4343  df-iom 4562  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-rn 4609  df-res 4610  df-ima 4611  df-iota 5147  df-fun 5184  df-fn 5185  df-f 5186  df-f1 5187  df-fo 5188  df-f1o 5189  df-fv 5190  df-riota 5792  df-ov 5839  df-oprab 5840  df-mpo 5841  df-1st 6100  df-2nd 6101  df-recs 6264  df-frec 6350  df-pnf 7926  df-mnf 7927  df-xr 7928  df-ltxr 7929  df-le 7930  df-sub 8062  df-neg 8063  df-reap 8464  df-ap 8471  df-div 8560  df-inn 8849  df-2 8907  df-n0 9106  df-z 9183  df-uz 9458  df-q 9549  df-rp 9581  df-fz 9936  df-fl 10195  df-mod 10248  df-seqfrec 10371  df-exp 10445  df-cj 10770  df-re 10771  df-im 10772  df-rsqrt 10926  df-abs 10927  df-dvds 11714

This theorem is referenced by:  bezoutlemex  11919