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

Theorem summodc 11183
 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 5428 . . . . . . . . . 10 (𝑚 = 𝑛 → (ℤ𝑚) = (ℤ𝑛))
21sseq2d 3131 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐴 ⊆ (ℤ𝑛)))
31raleqdv 2635 . . . . . . . . 9 (𝑚 = 𝑛 → (∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ↔ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴))
4 seqeq1 10251 . . . . . . . . . 10 (𝑚 = 𝑛 → seq𝑚( + , 𝐹) = seq𝑛( + , 𝐹))
54breq1d 3946 . . . . . . . . 9 (𝑚 = 𝑛 → (seq𝑚( + , 𝐹) ⇝ 𝑦 ↔ seq𝑛( + , 𝐹) ⇝ 𝑦))
62, 3, 53anbi123d 1291 . . . . . . . 8 (𝑚 = 𝑛 → ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
76cbvrexv 2658 . . . . . . 7 (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))
8 reeanv 2603 . . . . . . . . 9 (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
9 simprl3 1029 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑚( + , 𝐹) ⇝ 𝑥)
10 isummo.1 . . . . . . . . . . . . . 14 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 0))
11 simpll 519 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝜑)
12 isummo.2 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
1311, 12sylan 281 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘𝐴) → 𝐵 ∈ ℂ)
14 simplrl 525 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑚 ∈ ℤ)
15 simplrr 526 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑛 ∈ ℤ)
16 simprl1 1027 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ𝑚))
17 simprr1 1030 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ𝑛))
18 eleq1w 2201 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑘 → (𝑗𝐴𝑘𝐴))
1918dcbid 824 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (DECID 𝑗𝐴DECID 𝑘𝐴))
20 simprl2 1028 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)
2120adantr 274 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑚)) → ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)
22 simpr 109 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑚)) → 𝑘 ∈ (ℤ𝑚))
2319, 21, 22rspcdva 2797 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑚)) → DECID 𝑘𝐴)
24 simprr2 1031 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴)
2524adantr 274 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑛)) → ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴)
26 simpr 109 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘 ∈ (ℤ𝑛))
2719, 25, 26rspcdva 2797 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ𝑛)) → DECID 𝑘𝐴)
2810, 13, 14, 15, 16, 17, 23, 27sumrbdc 11179 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑛( + , 𝐹) ⇝ 𝑥))
299, 28mpbid 146 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑥)
30 simprr3 1032 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑦)
31 climuni 11093 . . . . . . . . . . . 12 ((seq𝑛( + , 𝐹) ⇝ 𝑥 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦)
3229, 30, 31syl2anc 409 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑥 = 𝑦)
3332exp31 362 . . . . . . . . . 10 (𝜑 → ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦)))
3433rexlimdvv 2559 . . . . . . . . 9 (𝜑 → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
358, 34syl5bir 152 . . . . . . . 8 (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
3635expdimp 257 . . . . . . 7 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ𝑛) ∧ ∀𝑗 ∈ (ℤ𝑛)DECID 𝑗𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
377, 36syl5bi 151 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
38 summodc.3 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0))
3910, 12, 38summodclem2 11182 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
4037, 39jaod 707 . . . . 5 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
4110, 12, 38summodclem2 11182 . . . . . . . 8 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑦 = 𝑥))
42 equcom 1683 . . . . . . . 8 (𝑦 = 𝑥𝑥 = 𝑦)
4341, 42syl6ib 160 . . . . . . 7 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
4443impancom 258 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
45 oveq2 5789 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
46 f1oeq2 5364 . . . . . . . . . . . 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 5428 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘𝑛))
4948eqeq2d 2152 . . . . . . . . . . 11 (𝑚 = 𝑛 → (𝑦 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑛)))
5047, 49anbi12d 465 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛))))
5150exbidv 1798 . . . . . . . . 9 (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛))))
52 f1oeq1 5363 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑓:(1...𝑛)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴))
53 breq1 3939 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑎 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑎 ≤ (♯‘𝐴)))
54 fveq2 5428 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑎 → (𝑓𝑛) = (𝑓𝑎))
5554csbeq1d 3013 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑎(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑎) / 𝑘𝐵)
5653, 55ifbieq1d 3498 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑎 → if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0) = if(𝑎 ≤ (♯‘𝐴), (𝑓𝑎) / 𝑘𝐵, 0))
5756cbvmptv 4031 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑓𝑎) / 𝑘𝐵, 0))
58 fveq1 5427 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑔 → (𝑓𝑎) = (𝑔𝑎))
5958csbeq1d 3013 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑔(𝑓𝑎) / 𝑘𝐵 = (𝑔𝑎) / 𝑘𝐵)
6059ifeq1d 3493 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → if(𝑎 ≤ (♯‘𝐴), (𝑓𝑎) / 𝑘𝐵, 0) = if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0))
6160mpteq2dv 4026 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑓𝑎) / 𝑘𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))
6257, 61syl5eq 2185 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))
6338, 62syl5eq 2185 . . . . . . . . . . . . . 14 (𝑓 = 𝑔𝐺 = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))
6463seqeq3d 10256 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → seq1( + , 𝐺) = seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0))))
6564fveq1d 5430 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (seq1( + , 𝐺)‘𝑛) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))
6665eqeq2d 2152 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑦 = (seq1( + , 𝐺)‘𝑛) ↔ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)))
6752, 66anbi12d 465 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))))
6867cbvexv 1891 . . . . . . . . 9 (∃𝑓(𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)))
6951, 68syl6bb 195 . . . . . . . 8 (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))))
7069cbvrexv 2658 . . . . . . 7 (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)))
71 reeanv 2603 . . . . . . . . 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 1905 . . . . . . . . . . 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 576 . . . . . . . . . . . . 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 9104 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 1 ∈ ℤ)
75 simplrr 526 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑛 ∈ ℕ)
7675nnzd 9195 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑛 ∈ ℤ)
7774, 76fzfigd 10234 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (1...𝑛) ∈ Fin)
78 simprr 522 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑔:(1...𝑛)–1-1-onto𝐴)
7977, 78fihasheqf1od 10567 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘(1...𝑛)) = (♯‘𝐴))
8075nnnn0d 9053 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑛 ∈ ℕ0)
81 hashfz1 10560 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ0 → (♯‘(1...𝑛)) = 𝑛)
8280, 81syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘(1...𝑛)) = 𝑛)
8379, 82eqtr3d 2175 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘𝐴) = 𝑛)
8483breq2d 3948 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (𝑎 ≤ (♯‘𝐴) ↔ 𝑎𝑛))
8584ifbid 3497 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0) = if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0))
8685mpteq2dv 4026 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))
8786seqeq3d 10256 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0))) = seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0))))
8887fveq1d 5430 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))
8988eqeq2d 2152 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛) ↔ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)))
9089anbi2d 460 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)) ↔ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))))
91 simplrl 525 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑚 ∈ ℕ)
9291nnnn0d 9053 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑚 ∈ ℕ0)
93 hashfz1 10560 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ0 → (♯‘(1...𝑚)) = 𝑚)
9492, 93syl 14 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘(1...𝑚)) = 𝑚)
9591nnzd 9195 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑚 ∈ ℤ)
9674, 95fzfigd 10234 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (1...𝑚) ∈ Fin)
97 simprl 521 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑓:(1...𝑚)–1-1-onto𝐴)
9896, 97fihasheqf1od 10567 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘(1...𝑚)) = (♯‘𝐴))
9994, 98eqtr3d 2175 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑚 = (♯‘𝐴))
10099fveq2d 5432 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘(♯‘𝐴)))
101 simpll 519 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝜑)
102101, 12sylan 281 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) ∧ 𝑘𝐴) → 𝐵 ∈ ℂ)
10399, 91eqeltrrd 2218 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (♯‘𝐴) ∈ ℕ)
104103, 75jca 304 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → ((♯‘𝐴) ∈ ℕ ∧ 𝑛 ∈ ℕ))
10599oveq2d 5797 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (1...𝑚) = (1...(♯‘𝐴)))
106 f1oeq2 5364 . . . . . . . . . . . . . . . . . . . 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 146 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)
109 breq1 3939 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
110 fveq2 5428 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑗 → (𝑓𝑛) = (𝑓𝑗))
111110csbeq1d 3013 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑗(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑗) / 𝑘𝐵)
112109, 111ifbieq1d 3498 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0) = if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 0))
113112cbvmptv 4031 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (𝑓𝑛) / 𝑘𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 0))
11438, 113eqtri 2161 . . . . . . . . . . . . . . . . . 18 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (𝑓𝑗) / 𝑘𝐵, 0))
115 breq1 3939 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑗 → (𝑎𝑛𝑗𝑛))
116 fveq2 5428 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑗 → (𝑔𝑎) = (𝑔𝑗))
117116csbeq1d 3013 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑗(𝑔𝑎) / 𝑘𝐵 = (𝑔𝑗) / 𝑘𝐵)
118115, 117ifbieq1d 3498 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑗 → if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0) = if(𝑗𝑛, (𝑔𝑗) / 𝑘𝐵, 0))
119118cbvmptv 4031 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗𝑛, (𝑔𝑗) / 𝑘𝐵, 0))
12010, 102, 104, 108, 78, 114, 119summodclem3 11180 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))
121100, 120eqtrd 2173 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))
122 eqeq12 2153 . . . . . . . . . . . . . . . 16 ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)) → (𝑥 = 𝑦 ↔ (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)))
123121, 122syl5ibrcom 156 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎𝑛, (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)) → 𝑥 = 𝑦))
12490, 123sylbid 149 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)) → 𝑥 = 𝑦))
125124expimpd 361 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴) ∧ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
12673, 125syl5bi 151 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
127126exlimdvv 1870 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (∃𝑓𝑔((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
12872, 127syl5bir 152 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
129128rexlimdvva 2560 . . . . . . . . 9 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
13071, 129syl5bir 152 . . . . . . . 8 (𝜑 → ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
131130expdimp 257 . . . . . . 7 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), (𝑔𝑎) / 𝑘𝐵, 0)))‘𝑛)) → 𝑥 = 𝑦))
13270, 131syl5bi 151 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
13344, 132jaod 707 . . . . 5 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
13440, 133jaodan 787 . . . 4 ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
135134expimpd 361 . . 3 (𝜑 → (((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
136135alrimivv 1848 . 2 (𝜑 → ∀𝑥𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
137 breq2 3940 . . . . . 6 (𝑥 = 𝑦 → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑚( + , 𝐹) ⇝ 𝑦))
1381373anbi3d 1297 . . . . 5 (𝑥 = 𝑦 → ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
139138rexbidv 2439 . . . 4 (𝑥 = 𝑦 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
140 eqeq1 2147 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑚)))
141140anbi2d 460 . . . . . 6 (𝑥 = 𝑦 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))))
142141exbidv 1798 . . . . 5 (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))))
143142rexbidv 2439 . . . 4 (𝑥 = 𝑦 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))))
144139, 143orbi12d 783 . . 3 (𝑥 = 𝑦 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))))
145144mo4 2061 . 2 (∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ ∀𝑥𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
146136, 145sylibr 133 1 (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820   ∧ w3a 963  ∀wal 1330   = wceq 1332  ∃wex 1469   ∈ wcel 1481  ∃*wmo 2001  ∀wral 2417  ∃wrex 2418  ⦋csb 3006   ⊆ wss 3075  ifcif 3478   class class class wbr 3936   ↦ cmpt 3996  –1-1-onto→wf1o 5129  ‘cfv 5130  (class class class)co 5781  ℂcc 7641  0cc0 7643  1c1 7644   + caddc 7646   ≤ cle 7824  ℕcn 8743  ℕ0cn0 9000  ℤcz 9077  ℤ≥cuz 9349  ...cfz 9820  seqcseq 10248  ♯chash 10552   ⇝ cli 11078 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4050  ax-sep 4053  ax-nul 4061  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-iinf 4509  ax-cnex 7734  ax-resscn 7735  ax-1cn 7736  ax-1re 7737  ax-icn 7738  ax-addcl 7739  ax-addrcl 7740  ax-mulcl 7741  ax-mulrcl 7742  ax-addcom 7743  ax-mulcom 7744  ax-addass 7745  ax-mulass 7746  ax-distr 7747  ax-i2m1 7748  ax-0lt1 7749  ax-1rid 7750  ax-0id 7751  ax-rnegex 7752  ax-precex 7753  ax-cnre 7754  ax-pre-ltirr 7755  ax-pre-ltwlin 7756  ax-pre-lttrn 7757  ax-pre-apti 7758  ax-pre-ltadd 7759  ax-pre-mulgt0 7760  ax-pre-mulext 7761  ax-arch 7762  ax-caucvg 7763 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-nul 3368  df-if 3479  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-int 3779  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-tr 4034  df-id 4222  df-po 4225  df-iso 4226  df-iord 4295  df-on 4297  df-ilim 4298  df-suc 4300  df-iom 4512  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-isom 5139  df-riota 5737  df-ov 5784  df-oprab 5785  df-mpo 5786  df-1st 6045  df-2nd 6046  df-recs 6209  df-irdg 6274  df-frec 6295  df-1o 6320  df-oadd 6324  df-er 6436  df-en 6642  df-dom 6643  df-fin 6644  df-pnf 7825  df-mnf 7826  df-xr 7827  df-ltxr 7828  df-le 7829  df-sub 7958  df-neg 7959  df-reap 8360  df-ap 8367  df-div 8456  df-inn 8744  df-2 8802  df-3 8803  df-4 8804  df-n0 9001  df-z 9078  df-uz 9350  df-q 9438  df-rp 9470  df-fz 9821  df-fzo 9950  df-seqfrec 10249  df-exp 10323  df-ihash 10553  df-cj 10645  df-re 10646  df-im 10647  df-rsqrt 10801  df-abs 10802  df-clim 11079 This theorem is referenced by:  fsum3  11187
 Copyright terms: Public domain W3C validator