Theorem posbezout 42867

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 7418	. . . . 5 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → (𝐴 · 𝑥) = (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
2	1	oveq1d 7425	. . . 4 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)))
3	2	eqeq2d 2774	. . 3 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦))))
4		oveq2 7418	. . . . 5 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → (𝐵 · 𝑦) = (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
5	4	oveq2d 7426	. . . 4 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
6	5	eqeq2d 2774	. . 3 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)) ↔ (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))))
7		simplr 780	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℤ)
8		simpllr 787	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℕ)
9	8	nnzd 12612	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℤ)
10	7, 7	zmulcld 12701	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℤ)
11		simpr 489	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
12	11, 11	zmulcld 12701	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℤ)
13	10, 12	zaddcld 12699	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℤ)
14		2z 12621	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
15	14	a1i 11	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℤ)
16	13, 15	zaddcld 12699	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℤ)
17	9, 16	zmulcld 12701	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℤ)
18	7, 17	zaddcld 12699	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ)
19	7	zred 12695	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℝ)
20	19	renegcld 11636	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -𝑤 ∈ ℝ)
21	20	adantr 485	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 ∈ ℝ)
22		0red 11206	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ∈ ℝ)
23	17	zred 12695	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
24	23	adantr 485	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
25		df-neg 11439	. . . . . . . . . . . 12 ⊢ -𝑤 = (0 − 𝑤)
26	25	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 = (0 − 𝑤))
27	19	adantr 485	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 𝑤 ∈ ℝ)
28	22	leidd 11775	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ 0)
29		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ 𝑤)
30	22, 27, 28, 29	addge0d 11785	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ (0 + 𝑤))
31	22, 27, 22	lesubaddd 11806	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → ((0 − 𝑤) ≤ 0 ↔ 0 ≤ (0 + 𝑤)))
32	30, 31	mpbird 260	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → (0 − 𝑤) ≤ 0)
33	26, 32	eqbrtrd 5133	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 ≤ 0)
34	8	nnred 12243	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℝ)
35	16	zred 12695	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℝ)
36	8	nngt0d 12280	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < 𝐵)
37		0red 11206	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ∈ ℝ)
38		2re 12310	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
39	38	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℝ)
40	37, 39	readdcld 11233	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 + 2) ∈ ℝ)
41		2pos 12340	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
42		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ 2 = 2
43		2cn 12311	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℂ
44	43	addlidi 11393	. . . . . . . . . . . . . . . 16 ⊢ (0 + 2) = 2
45	42, 44	eqtr4i 2789	. . . . . . . . . . . . . . 15 ⊢ 2 = (0 + 2)
46	41, 45	breqtri 5136	. . . . . . . . . . . . . 14 ⊢ 0 < (0 + 2)
47	46	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (0 + 2))
48	13	zred 12695	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℝ)
49	19, 19	remulcld 11234	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℝ)
50	12	zred 12695	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℝ)
51	19	msqge0d 11777	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ (𝑤 · 𝑤))
52	11	zred 12695	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℝ)
53	52	msqge0d 11777	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ (𝑧 · 𝑧))
54	49, 50, 51, 53	addge0d 11785	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ ((𝑤 · 𝑤) + (𝑧 · 𝑧)))
55	39	leidd 11775	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ≤ 2)
56	37, 39, 48, 39, 54, 55	le2addd 11828	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 + 2) ≤ (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
57	37, 40, 35, 47, 56	ltletrd 11365	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
58	34, 35, 36, 57	mulgt0d 11360	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
59	58	adantr 485	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
60	21, 22, 24, 33, 59	lelttrd 11363	. . . . . . . . 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 11234	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℝ)
66	63, 65	remulcld 11234	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℝ)
67	19	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑤 ∈ ℝ)
68	67, 67	remulcld 11234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑤 · 𝑤) ∈ ℝ)
69	38	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℝ)
70	68, 69	readdcld 11233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℝ)
71	63, 70	remulcld 11234	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑤 · 𝑤) + 2)) ∈ ℝ)
72	71, 67	readdcld 11233	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤) ∈ ℝ)
73	66, 72	readdcld 11233	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) ∈ ℝ)
74	8	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℕ)
75	74	nnnn0d 12560	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℕ0)
76	75	nn0ge0d 12563	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 𝐵)
77	64	msqge0d 11777	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝑧 · 𝑧))
78	63, 65, 76, 77	mulge0d 11786	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝐵 · (𝑧 · 𝑧)))
79	63	recnd 11232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℂ)
80	64	recnd 11232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℂ)
81	80, 80	mulcld 11224	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℂ)
82	79, 81	mulcld 11224	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℂ)
83	82	subidd 11552	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) = 0)
84		1red 11204	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 1 ∈ ℝ)
85	84, 70	remulcld 11234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) ∈ ℝ)
86	85, 67	readdcld 11233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤) ∈ ℝ)
87	20	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ∈ ℝ)
88	19	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℝ)
89	88, 88	remulcld 11234	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (𝑤 · 𝑤) ∈ ℝ)
90	38	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 2 ∈ ℝ)
91	89, 90	readdcld 11233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℝ)
92	37	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ∈ ℝ)
93	87, 87	remulcld 11234	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ∈ ℝ)
94	93, 90	readdcld 11233	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 2) ∈ ℝ)
95		1red 11204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 1 ∈ ℝ)
96	95	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 1 ∈ ℝ)
97		0le1 11732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ≤ 1
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ≤ 1)
99		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 1 ≤ -𝑤)
100	92, 96, 87, 98, 99	letrd 11362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ≤ -𝑤)
101	87, 87, 100, 99	lemulge11d 12147	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ≤ (-𝑤 · -𝑤))
102	93, 92	readdcld 11233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) ∈ ℝ)
103	93	leidd 11775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ≤ (-𝑤 · -𝑤))
104	88	recnd 11232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℂ)
105	104	negcld 11551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ∈ ℂ)
106	105, 105	mulcld 11224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ∈ ℂ)
107	106	addridd 11405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) = (-𝑤 · -𝑤))
108	107	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) = ((-𝑤 · -𝑤) + 0))
109	103, 108	breqtrd 5137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ≤ ((-𝑤 · -𝑤) + 0))
110	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < 2)
111	92, 90, 93, 110	ltadd2dd 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) < ((-𝑤 · -𝑤) + 2))
112	93, 102, 94, 109, 111	lelttrd 11363	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) < ((-𝑤 · -𝑤) + 2))
113	87, 93, 94, 101, 112	lelttrd 11363	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < ((-𝑤 · -𝑤) + 2))
114	104, 104	mul2negd 11664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) = (𝑤 · 𝑤))
115	114	oveq1d 7425	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 2) = ((𝑤 · 𝑤) + 2))
116	113, 115	breqtrd 5137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < ((𝑤 · 𝑤) + 2))
117	91	recnd 11232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
118	117	subid1d 11553	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (((𝑤 · 𝑤) + 2) − 0) = ((𝑤 · 𝑤) + 2))
119	118	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) = (((𝑤 · 𝑤) + 2) − 0))
120	116, 119	breqtrd 5137	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < (((𝑤 · 𝑤) + 2) − 0))
121	87, 91, 92, 120	ltsub13d 11815	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < (((𝑤 · 𝑤) + 2) − -𝑤))
122	7	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℤ)
123	122	zcnd 12696	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℂ)
124	123, 123	mulcld 11224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (𝑤 · 𝑤) ∈ ℂ)
125		2cnd 12314	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 2 ∈ ℂ)
126	124, 125	addcld 11223	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
127	126, 123	subnegd 11571	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (((𝑤 · 𝑤) + 2) − -𝑤) = (((𝑤 · 𝑤) + 2) + 𝑤))
128	121, 127	breqtrd 5137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < (((𝑤 · 𝑤) + 2) + 𝑤))
129	128	ex 417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (1 ≤ -𝑤 → 0 < (((𝑤 · 𝑤) + 2) + 𝑤)))
130		0zd 12598	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ∈ ℤ)
131	7, 130	zltlem1d 12643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ 𝑤 ≤ (0 − 1)))
132		df-neg 11439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ -1 = (0 − 1)
133	132	eqcomi 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (0 − 1) = -1
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 − 1) = -1)
135	134	breq2d 5121	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 ≤ (0 − 1) ↔ 𝑤 ≤ -1))
136	131, 135	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ 𝑤 ≤ -1))
137	95	renegcld 11636	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -1 ∈ ℝ)
138	19, 137	lenegd 11788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 ≤ -1 ↔ --1 ≤ -𝑤))
139	136, 138	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ --1 ≤ -𝑤))
140		1cnd 11197	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 1 ∈ ℂ)
141	140	negnegd 11555	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → --1 = 1)
142	141	breq1d 5119	. . . . . . . . . . . . . . . . . . . . . . . . 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 11232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
149	148	mullidd 11222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) = ((𝑤 · 𝑤) + 2))
150	149	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) = (1 · ((𝑤 · 𝑤) + 2)))
151	150	oveq1d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑤 · 𝑤) + 2) + 𝑤) = ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤))
152	147, 151	breqtrd 5137	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤))
153	40	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 + 2) ∈ ℝ)
154	62	leidd 11775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 0)
155		0le2 12338	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≤ 2
156	155	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 2)
157	62, 69, 154, 156	addge0d 11785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (0 + 2))
158	51	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝑤 · 𝑤))
159	62, 68, 69, 158	leadd1dd 11823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 + 2) ≤ ((𝑤 · 𝑤) + 2))
160	62, 153, 70, 157, 159	letrd 11362	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ ((𝑤 · 𝑤) + 2))
161	74	nnge1d 12279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 1 ≤ 𝐵)
162	84, 63, 70, 160, 161	lemul1ad 12149	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) ≤ (𝐵 · ((𝑤 · 𝑤) + 2)))
163	85, 71, 67, 162	leadd1dd 11823	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤) ≤ ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
164	62, 86, 72, 152, 163	ltletrd 11365	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
165	83, 164	eqbrtrd 5133	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
166	66, 66, 72	ltsubadd2d 11807	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤) ↔ (𝐵 · (𝑧 · 𝑧)) < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))))
167	165, 166	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
168	62, 66, 73, 78, 167	lelttrd 11363	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
169	74	nncnd 12244	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℂ)
170	11	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℤ)
171	170	zcnd 12696	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℂ)
172	171, 171	mulcld 11224	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℂ)
173	169, 172	mulcld 11224	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℂ)
174	67	recnd 11232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑤 ∈ ℂ)
175	174, 174	mulcld 11224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑤 · 𝑤) ∈ ℂ)
176		2cnd 12314	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℂ)
177	175, 176	addcld 11223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
178	169, 177	mulcld 11224	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑤 · 𝑤) + 2)) ∈ ℂ)
179	173, 178, 174	addassd 11226	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
180	179	eqcomd 2769	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤))
181	169, 172, 177	adddid 11228	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) = ((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))))
182	181	eqcomd 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) = (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))))
183	182	oveq1d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤))
184	180, 183	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤))
185	43	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℂ)
186	172, 175, 185	addassd 11226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2) = ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)))
187	186	eqcomd 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)) = (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2))
188	172, 175	addcomd 11407	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + (𝑤 · 𝑤)) = ((𝑤 · 𝑤) + (𝑧 · 𝑧)))
189	188	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2) = (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
190	187, 189	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)) = (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
191	190	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) = (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
192	191	oveq1d 7425	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
193	184, 192	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
194	168, 193	breqtrd 5137	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
195	23	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
196	62, 67, 195	ltsubaddd 11805	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((0 − 𝑤) < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ↔ 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤)))
197	194, 196	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 − 𝑤) < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
198	61, 197	eqbrtrd 5133	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
199	198	ex 417	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
200	19, 37	ltnled 11352	. . . . . . . . . . . . . 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 11796	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (-𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ↔ 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤)))
208	206, 207	mpbid 235	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤))
209	17	zcnd 12696	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
210	7	zcnd 12696	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℂ)
211	209, 210	subnegd 11571	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
212	209, 210	addcomd 11407	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤) = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
213	211, 212	eqtrd 2798	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤) = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
214	208, 213	breqtrd 5137	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
215	18, 214	jca 520	. . . . 5 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ ∧ 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
216		elnnz 12596	. . . . 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 12612	. . . . 5 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝐴 ∈ ℤ)
222		simpllr 787	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝑤 ∈ ℤ)
223	222, 222	zmulcld 12701	. . . . . . 7 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑤 · 𝑤) ∈ ℤ)
224	219, 219	zmulcld 12701	. . . . . . 7 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑧 · 𝑧) ∈ ℤ)
225	223, 224	zaddcld 12699	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℤ)
226	14	a1i 11	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 2 ∈ ℤ)
227	225, 226	zaddcld 12699	. . . . 5 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℤ)
228	221, 227	zmulcld 12701	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℤ)
229	219, 228	zsubcld 12700	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ)
230		simpr 489	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
231		simplll 786	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐴 ∈ ℕ)
232	231	nncnd 12244	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐴 ∈ ℂ)
233	232, 210	mulcld 11224	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · 𝑤) ∈ ℂ)
234	8	nncnd 12244	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℂ)
235	210, 210	mulcld 11224	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℂ)
236	11	zcnd 12696	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℂ)
237	236, 236	mulcld 11224	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℂ)
238	235, 237	addcld 11223	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℂ)
239		2cnd 12314	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℂ)
240	238, 239	addcld 11223	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℂ)
241	234, 240	mulcld 11224	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
242	232, 241	mulcld 11224	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℂ)
243	234, 236	mulcld 11224	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · 𝑧) ∈ ℂ)
244	233, 242, 243	ppncand 11604	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
245		eqidd 2764	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
246	244, 245	eqtr2d 2799	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
247	16	zcnd 12696	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℂ)
248	232, 234, 247	mul12d 11414	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) = (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
249	248	oveq2d 7426	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
250	249	oveq2d 7426	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
251	246, 250	eqtrd 2798	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
252	232, 210, 209	adddid 11228	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
253	252	eqcomd 2769	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
254	232, 240	mulcld 11224	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
255	234, 236, 254	subdid 11665	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
256	255	eqcomd 2769	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
257	253, 256	oveq12d 7428	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
258	251, 257	eqtrd 2798	. . . . 5 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
259	258	adantr 485	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
260	230, 259	eqtrd 2798	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
261	3, 6, 218, 229, 260	2rspcedvdw 3595	. 2 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))
262		nnz 12607	. . . . 5 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
263	262	adantr 485	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈ ℤ)
264		nnz 12607	. . . . 5 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℤ)
265	264	adantl 486	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℤ)
266	263, 265	jca 520	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))
267		bezout 16596	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑤 ∈ ℤ ∃𝑧 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
268	266, 267	syl 18	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑤 ∈ ℤ ∃𝑧 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
269	261, 268	r19.29vva 3225	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃wrex 3089   class class class wbr 5109  (class class class)co 7410  ℂcc 11093  ℝcr 11094  0cc0 11095  1c1 11096   + caddc 11098   · cmul 11100   < clt 11238   ≤ cle 11239   − cmin 11436  -cneg 11437  ℕcn 12228  2c2 12290  ℤcz 12586   gcd cgcd 16547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-pre-sup 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-sup 9398  df-inf 9399  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867  df-nn 12229  df-2 12298  df-3 12299  df-n0 12500  df-z 12587  df-uz 12858  df-rp 13012  df-fl 13821  df-mod 13899  df-seq 14034  df-exp 14094  df-cj 15146  df-re 15147  df-im 15148  df-sqrt 15282  df-abs 15283  df-dvds 16306  df-gcd 16548

This theorem is referenced by:  primrootscoprbij2  42870