Metamath Proof Explorer

Theorem 4sqlem19

Description: Lemma for 4sq . The proof is by strong induction - we show that if all the integers less than k are in S , then k is as well. In this part of the proof we do the induction argument and dispense with all the cases except the odd prime case, which is sent to 4sqlem18 . If k is 0 , 1 , 2 , we show k e. S directly; otherwise if k is composite, k is the product of two numbers less than it (and hence in S by assumption), so by mul4sq k e. S . (Contributed by Mario Carneiro, 14-Jul-2014) (Revised by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypothesis 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
Assertion 4sqlem19 ℕ0 = 𝑆

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2 elnn0 ⊢ ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
3 eleq1 ⊢ ( 𝑗 = 1 → ( 𝑗 ∈ 𝑆 ↔ 1 ∈ 𝑆 ) )
4 eleq1 ⊢ ( 𝑗 = 𝑚 → ( 𝑗 ∈ 𝑆 ↔ 𝑚 ∈ 𝑆 ) )
5 eleq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 ∈ 𝑆 ↔ 𝑖 ∈ 𝑆 ) )
6 eleq1 ⊢ ( 𝑗 = ( 𝑚 · 𝑖 ) → ( 𝑗 ∈ 𝑆 ↔ ( 𝑚 · 𝑖 ) ∈ 𝑆 ) )
7 eleq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆 ) )
8 abs1 ⊢ ( abs ‘ 1 ) = 1
9 8 oveq1i ⊢ ( ( abs ‘ 1 ) ↑ 2 ) = ( 1 ↑ 2 )
10 sq1 ⊢ ( 1 ↑ 2 ) = 1
11 9 10 eqtri ⊢ ( ( abs ‘ 1 ) ↑ 2 ) = 1
12 abs0 ⊢ ( abs ‘ 0 ) = 0
13 12 oveq1i ⊢ ( ( abs ‘ 0 ) ↑ 2 ) = ( 0 ↑ 2 )
14 sq0 ⊢ ( 0 ↑ 2 ) = 0
15 13 14 eqtri ⊢ ( ( abs ‘ 0 ) ↑ 2 ) = 0
16 11 15 oveq12i ⊢ ( ( ( abs ‘ 1 ) ↑ 2 ) + ( ( abs ‘ 0 ) ↑ 2 ) ) = ( 1 + 0 )
17 1p0e1 ⊢ ( 1 + 0 ) = 1
18 16 17 eqtri ⊢ ( ( ( abs ‘ 1 ) ↑ 2 ) + ( ( abs ‘ 0 ) ↑ 2 ) ) = 1
19 1z ⊢ 1 ∈ ℤ
20 zgz ⊢ ( 1 ∈ ℤ → 1 ∈ ℤ[i] )
21 19 20 ax-mp ⊢ 1 ∈ ℤ[i]
22 0z ⊢ 0 ∈ ℤ
23 zgz ⊢ ( 0 ∈ ℤ → 0 ∈ ℤ[i] )
24 22 23 ax-mp ⊢ 0 ∈ ℤ[i]
25 1 4sqlem4a ⊢ ( ( 1 ∈ ℤ[i] ∧ 0 ∈ ℤ[i] ) → ( ( ( abs ‘ 1 ) ↑ 2 ) + ( ( abs ‘ 0 ) ↑ 2 ) ) ∈ 𝑆 )
26 21 24 25 mp2an ⊢ ( ( ( abs ‘ 1 ) ↑ 2 ) + ( ( abs ‘ 0 ) ↑ 2 ) ) ∈ 𝑆
27 18 26 eqeltrri ⊢ 1 ∈ 𝑆
28 eleq1 ⊢ ( 𝑗 = 2 → ( 𝑗 ∈ 𝑆 ↔ 2 ∈ 𝑆 ) )
29 eldifsn ⊢ ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑗 ∈ ℙ ∧ 𝑗 ≠ 2 ) )
30 oddprm ⊢ ( 𝑗 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑗 − 1 ) / 2 ) ∈ ℕ )
31 30 adantr ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( ( 𝑗 − 1 ) / 2 ) ∈ ℕ )
32 eldifi ⊢ ( 𝑗 ∈ ( ℙ ∖ { 2 } ) → 𝑗 ∈ ℙ )
33 32 adantr ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → 𝑗 ∈ ℙ )
34 prmnn ⊢ ( 𝑗 ∈ ℙ → 𝑗 ∈ ℕ )
35 nncn ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℂ )
36 33 34 35 3syl ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → 𝑗 ∈ ℂ )
37 ax-1cn ⊢ 1 ∈ ℂ
38 subcl ⊢ ( ( 𝑗 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑗 − 1 ) ∈ ℂ )
39 36 37 38 sylancl ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( 𝑗 − 1 ) ∈ ℂ )
40 2cnd ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → 2 ∈ ℂ )
41 2ne0 ⊢ 2 ≠ 0
42 41 a1i ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → 2 ≠ 0 )
43 39 40 42 divcan2d ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( 2 · ( ( 𝑗 − 1 ) / 2 ) ) = ( 𝑗 − 1 ) )
44 43 oveq1d ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( ( 2 · ( ( 𝑗 − 1 ) / 2 ) ) + 1 ) = ( ( 𝑗 − 1 ) + 1 ) )
45 npcan ⊢ ( ( 𝑗 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
46 36 37 45 sylancl ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
47 44 46 eqtr2d ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → 𝑗 = ( ( 2 · ( ( 𝑗 − 1 ) / 2 ) ) + 1 ) )
48 43 oveq2d ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( 0 ... ( 2 · ( ( 𝑗 − 1 ) / 2 ) ) ) = ( 0 ... ( 𝑗 − 1 ) ) )
49 nnm1nn0 ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 − 1 ) ∈ ℕ0 )
50 33 34 49 3syl ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( 𝑗 − 1 ) ∈ ℕ0 )
51 elnn0uz ⊢ ( ( 𝑗 − 1 ) ∈ ℕ0 ↔ ( 𝑗 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
52 50 51 sylib ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( 𝑗 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
53 eluzfz1 ⊢ ( ( 𝑗 − 1 ) ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... ( 𝑗 − 1 ) ) )
54 fzsplit ⊢ ( 0 ∈ ( 0 ... ( 𝑗 − 1 ) ) → ( 0 ... ( 𝑗 − 1 ) ) = ( ( 0 ... 0 ) ∪ ( ( 0 + 1 ) ... ( 𝑗 − 1 ) ) ) )
55 52 53 54 3syl ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( 0 ... ( 𝑗 − 1 ) ) = ( ( 0 ... 0 ) ∪ ( ( 0 + 1 ) ... ( 𝑗 − 1 ) ) ) )
56 48 55 eqtrd ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( 0 ... ( 2 · ( ( 𝑗 − 1 ) / 2 ) ) ) = ( ( 0 ... 0 ) ∪ ( ( 0 + 1 ) ... ( 𝑗 − 1 ) ) ) )
57 fz0sn ⊢ ( 0 ... 0 ) = { 0 }
58 15 15 oveq12i ⊢ ( ( ( abs ‘ 0 ) ↑ 2 ) + ( ( abs ‘ 0 ) ↑ 2 ) ) = ( 0 + 0 )
59 00id ⊢ ( 0 + 0 ) = 0
60 58 59 eqtri ⊢ ( ( ( abs ‘ 0 ) ↑ 2 ) + ( ( abs ‘ 0 ) ↑ 2 ) ) = 0
61 1 4sqlem4a ⊢ ( ( 0 ∈ ℤ[i] ∧ 0 ∈ ℤ[i] ) → ( ( ( abs ‘ 0 ) ↑ 2 ) + ( ( abs ‘ 0 ) ↑ 2 ) ) ∈ 𝑆 )
62 24 24 61 mp2an ⊢ ( ( ( abs ‘ 0 ) ↑ 2 ) + ( ( abs ‘ 0 ) ↑ 2 ) ) ∈ 𝑆
63 60 62 eqeltrri ⊢ 0 ∈ 𝑆
64 snssi ⊢ ( 0 ∈ 𝑆 → { 0 } ⊆ 𝑆 )
65 63 64 ax-mp ⊢ { 0 } ⊆ 𝑆
66 57 65 eqsstri ⊢ ( 0 ... 0 ) ⊆ 𝑆
67 66 a1i ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( 0 ... 0 ) ⊆ 𝑆 )
68 0p1e1 ⊢ ( 0 + 1 ) = 1
69 68 oveq1i ⊢ ( ( 0 + 1 ) ... ( 𝑗 − 1 ) ) = ( 1 ... ( 𝑗 − 1 ) )
70 dfss3 ⊢ ( ( 1 ... ( 𝑗 − 1 ) ) ⊆ 𝑆 ↔ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 )
71 70 bilanri ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( 1 ... ( 𝑗 − 1 ) ) ⊆ 𝑆 )
72 69 71 eqsstrid ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( ( 0 + 1 ) ... ( 𝑗 − 1 ) ) ⊆ 𝑆 )
73 67 72 unssd ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( ( 0 ... 0 ) ∪ ( ( 0 + 1 ) ... ( 𝑗 − 1 ) ) ) ⊆ 𝑆 )
74 56 73 eqsstrd ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → ( 0 ... ( 2 · ( ( 𝑗 − 1 ) / 2 ) ) ) ⊆ 𝑆 )
75 oveq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 · 𝑗 ) = ( 𝑖 · 𝑗 ) )
76 75 eleq1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 · 𝑗 ) ∈ 𝑆 ↔ ( 𝑖 · 𝑗 ) ∈ 𝑆 ) )
77 76 cbvrabv ⊢ { 𝑘 ∈ ℕ ∣ ( 𝑘 · 𝑗 ) ∈ 𝑆 } = { 𝑖 ∈ ℕ ∣ ( 𝑖 · 𝑗 ) ∈ 𝑆 }
78 eqid ⊢ inf ( { 𝑘 ∈ ℕ ∣ ( 𝑘 · 𝑗 ) ∈ 𝑆 } , ℝ , < ) = inf ( { 𝑘 ∈ ℕ ∣ ( 𝑘 · 𝑗 ) ∈ 𝑆 } , ℝ , < )
79 1 31 47 33 74 77 78 4sqlem18 ⊢ ( ( 𝑗 ∈ ( ℙ ∖ { 2 } ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → 𝑗 ∈ 𝑆 )
80 29 79 sylanbr ⊢ ( ( ( 𝑗 ∈ ℙ ∧ 𝑗 ≠ 2 ) ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → 𝑗 ∈ 𝑆 )
81 80 an32s ⊢ ( ( ( 𝑗 ∈ ℙ ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) ∧ 𝑗 ≠ 2 ) → 𝑗 ∈ 𝑆 )
82 11 11 oveq12i ⊢ ( ( ( abs ‘ 1 ) ↑ 2 ) + ( ( abs ‘ 1 ) ↑ 2 ) ) = ( 1 + 1 )
83 df-2 ⊢ 2 = ( 1 + 1 )
84 82 83 eqtr4i ⊢ ( ( ( abs ‘ 1 ) ↑ 2 ) + ( ( abs ‘ 1 ) ↑ 2 ) ) = 2
85 1 4sqlem4a ⊢ ( ( 1 ∈ ℤ[i] ∧ 1 ∈ ℤ[i] ) → ( ( ( abs ‘ 1 ) ↑ 2 ) + ( ( abs ‘ 1 ) ↑ 2 ) ) ∈ 𝑆 )
86 21 21 85 mp2an ⊢ ( ( ( abs ‘ 1 ) ↑ 2 ) + ( ( abs ‘ 1 ) ↑ 2 ) ) ∈ 𝑆
87 84 86 eqeltrri ⊢ 2 ∈ 𝑆
88 87 a1i ⊢ ( ( 𝑗 ∈ ℙ ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → 2 ∈ 𝑆 )
89 28 81 88 pm2.61ne ⊢ ( ( 𝑗 ∈ ℙ ∧ ∀ 𝑚 ∈ ( 1 ... ( 𝑗 − 1 ) ) 𝑚 ∈ 𝑆 ) → 𝑗 ∈ 𝑆 )
90 1 mul4sq ⊢ ( ( 𝑚 ∈ 𝑆 ∧ 𝑖 ∈ 𝑆 ) → ( 𝑚 · 𝑖 ) ∈ 𝑆 )
91 90 a1i ⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑚 ∈ 𝑆 ∧ 𝑖 ∈ 𝑆 ) → ( 𝑚 · 𝑖 ) ∈ 𝑆 ) )
92 3 4 5 6 7 27 89 91 prmind2 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ 𝑆 )
93 id ⊢ ( 𝑘 = 0 → 𝑘 = 0 )
94 93 63 eqeltrdi ⊢ ( 𝑘 = 0 → 𝑘 ∈ 𝑆 )
95 92 94 jaoi ⊢ ( ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) → 𝑘 ∈ 𝑆 )
96 2 95 sylbi ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ 𝑆 )
97 96 ssriv ⊢ ℕ0 ⊆ 𝑆
98 1 4sqlem1 ⊢ 𝑆 ⊆ ℕ0
99 97 98 eqssi ⊢ ℕ0 = 𝑆