Metamath Proof Explorer

Theorem flt4lem2

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

Ref Expression
Hypotheses flt4lem2.a ⊢ φ → A ∈ ℕ
flt4lem2.b ⊢ φ → B ∈ ℕ
flt4lem2.c ⊢ φ → C ∈ ℕ
flt4lem2.1 ⊢ φ → 2 ∥ A
flt4lem2.2 ⊢ φ → A gcd C = 1
flt4lem2.3 ⊢ φ → A 2 + B 2 = C 2
Assertion flt4lem2 ⊢ φ → ¬ 2 ∥ B

Proof

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