posbezout

Description: Bezout's identity restricted on positive integers in all but one variable. (Contributed by metakunt, 26-Apr-2025)

		Ref	Expression
	Assertion	posbezout	$⊢ (A \in ℕ \land B \in ℕ) \to \exists x \in ℕ \exists y \in ℤ A \gcd B = A x + B y$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = w + B (w w + z z + 2) \to A x = A (w + B (w w + z z + 2))$
2	1	oveq1d	$⊢ x = w + B (w w + z z + 2) \to A x + B y = A (w + B (w w + z z + 2)) + B y$
3	2	eqeq2d	$⊢ x = w + B (w w + z z + 2) \to (A \gcd B = A x + B y \leftrightarrow A \gcd B = A (w + B (w w + z z + 2)) + B y)$
4		oveq2	$⊢ y = z - A (w w + z z + 2) \to B y = B (z - A (w w + z z + 2))$
5	4	oveq2d	$⊢ y = z - A (w w + z z + 2) \to A (w + B (w w + z z + 2)) + B y = A (w + B (w w + z z + 2)) + B (z - A (w w + z z + 2))$
6	5	eqeq2d	$⊢ y = z - A (w w + z z + 2) \to (A \gcd B = A (w + B (w w + z z + 2)) + B y \leftrightarrow A \gcd B = A (w + B (w w + z z + 2)) + B (z - A (w w + z z + 2)))$
7		simplr	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w \in ℤ$
8		simpllr	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B \in ℕ$
9	8	nnzd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B \in ℤ$
10	7 7	zmulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w w \in ℤ$
11		simpr	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to z \in ℤ$
12	11 11	zmulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to z z \in ℤ$
13	10 12	zaddcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w w + z z \in ℤ$
14		2z	$⊢ 2 \in ℤ$
15	14	a1i	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 2 \in ℤ$
16	13 15	zaddcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w w + z z + 2 \in ℤ$
17	9 16	zmulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B (w w + z z + 2) \in ℤ$
18	7 17	zaddcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w + B (w w + z z + 2) \in ℤ$
19	7	zred	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w \in ℝ$
20	19	renegcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to - w \in ℝ$
21	20	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to - w \in ℝ$
22		0red	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to 0 \in ℝ$
23	17	zred	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B (w w + z z + 2) \in ℝ$
24	23	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to B (w w + z z + 2) \in ℝ$
25		df-neg	$⊢ - w = 0 - w$
26	25	a1i	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to - w = 0 - w$
27	19	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to w \in ℝ$
28	22	leidd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to 0 \leq 0$
29		simpr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to 0 \leq w$
30	22 27 28 29	addge0d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to 0 \leq 0 + w$
31	22 27 22	lesubaddd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to (0 - w \leq 0 \leftrightarrow 0 \leq 0 + w)$
32	30 31	mpbird	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to 0 - w \leq 0$
33	26 32	eqbrtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to - w \leq 0$
34	8	nnred	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B \in ℝ$
35	16	zred	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w w + z z + 2 \in ℝ$
36	8	nngt0d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 < B$
37		0red	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 \in ℝ$
38		2re	$⊢ 2 \in ℝ$
39	38	a1i	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 2 \in ℝ$
40	37 39	readdcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 + 2 \in ℝ$
41		2pos	$⊢ 0 < 2$
42		eqid	$⊢ 2 = 2$
43		2cn	$⊢ 2 \in ℂ$
44	43	addlidi	$⊢ 0 + 2 = 2$
45	42 44	eqtr4i	$⊢ 2 = 0 + 2$
46	41 45	breqtri	$⊢ 0 < 0 + 2$
47	46	a1i	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 < 0 + 2$
48	13	zred	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w w + z z \in ℝ$
49	19 19	remulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w w \in ℝ$
50	12	zred	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to z z \in ℝ$
51	19	msqge0d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 \leq w w$
52	11	zred	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to z \in ℝ$
53	52	msqge0d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 \leq z z$
54	49 50 51 53	addge0d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 \leq w w + z z$
55	39	leidd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 2 \leq 2$
56	37 39 48 39 54 55	le2addd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 + 2 \leq w w + z z + 2$
57	37 40 35 47 56	ltletrd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 < w w + z z + 2$
58	34 35 36 57	mulgt0d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 < B (w w + z z + 2)$
59	58	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to 0 < B (w w + z z + 2)$
60	21 22 24 33 59	lelttrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 0 \leq w) \to - w < B (w w + z z + 2)$
61	25	a1i	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to - w = 0 - w$
62	37	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 \in ℝ$
63	34	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B \in ℝ$
64	52	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z \in ℝ$
65	64 64	remulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z z \in ℝ$
66	63 65	remulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z \in ℝ$
67	19	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to w \in ℝ$
68	67 67	remulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to w w \in ℝ$
69	38	a1i	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 2 \in ℝ$
70	68 69	readdcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to w w + 2 \in ℝ$
71	63 70	remulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B (w w + 2) \in ℝ$
72	71 67	readdcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B (w w + 2) + w \in ℝ$
73	66 72	readdcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z + B (w w + 2) + w \in ℝ$
74	8	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B \in ℕ$
75	74	nnnn0d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B \in ℕ_{0}$
76	75	nn0ge0d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 \leq B$
77	64	msqge0d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 \leq z z$
78	63 65 76 77	mulge0d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 \leq B z z$
79	63	recnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B \in ℂ$
80	64	recnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z \in ℂ$
81	80 80	mulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z z \in ℂ$
82	79 81	mulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z \in ℂ$
83	82	subidd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z - B z z = 0$
84		1red	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 1 \in ℝ$
85	84 70	remulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 1 (w w + 2) \in ℝ$
86	85 67	readdcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 1 (w w + 2) + w \in ℝ$
87	20	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to - w \in ℝ$
88	19	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w \in ℝ$
89	88 88	remulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w w \in ℝ$
90	38	a1i	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to 2 \in ℝ$
91	89 90	readdcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w w + 2 \in ℝ$
92	37	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to 0 \in ℝ$
93	87 87	remulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) \in ℝ$
94	93 90	readdcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) + 2 \in ℝ$
95		1red	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 1 \in ℝ$
96	95	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to 1 \in ℝ$
97		0le1	$⊢ 0 \leq 1$
98	97	a1i	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to 0 \leq 1$
99		simpr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to 1 \leq - w$
100	92 96 87 98 99	letrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to 0 \leq - w$
101	87 87 100 99	lemulge11d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to - w \leq (- w) (- w)$
102	93 92	readdcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) + 0 \in ℝ$
103	93	leidd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) \leq (- w) (- w)$
104	88	recnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w \in ℂ$
105	104	negcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to - w \in ℂ$
106	105 105	mulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) \in ℂ$
107	106	addridd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) + 0 = (- w) (- w)$
108	107	eqcomd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) = (- w) (- w) + 0$
109	103 108	breqtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) \leq (- w) (- w) + 0$
110	41	a1i	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to 0 < 2$
111	92 90 93 110	ltadd2dd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) + 0 < (- w) (- w) + 2$
112	93 102 94 109 111	lelttrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) < (- w) (- w) + 2$
113	87 93 94 101 112	lelttrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to - w < (- w) (- w) + 2$
114	104 104	mul2negd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) = w w$
115	114	oveq1d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to (- w) (- w) + 2 = w w + 2$
116	113 115	breqtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to - w < w w + 2$
117	91	recnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w w + 2 \in ℂ$
118	117	subid1d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w w + 2 - 0 = w w + 2$
119	118	eqcomd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w w + 2 = w w + 2 - 0$
120	116 119	breqtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to - w < w w + 2 - 0$
121	87 91 92 120	ltsub13d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to 0 < w w + 2 - (- w)$
122	7	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w \in ℤ$
123	122	zcnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w \in ℂ$
124	123 123	mulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w w \in ℂ$
125		2cnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to 2 \in ℂ$
126	124 125	addcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w w + 2 \in ℂ$
127	126 123	subnegd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to w w + 2 - (- w) = w w + 2 + w$
128	121 127	breqtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land 1 \leq - w) \to 0 < w w + 2 + w$
129	128	ex	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (1 \leq - w \to 0 < w w + 2 + w)$
130		0zd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 \in ℤ$
131	7 130	zltlem1d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w < 0 \leftrightarrow w \leq 0 - 1)$
132		df-neg	$⊢ - 1 = 0 - 1$
133	132	eqcomi	$⊢ 0 - 1 = - 1$
134	133	a1i	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 - 1 = - 1$
135	134	breq2d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w \leq 0 - 1 \leftrightarrow w \leq - 1)$
136	131 135	bitrd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w < 0 \leftrightarrow w \leq - 1)$
137	95	renegcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to - 1 \in ℝ$
138	19 137	lenegd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w \leq - 1 \leftrightarrow - -1 \leq - w)$
139	136 138	bitrd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w < 0 \leftrightarrow - -1 \leq - w)$
140		1cnd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 1 \in ℂ$
141	140	negnegd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to - -1 = 1$
142	141	breq1d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (- -1 \leq - w \leftrightarrow 1 \leq - w)$
143	139 142	bitrd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w < 0 \leftrightarrow 1 \leq - w)$
144	143	biimpd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w < 0 \to 1 \leq - w)$
145	144	imim1d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to ((1 \leq - w \to 0 < w w + 2 + w) \to (w < 0 \to 0 < w w + 2 + w))$
146	129 145	mpd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w < 0 \to 0 < w w + 2 + w)$
147	146	imp	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 < w w + 2 + w$
148	70	recnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to w w + 2 \in ℂ$
149	148	mullidd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 1 (w w + 2) = w w + 2$
150	149	eqcomd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to w w + 2 = 1 (w w + 2)$
151	150	oveq1d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to w w + 2 + w = 1 (w w + 2) + w$
152	147 151	breqtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 < 1 (w w + 2) + w$
153	40	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 + 2 \in ℝ$
154	62	leidd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 \leq 0$
155		0le2	$⊢ 0 \leq 2$
156	155	a1i	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 \leq 2$
157	62 69 154 156	addge0d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 \leq 0 + 2$
158	51	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 \leq w w$
159	62 68 69 158	leadd1dd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 + 2 \leq w w + 2$
160	62 153 70 157 159	letrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 \leq w w + 2$
161	74	nnge1d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 1 \leq B$
162	84 63 70 160 161	lemul1ad	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 1 (w w + 2) \leq B (w w + 2)$
163	85 71 67 162	leadd1dd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 1 (w w + 2) + w \leq B (w w + 2) + w$
164	62 86 72 152 163	ltletrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 < B (w w + 2) + w$
165	83 164	eqbrtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z - B z z < B (w w + 2) + w$
166	66 66 72	ltsubadd2d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to (B z z - B z z < B (w w + 2) + w \leftrightarrow B z z < B z z + B (w w + 2) + w)$
167	165 166	mpbid	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z < B z z + B (w w + 2) + w$
168	62 66 73 78 167	lelttrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 < B z z + B (w w + 2) + w$
169	74	nncnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B \in ℂ$
170	11	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z \in ℤ$
171	170	zcnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z \in ℂ$
172	171 171	mulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z z \in ℂ$
173	169 172	mulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z \in ℂ$
174	67	recnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to w \in ℂ$
175	174 174	mulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to w w \in ℂ$
176		2cnd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 2 \in ℂ$
177	175 176	addcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to w w + 2 \in ℂ$
178	169 177	mulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B (w w + 2) \in ℂ$
179	173 178 174	addassd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z + B (w w + 2) + w = B z z + B (w w + 2) + w$
180	179	eqcomd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z + B (w w + 2) + w = B z z + B (w w + 2) + w$
181	169 172 177	adddid	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B (z z + w w + 2) = B z z + B (w w + 2)$
182	181	eqcomd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z + B (w w + 2) = B (z z + w w + 2)$
183	182	oveq1d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z + B (w w + 2) + w = B (z z + w w + 2) + w$
184	180 183	eqtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z + B (w w + 2) + w = B (z z + w w + 2) + w$
185	43	a1i	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 2 \in ℂ$
186	172 175 185	addassd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z z + w w + 2 = z z + w w + 2$
187	186	eqcomd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z z + w w + 2 = z z + w w + 2$
188	172 175	addcomd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z z + w w = w w + z z$
189	188	oveq1d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z z + w w + 2 = w w + z z + 2$
190	187 189	eqtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to z z + w w + 2 = w w + z z + 2$
191	190	oveq2d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B (z z + w w + 2) = B (w w + z z + 2)$
192	191	oveq1d	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B (z z + w w + 2) + w = B (w w + z z + 2) + w$
193	184 192	eqtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B z z + B (w w + 2) + w = B (w w + z z + 2) + w$
194	168 193	breqtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 < B (w w + z z + 2) + w$
195	23	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to B (w w + z z + 2) \in ℝ$
196	62 67 195	ltsubaddd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to (0 - w < B (w w + z z + 2) \leftrightarrow 0 < B (w w + z z + 2) + w)$
197	194 196	mpbird	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to 0 - w < B (w w + z z + 2)$
198	61 197	eqbrtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land w < 0) \to - w < B (w w + z z + 2)$
199	198	ex	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w < 0 \to - w < B (w w + z z + 2))$
200	19 37	ltnled	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w < 0 \leftrightarrow \neg 0 \leq w)$
201	200	bicomd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (\neg 0 \leq w \leftrightarrow w < 0)$
202	201	biimpd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (\neg 0 \leq w \to w < 0)$
203	202	imim1d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to ((w < 0 \to - w < B (w w + z z + 2)) \to (\neg 0 \leq w \to - w < B (w w + z z + 2)))$
204	199 203	mpd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (\neg 0 \leq w \to - w < B (w w + z z + 2))$
205	204	imp	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land \neg 0 \leq w) \to - w < B (w w + z z + 2)$
206	60 205	pm2.61dan	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to - w < B (w w + z z + 2)$
207	20 23	posdifd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (- w < B (w w + z z + 2) \leftrightarrow 0 < B (w w + z z + 2) - (- w))$
208	206 207	mpbid	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 < B (w w + z z + 2) - (- w)$
209	17	zcnd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B (w w + z z + 2) \in ℂ$
210	7	zcnd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w \in ℂ$
211	209 210	subnegd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B (w w + z z + 2) - (- w) = B (w w + z z + 2) + w$
212	209 210	addcomd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B (w w + z z + 2) + w = w + B (w w + z z + 2)$
213	211 212	eqtrd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B (w w + z z + 2) - (- w) = w + B (w w + z z + 2)$
214	208 213	breqtrd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 0 < w + B (w w + z z + 2)$
215	18 214	jca	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to (w + B (w w + z z + 2) \in ℤ \land 0 < w + B (w w + z z + 2))$
216		elnnz	$⊢ w + B (w w + z z + 2) \in ℕ \leftrightarrow (w + B (w w + z z + 2) \in ℤ \land 0 < w + B (w w + z z + 2))$
217	215 216	sylibr	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w + B (w w + z z + 2) \in ℕ$
218	217	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to w + B (w w + z z + 2) \in ℕ$
219		simplr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to z \in ℤ$
220		simp-4l	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to A \in ℕ$
221	220	nnzd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to A \in ℤ$
222		simpllr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to w \in ℤ$
223	222 222	zmulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to w w \in ℤ$
224	219 219	zmulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to z z \in ℤ$
225	223 224	zaddcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to w w + z z \in ℤ$
226	14	a1i	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to 2 \in ℤ$
227	225 226	zaddcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to w w + z z + 2 \in ℤ$
228	221 227	zmulcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to A (w w + z z + 2) \in ℤ$
229	219 228	zsubcld	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to z - A (w w + z z + 2) \in ℤ$
230		simpr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to A \gcd B = A w + B z$
231		simplll	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A \in ℕ$
232	231	nncnd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A \in ℂ$
233	232 210	mulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A w \in ℂ$
234	8	nncnd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B \in ℂ$
235	210 210	mulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w w \in ℂ$
236	11	zcnd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to z \in ℂ$
237	236 236	mulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to z z \in ℂ$
238	235 237	addcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w w + z z \in ℂ$
239		2cnd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to 2 \in ℂ$
240	238 239	addcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w w + z z + 2 \in ℂ$
241	234 240	mulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B (w w + z z + 2) \in ℂ$
242	232 241	mulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A B (w w + z z + 2) \in ℂ$
243	234 236	mulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B z \in ℂ$
244	233 242 243	ppncand	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A w + A B (w w + z z + 2) + (B z - A B (w w + z z + 2)) = A w + B z$
245		eqidd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A w + B z = A w + B z$
246	244 245	eqtr2d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A w + B z = A w + A B (w w + z z + 2) + (B z - A B (w w + z z + 2))$
247	16	zcnd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to w w + z z + 2 \in ℂ$
248	232 234 247	mul12d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A B (w w + z z + 2) = B A (w w + z z + 2)$
249	248	oveq2d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B z - A B (w w + z z + 2) = B z - B A (w w + z z + 2)$
250	249	oveq2d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A w + A B (w w + z z + 2) + (B z - A B (w w + z z + 2)) = A w + A B (w w + z z + 2) + (B z - B A (w w + z z + 2))$
251	246 250	eqtrd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A w + B z = A w + A B (w w + z z + 2) + (B z - B A (w w + z z + 2))$
252	232 210 209	adddid	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A (w + B (w w + z z + 2)) = A w + A B (w w + z z + 2)$
253	252	eqcomd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A w + A B (w w + z z + 2) = A (w + B (w w + z z + 2))$
254	232 240	mulcld	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A (w w + z z + 2) \in ℂ$
255	234 236 254	subdid	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B (z - A (w w + z z + 2)) = B z - B A (w w + z z + 2)$
256	255	eqcomd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to B z - B A (w w + z z + 2) = B (z - A (w w + z z + 2))$
257	253 256	oveq12d	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A w + A B (w w + z z + 2) + (B z - B A (w w + z z + 2)) = A (w + B (w w + z z + 2)) + B (z - A (w w + z z + 2))$
258	251 257	eqtrd	$⊢ (((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \to A w + B z = A (w + B (w w + z z + 2)) + B (z - A (w w + z z + 2))$
259	258	adantr	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to A w + B z = A (w + B (w w + z z + 2)) + B (z - A (w w + z z + 2))$
260	230 259	eqtrd	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to A \gcd B = A (w + B (w w + z z + 2)) + B (z - A (w w + z z + 2))$
261	3 6 218 229 260	2rspcedvdw	$⊢ ((((A \in ℕ \land B \in ℕ) \land w \in ℤ) \land z \in ℤ) \land A \gcd B = A w + B z) \to \exists x \in ℕ \exists y \in ℤ A \gcd B = A x + B y$
262		nnz	$⊢ A \in ℕ \to A \in ℤ$
263	262	adantr	$⊢ (A \in ℕ \land B \in ℕ) \to A \in ℤ$
264		nnz	$⊢ B \in ℕ \to B \in ℤ$
265	264	adantl	$⊢ (A \in ℕ \land B \in ℕ) \to B \in ℤ$
266	263 265	jca	$⊢ (A \in ℕ \land B \in ℕ) \to (A \in ℤ \land B \in ℤ)$
267		bezout	$⊢ (A \in ℤ \land B \in ℤ) \to \exists w \in ℤ \exists z \in ℤ A \gcd B = A w + B z$
268	266 267	syl	$⊢ (A \in ℕ \land B \in ℕ) \to \exists w \in ℤ \exists z \in ℤ A \gcd B = A w + B z$
269	261 268	r19.29vva	$⊢ (A \in ℕ \land B \in ℕ) \to \exists x \in ℕ \exists y \in ℤ A \gcd B = A x + B y$

Metamath Proof Explorer

Theorem posbezout

Proof