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 30821
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 11346 . . . . 5 1 ∈ ℕ0
54a1i 11 . . . 4 (𝜑 → 1 ∈ ℕ0)
63, 5nn0addcld 11393 . . 3 (𝜑 → (𝑆 + 1) ∈ ℕ0)
71, 2, 6reprval 30816 . 2 (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀})
8 simplr 807 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
9 elmapi 7921 . . . . . . . . . 10 (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
108, 9syl 17 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
113ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ ℕ0)
12 fzonn0p1 12584 . . . . . . . . . 10 (𝑆 ∈ ℕ0𝑆 ∈ (0..^(𝑆 + 1)))
1311, 12syl 17 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ (0..^(𝑆 + 1)))
1410, 13ffvelrnd 6400 . . . . . . . 8 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ 𝐴)
15 simpr 476 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → 𝑏 = (𝑒𝑆))
1615oveq2d 6706 . . . . . . . . . 10 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝑀𝑏) = (𝑀 − (𝑒𝑆)))
1716oveq2d 6706 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝐴(repr‘𝑆)(𝑀𝑏)) = (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))))
18 opeq2 4434 . . . . . . . . . . . . 13 (𝑏 = (𝑒𝑆) → ⟨𝑆, 𝑏⟩ = ⟨𝑆, (𝑒𝑆)⟩)
1918sneqd 4222 . . . . . . . . . . . 12 (𝑏 = (𝑒𝑆) → {⟨𝑆, 𝑏⟩} = {⟨𝑆, (𝑒𝑆)⟩})
2019uneq2d 3800 . . . . . . . . . . 11 (𝑏 = (𝑒𝑆) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}))
2120eqeq2d 2661 . . . . . . . . . 10 (𝑏 = (𝑒𝑆) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
2221adantl 481 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ 𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
2317, 22rexeqbidv 3183 . . . . . . . 8 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑏 = (𝑒𝑆)) → (∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩})))
249adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
253adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → 𝑆 ∈ ℕ0)
26 fzossfzop1 12585 . . . . . . . . . . . . . . . 16 (𝑆 ∈ ℕ0 → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
2725, 26syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
2824, 27fssresd 6109 . . . . . . . . . . . . . 14 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
2928adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)
30 nnex 11064 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
3130a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → ℕ ∈ V)
3231, 1ssexd 4838 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ V)
33 fzofi 12813 . . . . . . . . . . . . . . . 16 (0..^𝑆) ∈ Fin
3433elexi 3244 . . . . . . . . . . . . . . 15 (0..^𝑆) ∈ V
35 elmapg 7912 . . . . . . . . . . . . . . 15 ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3632, 34, 35sylancl 695 . . . . . . . . . . . . . 14 (𝜑 → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴))
3736ad2antrr 762 . . . . . . . . . . . . 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 11063 . . . . . . . . . . . . . . . . . . . 20 ℕ ⊆ ℂ
4140a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℕ ⊆ ℂ)
421, 41sstrd 3646 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ⊆ ℂ)
4342ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
4428ffvelrnda 6399 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ 𝐴)
4543, 44sseldd 3637 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
4639, 45fsumcl 14508 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
4746adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ)
4842adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → 𝐴 ⊆ ℂ)
4925, 12syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → 𝑆 ∈ (0..^(𝑆 + 1)))
5024, 49ffvelrnd 6400 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (𝑒𝑆) ∈ 𝐴)
5148, 50sseldd 3637 . . . . . . . . . . . . . . 15 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (𝑒𝑆) ∈ ℂ)
5251adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ ℂ)
5347, 52pncand 10431 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) − (𝑒𝑆)) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
54 nfv 1883 . . . . . . . . . . . . . . . . . 18 𝑎(𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
55 nfcv 2793 . . . . . . . . . . . . . . . . . 18 𝑎(𝑒𝑆)
56 fzonel 12522 . . . . . . . . . . . . . . . . . . 19 ¬ 𝑆 ∈ (0..^𝑆)
5756a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → ¬ 𝑆 ∈ (0..^𝑆))
5824adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
5927sselda 3636 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
6058, 59ffvelrnd 6400 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ 𝐴)
6143, 60sseldd 3637 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ ℂ)
62 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑆 → (𝑒𝑎) = (𝑒𝑆))
6354, 55, 39, 25, 57, 61, 62, 51fsumsplitsn 14518 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
64 fzosplitsn 12616 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ (ℤ‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
65 nn0uz 11760 . . . . . . . . . . . . . . . . . . . 20 0 = (ℤ‘0)
6664, 65eleq2s 2748 . . . . . . . . . . . . . . . . . . 19 (𝑆 ∈ ℕ0 → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
6725, 66syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
6867sumeq1d 14475 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎))
69 simpr 476 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
7069fvresd 6246 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑒𝑎))
7170sumeq2dv 14477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎))
7271oveq1d 6705 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
7363, 68, 723eqtr4d 2695 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)))
7473adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)))
75 simpr 476 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)
7674, 75eqtr3d 2687 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) = 𝑀)
7776oveq1d 6705 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒𝑆)) − (𝑒𝑆)) = (𝑀 − (𝑒𝑆)))
7853, 77eqtr3d 2687 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆)))
7938, 78jca 553 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
80 fveq1 6228 . . . . . . . . . . . . . 14 (𝑑 = (𝑒 ↾ (0..^𝑆)) → (𝑑𝑎) = ((𝑒 ↾ (0..^𝑆))‘𝑎))
8180sumeq2sdv 14479 . . . . . . . . . . . . 13 (𝑑 = (𝑒 ↾ (0..^𝑆)) → Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎))
8281eqeq1d 2653 . . . . . . . . . . . 12 (𝑑 = (𝑒 ↾ (0..^𝑆)) → (Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆)) ↔ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
8382elrab 3396 . . . . . . . . . . 11 ((𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))} ↔ ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴𝑚 (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒𝑆))))
8479, 83sylibr 224 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))})
851ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝐴 ⊆ ℕ)
862ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑀 ∈ ℤ)
87 nnssz 11435 . . . . . . . . . . . . . . 15 ℕ ⊆ ℤ
881, 87syl6ss 3648 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℤ)
8988ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝐴 ⊆ ℤ)
9089, 14sseldd 3637 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒𝑆) ∈ ℤ)
9186, 90zsubcld 11525 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑀 − (𝑒𝑆)) ∈ ℤ)
9285, 91, 11reprval 30816 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))) = {𝑑 ∈ (𝐴𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑𝑎) = (𝑀 − (𝑒𝑆))})
9384, 92eleqtrrd 2733 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆))))
94 simpr 476 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → 𝑐 = (𝑒 ↾ (0..^𝑆)))
9594uneq1d 3799 . . . . . . . . . 10 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
9695eqeq2d 2661 . . . . . . . . 9 ((((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}) ↔ 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩})))
9710ffnd 6084 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 Fn (0..^(𝑆 + 1)))
98 fnsnsplit 6491 . . . . . . . . . . 11 ((𝑒 Fn (0..^(𝑆 + 1)) ∧ 𝑆 ∈ (0..^(𝑆 + 1))) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
9997, 13, 98syl2anc 694 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10011, 65syl6eleq 2740 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑆 ∈ (ℤ‘0))
101 fzodif2 29680 . . . . . . . . . . . . 13 (𝑆 ∈ (ℤ‘0) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
102100, 101syl 17 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆))
103102reseq2d 5428 . . . . . . . . . . 11 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → (𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) = (𝑒 ↾ (0..^𝑆)))
104103uneq1d 3799 . . . . . . . . . 10 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {⟨𝑆, (𝑒𝑆)⟩}) = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10599, 104eqtrd 2685 . . . . . . . . 9 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10693, 96, 105rspcedvd 3348 . . . . . . . 8 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒𝑆)))𝑒 = (𝑐 ∪ {⟨𝑆, (𝑒𝑆)⟩}))
10714, 23, 106rspcedvd 3348 . . . . . . 7 (((𝜑𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) → ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
108107anasss 680 . . . . . 6 ((𝜑 ∧ (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)) → ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
109 simpr 476 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
1101adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → 𝐴 ⊆ ℕ)
111110adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝐴 ⊆ ℕ)
1122adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐴) → 𝑀 ∈ ℤ)
11388sselda 3636 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐴) → 𝑏 ∈ ℤ)
114112, 113zsubcld 11525 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → (𝑀𝑏) ∈ ℤ)
115114adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑀𝑏) ∈ ℤ)
1163adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐴) → 𝑆 ∈ ℕ0)
117116adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑆 ∈ ℕ0)
118 simpr 476 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)))
119111, 115, 117, 118reprf 30818 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐:(0..^𝑆)⟶𝐴)
120 simplr 807 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑏𝐴)
121117, 120fsnd 6217 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → {⟨𝑆, 𝑏⟩}:{𝑆}⟶𝐴)
122 fzodisjsn 12545 . . . . . . . . . . . . . 14 ((0..^𝑆) ∩ {𝑆}) = ∅
123122a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅)
124119, 121, 123fun2d 6106 . . . . . . . . . . . 12 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴)
125117, 66syl 17 . . . . . . . . . . . . 13 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
126125feq2d 6069 . . . . . . . . . . . 12 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶𝐴))
127124, 126mpbird 247 . . . . . . . . . . 11 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
128 ovex 6718 . . . . . . . . . . . . 13 (0..^(𝑆 + 1)) ∈ V
129 elmapg 7912 . . . . . . . . . . . . 13 ((𝐴 ∈ V ∧ (0..^(𝑆 + 1)) ∈ V) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
13032, 128, 129sylancl 695 . . . . . . . . . . . 12 (𝜑 → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
131130ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
132127, 131mpbird 247 . . . . . . . . . 10 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
133132adantr 480 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
134109, 133eqeltrd 2730 . . . . . . . 8 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))))
135125adantr 480 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
136135sumeq1d 14475 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎))
137 nfv 1883 . . . . . . . . . 10 𝑎(((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
13833a1i 11 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (0..^𝑆) ∈ Fin)
139117adantr 480 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ ℕ0)
14056a1i 11 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ¬ 𝑆 ∈ (0..^𝑆))
14142ad4antr 769 . . . . . . . . . . 11 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ)
142127adantr 480 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴)
143109feq1d 6068 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒:(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {⟨𝑆, 𝑏⟩}):(0..^(𝑆 + 1))⟶𝐴))
144142, 143mpbird 247 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
145144adantr 480 . . . . . . . . . . . 12 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴)
146 simpr 476 . . . . . . . . . . . . . 14 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
147 elun1 3813 . . . . . . . . . . . . . 14 (𝑎 ∈ (0..^𝑆) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
148146, 147syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆}))
149125ad2antrr 762 . . . . . . . . . . . . 13 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
150148, 149eleqtrrd 2733 . . . . . . . . . . . 12 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
151145, 150ffvelrnd 6400 . . . . . . . . . . 11 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ 𝐴)
152141, 151sseldd 3637 . . . . . . . . . 10 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ ℂ)
15342ad3antrrr 766 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℂ)
154139, 12syl 17 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ (0..^(𝑆 + 1)))
155144, 154ffvelrnd 6400 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) ∈ 𝐴)
156153, 155sseldd 3637 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) ∈ ℂ)
157137, 55, 138, 139, 140, 152, 62, 156fsumsplitsn 14518 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)))
158 simplr 807 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
159158fveq1d 6231 . . . . . . . . . . . . . . 15 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎))
160119ffnd 6084 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → 𝑐 Fn (0..^𝑆))
161160ad2antrr 762 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐 Fn (0..^𝑆))
162121ffnd 6084 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
163162ad2antrr 762 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
164122a1i 11 . . . . . . . . . . . . . . . 16 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅)
165 fvun1 6308 . . . . . . . . . . . . . . . 16 ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐𝑎))
166161, 163, 164, 146, 165syl112anc 1370 . . . . . . . . . . . . . . 15 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑐𝑎))
167159, 166eqtrd 2685 . . . . . . . . . . . . . 14 (((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) = (𝑐𝑎))
168167ralrimiva 2995 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ∀𝑎 ∈ (0..^𝑆)(𝑒𝑎) = (𝑐𝑎))
169168sumeq2d 14476 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎))
170111adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝐴 ⊆ ℕ)
171115adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑀𝑏) ∈ ℤ)
172118adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)))
173170, 171, 139, 172reprsum 30819 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = (𝑀𝑏))
174169, 173eqtrd 2685 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) = (𝑀𝑏))
175109fveq1d 6231 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) = ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
176160adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑐 Fn (0..^𝑆))
177162adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
178122a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((0..^𝑆) ∩ {𝑆}) = ∅)
179 snidg 4239 . . . . . . . . . . . . . 14 (𝑆 ∈ ℕ0𝑆 ∈ {𝑆})
180139, 179syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ {𝑆})
181 fvun2 6309 . . . . . . . . . . . . 13 ((𝑐 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
182176, 177, 178, 180, 181syl112anc 1370 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑐 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
183120adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏𝐴)
184 fvsng 6488 . . . . . . . . . . . . 13 ((𝑆 ∈ ℕ0𝑏𝐴) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
185139, 183, 184syl2anc 694 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
186175, 182, 1853eqtrd 2689 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒𝑆) = 𝑏)
187174, 186oveq12d 6708 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)) = ((𝑀𝑏) + 𝑏))
188 zsscn 11423 . . . . . . . . . . . 12 ℤ ⊆ ℂ
189112ad2antrr 762 . . . . . . . . . . . 12 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℤ)
190188, 189sseldi 3634 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑀 ∈ ℂ)
191186, 156eqeltrrd 2731 . . . . . . . . . . 11 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ ℂ)
192190, 191npcand 10434 . . . . . . . . . 10 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → ((𝑀𝑏) + 𝑏) = 𝑀)
193187, 192eqtrd 2685 . . . . . . . . 9 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒𝑎) + (𝑒𝑆)) = 𝑀)
194136, 157, 1933eqtrd 2689 . . . . . . . 8 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀)
195134, 194jca 553 . . . . . . 7 ((((𝜑𝑏𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))) ∧ 𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
196195r19.29ffa 29448 . . . . . 6 ((𝜑 ∧ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})) → (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
197108, 196impbida 895 . . . . 5 (𝜑 → ((𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ↔ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩})))
198 reprsuc.f . . . . . . 7 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏)) ↦ (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
199 vex 3234 . . . . . . . 8 𝑐 ∈ V
200 snex 4938 . . . . . . . 8 {⟨𝑆, 𝑏⟩} ∈ V
201199, 200unex 6998 . . . . . . 7 (𝑐 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
202198, 201elrnmpti 5408 . . . . . 6 (𝑒 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
203202rexbii 3070 . . . . 5 (∃𝑏𝐴 𝑒 ∈ ran 𝐹 ↔ ∃𝑏𝐴𝑐 ∈ (𝐴(repr‘𝑆)(𝑀𝑏))𝑒 = (𝑐 ∪ {⟨𝑆, 𝑏⟩}))
204197, 203syl6bbr 278 . . . 4 (𝜑 → ((𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀) ↔ ∃𝑏𝐴 𝑒 ∈ ran 𝐹))
205 fveq1 6228 . . . . . . . 8 (𝑐 = 𝑒 → (𝑐𝑎) = (𝑒𝑎))
206205sumeq2sdv 14479 . . . . . . 7 (𝑐 = 𝑒 → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎))
207206eqeq1d 2653 . . . . . 6 (𝑐 = 𝑒 → (Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
208207cbvrabv 3230 . . . . 5 {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} = {𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀}
209208rabeq2i 3228 . . . 4 (𝑒 ∈ {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} ↔ (𝑒 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒𝑎) = 𝑀))
210 eliun 4556 . . . 4 (𝑒 𝑏𝐴 ran 𝐹 ↔ ∃𝑏𝐴 𝑒 ∈ ran 𝐹)
211204, 209, 2103bitr4g 303 . . 3 (𝜑 → (𝑒 ∈ {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} ↔ 𝑒 𝑏𝐴 ran 𝐹))
212211eqrdv 2649 . 2 (𝜑 → {𝑐 ∈ (𝐴𝑚 (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐𝑎) = 𝑀} = 𝑏𝐴 ran 𝐹)
2137, 212eqtrd 2685 1 (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = 𝑏𝐴 ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  {csn 4210  cop 4216   ciun 4552  cmpt 4762  ran crn 5144  cres 5145   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  𝑚 cmap 7899  Fincfn 7997  cc 9972  0cc0 9974  1c1 9975   + caddc 9977  cmin 10304  cn 11058  0cn0 11330  cz 11415  cuz 11725  ..^cfzo 12504  Σcsu 14460  reprcrepr 30814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-repr 30815
This theorem is referenced by:  breprexplema  30836
  Copyright terms: Public domain W3C validator