jm2.19lem3

		Ref	Expression
	Assertion	jm2.19lem3	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℕ₀ ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑎 = 0 → ( 𝑎 · 𝑀 ) = ( 0 · 𝑀 ) )
2	1	oveq2d	⊢ ( 𝑎 = 0 → ( 𝑁 + ( 𝑎 · 𝑀 ) ) = ( 𝑁 + ( 0 · 𝑀 ) ) )
3	2	oveq2d	⊢ ( 𝑎 = 0 → ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) = ( 𝐴 Y_rm ( 𝑁 + ( 0 · 𝑀 ) ) ) )
4	3	breq2d	⊢ ( 𝑎 = 0 → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 0 · 𝑀 ) ) ) ) )
5	4	bibi2d	⊢ ( 𝑎 = 0 → ( ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ) ↔ ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 0 · 𝑀 ) ) ) ) ) )
6	5	imbi2d	⊢ ( 𝑎 = 0 → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 0 · 𝑀 ) ) ) ) ) ) )
7		oveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 · 𝑀 ) = ( 𝑏 · 𝑀 ) )
8	7	oveq2d	⊢ ( 𝑎 = 𝑏 → ( 𝑁 + ( 𝑎 · 𝑀 ) ) = ( 𝑁 + ( 𝑏 · 𝑀 ) ) )
9	8	oveq2d	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) = ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) )
10	9	breq2d	⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ) )
11	10	bibi2d	⊢ ( 𝑎 = 𝑏 → ( ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ) ↔ ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ) ) )
12	11	imbi2d	⊢ ( 𝑎 = 𝑏 → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ) ) ) )
13		oveq1	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑎 · 𝑀 ) = ( ( 𝑏 + 1 ) · 𝑀 ) )
14	13	oveq2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑁 + ( 𝑎 · 𝑀 ) ) = ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) )
15	14	oveq2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) = ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) )
16	15	breq2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) ) )
17	16	bibi2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ) ↔ ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) ) ) )
18	17	imbi2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) ) ) ) )
19		oveq1	⊢ ( 𝑎 = 𝐼 → ( 𝑎 · 𝑀 ) = ( 𝐼 · 𝑀 ) )
20	19	oveq2d	⊢ ( 𝑎 = 𝐼 → ( 𝑁 + ( 𝑎 · 𝑀 ) ) = ( 𝑁 + ( 𝐼 · 𝑀 ) ) )
21	20	oveq2d	⊢ ( 𝑎 = 𝐼 → ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) = ( 𝐴 Y_rm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) )
22	21	breq2d	⊢ ( 𝑎 = 𝐼 → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) )
23	22	bibi2d	⊢ ( 𝑎 = 𝐼 → ( ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ) ↔ ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) ) )
24	23	imbi2d	⊢ ( 𝑎 = 𝐼 → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑎 · 𝑀 ) ) ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) ) ) )
25		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
26	25	ad2antrl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑀 ∈ ℂ )
27	26	mul02d	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 0 · 𝑀 ) = 0 )
28	27	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁 + ( 0 · 𝑀 ) ) = ( 𝑁 + 0 ) )
29		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
30	29	ad2antll	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℂ )
31	30	addid1d	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁 + 0 ) = 𝑁 )
32	28 31	eqtr2d	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 = ( 𝑁 + ( 0 · 𝑀 ) ) )
33	32	oveq2d	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐴 Y_rm 𝑁 ) = ( 𝐴 Y_rm ( 𝑁 + ( 0 · 𝑀 ) ) ) )
34	33	breq2d	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 0 · 𝑀 ) ) ) ) )
35		simp3	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ) )
36		simprl	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
37		simprrl	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑀 ∈ ℤ )
38		simprrr	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑁 ∈ ℤ )
39		nn0z	⊢ ( 𝑏 ∈ ℕ₀ → 𝑏 ∈ ℤ )
40	39	adantr	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑏 ∈ ℤ )
41	40 37	zmulcld	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑏 · 𝑀 ) ∈ ℤ )
42	38 41	zaddcld	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑁 + ( 𝑏 · 𝑀 ) ) ∈ ℤ )
43		jm2.19lem2	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ ( 𝑁 + ( 𝑏 · 𝑀 ) ) ∈ ℤ ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( ( 𝑁 + ( 𝑏 · 𝑀 ) ) + 𝑀 ) ) ) )
44	36 37 42 43	syl3anc	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( ( 𝑁 + ( 𝑏 · 𝑀 ) ) + 𝑀 ) ) ) )
45	38	zcnd	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑁 ∈ ℂ )
46	41	zcnd	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑏 · 𝑀 ) ∈ ℂ )
47	37	zcnd	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑀 ∈ ℂ )
48	45 46 47	addassd	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝑁 + ( 𝑏 · 𝑀 ) ) + 𝑀 ) = ( 𝑁 + ( ( 𝑏 · 𝑀 ) + 𝑀 ) ) )
49		nn0cn	⊢ ( 𝑏 ∈ ℕ₀ → 𝑏 ∈ ℂ )
50	49	adantr	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑏 ∈ ℂ )
51		1cnd	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 1 ∈ ℂ )
52	50 51 47	adddird	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝑏 + 1 ) · 𝑀 ) = ( ( 𝑏 · 𝑀 ) + ( 1 · 𝑀 ) ) )
53	47	mulid2d	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 1 · 𝑀 ) = 𝑀 )
54	53	oveq2d	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝑏 · 𝑀 ) + ( 1 · 𝑀 ) ) = ( ( 𝑏 · 𝑀 ) + 𝑀 ) )
55	52 54	eqtr2d	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝑏 · 𝑀 ) + 𝑀 ) = ( ( 𝑏 + 1 ) · 𝑀 ) )
56	55	oveq2d	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑁 + ( ( 𝑏 · 𝑀 ) + 𝑀 ) ) = ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) )
57	48 56	eqtrd	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝑁 + ( 𝑏 · 𝑀 ) ) + 𝑀 ) = ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) )
58	57	oveq2d	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( ( 𝑁 + ( 𝑏 · 𝑀 ) ) + 𝑀 ) ) = ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) )
59	58	breq2d	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( ( 𝑁 + ( 𝑏 · 𝑀 ) ) + 𝑀 ) ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) ) )
60	44 59	bitrd	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) ) )
61	60	3adant3	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) ) )
62	35 61	bitrd	⊢ ( ( 𝑏 ∈ ℕ₀ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) ) )
63	62	3exp	⊢ ( 𝑏 ∈ ℕ₀ → ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) ) ) ) )
64	63	a2d	⊢ ( 𝑏 ∈ ℕ₀ → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝑏 · 𝑀 ) ) ) ) ) → ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( ( 𝑏 + 1 ) · 𝑀 ) ) ) ) ) ) )
65	6 12 18 24 34 64	nn0ind	⊢ ( 𝐼 ∈ ℕ₀ → ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) ) )
66	65	com12	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐼 ∈ ℕ₀ → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) ) )
67	66	3impia	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℕ₀ ) → ( ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm 𝑁 ) ↔ ( 𝐴 Y_rm 𝑀 ) ∥ ( 𝐴 Y_rm ( 𝑁 + ( 𝐼 · 𝑀 ) ) ) ) )

Metamath Proof Explorer

Theorem jm2.19lem3

Proof