Metamath Proof Explorer

Theorem 2sq2

Description: 2 is the sum of squares of two nonnegative integers iff the two integers are 1 . (Contributed by AV, 19-Jun-2023)

Ref Expression
Assertion 2sq2 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ↔ ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )

Proof

Step Hyp Ref Expression
1 nn0sqcl ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ↑ 2 ) ∈ ℕ0 )
2 nn0sqcl ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 ↑ 2 ) ∈ ℕ0 )
3 2 nn0red ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 ↑ 2 ) ∈ ℝ )
4 1 3 anim12ci ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐵 ↑ 2 ) ∈ ℝ ∧ ( 𝐴 ↑ 2 ) ∈ ℕ0 ) )
5 4 adantr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( ( 𝐵 ↑ 2 ) ∈ ℝ ∧ ( 𝐴 ↑ 2 ) ∈ ℕ0 ) )
6 nn0addge2 ⊢ ( ( ( 𝐵 ↑ 2 ) ∈ ℝ ∧ ( 𝐴 ↑ 2 ) ∈ ℕ0 ) → ( 𝐵 ↑ 2 ) ≤ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
7 5 6 syl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( 𝐵 ↑ 2 ) ≤ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
8 breq2 ⊢ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 → ( ( 𝐵 ↑ 2 ) ≤ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ↔ ( 𝐵 ↑ 2 ) ≤ 2 ) )
9 8 adantl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( ( 𝐵 ↑ 2 ) ≤ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ↔ ( 𝐵 ↑ 2 ) ≤ 2 ) )
10 2 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( 𝐵 ↑ 2 ) ∈ ℕ0 )
11 nn0le2is012 ⊢ ( ( ( 𝐵 ↑ 2 ) ∈ ℕ0 ∧ ( 𝐵 ↑ 2 ) ≤ 2 ) → ( ( 𝐵 ↑ 2 ) = 0 ∨ ( 𝐵 ↑ 2 ) = 1 ∨ ( 𝐵 ↑ 2 ) = 2 ) )
12 11 ex ⊢ ( ( 𝐵 ↑ 2 ) ∈ ℕ0 → ( ( 𝐵 ↑ 2 ) ≤ 2 → ( ( 𝐵 ↑ 2 ) = 0 ∨ ( 𝐵 ↑ 2 ) = 1 ∨ ( 𝐵 ↑ 2 ) = 2 ) ) )
13 10 12 syl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( ( 𝐵 ↑ 2 ) ≤ 2 → ( ( 𝐵 ↑ 2 ) = 0 ∨ ( 𝐵 ↑ 2 ) = 1 ∨ ( 𝐵 ↑ 2 ) = 2 ) ) )
14 oveq2 ⊢ ( ( 𝐵 ↑ 2 ) = 0 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + 0 ) )
15 14 eqeq1d ⊢ ( ( 𝐵 ↑ 2 ) = 0 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ↔ ( ( 𝐴 ↑ 2 ) + 0 ) = 2 ) )
16 15 adantl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( 𝐵 ↑ 2 ) = 0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ↔ ( ( 𝐴 ↑ 2 ) + 0 ) = 2 ) )
17 1 nn0cnd ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ↑ 2 ) ∈ ℂ )
18 17 addridd ⊢ ( 𝐴 ∈ ℕ0 → ( ( 𝐴 ↑ 2 ) + 0 ) = ( 𝐴 ↑ 2 ) )
19 18 adantr ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 ↑ 2 ) + 0 ) = ( 𝐴 ↑ 2 ) )
20 19 eqeq1d ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + 0 ) = 2 ↔ ( 𝐴 ↑ 2 ) = 2 ) )
21 1 nn0red ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ↑ 2 ) ∈ ℝ )
22 nn0re ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
23 22 sqge0d ⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ ( 𝐴 ↑ 2 ) )
24 2nn0 ⊢ 2 ∈ ℕ0
25 24 a1i ⊢ ( 𝐴 ∈ ℕ0 → 2 ∈ ℕ0 )
26 25 nn0red ⊢ ( 𝐴 ∈ ℕ0 → 2 ∈ ℝ )
27 0le2 ⊢ 0 ≤ 2
28 27 a1i ⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 2 )
29 sqrt11 ⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 ↑ 2 ) ) ∧ ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ) → ( ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( √ ‘ 2 ) ↔ ( 𝐴 ↑ 2 ) = 2 ) )
30 21 23 26 28 29 syl22anc ⊢ ( 𝐴 ∈ ℕ0 → ( ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( √ ‘ 2 ) ↔ ( 𝐴 ↑ 2 ) = 2 ) )
31 nn0ge0 ⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
32 22 31 sqrtsqd ⊢ ( 𝐴 ∈ ℕ0 → ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 )
33 32 eqeq1d ⊢ ( 𝐴 ∈ ℕ0 → ( ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( √ ‘ 2 ) ↔ 𝐴 = ( √ ‘ 2 ) ) )
34 sqrt2irr ⊢ ( √ ‘ 2 ) ∉ ℚ
35 df-nel ⊢ ( ( √ ‘ 2 ) ∉ ℚ ↔ ¬ ( √ ‘ 2 ) ∈ ℚ )
36 id ⊢ ( ( √ ‘ 2 ) = 𝐴 → ( √ ‘ 2 ) = 𝐴 )
37 36 eqcoms ⊢ ( 𝐴 = ( √ ‘ 2 ) → ( √ ‘ 2 ) = 𝐴 )
38 37 eleq1d ⊢ ( 𝐴 = ( √ ‘ 2 ) → ( ( √ ‘ 2 ) ∈ ℚ ↔ 𝐴 ∈ ℚ ) )
39 38 notbid ⊢ ( 𝐴 = ( √ ‘ 2 ) → ( ¬ ( √ ‘ 2 ) ∈ ℚ ↔ ¬ 𝐴 ∈ ℚ ) )
40 39 adantl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 = ( √ ‘ 2 ) ) → ( ¬ ( √ ‘ 2 ) ∈ ℚ ↔ ¬ 𝐴 ∈ ℚ ) )
41 nn0z ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
42 zq ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℚ )
43 41 42 syl ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℚ )
44 43 pm2.24d ⊢ ( 𝐴 ∈ ℕ0 → ( ¬ 𝐴 ∈ ℚ → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
45 44 adantr ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 = ( √ ‘ 2 ) ) → ( ¬ 𝐴 ∈ ℚ → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
46 40 45 sylbid ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 = ( √ ‘ 2 ) ) → ( ¬ ( √ ‘ 2 ) ∈ ℚ → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
47 46 com12 ⊢ ( ¬ ( √ ‘ 2 ) ∈ ℚ → ( ( 𝐴 ∈ ℕ0 ∧ 𝐴 = ( √ ‘ 2 ) ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
48 47 expd ⊢ ( ¬ ( √ ‘ 2 ) ∈ ℚ → ( 𝐴 ∈ ℕ0 → ( 𝐴 = ( √ ‘ 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) ) )
49 35 48 sylbi ⊢ ( ( √ ‘ 2 ) ∉ ℚ → ( 𝐴 ∈ ℕ0 → ( 𝐴 = ( √ ‘ 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) ) )
50 34 49 ax-mp ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 = ( √ ‘ 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
51 33 50 sylbid ⊢ ( 𝐴 ∈ ℕ0 → ( ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( √ ‘ 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
52 30 51 sylbird ⊢ ( 𝐴 ∈ ℕ0 → ( ( 𝐴 ↑ 2 ) = 2 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
53 52 adantr ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 ↑ 2 ) = 2 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
54 20 53 sylbid ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + 0 ) = 2 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
55 54 adantr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( 𝐵 ↑ 2 ) = 0 ) → ( ( ( 𝐴 ↑ 2 ) + 0 ) = 2 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
56 16 55 sylbid ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( 𝐵 ↑ 2 ) = 0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
57 56 impancom ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( ( 𝐵 ↑ 2 ) = 0 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
58 oveq2 ⊢ ( ( 𝐵 ↑ 2 ) = 1 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + 1 ) )
59 58 eqeq1d ⊢ ( ( 𝐵 ↑ 2 ) = 1 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ↔ ( ( 𝐴 ↑ 2 ) + 1 ) = 2 ) )
60 2cnd ⊢ ( 𝐴 ∈ ℕ0 → 2 ∈ ℂ )
61 1cnd ⊢ ( 𝐴 ∈ ℕ0 → 1 ∈ ℂ )
62 60 61 17 3jca ⊢ ( 𝐴 ∈ ℕ0 → ( 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) )
63 62 adantr ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) )
64 subadd2 ⊢ ( ( 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( ( 2 − 1 ) = ( 𝐴 ↑ 2 ) ↔ ( ( 𝐴 ↑ 2 ) + 1 ) = 2 ) )
65 63 64 syl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 2 − 1 ) = ( 𝐴 ↑ 2 ) ↔ ( ( 𝐴 ↑ 2 ) + 1 ) = 2 ) )
66 65 bicomd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + 1 ) = 2 ↔ ( 2 − 1 ) = ( 𝐴 ↑ 2 ) ) )
67 59 66 sylan9bbr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( 𝐵 ↑ 2 ) = 1 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ↔ ( 2 − 1 ) = ( 𝐴 ↑ 2 ) ) )
68 nn0sqeq1 ⊢ ( ( 𝐵 ∈ ℕ0 ∧ ( 𝐵 ↑ 2 ) = 1 ) → 𝐵 = 1 )
69 68 ex ⊢ ( 𝐵 ∈ ℕ0 → ( ( 𝐵 ↑ 2 ) = 1 → 𝐵 = 1 ) )
70 69 adantl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐵 ↑ 2 ) = 1 → 𝐵 = 1 ) )
71 2m1e1 ⊢ ( 2 − 1 ) = 1
72 71 a1i ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 2 − 1 ) = 1 )
73 72 eqeq1d ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 2 − 1 ) = ( 𝐴 ↑ 2 ) ↔ 1 = ( 𝐴 ↑ 2 ) ) )
74 eqcom ⊢ ( 1 = ( 𝐴 ↑ 2 ) ↔ ( 𝐴 ↑ 2 ) = 1 )
75 73 74 bitrdi ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 2 − 1 ) = ( 𝐴 ↑ 2 ) ↔ ( 𝐴 ↑ 2 ) = 1 ) )
76 nn0sqeq1 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐴 ↑ 2 ) = 1 ) → 𝐴 = 1 )
77 76 ex ⊢ ( 𝐴 ∈ ℕ0 → ( ( 𝐴 ↑ 2 ) = 1 → 𝐴 = 1 ) )
78 77 adantr ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 ↑ 2 ) = 1 → 𝐴 = 1 ) )
79 id ⊢ ( ( 𝐴 = 1 ∧ 𝐵 = 1 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) )
80 79 ex ⊢ ( 𝐴 = 1 → ( 𝐵 = 1 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
81 78 80 syl6 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 ↑ 2 ) = 1 → ( 𝐵 = 1 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) ) )
82 75 81 sylbid ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 2 − 1 ) = ( 𝐴 ↑ 2 ) → ( 𝐵 = 1 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) ) )
83 82 com23 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐵 = 1 → ( ( 2 − 1 ) = ( 𝐴 ↑ 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) ) )
84 70 83 syld ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐵 ↑ 2 ) = 1 → ( ( 2 − 1 ) = ( 𝐴 ↑ 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) ) )
85 84 imp ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( 𝐵 ↑ 2 ) = 1 ) → ( ( 2 − 1 ) = ( 𝐴 ↑ 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
86 67 85 sylbid ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( 𝐵 ↑ 2 ) = 1 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
87 86 impancom ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( ( 𝐵 ↑ 2 ) = 1 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
88 nn0re ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℝ )
89 nn0ge0 ⊢ ( 𝐵 ∈ ℕ0 → 0 ≤ 𝐵 )
90 88 89 sqrtsqd ⊢ ( 𝐵 ∈ ℕ0 → ( √ ‘ ( 𝐵 ↑ 2 ) ) = 𝐵 )
91 90 eqcomd ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 = ( √ ‘ ( 𝐵 ↑ 2 ) ) )
92 91 eqeq1d ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 = ( √ ‘ 2 ) ↔ ( √ ‘ ( 𝐵 ↑ 2 ) ) = ( √ ‘ 2 ) ) )
93 88 sqge0d ⊢ ( 𝐵 ∈ ℕ0 → 0 ≤ ( 𝐵 ↑ 2 ) )
94 2re ⊢ 2 ∈ ℝ
95 94 a1i ⊢ ( 𝐵 ∈ ℕ0 → 2 ∈ ℝ )
96 27 a1i ⊢ ( 𝐵 ∈ ℕ0 → 0 ≤ 2 )
97 sqrt11 ⊢ ( ( ( ( 𝐵 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐵 ↑ 2 ) ) ∧ ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ) → ( ( √ ‘ ( 𝐵 ↑ 2 ) ) = ( √ ‘ 2 ) ↔ ( 𝐵 ↑ 2 ) = 2 ) )
98 3 93 95 96 97 syl22anc ⊢ ( 𝐵 ∈ ℕ0 → ( ( √ ‘ ( 𝐵 ↑ 2 ) ) = ( √ ‘ 2 ) ↔ ( 𝐵 ↑ 2 ) = 2 ) )
99 92 98 bitrd ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 = ( √ ‘ 2 ) ↔ ( 𝐵 ↑ 2 ) = 2 ) )
100 id ⊢ ( ( √ ‘ 2 ) = 𝐵 → ( √ ‘ 2 ) = 𝐵 )
101 100 eqcoms ⊢ ( 𝐵 = ( √ ‘ 2 ) → ( √ ‘ 2 ) = 𝐵 )
102 101 eleq1d ⊢ ( 𝐵 = ( √ ‘ 2 ) → ( ( √ ‘ 2 ) ∈ ℚ ↔ 𝐵 ∈ ℚ ) )
103 102 adantl ⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐵 = ( √ ‘ 2 ) ) → ( ( √ ‘ 2 ) ∈ ℚ ↔ 𝐵 ∈ ℚ ) )
104 103 notbid ⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐵 = ( √ ‘ 2 ) ) → ( ¬ ( √ ‘ 2 ) ∈ ℚ ↔ ¬ 𝐵 ∈ ℚ ) )
105 nn0z ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℤ )
106 zq ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℚ )
107 105 106 syl ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℚ )
108 107 pm2.24d ⊢ ( 𝐵 ∈ ℕ0 → ( ¬ 𝐵 ∈ ℚ → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
109 108 adantr ⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐵 = ( √ ‘ 2 ) ) → ( ¬ 𝐵 ∈ ℚ → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
110 104 109 sylbid ⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐵 = ( √ ‘ 2 ) ) → ( ¬ ( √ ‘ 2 ) ∈ ℚ → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
111 110 com12 ⊢ ( ¬ ( √ ‘ 2 ) ∈ ℚ → ( ( 𝐵 ∈ ℕ0 ∧ 𝐵 = ( √ ‘ 2 ) ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
112 111 expd ⊢ ( ¬ ( √ ‘ 2 ) ∈ ℚ → ( 𝐵 ∈ ℕ0 → ( 𝐵 = ( √ ‘ 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) ) )
113 35 112 sylbi ⊢ ( ( √ ‘ 2 ) ∉ ℚ → ( 𝐵 ∈ ℕ0 → ( 𝐵 = ( √ ‘ 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) ) )
114 34 113 ax-mp ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 = ( √ ‘ 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
115 99 114 sylbird ⊢ ( 𝐵 ∈ ℕ0 → ( ( 𝐵 ↑ 2 ) = 2 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
116 115 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( ( 𝐵 ↑ 2 ) = 2 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
117 57 87 116 3jaod ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( ( ( 𝐵 ↑ 2 ) = 0 ∨ ( 𝐵 ↑ 2 ) = 1 ∨ ( 𝐵 ↑ 2 ) = 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
118 13 117 syld ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( ( 𝐵 ↑ 2 ) ≤ 2 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
119 9 118 sylbid ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( ( 𝐵 ↑ 2 ) ≤ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
120 7 119 mpd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ) → ( 𝐴 = 1 ∧ 𝐵 = 1 ) )
121 120 ex ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 → ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )
122 oveq1 ⊢ ( 𝐴 = 1 → ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) )
123 sq1 ⊢ ( 1 ↑ 2 ) = 1
124 122 123 eqtrdi ⊢ ( 𝐴 = 1 → ( 𝐴 ↑ 2 ) = 1 )
125 oveq1 ⊢ ( 𝐵 = 1 → ( 𝐵 ↑ 2 ) = ( 1 ↑ 2 ) )
126 125 123 eqtrdi ⊢ ( 𝐵 = 1 → ( 𝐵 ↑ 2 ) = 1 )
127 124 126 oveqan12d ⊢ ( ( 𝐴 = 1 ∧ 𝐵 = 1 ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 1 + 1 ) )
128 1p1e2 ⊢ ( 1 + 1 ) = 2
129 127 128 eqtrdi ⊢ ( ( 𝐴 = 1 ∧ 𝐵 = 1 ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 )
130 121 129 impbid1 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 2 ↔ ( 𝐴 = 1 ∧ 𝐵 = 1 ) ) )