Theorem bezoutlem2

Description: Lemma for bezout . (Contributed by Mario Carneiro, 15-Mar-2014) ( Revised by AV, 30-Sep-2020.)

	Ref	Expression
Hypotheses	bezout.1	⊢ 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) }
	bezout.3	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
	bezout.4	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
	bezout.2	⊢ 𝐺 = inf ( 𝑀 , ℝ , < )
	bezout.5	⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
Assertion	bezoutlem2	⊢ ( 𝜑 → 𝐺 ∈ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		bezout.1	⊢ 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) }
2		bezout.3	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3		bezout.4	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
4		bezout.2	⊢ 𝐺 = inf ( 𝑀 , ℝ , < )
5		bezout.5	⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
6	1	ssrab3	⊢ 𝑀 ⊆ ℕ
7		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
8	6 7	sseqtri	⊢ 𝑀 ⊆ ( ℤ≥ ‘ 1 )
9	1 2 3	bezoutlem1	⊢ ( 𝜑 → ( 𝐴 ≠ 0 → ( abs ‘ 𝐴 ) ∈ 𝑀 ) )
10		ne0i	⊢ ( ( abs ‘ 𝐴 ) ∈ 𝑀 → 𝑀 ≠ ∅ )
11	9 10	syl6	⊢ ( 𝜑 → ( 𝐴 ≠ 0 → 𝑀 ≠ ∅ ) )
12		eqid	⊢ { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } = { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) }
13	12 3 2	bezoutlem1	⊢ ( 𝜑 → ( 𝐵 ≠ 0 → ( abs ‘ 𝐵 ) ∈ { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } ) )
14		rexcom	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
15	2	zcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
16	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝐴 ∈ ℂ )
17		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
18	17	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝑥 ∈ ℂ )
19	16 18	mulcld	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
20	3	zcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
21	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
22		zcn	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
23	22	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → 𝑦 ∈ ℂ )
24	21 23	mulcld	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( 𝐵 · 𝑦 ) ∈ ℂ )
25	19 24	addcomd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) )
26	25	eqeq2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ) → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) ) )
27	26	2rexbidva	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) ) )
28	14 27	syl5bb	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) ) )
29	28	rabbidv	⊢ ( 𝜑 → { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) } = { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } )
30	1 29	eqtrid	⊢ ( 𝜑 → 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } )
31	30	eleq2d	⊢ ( 𝜑 → ( ( abs ‘ 𝐵 ) ∈ 𝑀 ↔ ( abs ‘ 𝐵 ) ∈ { 𝑧 ∈ ℕ ∣ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 𝐵 · 𝑦 ) + ( 𝐴 · 𝑥 ) ) } ) )
32	13 31	sylibrd	⊢ ( 𝜑 → ( 𝐵 ≠ 0 → ( abs ‘ 𝐵 ) ∈ 𝑀 ) )
33		ne0i	⊢ ( ( abs ‘ 𝐵 ) ∈ 𝑀 → 𝑀 ≠ ∅ )
34	32 33	syl6	⊢ ( 𝜑 → ( 𝐵 ≠ 0 → 𝑀 ≠ ∅ ) )
35		neorian	⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
36	5 35	sylibr	⊢ ( 𝜑 → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
37	11 34 36	mpjaod	⊢ ( 𝜑 → 𝑀 ≠ ∅ )
38		infssuzcl	⊢ ( ( 𝑀 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ≠ ∅ ) → inf ( 𝑀 , ℝ , < ) ∈ 𝑀 )
39	8 37 38	sylancr	⊢ ( 𝜑 → inf ( 𝑀 , ℝ , < ) ∈ 𝑀 )
40	4 39	eqeltrid	⊢ ( 𝜑 → 𝐺 ∈ 𝑀 )