Theorem bezoutlemmain 12046

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 1851	. . . . . . 7 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑟]𝜑 ↔ [𝑧 / 𝑟]𝜑))
2	1	anbi2d 464	. . . . . 6 ⊢ (𝑤 = 𝑧 → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) ↔ (𝜃 ∧ [𝑧 / 𝑟]𝜑)))
3		sbequ 1851	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
4	3	anbi1d 465	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
5	4	rexbidv 2491	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
6	5	imbi2d 230	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
7	6	ralbidv 2490	. . . . . 6 ⊢ (𝑤 = 𝑧 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
8	2, 7	imbi12d 234	. . . . 5 ⊢ (𝑤 = 𝑧 → (((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))))
9		sbequ 1851	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑟]𝜑 ↔ [𝑥 / 𝑟]𝜑))
10	9	anbi2d 464	. . . . . 6 ⊢ (𝑤 = 𝑥 → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) ↔ (𝜃 ∧ [𝑥 / 𝑟]𝜑)))
11		sbequ12r 1783	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜓 ↔ 𝜓))
12	11	anbi1d 465	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ (𝜓 ∧ 𝜑)))
13	12	rexbidv 2491	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))
14	13	imbi2d 230	. . . . . . 7 ⊢ (𝑤 = 𝑥 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
15	14	ralbidv 2490	. . . . . 6 ⊢ (𝑤 = 𝑥 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
16	10, 15	imbi12d 234	. . . . 5 ⊢ (𝑤 = 𝑥 → (((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [𝑥 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))))
17		nfv 1539	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑤 ∈ ℕ0
18		nfcv 2332	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(0...(𝑤 − 1))
19		nfv 1539	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝜃 ∧ [𝑧 / 𝑟]𝜑)
20		nfra1 2521	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
21	19, 20	nfim 1583	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
22	18, 21	nfralxy 2528	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
23	17, 22	nfan 1576	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
24		nfv 1539	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜃 ∧ [𝑤 / 𝑟]𝜑)
25	23, 24	nfan 1576	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
26		nfv 1539	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑤 = 0
27	25, 26	nfan 1576	. . . . . . . 8 ⊢ Ⅎ𝑦(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0)
28		simplr 528	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑦 ∈ ℕ0)
29		nfv 1539	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))
30		breq2 4029	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑦 → (𝑧 ∥ 𝑟 ↔ 𝑧 ∥ 𝑦))
31	30	imbi1d 231	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑦 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
32	31	ralbidv 2490	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑦 → (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
33	29, 32	sbie 1802	. . . . . . . . . . . . 13 ⊢ ([𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
34		nn0z 9314	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∈ ℤ)
35		dvds0 11860	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℤ → 𝑧 ∥ 0)
36	34, 35	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ0 → 𝑧 ∥ 0)
37	36	biantrurd 305	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℕ0 → (𝑧 ∥ 𝑦 ↔ (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
38	37	biimpd 144	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℕ0 → (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
39	33, 38	mprgbir 2548	. . . . . . . . . . . 12 ⊢ [𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))
40		nfv 1539	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟 𝑤 = 0
41		dfsbcq2 2984	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 0 → ([𝑤 / 𝑥]𝜓 ↔ [0 / 𝑥]𝜓))
42		bezout.sub-gcd	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))
43	42	sbcbii 3041	. . . . . . . . . . . . . . 15 ⊢ ([0 / 𝑥]𝜓 ↔ [0 / 𝑥]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))
44		c0ex 7992	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ V
45		breq2 4029	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑧 ∥ 𝑥 ↔ 𝑧 ∥ 0))
46	45	anbi1d 465	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → ((𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦) ↔ (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
47	46	imbi2d 230	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
48	47	ralbidv 2490	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
49	44, 48	sbcie 3016	. . . . . . . . . . . . . . 15 ⊢ ([0 / 𝑥]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
50	43, 49	bitri 184	. . . . . . . . . . . . . 14 ⊢ ([0 / 𝑥]𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))
51	41, 50	bitrdi 196	. . . . . . . . . . . . 13 ⊢ (𝑤 = 0 → ([𝑤 / 𝑥]𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
52	40, 51	sbbid 1857	. . . . . . . . . . . 12 ⊢ (𝑤 = 0 → ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ↔ [𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))))
53	39, 52	mpbiri 168	. . . . . . . . . . 11 ⊢ (𝑤 = 0 → [𝑦 / 𝑟][𝑤 / 𝑥]𝜓)
54	53	ad3antlr 493	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟][𝑤 / 𝑥]𝜓)
55		simpr 110	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟]𝜑)
56		nfs1v 1951	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟[𝑦 / 𝑟][𝑤 / 𝑥]𝜓
57		nfs1v 1951	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟[𝑦 / 𝑟]𝜑
58	56, 57	nfan 1576	. . . . . . . . . . 11 ⊢ Ⅎ𝑟([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)
59		sbequ12 1782	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑦 → ([𝑤 / 𝑥]𝜓 ↔ [𝑦 / 𝑟][𝑤 / 𝑥]𝜓))
60		sbequ12 1782	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑟]𝜑))
61	59, 60	anbi12d 473	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑦 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)))
62	58, 61	rspce 2855	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ0 ∧ ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
63	28, 54, 55, 62	syl12anc 1247	. . . . . . . . 9 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
64	63	exp31 364	. . . . . . . 8 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) → (𝑦 ∈ ℕ0 → ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))))
65	27, 64	ralrimi 2561	. . . . . . 7 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
66		nfv 1539	. . . . . . . . . 10 ⊢ Ⅎ𝑦0 < 𝑤
67	25, 66	nfan 1576	. . . . . . . . 9 ⊢ Ⅎ𝑦(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
68		bezout.is-bezout	. . . . . . . . . . 11 ⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))
69		simplrl 535	. . . . . . . . . . . . 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 488	. . . . . . . . . . 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 488	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝐵 ∈ ℕ0)
76		simplll 533	. . . . . . . . . . . . 13 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝑤 ∈ ℕ0)
77		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 0 < 𝑤)
78		elnnnn0b 9261	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ℕ ↔ (𝑤 ∈ ℕ0 ∧ 0 < 𝑤))
79	76, 77, 78	sylanbrc 417	. . . . . . . . . . . 12 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝑤 ∈ ℕ)
80	79	ad2antrr 488	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑤 ∈ ℕ)
81		simpr 110	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟]𝜑)
82		simplr 528	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑦 ∈ ℕ0)
83		simplrr 536	. . . . . . . . . . . . 13 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → [𝑤 / 𝑟]𝜑)
84		sbsbc 2985	. . . . . . . . . . . . 13 ⊢ ([𝑤 / 𝑟]𝜑 ↔ [𝑤 / 𝑟]𝜑)
85	83, 84	sylib 122	. . . . . . . . . . . 12 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → [𝑤 / 𝑟]𝜑)
86	85	ad2antrr 488	. . . . . . . . . . 11 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑤 / 𝑟]𝜑)
87		breq1 4028	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑟 ↔ 𝑎 ∥ 𝑟))
88		breq1 4028	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑥 ↔ 𝑎 ∥ 𝑥))
89		breq1 4028	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑦 ↔ 𝑎 ∥ 𝑦))
90	88, 89	anbi12d 473	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑎 → ((𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦) ↔ (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))
91	87, 90	imbi12d 234	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑎 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦))))
92	91	cbvralv 2722	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑎 ∈ ℕ0 (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))
93	42, 92	bitri 184	. . . . . . . . . . 11 ⊢ (𝜓 ↔ ∀𝑎 ∈ ℕ0 (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))
94	69	ad3antrrr 492	. . . . . . . . . . . . 13 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝜃)
95		simpr 110	. . . . . . . . . . . . 13 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → [(𝑦 mod 𝑤) / 𝑟]𝜑)
96	94, 95	jca 306	. . . . . . . . . . . 12 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → (𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑))
97	83	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → [𝑤 / 𝑟]𝜑)
98		dfsbcq2 2984	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑦 mod 𝑤) → ([𝑧 / 𝑟]𝜑 ↔ [(𝑦 mod 𝑤) / 𝑟]𝜑))
99	98	anbi2d 464	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑦 mod 𝑤) → ((𝜃 ∧ [𝑧 / 𝑟]𝜑) ↔ (𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑)))
100		sbsbc 2985	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
101		sbsbc 2985	. . . . . . . . . . . . . . . . . . . 20 ⊢ ([𝑤 / 𝑦]𝜓 ↔ [𝑤 / 𝑦]𝜓)
102	101	sbcbii 3041	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
103	100, 102	bitri 184	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)
104	103	anbi1i 458	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))
105		dfsbcq 2983	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑦 mod 𝑤) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓))
106	105	anbi1d 465	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
107	104, 106	bitrid 192	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
108	107	rexbidv 2491	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑦 mod 𝑤) → (∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
109	108	imbi2d 230	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)) ↔ ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
110	99, 109	imbi12d 234	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑦 mod 𝑤) → (((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))))
111		simpll 527	. . . . . . . . . . . . . 14 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → (((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤))
112		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
113	112	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ (((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
114		nfv 1539	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦[𝑤 / 𝑟]𝜑
115		nfcv 2332	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦ℕ0
116		nfs1v 1951	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜓
117	116	nfsbxy 1954	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜓
118		nfv 1539	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦𝜑
119	117, 118	nfan 1576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑦([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)
120	115, 119	nfrexxy 2529	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)
121	114, 120	nfim 1583	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))
122		sbequ 1851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → ([𝑦 / 𝑟]𝜑 ↔ [𝑤 / 𝑟]𝜑))
123		nfv 1539	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥 𝑦 = 𝑤
124		sbequ12 1782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑦]𝜓))
125	123, 124	sbbid 1857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓))
126	125	anbi1d 465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑤 → (([𝑧 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
127	126	rexbidv 2491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → (∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))
128	122, 127	imbi12d 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑤 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
129	121, 128	rspc 2854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ0 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
130	129	imim2d 54	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℕ0 → (((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))))
131	130	ralimdv 2558	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℕ0 → (∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))))
132	131	ad4antr 494	. . . . . . . . . . . . . . 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 283	. . . . . . . . . . . . 13 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))
135		simpllr 534	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑦 ∈ ℕ0)
136	135	nn0zd 9414	. . . . . . . . . . . . . 14 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑦 ∈ ℤ)
137	79	ad3antrrr 492	. . . . . . . . . . . . . 14 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑤 ∈ ℕ)
138		zmodfz 10389	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℤ ∧ 𝑤 ∈ ℕ) → (𝑦 mod 𝑤) ∈ (0...(𝑤 − 1)))
139	136, 137, 138	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → (𝑦 mod 𝑤) ∈ (0...(𝑤 − 1)))
140	110, 134, 139	rspcdva 2865	. . . . . . . . . . . 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 1539	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ ℕ0
143		nfcv 2332	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(0...(𝑤 − 1))
144		nfv 1539	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝜃 ∧ [𝑧 / 𝑟]𝜑)
145		nfcv 2332	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥ℕ0
146		nfv 1539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝜑
147	146	nfsbxy 1954	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥[𝑦 / 𝑟]𝜑
148		nfs1v 1951	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜓
149	148, 146	nfan 1576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥([𝑧 / 𝑥]𝜓 ∧ 𝜑)
150	145, 149	nfrexxy 2529	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)
151	147, 150	nfim 1583	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
152	145, 151	nfralxy 2528	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
153	144, 152	nfim 1583	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
154	143, 153	nfralxy 2528	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
155	142, 154	nfan 1576	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
156		nfv 1539	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝜃 ∧ [𝑤 / 𝑟]𝜑)
157	155, 156	nfan 1576	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
158		nfv 1539	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥0 < 𝑤
159	157, 158	nfan 1576	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
160		nfv 1539	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑦 ∈ ℕ0
161	159, 160	nfan 1576	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0)
162	161, 147	nfan 1576	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑)
163		nfv 1539	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟 𝑤 ∈ ℕ0
164		nfcv 2332	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟(0...(𝑤 − 1))
165		nfv 1539	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟𝜃
166		nfs1v 1951	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟[𝑧 / 𝑟]𝜑
167	165, 166	nfan 1576	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟(𝜃 ∧ [𝑧 / 𝑟]𝜑)
168		nfcv 2332	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟ℕ0
169		nfre1 2533	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑟∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)
170	57, 169	nfim 1583	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
171	168, 170	nfralxy 2528	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))
172	167, 171	nfim 1583	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
173	164, 172	nfralxy 2528	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))
174	163, 173	nfan 1576	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟(𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))
175		nfs1v 1951	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟[𝑤 / 𝑟]𝜑
176	165, 175	nfan 1576	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟(𝜃 ∧ [𝑤 / 𝑟]𝜑)
177	174, 176	nfan 1576	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑))
178		nfv 1539	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑟0 < 𝑤
179	177, 178	nfan 1576	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟(((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)
180		nfv 1539	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑟 𝑦 ∈ ℕ0
181	179, 180	nfan 1576	. . . . . . . . . . . 12 ⊢ Ⅎ𝑟((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0)
182	181, 57	nfan 1576	. . . . . . . . . . 11 ⊢ Ⅎ𝑟(((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑)
183	68, 72, 75, 80, 81, 82, 86, 93, 141, 162, 182	bezoutlemstep 12045	. . . . . . . . . 10 ⊢ ((((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
184	183	exp31 364	. . . . . . . . 9 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → (𝑦 ∈ ℕ0 → ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))))
185	67, 184	ralrimi 2561	. . . . . . . 8 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
186		sbsbc 2985	. . . . . . . . . . . 12 ⊢ ([𝑤 / 𝑥]𝜓 ↔ [𝑤 / 𝑥]𝜓)
187	186	anbi1i 458	. . . . . . . . . . 11 ⊢ (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
188	187	rexbii 2497	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))
189	188	imbi2i 226	. . . . . . . . 9 ⊢ (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
190	189	ralbii 2496	. . . . . . . 8 ⊢ (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
191	185, 190	sylibr 134	. . . . . . 7 ⊢ ((((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
192		nn0nlt0 9243	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ0 → ¬ 𝑤 < 0)
193		nn0z 9314	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℕ0 → 𝑤 ∈ ℤ)
194		ztri3or0 9336	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℤ → (𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤))
195	193, 194	syl 14	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℕ0 → (𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤))
196		3orass 983	. . . . . . . . . . 11 ⊢ ((𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤) ↔ (𝑤 < 0 ∨ (𝑤 = 0 ∨ 0 < 𝑤)))
197	195, 196	sylib 122	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℕ0 → (𝑤 < 0 ∨ (𝑤 = 0 ∨ 0 < 𝑤)))
198	197	orcomd 730	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ0 → ((𝑤 = 0 ∨ 0 < 𝑤) ∨ 𝑤 < 0))
199	192, 198	ecased 1360	. . . . . . . 8 ⊢ (𝑤 ∈ ℕ0 → (𝑤 = 0 ∨ 0 < 𝑤))
200	199	ad2antrr 488	. . . . . . 7 ⊢ (((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) → (𝑤 = 0 ∨ 0 < 𝑤))
201	65, 191, 200	mpjaodan 799	. . . . . 6 ⊢ (((𝑤 ∈ ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))
202	201	exp31 364	. . . . 5 ⊢ (𝑤 ∈ ℕ0 → (∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))))
203	8, 16, 202	nn0sinds 10489	. . . 4 ⊢ (𝑥 ∈ ℕ0 → ((𝜃 ∧ [𝑥 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
204	203	expd 258	. . 3 ⊢ (𝑥 ∈ ℕ0 → (𝜃 → ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))))
205	204	impcom 125	. 2 ⊢ ((𝜃 ∧ 𝑥 ∈ ℕ0) → ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
206	205	ralrimiva 2563	1 ⊢ (𝜃 → ∀𝑥 ∈ ℕ0 ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709   ∨ w3o 979   = wceq 1364  [wsb 1773   ∈ wcel 2160  ∀wral 2468  ∃wrex 2469  [wsbc 2981   class class class wbr 4025  (class class class)co 5904  0cc0 7851  1c1 7852   + caddc 7854   · cmul 7856   < clt 8033   − cmin 8169  ℕcn 8960  ℕ₀cn0 9217  ℤcz 9294  ...cfz 10050   mod cmo 10365   ∥ cdvds 11841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4140  ax-sep 4143  ax-nul 4151  ax-pow 4199  ax-pr 4234  ax-un 4458  ax-setind 4561  ax-iinf 4612  ax-cnex 7942  ax-resscn 7943  ax-1cn 7944  ax-1re 7945  ax-icn 7946  ax-addcl 7947  ax-addrcl 7948  ax-mulcl 7949  ax-mulrcl 7950  ax-addcom 7951  ax-mulcom 7952  ax-addass 7953  ax-mulass 7954  ax-distr 7955  ax-i2m1 7956  ax-0lt1 7957  ax-1rid 7958  ax-0id 7959  ax-rnegex 7960  ax-precex 7961  ax-cnre 7962  ax-pre-ltirr 7963  ax-pre-ltwlin 7964  ax-pre-lttrn 7965  ax-pre-apti 7966  ax-pre-ltadd 7967  ax-pre-mulgt0 7968  ax-pre-mulext 7969  ax-arch 7970

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2758  df-sbc 2982  df-csb 3077  df-dif 3150  df-un 3152  df-in 3154  df-ss 3161  df-nul 3442  df-if 3554  df-pw 3599  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3832  df-int 3867  df-iun 3910  df-br 4026  df-opab 4087  df-mpt 4088  df-tr 4124  df-id 4318  df-po 4321  df-iso 4322  df-iord 4391  df-on 4393  df-ilim 4394  df-suc 4396  df-iom 4615  df-xp 4657  df-rel 4658  df-cnv 4659  df-co 4660  df-dm 4661  df-rn 4662  df-res 4663  df-ima 4664  df-iota 5203  df-fun 5244  df-fn 5245  df-f 5246  df-f1 5247  df-fo 5248  df-f1o 5249  df-fv 5250  df-riota 5859  df-ov 5907  df-oprab 5908  df-mpo 5909  df-1st 6173  df-2nd 6174  df-recs 6338  df-frec 6424  df-pnf 8035  df-mnf 8036  df-xr 8037  df-ltxr 8038  df-le 8039  df-sub 8171  df-neg 8172  df-reap 8573  df-ap 8580  df-div 8671  df-inn 8961  df-2 9019  df-n0 9218  df-z 9295  df-uz 9570  df-q 9662  df-rp 9696  df-fz 10051  df-fl 10313  df-mod 10366  df-seqfrec 10491  df-exp 10566  df-cj 10898  df-re 10899  df-im 10900  df-rsqrt 11054  df-abs 11055  df-dvds 11842

This theorem is referenced by:  bezoutlemex  12049