Metamath Proof Explorer

Theorem sge0rpcpnf

Description: The sum of an infinite number of a positive constant, is +oo (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0rpcpnf.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sge0rpcpnf.nfi ⊢ ( 𝜑 → ¬ 𝐴 ∈ Fin )
sge0rpcpnf.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
Assertion sge0rpcpnf ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )

Proof

Step Hyp Ref Expression
1 sge0rpcpnf.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 sge0rpcpnf.nfi ⊢ ( 𝜑 → ¬ 𝐴 ∈ Fin )
3 sge0rpcpnf.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4 1 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → 𝐴 ∈ 𝑉 )
5 0xr ⊢ 0 ∈ ℝ*
6 5 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
7 pnfxr ⊢ +∞ ∈ ℝ*
8 7 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
9 3 rpxrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
10 3 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝐵 )
11 3 rpred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
12 ltpnf ⊢ ( 𝐵 ∈ ℝ → 𝐵 < +∞ )
13 11 12 syl ⊢ ( 𝜑 → 𝐵 < +∞ )
14 9 8 13 xrltled ⊢ ( 𝜑 → 𝐵 ≤ +∞ )
15 6 8 9 10 14 eliccxrd ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
17 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
18 16 17 fmptd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
20 4 19 sge0xrcl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ* )
21 7 a1i ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → +∞ ∈ ℝ* )
22 simpr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ )
23 20 21 22 xrgtned ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → +∞ ≠ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
24 23 necomd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ≠ +∞ )
25 24 neneqd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ¬ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
26 4 19 sge0repnf ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) )
27 25 26 mpbird ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
28 11 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → 𝐵 ∈ ℝ )
29 3 rpne0d ⊢ ( 𝜑 → 𝐵 ≠ 0 )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → 𝐵 ≠ 0 )
31 27 28 30 redivcld ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) ∈ ℝ )
32 arch ⊢ ( ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) ∈ ℝ → ∃ 𝑛 ∈ ℕ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 )
33 31 32 syl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ∃ 𝑛 ∈ ℕ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 )
34 ishashinf ⊢ ( ¬ 𝐴 ∈ Fin → ∀ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑦 ) = 𝑛 )
35 2 34 syl ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑦 ) = 𝑛 )
36 35 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑦 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑦 ) = 𝑛 )
37 df-rex ⊢ ( ∃ 𝑦 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑦 ) = 𝑛 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) )
38 36 37 sylib ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑦 ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) )
39 38 adantlr ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ) → ∃ 𝑦 ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) )
40 39 3adant3 ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → ∃ 𝑦 ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) )
41 nfv ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 )
42 simprl ⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → 𝑦 ∈ 𝒫 𝐴 )
43 simpr ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) → ( ♯ ‘ 𝑦 ) = 𝑛 )
44 simpl ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) → 𝑛 ∈ ℕ )
45 43 44 eqeltrd ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) → ( ♯ ‘ 𝑦 ) ∈ ℕ )
46 nnnn0 ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℕ → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
47 vex ⊢ 𝑦 ∈ V
48 47 a1i ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℕ → 𝑦 ∈ V )
49 hashclb ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ Fin ↔ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ) )
50 48 49 syl ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℕ → ( 𝑦 ∈ Fin ↔ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ) )
51 46 50 mpbird ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℕ → 𝑦 ∈ Fin )
52 45 51 syl ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) → 𝑦 ∈ Fin )
53 52 adantrl ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → 𝑦 ∈ Fin )
54 53 3ad2antl2 ⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → 𝑦 ∈ Fin )
55 42 54 elind ⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
56 simp3 ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 )
57 27 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
58 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
59 58 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → 𝑛 ∈ ℝ )
60 3 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → 𝐵 ∈ ℝ+ )
61 60 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → 𝐵 ∈ ℝ+ )
62 57 59 61 ltdivmul2d ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → ( ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ↔ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( 𝑛 · 𝐵 ) ) )
63 56 62 mpbid ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( 𝑛 · 𝐵 ) )
64 63 adantr ⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( 𝑛 · 𝐵 ) )
65 53 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → 𝑦 ∈ Fin )
66 5 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) ∧ 𝑥 ∈ 𝑦 ) → 0 ∈ ℝ* )
67 7 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) ∧ 𝑥 ∈ 𝑦 ) → +∞ ∈ ℝ* )
68 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝐵 ∈ ℝ* )
69 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) ∧ 𝑥 ∈ 𝑦 ) → 0 ≤ 𝐵 )
70 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝐵 < +∞ )
71 66 67 68 69 70 elicod ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
72 65 71 sge0fsummpt ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) = Σ 𝑥 ∈ 𝑦 𝐵 )
73 11 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
74 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → 𝐵 ∈ ℂ )
75 fsumconst ⊢ ( ( 𝑦 ∈ Fin ∧ 𝐵 ∈ ℂ ) → Σ 𝑥 ∈ 𝑦 𝐵 = ( ( ♯ ‘ 𝑦 ) · 𝐵 ) )
76 65 74 75 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → Σ 𝑥 ∈ 𝑦 𝐵 = ( ( ♯ ‘ 𝑦 ) · 𝐵 ) )
77 oveq1 ⊢ ( ( ♯ ‘ 𝑦 ) = 𝑛 → ( ( ♯ ‘ 𝑦 ) · 𝐵 ) = ( 𝑛 · 𝐵 ) )
78 77 adantl ⊢ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) → ( ( ♯ ‘ 𝑦 ) · 𝐵 ) = ( 𝑛 · 𝐵 ) )
79 78 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → ( ( ♯ ‘ 𝑦 ) · 𝐵 ) = ( 𝑛 · 𝐵 ) )
80 72 76 79 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → ( 𝑛 · 𝐵 ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
81 80 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → ( 𝑛 · 𝐵 ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
82 81 3adantl3 ⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → ( 𝑛 · 𝐵 ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
83 64 82 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
84 55 83 jca ⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) ∧ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) ) → ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ) )
85 84 ex ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) → ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ) ) )
86 41 85 eximd ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → ( ∃ 𝑦 ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑦 ) = 𝑛 ) → ∃ 𝑦 ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ) ) )
87 40 86 mpd ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → ∃ 𝑦 ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ) )
88 df-rex ⊢ ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ) )
89 87 88 sylibr ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) ∧ 𝑛 ∈ ℕ ∧ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
90 89 3exp ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ( 𝑛 ∈ ℕ → ( ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ) ) )
91 90 rexlimdv ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ( ∃ 𝑛 ∈ ℕ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) / 𝐵 ) < 𝑛 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ) )
92 33 91 mpd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
93 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐴 ∈ 𝑉 )
94 16 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
95 elpwinss ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
96 95 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ⊆ 𝐴 )
97 93 94 96 sge0lessmpt ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
98 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
99 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑦 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
100 eqid ⊢ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑦 ↦ 𝐵 )
101 99 100 fmptd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) : 𝑦 ⟶ ( 0 [,] +∞ ) )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) : 𝑦 ⟶ ( 0 [,] +∞ ) )
103 98 102 sge0xrcl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ∈ ℝ* )
104 1 18 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ* )
105 104 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ* )
106 103 105 xrlenltd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ↔ ¬ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ) )
107 97 106 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ¬ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
108 107 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ¬ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
109 ralnex ⊢ ( ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ¬ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) ↔ ¬ ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
110 108 109 sylib ⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
111 110 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) → ¬ ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
112 92 111 pm2.65da ⊢ ( 𝜑 → ¬ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ )
113 nltpnft ⊢ ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ* → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ↔ ¬ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) )
114 104 113 syl ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ↔ ¬ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < +∞ ) )
115 112 114 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )