Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  reprsuc Structured version   Visualization version   GIF version

Theorem reprsuc 31076
Description: Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021.)
Hypotheses
Ref Expression
reprval.a (𝜑𝐴 ⊆ ℕ)
reprval.m (𝜑𝑀 ∈ ℤ)
reprval.s (𝜑𝑆 ∈ ℕ0)
reprsuc.f 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
Assertion
Ref Expression
reprsuc (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = 𝑏𝐴 ran 𝐹)
Distinct variable groups:   𝐴,𝑏,𝑐   𝑀,𝑏,𝑐   𝑆,𝑏,𝑐   𝜑,𝑏,𝑐
Allowed substitution hints:   𝐹(𝑏,𝑐)

Proof of Theorem reprsuc
Dummy variables 𝑎 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reprval.a . . 3 (𝜑𝐴 ⊆ ℕ)
2 reprval.m . . 3 (𝜑𝑀 ∈ ℤ)
3 reprval.s . . . 4 (𝜑𝑆 ∈ ℕ0)
4 1nn0 11556 . . . . 5 1 ∈ ℕ0
54a1i 11 . . . 4 (𝜑 → 1 ∈ ℕ0)
63, 5nn0addcld 11602 . . 3 (𝜑 → (𝑆 + 1) ∈ ℕ0)
71, 2, 6reprval 31071 . 2 (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀})
8 simplr 785 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
9 elmapi 8082 . . . . . . . . . 10 (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
108, 9syl 17 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
113ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ ℕ0)
12 fzonn0p1 12753 . . . . . . . . . 10 (𝑆 ∈ ℕ0𝑆 ∈ (0..^(𝑆 + 1)))
1311, 12syl 17 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ (0..^(𝑆 + 1)))
1410, 13ffvelrnd 6550 . . . . . . . 8 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ 𝐴)
15 simpr 477 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → 𝑏 = (𝑒𝑆))
1615oveq2d 6858 . . . . . . . . . 10 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝑀𝑏) = (𝑀 − (𝑒𝑆)))
1716oveq2d 6858 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝐴(repr‘𝑆)(𝑀𝑏)) = (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))))
18 opeq2 4560 . . . . . . . . . . . . 13 (𝑏 = (𝑒𝑆) → ⟨𝑆, 𝑏⟩ = ⟨𝑆, (𝑒𝑆)⟩)
1918sneqd 4346 . . . . . . . . . . . 12 (𝑏 = (𝑒𝑆) → {⟨𝑆, 𝑏⟩} = {⟨𝑆, (𝑒𝑆)⟩})
2019uneq2d 3929 . . . . . . . . . . 11 (𝑏 = (𝑒𝑆) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}))
2120eqeq2d 2775 . . . . . . . . . 10 (𝑏 = (𝑒𝑆) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
2221adantl 473 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
2317, 22rexeqbidv 3301 . . . . . . . 8 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
249adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
253adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → 𝑆 ∈ ℕ0)
26 fzossfzop1 12754 . . . . . . . . . . . . . . . 16 (𝑆 ∈ ℕ0 → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
2725, 26syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
2824, 27fssresd 6253 . . . . . . . . . . . . . 14 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
2928adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
30 nnex 11281 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
3130a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ℕ ∈ V)
3231, 1ssexd 4966 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ V)
33 fzofi 12981 . . . . . . . . . . . . . . . 16 (0..^𝑆) ∈ Fin
3433elexi 3366 . . . . . . . . . . . . . . 15 (0..^𝑆) ∈ V
35 elmapg 8073 . . . . . . . . . . . . . . 15 ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3632, 34, 35sylancl 580 . . . . . . . . . . . . . 14 (𝜑 → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3736ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3829, 37mpbird 248 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)))
3933a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (0..^𝑆) ∈ Fin)
40 nnsscn 11279 . . . . . . . . . . . . . . . . . . . 20 ℕ ⊆ ℂ
4140a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℕ ⊆ ℂ)
421, 41sstrd 3771 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ⊆ ℂ)
4342ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
4428ffvelrnda 6549 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ 𝐴)
4543, 44sseldd 3762 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
4639, 45fsumcl 14751 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
4746adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
4842adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → 𝐴 ⊆ ℂ)
4925, 12syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → 𝑆 ∈ (0..^(𝑆 + 1)))
5024, 49ffvelrnd 6550 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (𝑒𝑆) ∈ 𝐴)
5148, 50sseldd 3762 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (𝑒𝑆) ∈ ℂ)
5251adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ ℂ)
5347, 52pncand 10647 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) − (𝑒𝑆)) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
54 nfv 2009 . . . . . . . . . . . . . . . . . 18 𝑎(𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
55 nfcv 2907 . . . . . . . . . . . . . . . . . 18 𝑎(𝑒𝑆)
56 fzonel 12691 . . . . . . . . . . . . . . . . . . 19 ¬ 𝑆 ∈ (0..^𝑆)
5756a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → ¬ 𝑆 ∈ (0..^𝑆))
5824adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
5927sselda 3761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
6058, 59ffvelrnd 6550 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ 𝐴)
6143, 60sseldd 3762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ ℂ)
62 fveq2 6375 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑆 → (𝑒𝑎) = (𝑒𝑆))
6354, 55, 39, 25, 57, 61, 62, 51fsumsplitsn 14761 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
64 fzosplitsn 12784 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ (ℤ‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
65 nn0uz 11922 . . . . . . . . . . . . . . . . . . . 20 0 = (ℤ‘0)
6664, 65eleq2s 2862 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ ℕ0 → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
6725, 66syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
6867sumeq1d 14718 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎))
69 simpr 477 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
7069fvresd 6395 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑒𝑎))
7170sumeq2dv 14720 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎))
7271oveq1d 6857 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
7363, 68, 723eqtr4d 2809 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)))
7473adantr 472 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)))
75 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)
7674, 75eqtr3d 2801 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) = 𝑀)
7776oveq1d 6857 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) − (𝑒𝑆)) = (𝑀 − (𝑒𝑆)))
7853, 77eqtr3d 2801 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆)))
7938, 78jca 507 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
80 fveq1 6374 . . . . . . . . . . . . . 14 (𝑑 = (𝑒 ↾ (0..^𝑆)) → (𝑑𝑎) = ((𝑒 ↾ (0..^𝑆))‘𝑎))
8180sumeq2sdv 14722 . . . . . . . . . . . . 13 (𝑑 = (𝑒 ↾ (0..^𝑆)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
8281eqeq1d 2767 . . . . . . . . . . . 12 (𝑑 = (𝑒 ↾ (0..^𝑆)) → (Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆)) ↔ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
8382elrab 3519 . . . . . . . . . . 11 ((𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))} ↔ ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
8479, 83sylibr 225 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))})
851ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝐴 ⊆ ℕ)
862ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑀 ∈ ℤ)
87 nnssz 11644 . . . . . . . . . . . . . . 15 ℕ ⊆ ℤ
881, 87syl6ss 3773 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℤ)
8988ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝐴 ⊆ ℤ)
9089, 14sseldd 3762 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ ℤ)
9186, 90zsubcld 11734 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑀 − (𝑒𝑆)) ∈ ℤ)
9285, 91, 11reprval 31071 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))) = {𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))})
9384, 92eleqtrrd 2847 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))))
94 simpr 477 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → 𝑐 = (𝑒 ↾ (0..^𝑆)))
9594uneq1d 3928 . . . . . . . . . 10 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
9695eqeq2d 2775 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}) ↔ 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩})))
9710ffnd 6224 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 Fn (0..^(𝑆 + 1)))
98 fnsnsplit 6643 . . . . . . . . . . 11 ((𝑒 Fn (0..^(𝑆 + 1)) ∧ 𝑆 ∈ (0..^(𝑆 + 1))) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
9997, 13, 98syl2anc 579 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10011, 65syl6eleq 2854 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ (ℤ‘0))
101 fzodif2 29936 . . . . . . . . . . . . 13 (𝑆 ∈ (ℤ‘0) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
102100, 101syl 17 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
103102reseq2d 5565 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) = (𝑒 ↾ (0..^𝑆)))
104103uneq1d 3928 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10599, 104eqtrd 2799 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10693, 96, 105rspcedvd 3468 . . . . . . . 8 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10714, 23, 106rspcedvd 3468 . . . . . . 7 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
108107anasss 458 . . . . . 6 ((𝜑 ∧ (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)) → ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
109 simpr 477 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
1101adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → 𝐴 ⊆ ℕ)
111110adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝐴 ⊆ ℕ)
1122adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐴) → 𝑀 ∈ ℤ)
11388sselda 3761 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐴) → 𝑏 ∈ ℤ)
114112, 113zsubcld 11734 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → (𝑀𝑏) ∈ ℤ)
115114adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑀𝑏) ∈ ℤ)
1163adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → 𝑆 ∈ ℕ0)
117116adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑆 ∈ ℕ0)
118 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)))
119111, 115, 117, 118reprf 31073 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐:(0..^𝑆)⟶𝐴)
120 simplr 785 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑏𝐴)
121117, 120fsnd 6362 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → {⟨𝑆, 𝑏⟩}:{𝑆}⟶𝐴)
122 fzodisjsn 12714 . . . . . . . . . . . . . 14 ((0..^𝑆) ∩ {𝑆}) = ∅
123122a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅)
124119, 121, 123fun2d 6250 . . . . . . . . . . . 12 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴)
125117, 66syl 17 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
126125feq2d 6209 . . . . . . . . . . . 12 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴))
127124, 126mpbird 248 . . . . . . . . . . 11 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
128 ovex 6874 . . . . . . . . . . . . 13 (0..^(𝑆 + 1)) ∈ V
129 elmapg 8073 . . . . . . . . . . . . 13 ((𝐴 ∈ V ∧ (0..^(𝑆 + 1)) ∈ V) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
13032, 128, 129sylancl 580 . . . . . . . . . . . 12 (𝜑 → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
131130ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
132127, 131mpbird 248 . . . . . . . . . 10 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
133132adantr 472 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
134109, 133eqeltrd 2844 . . . . . . . 8 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
135125adantr 472 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
136135sumeq1d 14718 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎))
137 nfv 2009 . . . . . . . . . 10 𝑎(((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
13833a1i 11 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^𝑆) ∈ Fin)
139117adantr 472 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ ℕ0)
14056a1i 11 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ¬ 𝑆 ∈ (0..^𝑆))
14142ad4antr 724 . . . . . . . . . . 11 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
142127adantr 472 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
143109feq1d 6208 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒:(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
144142, 143mpbird 248 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
145144adantr 472 . . . . . . . . . . . 12 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
146 simpr 477 . . . . . . . . . . . . . 14 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
147 elun1 3942 . . . . . . . . . . . . . 14 (𝑎 ∈ (0..^𝑆) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
148146, 147syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
149125ad2antrr 717 . . . . . . . . . . . . 13 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
150148, 149eleqtrrd 2847 . . . . . . . . . . . 12 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
151145, 150ffvelrnd 6550 . . . . . . . . . . 11 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ 𝐴)
152141, 151sseldd 3762 . . . . . . . . . 10 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ ℂ)
15342ad3antrrr 721 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℂ)
154139, 12syl 17 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ (0..^(𝑆 + 1)))
155144, 154ffvelrnd 6550 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) ∈ 𝐴)
156153, 155sseldd 3762 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) ∈ ℂ)
157137, 55, 138, 139, 140, 152, 62, 156fsumsplitsn 14761 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
158 simplr 785 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
159158fveq1d 6377 . . . . . . . . . . . . . . 15 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎))
160119ffnd 6224 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐 Fn (0..^𝑆))
161160ad2antrr 717 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐 Fn (0..^𝑆))
162121ffnd 6224 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
163162ad2antrr 717 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
164122a1i 11 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅)
165 fvun1 6458 . . . . . . . . . . . . . . . 16 ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐𝑎))
166161, 163, 164, 146, 165syl112anc 1493 . . . . . . . . . . . . . . 15 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐𝑎))
167159, 166eqtrd 2799 . . . . . . . . . . . . . 14 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) = (𝑐𝑎))
168167ralrimiva 3113 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ∀𝑎 ∈ (0..^𝑆)(𝑒𝑎) = (𝑐𝑎))
169168sumeq2d 14719 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎))
170111adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℕ)
171115adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑀𝑏) ∈ ℤ)
172118adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)))
173170, 171, 139, 172reprsum 31074 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = (𝑀𝑏))
174169, 173eqtrd 2799 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) = (𝑀𝑏))
175109fveq1d 6377 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
176160adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 Fn (0..^𝑆))
177162adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
178122a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((0..^𝑆) ∩ {𝑆}) = ∅)
179 snidg 4364 . . . . . . . . . . . . . 14 (𝑆 ∈ ℕ0𝑆 ∈ {𝑆})
180139, 179syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ {𝑆})
181 fvun2 6459 . . . . . . . . . . . . 13 ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
182176, 177, 178, 180, 181syl112anc 1493 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
183120adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏𝐴)
184 fvsng 6640 . . . . . . . . . . . . 13 ((𝑆 ∈ ℕ0𝑏𝐴) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
185139, 183, 184syl2anc 579 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
186175, 182, 1853eqtrd 2803 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) = 𝑏)
187174, 186oveq12d 6860 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)) = ((𝑀𝑏) + 𝑏))
188 zsscn 11632 . . . . . . . . . . . 12 ℤ ⊆ ℂ
189112ad2antrr 717 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℤ)
190188, 189sseldi 3759 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℂ)
191186, 156eqeltrrd 2845 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ ℂ)
192190, 191npcand 10650 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑀𝑏) + 𝑏) = 𝑀)
193187, 192eqtrd 2799 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)) = 𝑀)
194136, 157, 1933eqtrd 2803 . . . . . . . 8 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)
195134, 194jca 507 . . . . . . 7 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
196195r19.29ffa 29711 . . . . . 6 ((𝜑 ∧ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
197108, 196impbida 835 . . . . 5 (𝜑 → ((𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ↔ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})))
198 reprsuc.f . . . . . . 7 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
199 vex 3353 . . . . . . . 8 𝑐 ∈ V
200 snex 5064 . . . . . . . 8 {⟨𝑆, 𝑏⟩} ∈ V
201199, 200unex 7154 . . . . . . 7 (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
202198, 201elrnmpti 5545 . . . . . 6 (𝑒 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
203202rexbii 3188 . . . . 5 (∃𝑏𝐴 𝑒 ∈ ran 𝐹 ↔ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
204197, 203syl6bbr 280 . . . 4 (𝜑 → ((𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ↔ ∃𝑏𝐴 𝑒 ∈ ran 𝐹))
205 fveq1 6374 . . . . . . . 8 (𝑐 = 𝑒 → (𝑐𝑎) = (𝑒𝑎))
206205sumeq2sdv 14722 . . . . . . 7 (𝑐 = 𝑒 → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎))
207206eqeq1d 2767 . . . . . 6 (𝑐 = 𝑒 → (Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
208207cbvrabv 3348 . . . . 5 {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} = {𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀}
209208rabeq2i 3346 . . . 4 (𝑒 ∈ {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} ↔ (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
210 eliun 4680 . . . 4 (𝑒 𝑏𝐴 ran 𝐹 ↔ ∃𝑏𝐴 𝑒 ∈ ran 𝐹)
211204, 209, 2103bitr4g 305 . . 3 (𝜑 → (𝑒 ∈ {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} ↔ 𝑒 𝑏𝐴 ran 𝐹))
212211eqrdv 2763 . 2 (𝜑 → {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} = 𝑏𝐴 ran 𝐹)
2137, 212eqtrd 2799 1 (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = 𝑏𝐴 ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wrex 3056  {crab 3059  Vcvv 3350  cdif 3729  cun 3730  cin 3731  wss 3732  c0 4079  {csn 4334  cop 4340   ciun 4676  cmpt 4888  ran crn 5278  cres 5279   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  𝑚 cmap 8060  Fincfn 8160  cc 10187  0cc0 10189  1c1 10190   + caddc 10192  cmin 10520  cn 11274  0cn0 11538  cz 11624  cuz 11886  ..^cfzo 12673  Σcsu 14703  reprcrepr 31069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-oi 8622  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-clim 14506  df-sum 14704  df-repr 31070
This theorem is referenced by:  breprexplema  31091
  Copyright terms: Public domain W3C validator