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

Metamath Proof Explorer

Theorem efnnfsumcl

Description: Finite sum closure in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Hypotheses efnnfsumcl.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
efnnfsumcl.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
efnnfsumcl.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( exp ‘ 𝐵 ) ∈ ℕ )
Assertion efnnfsumcl ( 𝜑 → ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 efnnfsumcl.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 efnnfsumcl.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 efnnfsumcl.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( exp ‘ 𝐵 ) ∈ ℕ )
4 ssrab2 ⊢ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ⊆ ℝ
5 ax-resscn ⊢ ℝ ⊆ ℂ
6 4 5 sstri ⊢ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ⊆ ℂ
7 6 a1i ⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ⊆ ℂ )
8 fveq2 ⊢ ( 𝑥 = 𝑦 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝑦 ) )
9 8 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ 𝑦 ) ∈ ℕ ) )
10 9 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) )
11 fveq2 ⊢ ( 𝑥 = 𝑧 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝑧 ) )
12 11 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ 𝑧 ) ∈ ℕ ) )
13 12 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) )
14 fveq2 ⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( exp ‘ 𝑥 ) = ( exp ‘ ( 𝑦 + 𝑧 ) ) )
15 14 eleq1d ⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ ( 𝑦 + 𝑧 ) ) ∈ ℕ ) )
16 simpll ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑦 ∈ ℝ )
17 simprl ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑧 ∈ ℝ )
18 16 17 readdcld ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( 𝑦 + 𝑧 ) ∈ ℝ )
19 16 recnd ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑦 ∈ ℂ )
20 17 recnd ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑧 ∈ ℂ )
21 efadd ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( exp ‘ ( 𝑦 + 𝑧 ) ) = ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) )
22 19 20 21 syl2anc ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( exp ‘ ( 𝑦 + 𝑧 ) ) = ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) )
23 nnmulcl ⊢ ( ( ( exp ‘ 𝑦 ) ∈ ℕ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) → ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) ∈ ℕ )
24 23 ad2ant2l ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) ∈ ℕ )
25 22 24 eqeltrd ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( exp ‘ ( 𝑦 + 𝑧 ) ) ∈ ℕ )
26 15 18 25 elrabd ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( 𝑦 + 𝑧 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
27 10 13 26 syl2anb ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ∧ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ) → ( 𝑦 + 𝑧 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
28 27 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ∧ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ) ) → ( 𝑦 + 𝑧 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
29 fveq2 ⊢ ( 𝑥 = 𝐵 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝐵 ) )
30 29 eleq1d ⊢ ( 𝑥 = 𝐵 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ 𝐵 ) ∈ ℕ ) )
31 30 2 3 elrabd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
32 0re ⊢ 0 ∈ ℝ
33 1nn ⊢ 1 ∈ ℕ
34 fveq2 ⊢ ( 𝑥 = 0 → ( exp ‘ 𝑥 ) = ( exp ‘ 0 ) )
35 ef0 ⊢ ( exp ‘ 0 ) = 1
36 34 35 eqtrdi ⊢ ( 𝑥 = 0 → ( exp ‘ 𝑥 ) = 1 )
37 36 eleq1d ⊢ ( 𝑥 = 0 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ 1 ∈ ℕ ) )
38 37 elrab ⊢ ( 0 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( 0 ∈ ℝ ∧ 1 ∈ ℕ ) )
39 32 33 38 mpbir2an ⊢ 0 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ }
40 39 a1i ⊢ ( 𝜑 → 0 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
41 7 28 1 31 40 fsumcllem ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
42 fveq2 ⊢ ( 𝑥 = Σ 𝑘 ∈ 𝐴 𝐵 → ( exp ‘ 𝑥 ) = ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) )
43 42 eleq1d ⊢ ( 𝑥 = Σ 𝑘 ∈ 𝐴 𝐵 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ℕ ) )
44 43 elrab ⊢ ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ ∧ ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ℕ ) )
45 44 simprbi ⊢ ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } → ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ℕ )
46 41 45 syl ⊢ ( 𝜑 → ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ℕ )