ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  summodc GIF version

Theorem summodc 11405
Description: A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)
Hypotheses
Ref Expression
isummo.1 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 0))
isummo.2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
summodclem2.g 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0))
summodc.3 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0))
Assertion
Ref Expression
summodc (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑛,𝐹   𝜑,𝑘,𝑛   𝐴,𝑓,𝑗,𝑚,𝑘,𝑛   𝐵,𝑛   𝑓,𝐹,𝑘,𝑚   𝜑,𝑓,𝑚,𝑥,𝑘,𝑛   𝑥,𝐴,𝑗   𝐵,𝑓,𝑗,𝑚   𝑗,𝐹,𝑥   𝑛,𝐺,𝑥   𝜑,𝑗,𝑥
Allowed substitution hints:   𝐵(𝑥,𝑘)   𝐺(𝑓,𝑗,𝑘,𝑚)

Proof of Theorem summodc
Dummy variables 𝑎 𝑔 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5527 . . . . . . . . . 10 (𝑚 = 𝑛 → (ℤ𝑚) = (ℤ𝑛))
21sseq2d 3197 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐴 ⊆ (ℤ𝑛)))
31raleqdv 2689 . . . . . . . . 9 (𝑚 = 𝑛 → (∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ↔ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴))
4 seqeq1 10462 . . . . . . . . . 10 (𝑚 = 𝑛 → seq𝑚( + , 𝐹) = seq𝑛( + , 𝐹))
54breq1d 4025 . . . . . . . . 9 (𝑚 = 𝑛 → (seq𝑚( + , 𝐹) ⇝ 𝑦 ↔ seq𝑛( + , 𝐹) ⇝ 𝑦))
62, 3, 53anbi123d 1322 . . . . . . . 8 (𝑚 = 𝑛 → ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
76cbvrexv 2716 . . . . . . 7 (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))
8 reeanv 2657 . . . . . . . . 9 (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
9 simprl3 1045 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑚( + , 𝐹) ⇝ 𝑥)
10 isummo.1 . . . . . . . . . . . . . 14 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 0))
11 simpll 527 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝜑)
12 isummo.2 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
1311, 12sylan 283 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘𝐴) → 𝐵 ∈ ℂ)
14 simplrl 535 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑚 ∈ ℤ)
15 simplrr 536 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑛 ∈ ℤ)
16 simprl1 1043 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ𝑚))
17 simprr1 1046 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ𝑛))
18 eleq1w 2248 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑘 → (𝑗𝐴𝑘𝐴))
1918dcbid 839 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (DECID 𝑗𝐴DECID 𝑘𝐴))
20 simprl2 1044 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)
2120adantr 276 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑚)) → ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)
22 simpr 110 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑚)) → 𝑘 ∈ (ℤ𝑚))
2319, 21, 22rspcdva 2858 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑚)) → DECID 𝑘𝐴)
24 simprr2 1047 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴)
2524adantr 276 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑛)) → ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴)
26 simpr 110 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘 ∈ (ℤ𝑛))
2719, 25, 26rspcdva 2858 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑛)) → DECID 𝑘𝐴)
2810, 13, 14, 15, 16, 17, 23, 27sumrbdc 11401 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑛( + , 𝐹) ⇝ 𝑥))
299, 28mpbid 147 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑥)
30 simprr3 1048 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑦)
31 climuni 11315 . . . . . . . . . . . 12 ((seq𝑛( + , 𝐹) ⇝ 𝑥 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦)
3229, 30, 31syl2anc 411 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑥 = 𝑦)
3332exp31 364 . . . . . . . . . 10 (𝜑 → ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦)))
3433rexlimdvv 2611 . . . . . . . . 9 (𝜑 → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
358, 34biimtrrid 153 . . . . . . . 8 (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
3635expdimp 259 . . . . . . 7 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
377, 36biimtrid 152 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
38 summodc.3 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0))
3910, 12, 38summodclem2 11404 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
4037, 39jaod 718 . . . . 5 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
4110, 12, 38summodclem2 11404 . . . . . . . 8 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑦 = 𝑥))
42 equcom 1716 . . . . . . . 8 (𝑦 = 𝑥𝑥 = 𝑦)
4341, 42imbitrdi 161 . . . . . . 7 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
4443impancom 260 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
45 oveq2 5896 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
46 f1oeq2 5462 . . . . . . . . . . . 12 ((1...𝑚) = (1...𝑛) → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑛)–1-1-onto𝐴))
4745, 46syl 14 . . . . . . . . . . 11 (𝑚 = 𝑛 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑛)–1-1-onto𝐴))
48 fveq2 5527 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘𝑛))
4948eqeq2d 2199 . . . . . . . . . . 11 (𝑚 = 𝑛 → (𝑦 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑛)))
5047, 49anbi12d 473 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛))))
5150exbidv 1835 . . . . . . . . 9 (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛))))
52 f1oeq1 5461 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑓:(1...𝑛)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴))
53 breq1 4018 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑎 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑎 ≤ (♯‘𝐴)))
54 fveq2 5527 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑎 → (𝑓𝑛) = (𝑓𝑎))
5554csbeq1d 3076 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑎(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑎) / 𝑘𝐵)
5653, 55ifbieq1d 3568 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑎 → if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0) = if(𝑎 ≤ (♯‘𝐴), (𝑓𝑎) / 𝑘𝐵, 0))
5756cbvmptv 4111 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑓𝑎) / 𝑘𝐵, 0))
58 fveq1 5526 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑔 → (𝑓𝑎) = (𝑔𝑎))
5958csbeq1d 3076 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑔(𝑓𝑎) / 𝑘𝐵 = (𝑔𝑎) / 𝑘𝐵)
6059ifeq1d 3563 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → if(𝑎 ≤ (♯‘𝐴), (𝑓𝑎) / 𝑘𝐵, 0) = if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0))
6160mpteq2dv 4106 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑓𝑎) / 𝑘𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))
6257, 61eqtrid 2232 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))
6338, 62eqtrid 2232 . . . . . . . . . . . . . 14 (𝑓 = 𝑔𝐺 = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))
6463seqeq3d 10467 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → seq1( + , 𝐺) = seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0))))
6564fveq1d 5529 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (seq1( + , 𝐺)‘𝑛) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))
6665eqeq2d 2199 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑦 = (seq1( + , 𝐺)‘𝑛) ↔ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)))
6752, 66anbi12d 473 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))))
6867cbvexv 1928 . . . . . . . . 9 (∃𝑓(𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)))
6951, 68bitrdi 196 . . . . . . . 8 (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))))
7069cbvrexv 2716 . . . . . . 7 (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)))
71 reeanv 2657 . . . . . . . . 9 (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) ↔ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))))
72 eeanv 1942 . . . . . . . . . . 11 (∃𝑓𝑔((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) ↔ (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))))
73 an4 586 . . . . . . . . . . . . 13 (((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) ↔ ((𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴) ∧ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))))
74 1zzd 9294 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 1 ∈ ℤ)
75 simplrr 536 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑛 ∈ ℕ)
7675nnzd 9388 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑛 ∈ ℤ)
7774, 76fzfigd 10445 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (1...𝑛) ∈ Fin)
78 simprr 531 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑔:(1...𝑛)–1-1-onto𝐴)
7977, 78fihasheqf1od 10783 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘(1...𝑛)) = (♯‘𝐴))
8075nnnn0d 9243 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑛 ∈ ℕ0)
81 hashfz1 10777 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ0 → (♯‘(1...𝑛)) = 𝑛)
8280, 81syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘(1...𝑛)) = 𝑛)
8379, 82eqtr3d 2222 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘𝐴) = 𝑛)
8483breq2d 4027 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (𝑎 ≤ (♯‘𝐴) ↔ 𝑎𝑛))
8584ifbid 3567 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0) = if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0))
8685mpteq2dv 4106 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))
8786seqeq3d 10467 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0))) = seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0))))
8887fveq1d 5529 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))
8988eqeq2d 2199 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛) ↔ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)))
9089anbi2d 464 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)) ↔ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))))
91 simplrl 535 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑚 ∈ ℕ)
9291nnnn0d 9243 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑚 ∈ ℕ0)
93 hashfz1 10777 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ0 → (♯‘(1...𝑚)) = 𝑚)
9492, 93syl 14 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘(1...𝑚)) = 𝑚)
9591nnzd 9388 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑚 ∈ ℤ)
9674, 95fzfigd 10445 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (1...𝑚) ∈ Fin)
97 simprl 529 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑓:(1...𝑚)–1-1-onto𝐴)
9896, 97fihasheqf1od 10783 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘(1...𝑚)) = (♯‘𝐴))
9994, 98eqtr3d 2222 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑚 = (♯‘𝐴))
10099fveq2d 5531 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘(♯‘𝐴)))
101 simpll 527 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝜑)
102101, 12sylan 283 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) ∧ 𝑘𝐴) → 𝐵 ∈ ℂ)
10399, 91eqeltrrd 2265 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘𝐴) ∈ ℕ)
104103, 75jca 306 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → ((♯‘𝐴) ∈ ℕ ∧ 𝑛 ∈ ℕ))
10599oveq2d 5904 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (1...𝑚) = (1...(♯‘𝐴)))
106 f1oeq2 5462 . . . . . . . . . . . . . . . . . . . 20 ((1...𝑚) = (1...(♯‘𝐴)) → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...(♯‘𝐴))–1-1-onto𝐴))
107105, 106syl 14 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...(♯‘𝐴))–1-1-onto𝐴))
10897, 107mpbid 147 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)
109 breq1 4018 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
110 fveq2 5527 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑗 → (𝑓𝑛) = (𝑓𝑗))
111110csbeq1d 3076 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑗(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑗) / 𝑘𝐵)
112109, 111ifbieq1d 3568 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0) = if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 0))
113112cbvmptv 4111 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 0))
11438, 113eqtri 2208 . . . . . . . . . . . . . . . . . 18 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 0))
115 breq1 4018 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑗 → (𝑎𝑛𝑗𝑛))
116 fveq2 5527 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑗 → (𝑔𝑎) = (𝑔𝑗))
117116csbeq1d 3076 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑗(𝑔𝑎) / 𝑘𝐵 = (𝑔𝑗) / 𝑘𝐵)
118115, 117ifbieq1d 3568 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑗 → if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0) = if(𝑗𝑛, (𝑔𝑗) / 𝑘𝐵, 0))
119118cbvmptv 4111 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗𝑛, (𝑔𝑗) / 𝑘𝐵, 0))
12010, 102, 104, 108, 78, 114, 119summodclem3 11402 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))
121100, 120eqtrd 2220 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))
122 eqeq12 2200 . . . . . . . . . . . . . . . 16 ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)) → (𝑥 = 𝑦 ↔ (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)))
123121, 122syl5ibrcom 157 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)) → 𝑥 = 𝑦))
12490, 123sylbid 150 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)) → 𝑥 = 𝑦))
125124expimpd 363 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴) ∧ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
12673, 125biimtrid 152 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
127126exlimdvv 1907 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (∃𝑓𝑔((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
12872, 127biimtrrid 153 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
129128rexlimdvva 2612 . . . . . . . . 9 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
13071, 129biimtrrid 153 . . . . . . . 8 (𝜑 → ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
131130expdimp 259 . . . . . . 7 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)) → 𝑥 = 𝑦))
13270, 131biimtrid 152 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
13344, 132jaod 718 . . . . 5 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
13440, 133jaodan 798 . . . 4 ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
135134expimpd 363 . . 3 (𝜑 → (((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
136135alrimivv 1885 . 2 (𝜑 → ∀𝑥𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
137 breq2 4019 . . . . . 6 (𝑥 = 𝑦 → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑚( + , 𝐹) ⇝ 𝑦))
1381373anbi3d 1328 . . . . 5 (𝑥 = 𝑦 → ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
139138rexbidv 2488 . . . 4 (𝑥 = 𝑦 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
140 eqeq1 2194 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑚)))
141140anbi2d 464 . . . . . 6 (𝑥 = 𝑦 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))))
142141exbidv 1835 . . . . 5 (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))))
143142rexbidv 2488 . . . 4 (𝑥 = 𝑦 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))))
144139, 143orbi12d 794 . . 3 (𝑥 = 𝑦 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))))
145144mo4 2097 . 2 (∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ ∀𝑥𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
146136, 145sylibr 134 1 (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wo 709  DECID wdc 835  w3a 979  wal 1361   = wceq 1363  wex 1502  ∃*wmo 2037  wcel 2158  wral 2465  wrex 2466  csb 3069  wss 3141  ifcif 3546   class class class wbr 4015  cmpt 4076  1-1-ontowf1o 5227  cfv 5228  (class class class)co 5888  cc 7823  0cc0 7825  1c1 7826   + caddc 7828  cle 8007  cn 8933  0cn0 9190  cz 9267  cuz 9542  ...cfz 10022  seqcseq 10459  chash 10769  cli 11300
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7916  ax-resscn 7917  ax-1cn 7918  ax-1re 7919  ax-icn 7920  ax-addcl 7921  ax-addrcl 7922  ax-mulcl 7923  ax-mulrcl 7924  ax-addcom 7925  ax-mulcom 7926  ax-addass 7927  ax-mulass 7928  ax-distr 7929  ax-i2m1 7930  ax-0lt1 7931  ax-1rid 7932  ax-0id 7933  ax-rnegex 7934  ax-precex 7935  ax-cnre 7936  ax-pre-ltirr 7937  ax-pre-ltwlin 7938  ax-pre-lttrn 7939  ax-pre-apti 7940  ax-pre-ltadd 7941  ax-pre-mulgt0 7942  ax-pre-mulext 7943  ax-arch 7944  ax-caucvg 7945
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6155  df-2nd 6156  df-recs 6320  df-irdg 6385  df-frec 6406  df-1o 6431  df-oadd 6435  df-er 6549  df-en 6755  df-dom 6756  df-fin 6757  df-pnf 8008  df-mnf 8009  df-xr 8010  df-ltxr 8011  df-le 8012  df-sub 8144  df-neg 8145  df-reap 8546  df-ap 8553  df-div 8644  df-inn 8934  df-2 8992  df-3 8993  df-4 8994  df-n0 9191  df-z 9268  df-uz 9543  df-q 9634  df-rp 9668  df-fz 10023  df-fzo 10157  df-seqfrec 10460  df-exp 10534  df-ihash 10770  df-cj 10865  df-re 10866  df-im 10867  df-rsqrt 11021  df-abs 11022  df-clim 11301
This theorem is referenced by:  fsum3  11409
  Copyright terms: Public domain W3C validator