Theorem flt4lem2

Description: If A is even, B is odd. (Contributed by SN, 22-Aug-2024)

	Ref	Expression
Hypotheses	flt4lem2.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	flt4lem2.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	flt4lem2.1	⊢ ( 𝜑 → 2 ∥ 𝐴 )
	flt4lem2.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
Assertion	flt4lem2	⊢ ( 𝜑 → ¬ 2 ∥ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		flt4lem2.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2		flt4lem2.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		flt4lem2.1	⊢ ( 𝜑 → 2 ∥ 𝐴 )
4		flt4lem2.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
5		breq1	⊢ ( 𝑖 = 2 → ( 𝑖 ∥ 𝐴 ↔ 2 ∥ 𝐴 ) )
6		breq1	⊢ ( 𝑖 = 2 → ( 𝑖 ∥ 𝐵 ↔ 2 ∥ 𝐵 ) )
7	5 6	anbi12d	⊢ ( 𝑖 = 2 → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ↔ ( 2 ∥ 𝐴 ∧ 2 ∥ 𝐵 ) ) )
8		2prm	⊢ 2 ∈ ℙ
9	8	a1i	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∈ ℙ )
10	3	anim1i	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( 2 ∥ 𝐴 ∧ 2 ∥ 𝐵 ) )
11	7 9 10	rspcedvdw	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ∃ 𝑖 ∈ ℙ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) )
12	1	adantr	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐴 ∈ ℕ )
13	2	adantr	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐵 ∈ ℕ )
14	12 13	prmdvdsncoprmbd	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( ∃ 𝑖 ∈ ℙ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
15	11 14	mpbid	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( 𝐴 gcd 𝐵 ) ≠ 1 )
16	15	ex	⊢ ( 𝜑 → ( 2 ∥ 𝐵 → ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
17	16	necon2bd	⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) = 1 → ¬ 2 ∥ 𝐵 ) )
18	4 17	mpd	⊢ ( 𝜑 → ¬ 2 ∥ 𝐵 )