bezoutlem3

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

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

Proof

Step	Hyp	Ref	Expression
1		bezout.1	⊢ 𝑀 = { 𝑧 ∈ ℕ ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) }
2		bezout.3	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3		bezout.4	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
4		bezout.2	⊢ 𝐺 = inf ( 𝑀 , ℝ , < )
5		bezout.5	⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
6		eqeq1	⊢ ( 𝑧 = 𝐶 → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
7	6	2rexbidv	⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
8		oveq2	⊢ ( 𝑥 = 𝑠 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑠 ) )
9	8	oveq1d	⊢ ( 𝑥 = 𝑠 → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑦 ) ) )
10	9	eqeq2d	⊢ ( 𝑥 = 𝑠 → ( 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑦 ) ) ) )
11		oveq2	⊢ ( 𝑦 = 𝑡 → ( 𝐵 · 𝑦 ) = ( 𝐵 · 𝑡 ) )
12	11	oveq2d	⊢ ( 𝑦 = 𝑡 → ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) )
13	12	eqeq2d	⊢ ( 𝑦 = 𝑡 → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ) )
14	10 13	cbvrex2vw	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) )
15	7 14	bitrdi	⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ) )
16	15 1	elrab2	⊢ ( 𝐶 ∈ 𝑀 ↔ ( 𝐶 ∈ ℕ ∧ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ) )
17	16	bilani	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 ∈ ℕ ∧ ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ) )
18	17	simpld	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐶 ∈ ℕ )
19	18	nnred	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐶 ∈ ℝ )
20	1 2 3 4 5	bezoutlem2	⊢ ( 𝜑 → 𝐺 ∈ 𝑀 )
21		oveq2	⊢ ( 𝑥 = 𝑢 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑢 ) )
22	21	oveq1d	⊢ ( 𝑥 = 𝑢 → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) )
23	22	eqeq2d	⊢ ( 𝑥 = 𝑢 → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) ) )
24		oveq2	⊢ ( 𝑦 = 𝑣 → ( 𝐵 · 𝑦 ) = ( 𝐵 · 𝑣 ) )
25	24	oveq2d	⊢ ( 𝑦 = 𝑣 → ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
26	25	eqeq2d	⊢ ( 𝑦 = 𝑣 → ( 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑦 ) ) ↔ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
27	23 26	cbvrex2vw	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
28		eqeq1	⊢ ( 𝑧 = 𝐺 → ( 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ↔ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
29	28	2rexbidv	⊢ ( 𝑧 = 𝐺 → ( ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
30	27 29	bitrid	⊢ ( 𝑧 = 𝐺 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
31	30 1	elrab2	⊢ ( 𝐺 ∈ 𝑀 ↔ ( 𝐺 ∈ ℕ ∧ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
32	20 31	sylib	⊢ ( 𝜑 → ( 𝐺 ∈ ℕ ∧ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) )
33	32	simpld	⊢ ( 𝜑 → 𝐺 ∈ ℕ )
34	33	nnrpd	⊢ ( 𝜑 → 𝐺 ∈ ℝ⁺ )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐺 ∈ ℝ⁺ )
36		modlt	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐺 ∈ ℝ⁺ ) → ( 𝐶 mod 𝐺 ) < 𝐺 )
37	19 35 36	syl2anc	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 mod 𝐺 ) < 𝐺 )
38	18	nnzd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐶 ∈ ℤ )
39	33	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐺 ∈ ℕ )
40	38 39	zmodcld	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 mod 𝐺 ) ∈ ℕ₀ )
41	40	nn0red	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 mod 𝐺 ) ∈ ℝ )
42	33	nnred	⊢ ( 𝜑 → 𝐺 ∈ ℝ )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐺 ∈ ℝ )
44	41 43	ltnled	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝐶 mod 𝐺 ) < 𝐺 ↔ ¬ 𝐺 ≤ ( 𝐶 mod 𝐺 ) ) )
45	37 44	mpbid	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ¬ 𝐺 ≤ ( 𝐶 mod 𝐺 ) )
46	17	simprd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) )
47	32	simprd	⊢ ( 𝜑 → ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
48	47	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) → ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) )
49		simprll	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑠 ∈ ℤ )
50		simprrl	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑢 ∈ ℤ )
51	19 39	nndivred	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 / 𝐺 ) ∈ ℝ )
52	51	flcld	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ∈ ℤ )
53	52	adantr	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ∈ ℤ )
54	50 53	zmulcld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ∈ ℤ )
55	49 54	zsubcld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℤ )
56		simprlr	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑡 ∈ ℤ )
57		simprrr	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑣 ∈ ℤ )
58	57 53	zmulcld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ∈ ℤ )
59	56 58	zsubcld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℤ )
60	2	zcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
61	60	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝐴 ∈ ℂ )
62	49	zcnd	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑠 ∈ ℂ )
63	61 62	mulcld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐴 · 𝑠 ) ∈ ℂ )
64	3	zcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
65	64	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝐵 ∈ ℂ )
66	56	zcnd	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑡 ∈ ℂ )
67	65 66	mulcld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐵 · 𝑡 ) ∈ ℂ )
68	54	zcnd	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ∈ ℂ )
69	61 68	mulcld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℂ )
70	58	zcnd	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ∈ ℂ )
71	65 70	mulcld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℂ )
72	63 67 69 71	addsub4d	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) + ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) = ( ( ( 𝐴 · 𝑠 ) − ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( ( 𝐵 · 𝑡 ) − ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) )
73	50	zcnd	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑢 ∈ ℂ )
74	61 73	mulcld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐴 · 𝑢 ) ∈ ℂ )
75	52	zcnd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ∈ ℂ )
76	75	adantr	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ∈ ℂ )
77	57	zcnd	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → 𝑣 ∈ ℂ )
78	65 77	mulcld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐵 · 𝑣 ) ∈ ℂ )
79	61 73 76	mulassd	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( 𝐴 · 𝑢 ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) = ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
80	65 77 76	mulassd	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( 𝐵 · 𝑣 ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) = ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
81	79 80	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( ( 𝐴 · 𝑢 ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) + ( ( 𝐵 · 𝑣 ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) + ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
82	74 76 78 81	joinlmuladdmuld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) = ( ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) + ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
83	82	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) + ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) )
84	61 62 68	subdid	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) = ( ( 𝐴 · 𝑠 ) − ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
85	65 66 70	subdid	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) = ( ( 𝐵 · 𝑡 ) − ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
86	84 85	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) = ( ( ( 𝐴 · 𝑠 ) − ( 𝐴 · ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( ( 𝐵 · 𝑡 ) − ( 𝐵 · ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) )
87	72 83 86	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) )
88		oveq2	⊢ ( 𝑥 = ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( 𝐴 · 𝑥 ) = ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
89	88	oveq1d	⊢ ( 𝑥 = ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · 𝑦 ) ) )
90	89	eqeq2d	⊢ ( 𝑥 = ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · 𝑦 ) ) ) )
91		oveq2	⊢ ( 𝑦 = ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( 𝐵 · 𝑦 ) = ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) )
92	91	oveq2d	⊢ ( 𝑦 = ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · 𝑦 ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) )
93	92	eqeq2d	⊢ ( 𝑦 = ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · 𝑦 ) ) ↔ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) ) )
94	90 93	rspc2ev	⊢ ( ( ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℤ ∧ ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ∈ ℤ ∧ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · ( 𝑠 − ( 𝑢 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) + ( 𝐵 · ( 𝑡 − ( 𝑣 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
95	55 59 87 94	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
96		oveq1	⊢ ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) = ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) )
97		oveq12	⊢ ( ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ∧ ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) = ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) → ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
98	96 97	sylan2	⊢ ( ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ∧ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) → ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
99	98	eqeq1d	⊢ ( ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ∧ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) → ( ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
100	99	2rexbidv	⊢ ( ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ∧ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) − ( ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
101	95 100	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) ∧ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
102	101	expcomd	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ∧ ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) ) ) → ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) ) )
103	102	expr	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) → ( ( 𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ ) → ( 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) ) ) )
104	103	rexlimdvv	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) → ( ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℤ 𝐺 = ( ( 𝐴 · 𝑢 ) + ( 𝐵 · 𝑣 ) ) → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) ) )
105	48 104	mpd	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) ) → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
106	105	ex	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) ) )
107	106	rexlimdvv	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ∃ 𝑠 ∈ ℤ ∃ 𝑡 ∈ ℤ 𝐶 = ( ( 𝐴 · 𝑠 ) + ( 𝐵 · 𝑡 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
108	46 107	mpd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
109		modval	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐺 ∈ ℝ⁺ ) → ( 𝐶 mod 𝐺 ) = ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
110	19 35 109	syl2anc	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 mod 𝐺 ) = ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) )
111	110	eqcomd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( 𝐶 mod 𝐺 ) )
112	111	eqeq1d	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
113	112	2rexbidv	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 − ( 𝐺 · ( ⌊ ‘ ( 𝐶 / 𝐺 ) ) ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
114	108 113	mpbid	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )
115		eqeq1	⊢ ( 𝑧 = ( 𝐶 mod 𝐺 ) → ( 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
116	115	2rexbidv	⊢ ( 𝑧 = ( 𝐶 mod 𝐺 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
117	116 1	elrab2	⊢ ( ( 𝐶 mod 𝐺 ) ∈ 𝑀 ↔ ( ( 𝐶 mod 𝐺 ) ∈ ℕ ∧ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) ) )
118	117	simplbi2com	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 mod 𝐺 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) → ( ( 𝐶 mod 𝐺 ) ∈ ℕ → ( 𝐶 mod 𝐺 ) ∈ 𝑀 ) )
119	114 118	syl	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝐶 mod 𝐺 ) ∈ ℕ → ( 𝐶 mod 𝐺 ) ∈ 𝑀 ) )
120	1	ssrab3	⊢ 𝑀 ⊆ ℕ
121		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
122	120 121	sseqtri	⊢ 𝑀 ⊆ ( ℤ_≥ ‘ 1 )
123		infssuzle	⊢ ( ( 𝑀 ⊆ ( ℤ_≥ ‘ 1 ) ∧ ( 𝐶 mod 𝐺 ) ∈ 𝑀 ) → inf ( 𝑀 , ℝ , < ) ≤ ( 𝐶 mod 𝐺 ) )
124	122 123	mpan	⊢ ( ( 𝐶 mod 𝐺 ) ∈ 𝑀 → inf ( 𝑀 , ℝ , < ) ≤ ( 𝐶 mod 𝐺 ) )
125	4 124	eqbrtrid	⊢ ( ( 𝐶 mod 𝐺 ) ∈ 𝑀 → 𝐺 ≤ ( 𝐶 mod 𝐺 ) )
126	119 125	syl6	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝐶 mod 𝐺 ) ∈ ℕ → 𝐺 ≤ ( 𝐶 mod 𝐺 ) ) )
127	45 126	mtod	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ¬ ( 𝐶 mod 𝐺 ) ∈ ℕ )
128		elnn0	⊢ ( ( 𝐶 mod 𝐺 ) ∈ ℕ₀ ↔ ( ( 𝐶 mod 𝐺 ) ∈ ℕ ∨ ( 𝐶 mod 𝐺 ) = 0 ) )
129	40 128	sylib	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ( 𝐶 mod 𝐺 ) ∈ ℕ ∨ ( 𝐶 mod 𝐺 ) = 0 ) )
130	129	ord	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( ¬ ( 𝐶 mod 𝐺 ) ∈ ℕ → ( 𝐶 mod 𝐺 ) = 0 ) )
131	127 130	mpd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐶 mod 𝐺 ) = 0 )
132		dvdsval3	⊢ ( ( 𝐺 ∈ ℕ ∧ 𝐶 ∈ ℤ ) → ( 𝐺 ∥ 𝐶 ↔ ( 𝐶 mod 𝐺 ) = 0 ) )
133	39 38 132	syl2anc	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → ( 𝐺 ∥ 𝐶 ↔ ( 𝐶 mod 𝐺 ) = 0 ) )
134	131 133	mpbird	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑀 ) → 𝐺 ∥ 𝐶 )
135	134	ex	⊢ ( 𝜑 → ( 𝐶 ∈ 𝑀 → 𝐺 ∥ 𝐶 ) )

Metamath Proof Explorer

Theorem bezoutlem3

Proof