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

Metamath Proof Explorer

Theorem bezoutlem3

Proof