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 31000
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 11498 . . . . 5 1 ∈ ℕ0
54a1i 11 . . . 4 (𝜑 → 1 ∈ ℕ0)
63, 5nn0addcld 11545 . . 3 (𝜑 → (𝑆 + 1) ∈ ℕ0)
71, 2, 6reprval 30995 . 2 (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀})
8 simplr 809 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
9 elmapi 8043 . . . . . . . . . 10 (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
108, 9syl 17 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
113ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ ℕ0)
12 fzonn0p1 12737 . . . . . . . . . 10 (𝑆 ∈ ℕ0𝑆 ∈ (0..^(𝑆 + 1)))
1311, 12syl 17 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ (0..^(𝑆 + 1)))
1410, 13ffvelrnd 6521 . . . . . . . 8 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ 𝐴)
15 simpr 479 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → 𝑏 = (𝑒𝑆))
1615oveq2d 6827 . . . . . . . . . 10 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝑀𝑏) = (𝑀 − (𝑒𝑆)))
1716oveq2d 6827 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝐴(repr‘𝑆)(𝑀𝑏)) = (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))))
18 opeq2 4552 . . . . . . . . . . . . 13 (𝑏 = (𝑒𝑆) → ⟨𝑆, 𝑏⟩ = ⟨𝑆, (𝑒𝑆)⟩)
1918sneqd 4331 . . . . . . . . . . . 12 (𝑏 = (𝑒𝑆) → {⟨𝑆, 𝑏⟩} = {⟨𝑆, (𝑒𝑆)⟩})
2019uneq2d 3908 . . . . . . . . . . 11 (𝑏 = (𝑒𝑆) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}))
2120eqeq2d 2768 . . . . . . . . . 10 (𝑏 = (𝑒𝑆) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
2221adantl 473 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
2317, 22rexeqbidv 3290 . . . . . . . 8 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
249adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
253adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → 𝑆 ∈ ℕ0)
26 fzossfzop1 12738 . . . . . . . . . . . . . . . 16 (𝑆 ∈ ℕ0 → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
2725, 26syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
2824, 27fssresd 6230 . . . . . . . . . . . . . 14 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
2928adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
30 nnex 11216 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
3130a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ℕ ∈ V)
3231, 1ssexd 4955 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ V)
33 fzofi 12965 . . . . . . . . . . . . . . . 16 (0..^𝑆) ∈ Fin
3433elexi 3351 . . . . . . . . . . . . . . 15 (0..^𝑆) ∈ V
35 elmapg 8034 . . . . . . . . . . . . . . 15 ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3632, 34, 35sylancl 697 . . . . . . . . . . . . . 14 (𝜑 → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3736ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3829, 37mpbird 247 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)))
3933a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (0..^𝑆) ∈ Fin)
40 nnsscn 11215 . . . . . . . . . . . . . . . . . . . 20 ℕ ⊆ ℂ
4140a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℕ ⊆ ℂ)
421, 41sstrd 3752 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ⊆ ℂ)
4342ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
4428ffvelrnda 6520 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ 𝐴)
4543, 44sseldd 3743 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
4639, 45fsumcl 14661 . . . . . . . . . . . . . . 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 6521 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (𝑒𝑆) ∈ 𝐴)
5148, 50sseldd 3743 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (𝑒𝑆) ∈ ℂ)
5251adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ ℂ)
5347, 52pncand 10583 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) − (𝑒𝑆)) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
54 nfv 1990 . . . . . . . . . . . . . . . . . 18 𝑎(𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
55 nfcv 2900 . . . . . . . . . . . . . . . . . 18 𝑎(𝑒𝑆)
56 fzonel 12675 . . . . . . . . . . . . . . . . . . 19 ¬ 𝑆 ∈ (0..^𝑆)
5756a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → ¬ 𝑆 ∈ (0..^𝑆))
5824adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
5927sselda 3742 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
6058, 59ffvelrnd 6521 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ 𝐴)
6143, 60sseldd 3743 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ ℂ)
62 fveq2 6350 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑆 → (𝑒𝑎) = (𝑒𝑆))
6354, 55, 39, 25, 57, 61, 62, 51fsumsplitsn 14671 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
64 fzosplitsn 12768 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ (ℤ‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
65 nn0uz 11913 . . . . . . . . . . . . . . . . . . . 20 0 = (ℤ‘0)
6664, 65eleq2s 2855 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ ℕ0 → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
6725, 66syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
6867sumeq1d 14628 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎))
69 simpr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
7069fvresd 6367 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑒𝑎))
7170sumeq2dv 14630 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎))
7271oveq1d 6826 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
7363, 68, 723eqtr4d 2802 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)))
7473adantr 472 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)))
75 simpr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)
7674, 75eqtr3d 2794 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) = 𝑀)
7776oveq1d 6826 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) − (𝑒𝑆)) = (𝑀 − (𝑒𝑆)))
7853, 77eqtr3d 2794 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆)))
7938, 78jca 555 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
80 fveq1 6349 . . . . . . . . . . . . . 14 (𝑑 = (𝑒 ↾ (0..^𝑆)) → (𝑑𝑎) = ((𝑒 ↾ (0..^𝑆))‘𝑎))
8180sumeq2sdv 14632 . . . . . . . . . . . . 13 (𝑑 = (𝑒 ↾ (0..^𝑆)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
8281eqeq1d 2760 . . . . . . . . . . . 12 (𝑑 = (𝑒 ↾ (0..^𝑆)) → (Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆)) ↔ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
8382elrab 3502 . . . . . . . . . . 11 ((𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))} ↔ ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
8479, 83sylibr 224 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))})
851ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝐴 ⊆ ℕ)
862ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑀 ∈ ℤ)
87 nnssz 11587 . . . . . . . . . . . . . . 15 ℕ ⊆ ℤ
881, 87syl6ss 3754 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℤ)
8988ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝐴 ⊆ ℤ)
9089, 14sseldd 3743 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ ℤ)
9186, 90zsubcld 11677 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑀 − (𝑒𝑆)) ∈ ℤ)
9285, 91, 11reprval 30995 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))) = {𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))})
9384, 92eleqtrrd 2840 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))))
94 simpr 479 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → 𝑐 = (𝑒 ↾ (0..^𝑆)))
9594uneq1d 3907 . . . . . . . . . 10 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
9695eqeq2d 2768 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}) ↔ 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩})))
9710ffnd 6205 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 Fn (0..^(𝑆 + 1)))
98 fnsnsplit 6612 . . . . . . . . . . 11 ((𝑒 Fn (0..^(𝑆 + 1)) ∧ 𝑆 ∈ (0..^(𝑆 + 1))) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
9997, 13, 98syl2anc 696 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10011, 65syl6eleq 2847 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ (ℤ‘0))
101 fzodif2 29859 . . . . . . . . . . . . 13 (𝑆 ∈ (ℤ‘0) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
102100, 101syl 17 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
103102reseq2d 5549 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) = (𝑒 ↾ (0..^𝑆)))
104103uneq1d 3907 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10599, 104eqtrd 2792 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10693, 96, 105rspcedvd 3454 . . . . . . . 8 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10714, 23, 106rspcedvd 3454 . . . . . . 7 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
108107anasss 682 . . . . . 6 ((𝜑 ∧ (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)) → ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
109 simpr 479 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
1101adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → 𝐴 ⊆ ℕ)
111110adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝐴 ⊆ ℕ)
1122adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐴) → 𝑀 ∈ ℤ)
11388sselda 3742 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐴) → 𝑏 ∈ ℤ)
114112, 113zsubcld 11677 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → (𝑀𝑏) ∈ ℤ)
115114adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑀𝑏) ∈ ℤ)
1163adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → 𝑆 ∈ ℕ0)
117116adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑆 ∈ ℕ0)
118 simpr 479 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)))
119111, 115, 117, 118reprf 30997 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐:(0..^𝑆)⟶𝐴)
120 simplr 809 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑏𝐴)
121117, 120fsnd 6338 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → {⟨𝑆, 𝑏⟩}:{𝑆}⟶𝐴)
122 fzodisjsn 12698 . . . . . . . . . . . . . 14 ((0..^𝑆) ∩ {𝑆}) = ∅
123122a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅)
124119, 121, 123fun2d 6227 . . . . . . . . . . . 12 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴)
125117, 66syl 17 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
126125feq2d 6190 . . . . . . . . . . . 12 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴))
127124, 126mpbird 247 . . . . . . . . . . 11 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
128 ovex 6839 . . . . . . . . . . . . 13 (0..^(𝑆 + 1)) ∈ V
129 elmapg 8034 . . . . . . . . . . . . 13 ((𝐴 ∈ V ∧ (0..^(𝑆 + 1)) ∈ V) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
13032, 128, 129sylancl 697 . . . . . . . . . . . 12 (𝜑 → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
131130ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
132127, 131mpbird 247 . . . . . . . . . 10 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
133132adantr 472 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
134109, 133eqeltrd 2837 . . . . . . . 8 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
135125adantr 472 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
136135sumeq1d 14628 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎))
137 nfv 1990 . . . . . . . . . 10 𝑎(((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
13833a1i 11 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^𝑆) ∈ Fin)
139117adantr 472 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ ℕ0)
14056a1i 11 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ¬ 𝑆 ∈ (0..^𝑆))
14142ad4antr 771 . . . . . . . . . . 11 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
142127adantr 472 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
143109feq1d 6189 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒:(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
144142, 143mpbird 247 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
145144adantr 472 . . . . . . . . . . . 12 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
146 simpr 479 . . . . . . . . . . . . . 14 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
147 elun1 3921 . . . . . . . . . . . . . 14 (𝑎 ∈ (0..^𝑆) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
148146, 147syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
149125ad2antrr 764 . . . . . . . . . . . . 13 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
150148, 149eleqtrrd 2840 . . . . . . . . . . . 12 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
151145, 150ffvelrnd 6521 . . . . . . . . . . 11 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ 𝐴)
152141, 151sseldd 3743 . . . . . . . . . 10 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ ℂ)
15342ad3antrrr 768 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℂ)
154139, 12syl 17 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ (0..^(𝑆 + 1)))
155144, 154ffvelrnd 6521 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) ∈ 𝐴)
156153, 155sseldd 3743 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) ∈ ℂ)
157137, 55, 138, 139, 140, 152, 62, 156fsumsplitsn 14671 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
158 simplr 809 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
159158fveq1d 6352 . . . . . . . . . . . . . . 15 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎))
160119ffnd 6205 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐 Fn (0..^𝑆))
161160ad2antrr 764 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐 Fn (0..^𝑆))
162121ffnd 6205 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
163162ad2antrr 764 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
164122a1i 11 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅)
165 fvun1 6429 . . . . . . . . . . . . . . . 16 ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐𝑎))
166161, 163, 164, 146, 165syl112anc 1481 . . . . . . . . . . . . . . 15 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐𝑎))
167159, 166eqtrd 2792 . . . . . . . . . . . . . 14 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) = (𝑐𝑎))
168167ralrimiva 3102 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ∀𝑎 ∈ (0..^𝑆)(𝑒𝑎) = (𝑐𝑎))
169168sumeq2d 14629 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎))
170111adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℕ)
171115adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑀𝑏) ∈ ℤ)
172118adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)))
173170, 171, 139, 172reprsum 30998 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = (𝑀𝑏))
174169, 173eqtrd 2792 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) = (𝑀𝑏))
175109fveq1d 6352 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
176160adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 Fn (0..^𝑆))
177162adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
178122a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((0..^𝑆) ∩ {𝑆}) = ∅)
179 snidg 4349 . . . . . . . . . . . . . 14 (𝑆 ∈ ℕ0𝑆 ∈ {𝑆})
180139, 179syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ {𝑆})
181 fvun2 6430 . . . . . . . . . . . . 13 ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
182176, 177, 178, 180, 181syl112anc 1481 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
183120adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏𝐴)
184 fvsng 6609 . . . . . . . . . . . . 13 ((𝑆 ∈ ℕ0𝑏𝐴) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
185139, 183, 184syl2anc 696 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
186175, 182, 1853eqtrd 2796 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) = 𝑏)
187174, 186oveq12d 6829 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)) = ((𝑀𝑏) + 𝑏))
188 zsscn 11575 . . . . . . . . . . . 12 ℤ ⊆ ℂ
189112ad2antrr 764 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℤ)
190188, 189sseldi 3740 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℂ)
191186, 156eqeltrrd 2838 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ ℂ)
192190, 191npcand 10586 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑀𝑏) + 𝑏) = 𝑀)
193187, 192eqtrd 2792 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)) = 𝑀)
194136, 157, 1933eqtrd 2796 . . . . . . . 8 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)
195134, 194jca 555 . . . . . . 7 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
196195r19.29ffa 29627 . . . . . 6 ((𝜑 ∧ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
197108, 196impbida 913 . . . . 5 (𝜑 → ((𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ↔ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})))
198 reprsuc.f . . . . . . 7 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
199 vex 3341 . . . . . . . 8 𝑐 ∈ V
200 snex 5055 . . . . . . . 8 {⟨𝑆, 𝑏⟩} ∈ V
201199, 200unex 7119 . . . . . . 7 (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
202198, 201elrnmpti 5529 . . . . . 6 (𝑒 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
203202rexbii 3177 . . . . 5 (∃𝑏𝐴 𝑒 ∈ ran 𝐹 ↔ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
204197, 203syl6bbr 278 . . . 4 (𝜑 → ((𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ↔ ∃𝑏𝐴 𝑒 ∈ ran 𝐹))
205 fveq1 6349 . . . . . . . 8 (𝑐 = 𝑒 → (𝑐𝑎) = (𝑒𝑎))
206205sumeq2sdv 14632 . . . . . . 7 (𝑐 = 𝑒 → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎))
207206eqeq1d 2760 . . . . . 6 (𝑐 = 𝑒 → (Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
208207cbvrabv 3337 . . . . 5 {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} = {𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀}
209208rabeq2i 3335 . . . 4 (𝑒 ∈ {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} ↔ (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
210 eliun 4674 . . . 4 (𝑒 𝑏𝐴 ran 𝐹 ↔ ∃𝑏𝐴 𝑒 ∈ ran 𝐹)
211204, 209, 2103bitr4g 303 . . 3 (𝜑 → (𝑒 ∈ {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} ↔ 𝑒 𝑏𝐴 ran 𝐹))
212211eqrdv 2756 . 2 (𝜑 → {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} = 𝑏𝐴 ran 𝐹)
2137, 212eqtrd 2792 1 (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = 𝑏𝐴 ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1630  wcel 2137  wrex 3049  {crab 3052  Vcvv 3338  cdif 3710  cun 3711  cin 3712  wss 3713  c0 4056  {csn 4319  cop 4325   ciun 4670  cmpt 4879  ran crn 5265  cres 5266   Fn wfn 6042  wf 6043  cfv 6047  (class class class)co 6811  𝑚 cmap 8021  Fincfn 8119  cc 10124  0cc0 10126  1c1 10127   + caddc 10129  cmin 10456  cn 11210  0cn0 11482  cz 11567  cuz 11877  ..^cfzo 12657  Σcsu 14613  reprcrepr 30993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-inf2 8709  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-fal 1636  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-int 4626  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-se 5224  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-isom 6056  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-1st 7331  df-2nd 7332  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-oadd 7731  df-er 7909  df-map 8023  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-sup 8511  df-oi 8578  df-card 8953  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-div 10875  df-nn 11211  df-2 11269  df-3 11270  df-n0 11483  df-z 11568  df-uz 11878  df-rp 12024  df-fz 12518  df-fzo 12658  df-seq 12994  df-exp 13053  df-hash 13310  df-cj 14036  df-re 14037  df-im 14038  df-sqrt 14172  df-abs 14173  df-clim 14416  df-sum 14614  df-repr 30994
This theorem is referenced by:  breprexplema  31015
  Copyright terms: Public domain W3C validator