Theorem posbezout 42553

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 7368	. . . . 5 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → (𝐴 · 𝑥) = (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
2	1	oveq1d 7375	. . . 4 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)))
3	2	eqeq2d 2748	. . 3 ⊢ (𝑥 = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦))))
4		oveq2 7368	. . . . 5 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → (𝐵 · 𝑦) = (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
5	4	oveq2d 7376	. . . 4 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
6	5	eqeq2d 2748	. . 3 ⊢ (𝑦 = (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → ((𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · 𝑦)) ↔ (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))))
7		simplr 769	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℤ)
8		simpllr 776	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℕ)
9	8	nnzd 12541	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℤ)
10	7, 7	zmulcld 12630	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℤ)
11		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
12	11, 11	zmulcld 12630	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℤ)
13	10, 12	zaddcld 12628	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℤ)
14		2z 12550	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
15	14	a1i 11	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℤ)
16	13, 15	zaddcld 12628	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℤ)
17	9, 16	zmulcld 12630	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℤ)
18	7, 17	zaddcld 12628	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ)
19	7	zred 12624	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℝ)
20	19	renegcld 11568	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -𝑤 ∈ ℝ)
21	20	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 ∈ ℝ)
22		0red 11138	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ∈ ℝ)
23	17	zred 12624	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
24	23	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
25		df-neg 11371	. . . . . . . . . . . 12 ⊢ -𝑤 = (0 − 𝑤)
26	25	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 = (0 − 𝑤))
27	19	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 𝑤 ∈ ℝ)
28	22	leidd 11707	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ 0)
29		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ 𝑤)
30	22, 27, 28, 29	addge0d 11717	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 ≤ (0 + 𝑤))
31	22, 27, 22	lesubaddd 11738	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → ((0 − 𝑤) ≤ 0 ↔ 0 ≤ (0 + 𝑤)))
32	30, 31	mpbird 257	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → (0 − 𝑤) ≤ 0)
33	26, 32	eqbrtrd 5108	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 ≤ 0)
34	8	nnred 12180	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℝ)
35	16	zred 12624	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℝ)
36	8	nngt0d 12217	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < 𝐵)
37		0red 11138	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ∈ ℝ)
38		2re 12246	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
39	38	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℝ)
40	37, 39	readdcld 11165	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 + 2) ∈ ℝ)
41		2pos 12275	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
42		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ 2 = 2
43		2cn 12247	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℂ
44	43	addlidi 11325	. . . . . . . . . . . . . . . 16 ⊢ (0 + 2) = 2
45	42, 44	eqtr4i 2763	. . . . . . . . . . . . . . 15 ⊢ 2 = (0 + 2)
46	41, 45	breqtri 5111	. . . . . . . . . . . . . 14 ⊢ 0 < (0 + 2)
47	46	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (0 + 2))
48	13	zred 12624	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℝ)
49	19, 19	remulcld 11166	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℝ)
50	12	zred 12624	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℝ)
51	19	msqge0d 11709	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ (𝑤 · 𝑤))
52	11	zred 12624	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℝ)
53	52	msqge0d 11709	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ (𝑧 · 𝑧))
54	49, 50, 51, 53	addge0d 11717	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ≤ ((𝑤 · 𝑤) + (𝑧 · 𝑧)))
55	39	leidd 11707	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ≤ 2)
56	37, 39, 48, 39, 54, 55	le2addd 11760	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 + 2) ≤ (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
57	37, 40, 35, 47, 56	ltletrd 11297	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
58	34, 35, 36, 57	mulgt0d 11292	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
59	58	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → 0 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
60	21, 22, 24, 33, 59	lelttrd 11295	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 0 ≤ 𝑤) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
61	25	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → -𝑤 = (0 − 𝑤))
62	37	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ∈ ℝ)
63	34	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℝ)
64	52	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℝ)
65	64, 64	remulcld 11166	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℝ)
66	63, 65	remulcld 11166	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℝ)
67	19	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑤 ∈ ℝ)
68	67, 67	remulcld 11166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑤 · 𝑤) ∈ ℝ)
69	38	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℝ)
70	68, 69	readdcld 11165	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℝ)
71	63, 70	remulcld 11166	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑤 · 𝑤) + 2)) ∈ ℝ)
72	71, 67	readdcld 11165	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤) ∈ ℝ)
73	66, 72	readdcld 11165	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) ∈ ℝ)
74	8	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℕ)
75	74	nnnn0d 12489	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℕ0)
76	75	nn0ge0d 12492	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 𝐵)
77	64	msqge0d 11709	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝑧 · 𝑧))
78	63, 65, 76, 77	mulge0d 11718	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝐵 · (𝑧 · 𝑧)))
79	63	recnd 11164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℂ)
80	64	recnd 11164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℂ)
81	80, 80	mulcld 11156	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℂ)
82	79, 81	mulcld 11156	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℂ)
83	82	subidd 11484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) = 0)
84		1red 11136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 1 ∈ ℝ)
85	84, 70	remulcld 11166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) ∈ ℝ)
86	85, 67	readdcld 11165	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤) ∈ ℝ)
87	20	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ∈ ℝ)
88	19	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℝ)
89	88, 88	remulcld 11166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (𝑤 · 𝑤) ∈ ℝ)
90	38	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 2 ∈ ℝ)
91	89, 90	readdcld 11165	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℝ)
92	37	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ∈ ℝ)
93	87, 87	remulcld 11166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ∈ ℝ)
94	93, 90	readdcld 11165	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 2) ∈ ℝ)
95		1red 11136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 1 ∈ ℝ)
96	95	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 1 ∈ ℝ)
97		0le1 11664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 0 ≤ 1
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ≤ 1)
99		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 1 ≤ -𝑤)
100	92, 96, 87, 98, 99	letrd 11294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 ≤ -𝑤)
101	87, 87, 100, 99	lemulge11d 12084	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ≤ (-𝑤 · -𝑤))
102	93, 92	readdcld 11165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) ∈ ℝ)
103	93	leidd 11707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ≤ (-𝑤 · -𝑤))
104	88	recnd 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℂ)
105	104	negcld 11483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 ∈ ℂ)
106	105, 105	mulcld 11156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ∈ ℂ)
107	106	addridd 11337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) = (-𝑤 · -𝑤))
108	107	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) = ((-𝑤 · -𝑤) + 0))
109	103, 108	breqtrd 5112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) ≤ ((-𝑤 · -𝑤) + 0))
110	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < 2)
111	92, 90, 93, 110	ltadd2dd 11296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 0) < ((-𝑤 · -𝑤) + 2))
112	93, 102, 94, 109, 111	lelttrd 11295	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) < ((-𝑤 · -𝑤) + 2))
113	87, 93, 94, 101, 112	lelttrd 11295	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < ((-𝑤 · -𝑤) + 2))
114	104, 104	mul2negd 11596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (-𝑤 · -𝑤) = (𝑤 · 𝑤))
115	114	oveq1d 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((-𝑤 · -𝑤) + 2) = ((𝑤 · 𝑤) + 2))
116	113, 115	breqtrd 5112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < ((𝑤 · 𝑤) + 2))
117	91	recnd 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
118	117	subid1d 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (((𝑤 · 𝑤) + 2) − 0) = ((𝑤 · 𝑤) + 2))
119	118	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) = (((𝑤 · 𝑤) + 2) − 0))
120	116, 119	breqtrd 5112	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → -𝑤 < (((𝑤 · 𝑤) + 2) − 0))
121	87, 91, 92, 120	ltsub13d 11747	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < (((𝑤 · 𝑤) + 2) − -𝑤))
122	7	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℤ)
123	122	zcnd 12625	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 𝑤 ∈ ℂ)
124	123, 123	mulcld 11156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (𝑤 · 𝑤) ∈ ℂ)
125		2cnd 12250	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 2 ∈ ℂ)
126	124, 125	addcld 11155	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
127	126, 123	subnegd 11503	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → (((𝑤 · 𝑤) + 2) − -𝑤) = (((𝑤 · 𝑤) + 2) + 𝑤))
128	121, 127	breqtrd 5112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 1 ≤ -𝑤) → 0 < (((𝑤 · 𝑤) + 2) + 𝑤))
129	128	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (1 ≤ -𝑤 → 0 < (((𝑤 · 𝑤) + 2) + 𝑤)))
130		0zd 12527	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 ∈ ℤ)
131	7, 130	zltlem1d 12572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ 𝑤 ≤ (0 − 1)))
132		df-neg 11371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ -1 = (0 − 1)
133	132	eqcomi 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (0 − 1) = -1
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (0 − 1) = -1)
135	134	breq2d 5098	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 ≤ (0 − 1) ↔ 𝑤 ≤ -1))
136	131, 135	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ 𝑤 ≤ -1))
137	95	renegcld 11568	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -1 ∈ ℝ)
138	19, 137	lenegd 11720	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 ≤ -1 ↔ --1 ≤ -𝑤))
139	136, 138	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ --1 ≤ -𝑤))
140		1cnd 11130	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 1 ∈ ℂ)
141	140	negnegd 11487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → --1 = 1)
142	141	breq1d 5096	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (--1 ≤ -𝑤 ↔ 1 ≤ -𝑤))
143	139, 142	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ 1 ≤ -𝑤))
144	143	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 → 1 ≤ -𝑤))
145	144	imim1d 82	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((1 ≤ -𝑤 → 0 < (((𝑤 · 𝑤) + 2) + 𝑤)) → (𝑤 < 0 → 0 < (((𝑤 · 𝑤) + 2) + 𝑤))))
146	129, 145	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 → 0 < (((𝑤 · 𝑤) + 2) + 𝑤)))
147	146	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < (((𝑤 · 𝑤) + 2) + 𝑤))
148	70	recnd 11164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
149	148	mullidd 11154	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) = ((𝑤 · 𝑤) + 2))
150	149	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) = (1 · ((𝑤 · 𝑤) + 2)))
151	150	oveq1d 7375	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑤 · 𝑤) + 2) + 𝑤) = ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤))
152	147, 151	breqtrd 5112	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤))
153	40	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 + 2) ∈ ℝ)
154	62	leidd 11707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 0)
155		0le2 12274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≤ 2
156	155	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ 2)
157	62, 69, 154, 156	addge0d 11717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (0 + 2))
158	51	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ (𝑤 · 𝑤))
159	62, 68, 69, 158	leadd1dd 11755	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 + 2) ≤ ((𝑤 · 𝑤) + 2))
160	62, 153, 70, 157, 159	letrd 11294	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 ≤ ((𝑤 · 𝑤) + 2))
161	74	nnge1d 12216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 1 ≤ 𝐵)
162	84, 63, 70, 160, 161	lemul1ad 12086	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (1 · ((𝑤 · 𝑤) + 2)) ≤ (𝐵 · ((𝑤 · 𝑤) + 2)))
163	85, 71, 67, 162	leadd1dd 11755	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((1 · ((𝑤 · 𝑤) + 2)) + 𝑤) ≤ ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
164	62, 86, 72, 152, 163	ltletrd 11297	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
165	83, 164	eqbrtrd 5108	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))
166	66, 66, 72	ltsubadd2d 11739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) − (𝐵 · (𝑧 · 𝑧))) < ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤) ↔ (𝐵 · (𝑧 · 𝑧)) < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤))))
167	165, 166	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
168	62, 66, 73, 78, 167	lelttrd 11295	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
169	74	nncnd 12181	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝐵 ∈ ℂ)
170	11	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℤ)
171	170	zcnd 12625	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑧 ∈ ℂ)
172	171, 171	mulcld 11156	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑧 · 𝑧) ∈ ℂ)
173	169, 172	mulcld 11156	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (𝑧 · 𝑧)) ∈ ℂ)
174	67	recnd 11164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 𝑤 ∈ ℂ)
175	174, 174	mulcld 11156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝑤 · 𝑤) ∈ ℂ)
176		2cnd 12250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℂ)
177	175, 176	addcld 11155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑤 · 𝑤) + 2) ∈ ℂ)
178	169, 177	mulcld 11156	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑤 · 𝑤) + 2)) ∈ ℂ)
179	173, 178, 174	addassd 11158	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)))
180	179	eqcomd 2743	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤))
181	169, 172, 177	adddid 11160	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) = ((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))))
182	181	eqcomd 2743	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) = (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))))
183	182	oveq1d 7375	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝐵 · (𝑧 · 𝑧)) + (𝐵 · ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤))
184	180, 183	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤))
185	43	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 2 ∈ ℂ)
186	172, 175, 185	addassd 11158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2) = ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)))
187	186	eqcomd 2743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)) = (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2))
188	172, 175	addcomd 11339	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + (𝑤 · 𝑤)) = ((𝑤 · 𝑤) + (𝑧 · 𝑧)))
189	188	oveq1d 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (((𝑧 · 𝑧) + (𝑤 · 𝑤)) + 2) = (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
190	187, 189	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2)) = (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))
191	190	oveq2d 7376	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) = (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
192	191	oveq1d 7375	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · ((𝑧 · 𝑧) + ((𝑤 · 𝑤) + 2))) + 𝑤) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
193	184, 192	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((𝐵 · (𝑧 · 𝑧)) + ((𝐵 · ((𝑤 · 𝑤) + 2)) + 𝑤)) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
194	168, 193	breqtrd 5112	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
195	23	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℝ)
196	62, 67, 195	ltsubaddd 11737	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → ((0 − 𝑤) < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ↔ 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤)))
197	194, 196	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → (0 − 𝑤) < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
198	61, 197	eqbrtrd 5108	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ 𝑤 < 0) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
199	198	ex 412	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
200	19, 37	ltnled 11284	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 < 0 ↔ ¬ 0 ≤ 𝑤))
201	200	bicomd 223	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (¬ 0 ≤ 𝑤 ↔ 𝑤 < 0))
202	201	biimpd 229	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (¬ 0 ≤ 𝑤 → 𝑤 < 0))
203	202	imim1d 82	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 < 0 → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) → (¬ 0 ≤ 𝑤 → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
204	199, 203	mpd 15	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (¬ 0 ≤ 𝑤 → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
205	204	imp 406	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ ¬ 0 ≤ 𝑤) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
206	60, 205	pm2.61dan 813	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → -𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))
207	20, 23	posdifd 11728	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (-𝑤 < (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ↔ 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤)))
208	206, 207	mpbid 232	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤))
209	17	zcnd 12625	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
210	7	zcnd 12625	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑤 ∈ ℂ)
211	209, 210	subnegd 11503	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤) = ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤))
212	209, 210	addcomd 11339	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) + 𝑤) = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
213	211, 212	eqtrd 2772	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) − -𝑤) = (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
214	208, 213	breqtrd 5112	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
215	18, 214	jca 511	. . . . 5 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ ∧ 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
216		elnnz 12525	. . . . 5 ⊢ ((𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℕ ↔ ((𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ ∧ 0 < (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
217	215, 216	sylibr 234	. . . 4 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℕ)
218	217	adantr 480	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℕ)
219		simplr 769	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝑧 ∈ ℤ)
220		simp-4l 783	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝐴 ∈ ℕ)
221	220	nnzd 12541	. . . . 5 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝐴 ∈ ℤ)
222		simpllr 776	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 𝑤 ∈ ℤ)
223	222, 222	zmulcld 12630	. . . . . . 7 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑤 · 𝑤) ∈ ℤ)
224	219, 219	zmulcld 12630	. . . . . . 7 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑧 · 𝑧) ∈ ℤ)
225	223, 224	zaddcld 12628	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℤ)
226	14	a1i 11	. . . . . 6 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → 2 ∈ ℤ)
227	225, 226	zaddcld 12628	. . . . 5 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℤ)
228	221, 227	zmulcld 12630	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℤ)
229	219, 228	zsubcld 12629	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℤ)
230		simpr 484	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
231		simplll 775	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐴 ∈ ℕ)
232	231	nncnd 12181	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐴 ∈ ℂ)
233	232, 210	mulcld 11156	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · 𝑤) ∈ ℂ)
234	8	nncnd 12181	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝐵 ∈ ℂ)
235	210, 210	mulcld 11156	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑤 · 𝑤) ∈ ℂ)
236	11	zcnd 12625	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℂ)
237	236, 236	mulcld 11156	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝑧 · 𝑧) ∈ ℂ)
238	235, 237	addcld 11155	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝑤 · 𝑤) + (𝑧 · 𝑧)) ∈ ℂ)
239		2cnd 12250	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → 2 ∈ ℂ)
240	238, 239	addcld 11155	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℂ)
241	234, 240	mulcld 11156	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
242	232, 241	mulcld 11156	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) ∈ ℂ)
243	234, 236	mulcld 11156	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · 𝑧) ∈ ℂ)
244	233, 242, 243	ppncand 11536	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
245		eqidd 2738	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
246	244, 245	eqtr2d 2773	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
247	16	zcnd 12625	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2) ∈ ℂ)
248	232, 234, 247	mul12d 11346	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))) = (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))
249	248	oveq2d 7376	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
250	249	oveq2d 7376	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
251	246, 250	eqtrd 2772	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
252	232, 210, 209	adddid 11160	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
253	252	eqcomd 2743	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = (𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
254	232, 240	mulcld 11156	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)) ∈ ℂ)
255	234, 236, 254	subdid 11597	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
256	255	eqcomd 2743	. . . . . . 7 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) = (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))))
257	253, 256	oveq12d 7378	. . . . . 6 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → (((𝐴 · 𝑤) + (𝐴 · (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + ((𝐵 · 𝑧) − (𝐵 · (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
258	251, 257	eqtrd 2772	. . . . 5 ⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
259	258	adantr 480	. . . 4 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ((𝐴 · 𝑤) + (𝐵 · 𝑧)) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
260	230, 259	eqtrd 2772	. . 3 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → (𝐴 gcd 𝐵) = ((𝐴 · (𝑤 + (𝐵 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2)))) + (𝐵 · (𝑧 − (𝐴 · (((𝑤 · 𝑤) + (𝑧 · 𝑧)) + 2))))))
261	3, 6, 218, 229, 260	2rspcedvdw 3579	. 2 ⊢ (((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ ℤ) ∧ 𝑧 ∈ ℤ) ∧ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧))) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))
262		nnz 12536	. . . . 5 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
263	262	adantr 480	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈ ℤ)
264		nnz 12536	. . . . 5 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℤ)
265	264	adantl 481	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℤ)
266	263, 265	jca 511	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))
267		bezout 16503	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑤 ∈ ℤ ∃𝑧 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
268	266, 267	syl 17	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑤 ∈ ℤ ∃𝑧 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑤) + (𝐵 · 𝑧)))
269	261, 268	r19.29vva 3198	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3062   class class class wbr 5086  (class class class)co 7360  ℂcc 11027  ℝcr 11028  0cc0 11029  1c1 11030   + caddc 11032   · cmul 11034   < clt 11170   ≤ cle 11171   − cmin 11368  -cneg 11369  ℕcn 12165  2c2 12227  ℤcz 12515   gcd cgcd 16454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-sup 9348  df-inf 9349  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-n0 12429  df-z 12516  df-uz 12780  df-rp 12934  df-fl 13742  df-mod 13820  df-seq 13955  df-exp 14015  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-dvds 16213  df-gcd 16455

This theorem is referenced by:  primrootscoprbij2  42556