This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flt4lem2

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

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

Proof

Step Hyp Ref Expression
1 flt4lem2.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 flt4lem2.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 flt4lem2.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 flt4lem2.1 ⊢ ( 𝜑 → 2 ∥ 𝐴 )
5 flt4lem2.2 ⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
6 flt4lem2.3 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
7 breq1 ⊢ ( 𝑖 = 2 → ( 𝑖 ∥ 𝐴 ↔ 2 ∥ 𝐴 ) )
8 breq1 ⊢ ( 𝑖 = 2 → ( 𝑖 ∥ 𝐶 ↔ 2 ∥ 𝐶 ) )
9 7 8 anbi12d ⊢ ( 𝑖 = 2 → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ↔ ( 2 ∥ 𝐴 ∧ 2 ∥ 𝐶 ) ) )
10 2z ⊢ 2 ∈ ℤ
11 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
12 10 11 ax-mp ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
13 12 a1i ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∈ ( ℤ≥ ‘ 2 ) )
14 4 adantr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∥ 𝐴 )
15 10 a1i ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∈ ℤ )
16 gcdnncl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
17 1 2 16 syl2anc ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
18 17 nnzd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
20 3 adantr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐶 ∈ ℕ )
21 20 nnzd ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐶 ∈ ℤ )
22 simpr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∥ 𝐵 )
23 1 adantr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐴 ∈ ℕ )
24 23 nnzd ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐴 ∈ ℤ )
25 2 nnzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐵 ∈ ℤ )
27 dvdsgcd ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 2 ∥ 𝐴 ∧ 2 ∥ 𝐵 ) → 2 ∥ ( 𝐴 gcd 𝐵 ) ) )
28 15 24 26 27 syl3anc ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( ( 2 ∥ 𝐴 ∧ 2 ∥ 𝐵 ) → 2 ∥ ( 𝐴 gcd 𝐵 ) ) )
29 14 22 28 mp2and ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∥ ( 𝐴 gcd 𝐵 ) )
30 2nn ⊢ 2 ∈ ℕ
31 30 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
32 1 2 3 31 6 fltdvdsabdvdsc ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∥ 𝐶 )
33 32 adantr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐶 )
34 15 19 21 29 33 dvdstrd ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∥ 𝐶 )
35 14 34 jca ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( 2 ∥ 𝐴 ∧ 2 ∥ 𝐶 ) )
36 9 13 35 rspcedvdw ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) )
37 ncoprmgcdne1b ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ↔ ( 𝐴 gcd 𝐶 ) ≠ 1 ) )
38 23 20 37 syl2anc ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ↔ ( 𝐴 gcd 𝐶 ) ≠ 1 ) )
39 36 38 mpbid ⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( 𝐴 gcd 𝐶 ) ≠ 1 )
40 39 ex ⊢ ( 𝜑 → ( 2 ∥ 𝐵 → ( 𝐴 gcd 𝐶 ) ≠ 1 ) )
41 40 necon2bd ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐶 ) = 1 → ¬ 2 ∥ 𝐵 ) )
42 5 41 mpd ⊢ ( 𝜑 → ¬ 2 ∥ 𝐵 )