Theorem posbezout 42756

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

Assertion

Ref	Expression
posbezout	⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem posbezout

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

Step	Hyp	Ref	Expression
1		oveq2 7419	. . . . 5 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → (𝐴 · 𝑥) = (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
2	1	oveq1d 7426	. . . 4 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)))
3	2	eqeq2d 2780	. . 3 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦))))
4		oveq2 7419	. . . . 5 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → (𝐵 · 𝑦) = (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
5	4	oveq2d 7427	. . . 4 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
6	5	eqeq2d 2780	. . 3 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)) ↔ (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))))
7		simplr 780	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℤ)
8		simpllr 787	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℕ)
9	8	nnzd 12616	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℤ)
10	7, 7	zmulcld 12705	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℤ)
11		simpr 489	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
12	11, 11	zmulcld 12705	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℤ)
13	10, 12	zaddcld 12703	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℤ)
14		2z 12625	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
15	14	a1i 11	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℤ)
16	13, 15	zaddcld 12703	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℤ)
17	9, 16	zmulcld 12705	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℤ)
18	7, 17	zaddcld 12703	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ)
19	7	zred 12699	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℝ)
20	19	renegcld 11640	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -𝑤 ∈ ℝ)
21	20	adantr 485	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 ∈ ℝ)
22		0red 11210	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ∈ ℝ)
23	17	zred 12699	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
24	23	adantr 485	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
25		df-neg 11443	. . . . . . . . . . . 12 ⊢ -𝑤 = (0 − 𝑤)
26	25	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 = (0 − 𝑤))
27	19	adantr 485	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 𝑤 ∈ ℝ)
28	22	leidd 11779	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ 0)
29		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ 𝑤)
30	22, 27, 28, 29	addge0d 11789	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ (0 + 𝑤))
31	22, 27, 22	lesubaddd 11810	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → ((0 − 𝑤) ≤ 0 ↔ 0 ≤ (0 + 𝑤)))
32	30, 31	mpbird 260	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → (0 − 𝑤) ≤ 0)
33	26, 32	eqbrtrd 5137	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 ≤ 0)
34	8	nnred 12247	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℝ)
35	16	zred 12699	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℝ)
36	8	nngt0d 12284	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < 𝐵)
37		0red 11210	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ∈ ℝ)
38		2re 12314	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
39	38	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℝ)
40	37, 39	readdcld 11237	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 + 2) ∈ ℝ)
41		2pos 12344	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
42		eqid 2769	. . . . . . . . . . . . . . . 16 ⊢ 2 = 2
43		2cn 12315	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℂ
44	43	addlidi 11397	. . . . . . . . . . . . . . . 16 ⊢ (0 + 2) = 2
45	42, 44	eqtr4i 2795	. . . . . . . . . . . . . . 15 ⊢ 2 = (0 + 2)
46	41, 45	breqtri 5140	. . . . . . . . . . . . . 14 ⊢ 0 < (0 + 2)
47	46	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (0 + 2))
48	13	zred 12699	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℝ)
49	19, 19	remulcld 11238	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℝ)
50	12	zred 12699	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℝ)
51	19	msqge0d 11781	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ (𝑤 · 𝑤))
52	11	zred 12699	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℝ)
53	52	msqge0d 11781	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ (𝑧 · 𝑧))
54	49, 50, 51, 53	addge0d 11789	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ ((𝑤 · 𝑤) + (𝑧 · 𝑧)))
55	39	leidd 11779	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ≤ 2)
56	37, 39, 48, 39, 54, 55	le2addd 11832	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 + 2) ≤ (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
57	37, 40, 35, 47, 56	ltletrd 11369	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
58	34, 35, 36, 57	mulgt0d 11364	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
59	58	adantr 485	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
60	21, 22, 24, 33, 59	lelttrd 11367	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
61	25	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → -𝑤 = (0 − 𝑤))
62	37	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ∈ ℝ)
63	34	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℝ)
64	52	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℝ)
65	64, 64	remulcld 11238	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℝ)
66	63, 65	remulcld 11238	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℝ)
67	19	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑤 ∈ ℝ)
68	67, 67	remulcld 11238	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑤 · 𝑤) ∈ ℝ)
69	38	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℝ)
70	68, 69	readdcld 11237	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℝ)
71	63, 70	remulcld 11238	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑤 · 𝑤) + 2)) ∈ ℝ)
72	71, 67	readdcld 11237	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤) ∈ ℝ)
73	66, 72	readdcld 11237	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) ∈ ℝ)
74	8	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℕ)
75	74	nnnn0d 12564	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℕ0)
76	75	nn0ge0d 12567	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 𝐵)
77	64	msqge0d 11781	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝑧 · 𝑧))
78	63, 65, 76, 77	mulge0d 11790	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝐵 · (𝑧 · 𝑧)))
79	63	recnd 11236	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℂ)
80	64	recnd 11236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℂ)
81	80, 80	mulcld 11228	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℂ)
82	79, 81	mulcld 11228	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℂ)
83	82	subidd 11556	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) = 0)
84		1red 11208	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 1 ∈ ℝ)
85	84, 70	remulcld 11238	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) ∈ ℝ)
86	85, 67	readdcld 11237	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤) ∈ ℝ)
87	20	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ∈ ℝ)
88	19	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℝ)
89	88, 88	remulcld 11238	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (𝑤 · 𝑤) ∈ ℝ)
90	38	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 2 ∈ ℝ)
91	89, 90	readdcld 11237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℝ)
92	37	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ∈ ℝ)
93	87, 87	remulcld 11238	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ∈ ℝ)
94	93, 90	readdcld 11237	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 2) ∈ ℝ)
95		1red 11208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 1 ∈ ℝ)
96	95	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 1 ∈ ℝ)
97		0le1 11736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ≤ 1
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ≤ 1)
99		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 1 ≤ -𝑤)
100	92, 96, 87, 98, 99	letrd 11366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ≤ -𝑤)
101	87, 87, 100, 99	lemulge11d 12151	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ≤ (-𝑤 · -𝑤))
102	93, 92	readdcld 11237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) ∈ ℝ)
103	93	leidd 11779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ≤ (-𝑤 · -𝑤))
104	88	recnd 11236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℂ)
105	104	negcld 11555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ∈ ℂ)
106	105, 105	mulcld 11228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ∈ ℂ)
107	106	addridd 11409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) = (-𝑤 · -𝑤))
108	107	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) = ((-𝑤 · -𝑤) + 0))
109	103, 108	breqtrd 5141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ≤ ((-𝑤 · -𝑤) + 0))
110	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < 2)
111	92, 90, 93, 110	ltadd2dd 11368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) < ((-𝑤 · -𝑤) + 2))
112	93, 102, 94, 109, 111	lelttrd 11367	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) < ((-𝑤 · -𝑤) + 2))
113	87, 93, 94, 101, 112	lelttrd 11367	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < ((-𝑤 · -𝑤) + 2))
114	104, 104	mul2negd 11668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) = (𝑤 · 𝑤))
115	114	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 2) = ((𝑤 · 𝑤) + 2))
116	113, 115	breqtrd 5141	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < ((𝑤 · 𝑤) + 2))
117	91	recnd 11236	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
118	117	subid1d 11557	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (((𝑤 · 𝑤) + 2) − 0) = ((𝑤 · 𝑤) + 2))
119	118	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) = (((𝑤 · 𝑤) + 2) − 0))
120	116, 119	breqtrd 5141	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < (((𝑤 · 𝑤) + 2) − 0))
121	87, 91, 92, 120	ltsub13d 11819	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < (((𝑤 · 𝑤) + 2) − -𝑤))
122	7	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℤ)
123	122	zcnd 12700	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℂ)
124	123, 123	mulcld 11228	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (𝑤 · 𝑤) ∈ ℂ)
125		2cnd 12318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 2 ∈ ℂ)
126	124, 125	addcld 11227	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
127	126, 123	subnegd 11575	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (((𝑤 · 𝑤) + 2) − -𝑤) = (((𝑤 · 𝑤) + 2) + 𝑤))
128	121, 127	breqtrd 5141	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < (((𝑤 · 𝑤) + 2) + 𝑤))
129	128	ex 417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (1 ≤ -𝑤 → 0 < (((𝑤 · 𝑤) + 2) + 𝑤)))
130		0zd 12602	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ∈ ℤ)
131	7, 130	zltlem1d 12647	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ 𝑤 ≤ (0 − 1)))
132		df-neg 11443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ -1 = (0 − 1)
133	132	eqcomi 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (0 − 1) = -1
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 − 1) = -1)
135	134	breq2d 5125	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 ≤ (0 − 1) ↔ 𝑤 ≤ -1))
136	131, 135	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ 𝑤 ≤ -1))
137	95	renegcld 11640	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -1 ∈ ℝ)
138	19, 137	lenegd 11792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 ≤ -1 ↔ --1 ≤ -𝑤))
139	136, 138	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ --1 ≤ -𝑤))
140		1cnd 11201	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 1 ∈ ℂ)
141	140	negnegd 11559	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → --1 = 1)
142	141	breq1d 5123	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (--1 ≤ -𝑤 ↔ 1 ≤ -𝑤))
143	139, 142	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ 1 ≤ -𝑤))
144	143	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 → 1 ≤ -𝑤))
145	144	imim1d 83	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((1 ≤ -𝑤 → 0 < (((𝑤 · 𝑤) + 2) + 𝑤)) → (𝑤 < 0 → 0 < (((𝑤 · 𝑤) + 2) + 𝑤))))
146	129, 145	mpd 16	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 → 0 < (((𝑤 · 𝑤) + 2) + 𝑤)))
147	146	imp 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < (((𝑤 · 𝑤) + 2) + 𝑤))
148	70	recnd 11236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
149	148	mullidd 11226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) = ((𝑤 · 𝑤) + 2))
150	149	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) = (1 · ((𝑤 · 𝑤) + 2)))
151	150	oveq1d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑤 · 𝑤) + 2) + 𝑤) = ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤))
152	147, 151	breqtrd 5141	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤))
153	40	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 + 2) ∈ ℝ)
154	62	leidd 11779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 0)
155		0le2 12342	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≤ 2
156	155	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 2)
157	62, 69, 154, 156	addge0d 11789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (0 + 2))
158	51	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝑤 · 𝑤))
159	62, 68, 69, 158	leadd1dd 11827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 + 2) ≤ ((𝑤 · 𝑤) + 2))
160	62, 153, 70, 157, 159	letrd 11366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ ((𝑤 · 𝑤) + 2))
161	74	nnge1d 12283	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 1 ≤ 𝐵)
162	84, 63, 70, 160, 161	lemul1ad 12153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) ≤ (𝐵 · ((𝑤 · 𝑤) + 2)))
163	85, 71, 67, 162	leadd1dd 11827	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤) ≤ ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
164	62, 86, 72, 152, 163	ltletrd 11369	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
165	83, 164	eqbrtrd 5137	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
166	66, 66, 72	ltsubadd2d 11811	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤) ↔ (𝐵 · (𝑧 · 𝑧)) < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))))
167	165, 166	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
168	62, 66, 73, 78, 167	lelttrd 11367	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
169	74	nncnd 12248	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℂ)
170	11	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℤ)
171	170	zcnd 12700	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℂ)
172	171, 171	mulcld 11228	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℂ)
173	169, 172	mulcld 11228	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℂ)
174	67	recnd 11236	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑤 ∈ ℂ)
175	174, 174	mulcld 11228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑤 · 𝑤) ∈ ℂ)
176		2cnd 12318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℂ)
177	175, 176	addcld 11227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
178	169, 177	mulcld 11228	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑤 · 𝑤) + 2)) ∈ ℂ)
179	173, 178, 174	addassd 11230	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
180	179	eqcomd 2775	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤))
181	169, 172, 177	adddid 11232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) = ((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))))
182	181	eqcomd 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) = (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))))
183	182	oveq1d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤))
184	180, 183	eqtrd 2804	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤))
185	43	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℂ)
186	172, 175, 185	addassd 11230	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2) = ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)))
187	186	eqcomd 2775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)) = (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2))
188	172, 175	addcomd 11411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + (𝑤 · 𝑤)) = ((𝑤 · 𝑤) + (𝑧 · 𝑧)))
189	188	oveq1d 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2) = (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
190	187, 189	eqtrd 2804	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)) = (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
191	190	oveq2d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) = (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
192	191	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
193	184, 192	eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
194	168, 193	breqtrd 5141	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
195	23	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
196	62, 67, 195	ltsubaddd 11809	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((0 − 𝑤) < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ↔ 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤)))
197	194, 196	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 − 𝑤) < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
198	61, 197	eqbrtrd 5137	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
199	198	ex 417	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
200	19, 37	ltnled 11356	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ ¬ 0 ≤ 𝑤))
201	200	bicomd 226	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (¬ 0 ≤ 𝑤 ↔ 𝑤 < 0))
202	201	biimpd 232	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (¬ 0 ≤ 𝑤 → 𝑤 < 0))
203	202	imim1d 83	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 < 0 → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → (¬ 0 ≤ 𝑤 → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
204	199, 203	mpd 16	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (¬ 0 ≤ 𝑤 → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
205	204	imp 411	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ ¬ 0 ≤ 𝑤) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
206	60, 205	pm2.61dan 824	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
207	20, 23	posdifd 11800	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (-𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ↔ 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤)))
208	206, 207	mpbid 235	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤))
209	17	zcnd 12700	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
210	7	zcnd 12700	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℂ)
211	209, 210	subnegd 11575	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
212	209, 210	addcomd 11411	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤) = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
213	211, 212	eqtrd 2804	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤) = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
214	208, 213	breqtrd 5141	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
215	18, 214	jca 520	. . . . 5 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ ∧ 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
216		elnnz 12600	. . . . 5 ⊢ ((𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℕ ↔ ((𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ ∧ 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
217	215, 216	sylibr 237	. . . 4 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℕ)
218	217	adantr 485	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℕ)
219		simplr 780	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝑧 ∈ ℤ)
220		simp-4l 794	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝐴 ∈ ℕ)
221	220	nnzd 12616	. . . . 5 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝐴 ∈ ℤ)
222		simpllr 787	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝑤 ∈ ℤ)
223	222, 222	zmulcld 12705	. . . . . . 7 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑤 · 𝑤) ∈ ℤ)
224	219, 219	zmulcld 12705	. . . . . . 7 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑧 · 𝑧) ∈ ℤ)
225	223, 224	zaddcld 12703	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℤ)
226	14	a1i 11	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 2 ∈ ℤ)
227	225, 226	zaddcld 12703	. . . . 5 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℤ)
228	221, 227	zmulcld 12705	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℤ)
229	219, 228	zsubcld 12704	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ)
230		simpr 489	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
231		simplll 786	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐴 ∈ ℕ)
232	231	nncnd 12248	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐴 ∈ ℂ)
233	232, 210	mulcld 11228	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · 𝑤) ∈ ℂ)
234	8	nncnd 12248	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℂ)
235	210, 210	mulcld 11228	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℂ)
236	11	zcnd 12700	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℂ)
237	236, 236	mulcld 11228	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℂ)
238	235, 237	addcld 11227	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℂ)
239		2cnd 12318	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℂ)
240	238, 239	addcld 11227	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℂ)
241	234, 240	mulcld 11228	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
242	232, 241	mulcld 11228	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℂ)
243	234, 236	mulcld 11228	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · 𝑧) ∈ ℂ)
244	233, 242, 243	ppncand 11608	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
245		eqidd 2770	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
246	244, 245	eqtr2d 2805	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
247	16	zcnd 12700	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℂ)
248	232, 234, 247	mul12d 11418	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) = (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
249	248	oveq2d 7427	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
250	249	oveq2d 7427	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
251	246, 250	eqtrd 2804	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
252	232, 210, 209	adddid 11232	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
253	252	eqcomd 2775	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
254	232, 240	mulcld 11228	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
255	234, 236, 254	subdid 11669	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
256	255	eqcomd 2775	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
257	253, 256	oveq12d 7429	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
258	251, 257	eqtrd 2804	. . . . 5 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
259	258	adantr 485	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
260	230, 259	eqtrd 2804	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
261	3, 6, 218, 229, 260	2rspcedvdw 3604	. 2 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))
262		nnz 12611	. . . . 5 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
263	262	adantr 485	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈ ℤ)
264		nnz 12611	. . . . 5 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℤ)
265	264	adantl 486	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℤ)
266	263, 265	jca 520	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))
267		bezout 16600	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑤 ∈ ℤ ∃𝑧 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
268	266, 267	syl 18	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑤 ∈ ℤ ∃𝑧 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
269	261, 268	r19.29vva 3231	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∃wrex 3095   class class class wbr 5113  (class class class)co 7411  ℂcc 11097  ℝcr 11098  0cc0 11099  1c1 11100   + caddc 11102   · cmul 11104   < clt 11242   ≤ cle 11243   − cmin 11440  -cneg 11441  ℕcn 12232  2c2 12294  ℤcz 12590   gcd cgcd 16551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176  ax-pre-sup 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-sup 9401  df-inf 9402  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-div 11871  df-nn 12233  df-2 12302  df-3 12303  df-n0 12504  df-z 12591  df-uz 12862  df-rp 13016  df-fl 13824  df-mod 13902  df-seq 14037  df-exp 14097  df-cj 15149  df-re 15150  df-im 15151  df-sqrt 15285  df-abs 15286  df-dvds 16310  df-gcd 16552

This theorem is referenced by:  primrootscoprbij2  42759