Theorem posbezout 42974

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 7425	. . . . 5 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → (𝐴 · 𝑥) = (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
2	1	oveq1d 7432	. . . 4 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)))
3	2	eqeq2d 2773	. . 3 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦))))
4		oveq2 7425	. . . . 5 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → (𝐵 · 𝑦) = (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
5	4	oveq2d 7433	. . . 4 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
6	5	eqeq2d 2773	. . 3 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)) ↔ (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))))
7		simplr 781	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℤ)
8		simpllr 788	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℕ)
9	8	nnzd 12645	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℤ)
10	7, 7	zmulcld 12735	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℤ)
11		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
12	11, 11	zmulcld 12735	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℤ)
13	10, 12	zaddcld 12733	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℤ)
14		2z 12654	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
15	14	a1i 11	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℤ)
16	13, 15	zaddcld 12733	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℤ)
17	9, 16	zmulcld 12735	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℤ)
18	7, 17	zaddcld 12733	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ)
19	7	zred 12729	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℝ)
20	19	renegcld 11669	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -𝑤 ∈ ℝ)
21	20	adantr 486	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 ∈ ℝ)
22		0red 11239	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ∈ ℝ)
23	17	zred 12729	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
24	23	adantr 486	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
25		df-neg 11472	. . . . . . . . . . . 12 ⊢ -𝑤 = (0 − 𝑤)
26	25	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 = (0 − 𝑤))
27	19	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 𝑤 ∈ ℝ)
28	22	leidd 11808	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ 0)
29		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ 𝑤)
30	22, 27, 28, 29	addge0d 11818	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ (0 + 𝑤))
31	22, 27, 22	lesubaddd 11839	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → ((0 − 𝑤) ≤ 0 ↔ 0 ≤ (0 + 𝑤)))
32	30, 31	mpbird 260	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → (0 − 𝑤) ≤ 0)
33	26, 32	eqbrtrd 5131	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 ≤ 0)
34	8	nnred 12276	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℝ)
35	16	zred 12729	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℝ)
36	8	nngt0d 12313	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < 𝐵)
37		0red 11239	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ∈ ℝ)
38		2re 12343	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
39	38	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℝ)
40	37, 39	readdcld 11266	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 + 2) ∈ ℝ)
41		2pos 12373	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
42		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ 2 = 2
43		2cn 12344	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℂ
44	43	addlidi 11426	. . . . . . . . . . . . . . . 16 ⊢ (0 + 2) = 2
45	42, 44	eqtr4i 2788	. . . . . . . . . . . . . . 15 ⊢ 2 = (0 + 2)
46	41, 45	breqtri 5134	. . . . . . . . . . . . . 14 ⊢ 0 < (0 + 2)
47	46	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (0 + 2))
48	13	zred 12729	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℝ)
49	19, 19	remulcld 11267	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℝ)
50	12	zred 12729	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℝ)
51	19	msqge0d 11810	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ (𝑤 · 𝑤))
52	11	zred 12729	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℝ)
53	52	msqge0d 11810	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ (𝑧 · 𝑧))
54	49, 50, 51, 53	addge0d 11818	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ ((𝑤 · 𝑤) + (𝑧 · 𝑧)))
55	39	leidd 11808	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ≤ 2)
56	37, 39, 48, 39, 54, 55	le2addd 11861	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 + 2) ≤ (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
57	37, 40, 35, 47, 56	ltletrd 11398	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
58	34, 35, 36, 57	mulgt0d 11393	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
59	58	adantr 486	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
60	21, 22, 24, 33, 59	lelttrd 11396	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
61	25	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → -𝑤 = (0 − 𝑤))
62	37	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ∈ ℝ)
63	34	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℝ)
64	52	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℝ)
65	64, 64	remulcld 11267	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℝ)
66	63, 65	remulcld 11267	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℝ)
67	19	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑤 ∈ ℝ)
68	67, 67	remulcld 11267	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑤 · 𝑤) ∈ ℝ)
69	38	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℝ)
70	68, 69	readdcld 11266	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℝ)
71	63, 70	remulcld 11267	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑤 · 𝑤) + 2)) ∈ ℝ)
72	71, 67	readdcld 11266	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤) ∈ ℝ)
73	66, 72	readdcld 11266	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) ∈ ℝ)
74	8	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℕ)
75	74	nnnn0d 12593	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℕ0)
76	75	nn0ge0d 12596	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 𝐵)
77	64	msqge0d 11810	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝑧 · 𝑧))
78	63, 65, 76, 77	mulge0d 11819	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝐵 · (𝑧 · 𝑧)))
79	63	recnd 11265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℂ)
80	64	recnd 11265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℂ)
81	80, 80	mulcld 11257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℂ)
82	79, 81	mulcld 11257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℂ)
83	82	subidd 11585	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) = 0)
84		1red 11237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 1 ∈ ℝ)
85	84, 70	remulcld 11267	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) ∈ ℝ)
86	85, 67	readdcld 11266	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤) ∈ ℝ)
87	20	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ∈ ℝ)
88	19	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℝ)
89	88, 88	remulcld 11267	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (𝑤 · 𝑤) ∈ ℝ)
90	38	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 2 ∈ ℝ)
91	89, 90	readdcld 11266	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℝ)
92	37	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ∈ ℝ)
93	87, 87	remulcld 11267	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ∈ ℝ)
94	93, 90	readdcld 11266	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 2) ∈ ℝ)
95		1red 11237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 1 ∈ ℝ)
96	95	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 1 ∈ ℝ)
97		0le1 11765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ≤ 1
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ≤ 1)
99		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 1 ≤ -𝑤)
100	92, 96, 87, 98, 99	letrd 11395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ≤ -𝑤)
101	87, 87, 100, 99	lemulge11d 12180	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ≤ (-𝑤 · -𝑤))
102	93, 92	readdcld 11266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) ∈ ℝ)
103	93	leidd 11808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ≤ (-𝑤 · -𝑤))
104	88	recnd 11265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℂ)
105	104	negcld 11584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ∈ ℂ)
106	105, 105	mulcld 11257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ∈ ℂ)
107	106	addridd 11438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) = (-𝑤 · -𝑤))
108	107	eqcomd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) = ((-𝑤 · -𝑤) + 0))
109	103, 108	breqtrd 5135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ≤ ((-𝑤 · -𝑤) + 0))
110	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < 2)
111	92, 90, 93, 110	ltadd2dd 11397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) < ((-𝑤 · -𝑤) + 2))
112	93, 102, 94, 109, 111	lelttrd 11396	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) < ((-𝑤 · -𝑤) + 2))
113	87, 93, 94, 101, 112	lelttrd 11396	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < ((-𝑤 · -𝑤) + 2))
114	104, 104	mul2negd 11697	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) = (𝑤 · 𝑤))
115	114	oveq1d 7432	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 2) = ((𝑤 · 𝑤) + 2))
116	113, 115	breqtrd 5135	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < ((𝑤 · 𝑤) + 2))
117	91	recnd 11265	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
118	117	subid1d 11586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (((𝑤 · 𝑤) + 2) − 0) = ((𝑤 · 𝑤) + 2))
119	118	eqcomd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) = (((𝑤 · 𝑤) + 2) − 0))
120	116, 119	breqtrd 5135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < (((𝑤 · 𝑤) + 2) − 0))
121	87, 91, 92, 120	ltsub13d 11848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < (((𝑤 · 𝑤) + 2) − -𝑤))
122	7	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℤ)
123	122	zcnd 12730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℂ)
124	123, 123	mulcld 11257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (𝑤 · 𝑤) ∈ ℂ)
125		2cnd 12347	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 2 ∈ ℂ)
126	124, 125	addcld 11256	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
127	126, 123	subnegd 11604	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (((𝑤 · 𝑤) + 2) − -𝑤) = (((𝑤 · 𝑤) + 2) + 𝑤))
128	121, 127	breqtrd 5135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < (((𝑤 · 𝑤) + 2) + 𝑤))
129	128	ex 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (1 ≤ -𝑤 → 0 < (((𝑤 · 𝑤) + 2) + 𝑤)))
130		0zd 12631	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ∈ ℤ)
131	7, 130	zltlem1d 12676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ 𝑤 ≤ (0 − 1)))
132		df-neg 11472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ -1 = (0 − 1)
133	132	eqcomi 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (0 − 1) = -1
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 − 1) = -1)
135	134	breq2d 5119	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 ≤ (0 − 1) ↔ 𝑤 ≤ -1))
136	131, 135	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ 𝑤 ≤ -1))
137	95	renegcld 11669	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -1 ∈ ℝ)
138	19, 137	lenegd 11821	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 ≤ -1 ↔ --1 ≤ -𝑤))
139	136, 138	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ --1 ≤ -𝑤))
140		1cnd 11230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 1 ∈ ℂ)
141	140	negnegd 11588	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → --1 = 1)
142	141	breq1d 5117	. . . . . . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < (((𝑤 · 𝑤) + 2) + 𝑤))
148	70	recnd 11265	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
149	148	mullidd 11255	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) = ((𝑤 · 𝑤) + 2))
150	149	eqcomd 2768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) = (1 · ((𝑤 · 𝑤) + 2)))
151	150	oveq1d 7432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑤 · 𝑤) + 2) + 𝑤) = ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤))
152	147, 151	breqtrd 5135	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤))
153	40	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 + 2) ∈ ℝ)
154	62	leidd 11808	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 0)
155		0le2 12371	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≤ 2
156	155	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 2)
157	62, 69, 154, 156	addge0d 11818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (0 + 2))
158	51	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝑤 · 𝑤))
159	62, 68, 69, 158	leadd1dd 11856	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 + 2) ≤ ((𝑤 · 𝑤) + 2))
160	62, 153, 70, 157, 159	letrd 11395	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ ((𝑤 · 𝑤) + 2))
161	74	nnge1d 12312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 1 ≤ 𝐵)
162	84, 63, 70, 160, 161	lemul1ad 12182	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) ≤ (𝐵 · ((𝑤 · 𝑤) + 2)))
163	85, 71, 67, 162	leadd1dd 11856	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤) ≤ ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
164	62, 86, 72, 152, 163	ltletrd 11398	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
165	83, 164	eqbrtrd 5131	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
166	66, 66, 72	ltsubadd2d 11840	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤) ↔ (𝐵 · (𝑧 · 𝑧)) < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))))
167	165, 166	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
168	62, 66, 73, 78, 167	lelttrd 11396	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
169	74	nncnd 12277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℂ)
170	11	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℤ)
171	170	zcnd 12730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℂ)
172	171, 171	mulcld 11257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℂ)
173	169, 172	mulcld 11257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℂ)
174	67	recnd 11265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑤 ∈ ℂ)
175	174, 174	mulcld 11257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑤 · 𝑤) ∈ ℂ)
176		2cnd 12347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℂ)
177	175, 176	addcld 11256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
178	169, 177	mulcld 11257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑤 · 𝑤) + 2)) ∈ ℂ)
179	173, 178, 174	addassd 11259	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
180	179	eqcomd 2768	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤))
181	169, 172, 177	adddid 11261	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) = ((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))))
182	181	eqcomd 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) = (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))))
183	182	oveq1d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤))
184	180, 183	eqtrd 2797	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤))
185	43	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℂ)
186	172, 175, 185	addassd 11259	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2) = ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)))
187	186	eqcomd 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)) = (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2))
188	172, 175	addcomd 11440	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + (𝑤 · 𝑤)) = ((𝑤 · 𝑤) + (𝑧 · 𝑧)))
189	188	oveq1d 7432	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2) = (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
190	187, 189	eqtrd 2797	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)) = (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
191	190	oveq2d 7433	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) = (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
192	191	oveq1d 7432	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
193	184, 192	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
194	168, 193	breqtrd 5135	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
195	23	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
196	62, 67, 195	ltsubaddd 11838	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((0 − 𝑤) < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ↔ 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤)))
197	194, 196	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 − 𝑤) < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
198	61, 197	eqbrtrd 5131	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
199	198	ex 418	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
200	19, 37	ltnled 11385	. . . . . . . . . . . . . 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 412	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ ¬ 0 ≤ 𝑤) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
206	60, 205	pm2.61dan 825	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
207	20, 23	posdifd 11829	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (-𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ↔ 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤)))
208	206, 207	mpbid 235	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤))
209	17	zcnd 12730	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
210	7	zcnd 12730	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℂ)
211	209, 210	subnegd 11604	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
212	209, 210	addcomd 11440	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤) = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
213	211, 212	eqtrd 2797	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤) = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
214	208, 213	breqtrd 5135	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
215	18, 214	jca 521	. . . . 5 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ ∧ 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
216		elnnz 12629	. . . . 5 ⊢ ((𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℕ ↔ ((𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ ∧ 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
217	215, 216	sylibr 237	. . . 4 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℕ)
218	217	adantr 486	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℕ)
219		simplr 781	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝑧 ∈ ℤ)
220		simp-4l 795	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝐴 ∈ ℕ)
221	220	nnzd 12645	. . . . 5 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝐴 ∈ ℤ)
222		simpllr 788	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝑤 ∈ ℤ)
223	222, 222	zmulcld 12735	. . . . . . 7 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑤 · 𝑤) ∈ ℤ)
224	219, 219	zmulcld 12735	. . . . . . 7 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑧 · 𝑧) ∈ ℤ)
225	223, 224	zaddcld 12733	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℤ)
226	14	a1i 11	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 2 ∈ ℤ)
227	225, 226	zaddcld 12733	. . . . 5 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℤ)
228	221, 227	zmulcld 12735	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℤ)
229	219, 228	zsubcld 12734	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ)
230		simpr 490	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
231		simplll 787	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐴 ∈ ℕ)
232	231	nncnd 12277	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐴 ∈ ℂ)
233	232, 210	mulcld 11257	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · 𝑤) ∈ ℂ)
234	8	nncnd 12277	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℂ)
235	210, 210	mulcld 11257	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℂ)
236	11	zcnd 12730	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℂ)
237	236, 236	mulcld 11257	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℂ)
238	235, 237	addcld 11256	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℂ)
239		2cnd 12347	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℂ)
240	238, 239	addcld 11256	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℂ)
241	234, 240	mulcld 11257	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
242	232, 241	mulcld 11257	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℂ)
243	234, 236	mulcld 11257	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · 𝑧) ∈ ℂ)
244	233, 242, 243	ppncand 11637	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
245		eqidd 2763	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
246	244, 245	eqtr2d 2798	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
247	16	zcnd 12730	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℂ)
248	232, 234, 247	mul12d 11447	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) = (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
249	248	oveq2d 7433	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
250	249	oveq2d 7433	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
251	246, 250	eqtrd 2797	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
252	232, 210, 209	adddid 11261	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
253	252	eqcomd 2768	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
254	232, 240	mulcld 11257	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
255	234, 236, 254	subdid 11698	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
256	255	eqcomd 2768	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
257	253, 256	oveq12d 7435	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
258	251, 257	eqtrd 2797	. . . . 5 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
259	258	adantr 486	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
260	230, 259	eqtrd 2797	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
261	3, 6, 218, 229, 260	2rspcedvdw 3593	. 2 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))
262		nnz 12640	. . . . 5 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
263	262	adantr 486	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈ ℤ)
264		nnz 12640	. . . . 5 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℤ)
265	264	adantl 487	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℤ)
266	263, 265	jca 521	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))
267		bezout 16639	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑤 ∈ ℤ ∃𝑧 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
268	266, 267	syl 18	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑤 ∈ ℤ ∃𝑧 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
269	261, 268	r19.29vva 3224	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3088   class class class wbr 5107  (class class class)co 7417  ℂcc 11126  ℝcr 11127  0cc0 11128  1c1 11129   + caddc 11131   · cmul 11133   < clt 11271   ≤ cle 11272   − cmin 11469  -cneg 11470  ℕcn 12261  2c2 12323  ℤcz 12619   gcd cgcd 16590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205  ax-pre-sup 11206

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  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 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-sup 9416  df-inf 9417  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-div 11900  df-nn 12262  df-2 12331  df-3 12332  df-n0 12533  df-z 12620  df-uz 12892  df-rp 13047  df-fl 13857  df-mod 13935  df-seq 14070  df-exp 14130  df-cj 15190  df-re 15191  df-im 15192  df-sqrt 15326  df-abs 15327  df-dvds 16349  df-gcd 16591

This theorem is used by:  primrootscoprbij2  42977