Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fmuldfeq Structured version   Visualization version   GIF version

Theorem fmuldfeq 43814
Description: X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
fmuldfeq.1 𝑖𝜑
fmuldfeq.2 𝑡𝑌
fmuldfeq.3 𝑃 = (𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
fmuldfeq.4 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
fmuldfeq.5 𝐹 = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
fmuldfeq.6 𝑍 = (𝑡𝑇 ↦ (seq1( · , (𝐹𝑡))‘𝑀))
fmuldfeq.7 (𝜑𝑇 ∈ V)
fmuldfeq.8 (𝜑𝑀 ∈ ℕ)
fmuldfeq.9 (𝜑𝑈:(1...𝑀)⟶𝑌)
fmuldfeq.10 ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ)
fmuldfeq.11 ((𝜑𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
Assertion
Ref Expression
fmuldfeq ((𝜑𝑡𝑇) → (𝑋𝑡) = (𝑍𝑡))
Distinct variable groups:   𝑡,𝑇   𝑓,𝑔,𝑡,𝑇   𝑓,𝑖,𝑡,𝑇   𝑓,𝐹,𝑔   𝑓,𝑀,𝑔   𝑈,𝑓,𝑔,𝑡   𝑓,𝑌,𝑔   𝜑,𝑓,𝑔   𝑖,𝑀   𝑈,𝑖
Allowed substitution hints:   𝜑(𝑡,𝑖)   𝑃(𝑡,𝑓,𝑔,𝑖)   𝐹(𝑡,𝑖)   𝑀(𝑡)   𝑋(𝑡,𝑓,𝑔,𝑖)   𝑌(𝑡,𝑖)   𝑍(𝑡,𝑓,𝑔,𝑖)

Proof of Theorem fmuldfeq
Dummy variables 𝑘 𝑏 𝑛 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1zzd 12534 . . . 4 ((𝜑𝑡𝑇) → 1 ∈ ℤ)
2 fmuldfeq.8 . . . . . 6 (𝜑𝑀 ∈ ℕ)
32nnzd 12526 . . . . 5 (𝜑𝑀 ∈ ℤ)
43adantr 481 . . . 4 ((𝜑𝑡𝑇) → 𝑀 ∈ ℤ)
52nnge1d 12201 . . . . 5 (𝜑 → 1 ≤ 𝑀)
65adantr 481 . . . 4 ((𝜑𝑡𝑇) → 1 ≤ 𝑀)
7 nnre 12160 . . . . . 6 (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8 leid 11251 . . . . . 6 (𝑀 ∈ ℝ → 𝑀𝑀)
92, 7, 83syl 18 . . . . 5 (𝜑𝑀𝑀)
109adantr 481 . . . 4 ((𝜑𝑡𝑇) → 𝑀𝑀)
111, 4, 4, 6, 10elfzd 13432 . . 3 ((𝜑𝑡𝑇) → 𝑀 ∈ (1...𝑀))
1223ad2ant1 1133 . . . 4 ((𝜑𝑡𝑇𝑀 ∈ (1...𝑀)) → 𝑀 ∈ ℕ)
13 eleq1 2825 . . . . . . 7 (𝑚 = 1 → (𝑚 ∈ (1...𝑀) ↔ 1 ∈ (1...𝑀)))
14133anbi3d 1442 . . . . . 6 (𝑚 = 1 → ((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) ↔ (𝜑𝑡𝑇 ∧ 1 ∈ (1...𝑀))))
15 fveq2 6842 . . . . . . . 8 (𝑚 = 1 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘1))
1615fveq1d 6844 . . . . . . 7 (𝑚 = 1 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
17 fveq2 6842 . . . . . . 7 (𝑚 = 1 → (seq1( · , (𝐹𝑡))‘𝑚) = (seq1( · , (𝐹𝑡))‘1))
1816, 17eqeq12d 2752 . . . . . 6 (𝑚 = 1 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹𝑡))‘1)))
1914, 18imbi12d 344 . . . . 5 (𝑚 = 1 → (((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚)) ↔ ((𝜑𝑡𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹𝑡))‘1))))
20 eleq1 2825 . . . . . . 7 (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑀) ↔ 𝑛 ∈ (1...𝑀)))
21203anbi3d 1442 . . . . . 6 (𝑚 = 𝑛 → ((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) ↔ (𝜑𝑡𝑇𝑛 ∈ (1...𝑀))))
22 fveq2 6842 . . . . . . . 8 (𝑚 = 𝑛 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑛))
2322fveq1d 6844 . . . . . . 7 (𝑚 = 𝑛 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡))
24 fveq2 6842 . . . . . . 7 (𝑚 = 𝑛 → (seq1( · , (𝐹𝑡))‘𝑚) = (seq1( · , (𝐹𝑡))‘𝑛))
2523, 24eqeq12d 2752 . . . . . 6 (𝑚 = 𝑛 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)))
2621, 25imbi12d 344 . . . . 5 (𝑚 = 𝑛 → (((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚)) ↔ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))))
27 eleq1 2825 . . . . . . 7 (𝑚 = (𝑛 + 1) → (𝑚 ∈ (1...𝑀) ↔ (𝑛 + 1) ∈ (1...𝑀)))
28273anbi3d 1442 . . . . . 6 (𝑚 = (𝑛 + 1) → ((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) ↔ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))))
29 fveq2 6842 . . . . . . . 8 (𝑚 = (𝑛 + 1) → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘(𝑛 + 1)))
3029fveq1d 6844 . . . . . . 7 (𝑚 = (𝑛 + 1) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡))
31 fveq2 6842 . . . . . . 7 (𝑚 = (𝑛 + 1) → (seq1( · , (𝐹𝑡))‘𝑚) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1)))
3230, 31eqeq12d 2752 . . . . . 6 (𝑚 = (𝑛 + 1) → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1))))
3328, 32imbi12d 344 . . . . 5 (𝑚 = (𝑛 + 1) → (((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚)) ↔ ((𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1)))))
34 eleq1 2825 . . . . . . 7 (𝑚 = 𝑀 → (𝑚 ∈ (1...𝑀) ↔ 𝑀 ∈ (1...𝑀)))
35343anbi3d 1442 . . . . . 6 (𝑚 = 𝑀 → ((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) ↔ (𝜑𝑡𝑇𝑀 ∈ (1...𝑀))))
36 fveq2 6842 . . . . . . . 8 (𝑚 = 𝑀 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑀))
3736fveq1d 6844 . . . . . . 7 (𝑚 = 𝑀 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
38 fveq2 6842 . . . . . . 7 (𝑚 = 𝑀 → (seq1( · , (𝐹𝑡))‘𝑚) = (seq1( · , (𝐹𝑡))‘𝑀))
3937, 38eqeq12d 2752 . . . . . 6 (𝑚 = 𝑀 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑀)))
4035, 39imbi12d 344 . . . . 5 (𝑚 = 𝑀 → (((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚)) ↔ ((𝜑𝑡𝑇𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))))
41 1z 12533 . . . . . . . 8 1 ∈ ℤ
42 seq1 13919 . . . . . . . 8 (1 ∈ ℤ → (seq1( · , (𝐹𝑡))‘1) = ((𝐹𝑡)‘1))
4341, 42ax-mp 5 . . . . . . 7 (seq1( · , (𝐹𝑡))‘1) = ((𝐹𝑡)‘1)
44 1zzd 12534 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℤ)
45 1le1 11783 . . . . . . . . . . . . 13 1 ≤ 1
4645a1i 11 . . . . . . . . . . . 12 (𝜑 → 1 ≤ 1)
4744, 3, 44, 46, 5elfzd 13432 . . . . . . . . . . 11 (𝜑 → 1 ∈ (1...𝑀))
48 nfv 1917 . . . . . . . . . . . . 13 𝑖 𝑡𝑇
49 fmuldfeq.5 . . . . . . . . . . . . . . . . 17 𝐹 = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
50 nfcv 2907 . . . . . . . . . . . . . . . . . 18 𝑖𝑇
51 nfmpt1 5213 . . . . . . . . . . . . . . . . . 18 𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
5250, 51nfmpt 5212 . . . . . . . . . . . . . . . . 17 𝑖(𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
5349, 52nfcxfr 2905 . . . . . . . . . . . . . . . 16 𝑖𝐹
54 nfcv 2907 . . . . . . . . . . . . . . . 16 𝑖𝑡
5553, 54nffv 6852 . . . . . . . . . . . . . . 15 𝑖(𝐹𝑡)
56 nfcv 2907 . . . . . . . . . . . . . . 15 𝑖1
5755, 56nffv 6852 . . . . . . . . . . . . . 14 𝑖((𝐹𝑡)‘1)
58 nffvmpt1 6853 . . . . . . . . . . . . . 14 𝑖((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1)
5957, 58nfeq 2920 . . . . . . . . . . . . 13 𝑖((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1)
6048, 59nfim 1899 . . . . . . . . . . . 12 𝑖(𝑡𝑇 → ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1))
61 fveq2 6842 . . . . . . . . . . . . . 14 (𝑖 = 1 → ((𝐹𝑡)‘𝑖) = ((𝐹𝑡)‘1))
62 fveq2 6842 . . . . . . . . . . . . . 14 (𝑖 = 1 → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1))
6361, 62eqeq12d 2752 . . . . . . . . . . . . 13 (𝑖 = 1 → (((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) ↔ ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1)))
6463imbi2d 340 . . . . . . . . . . . 12 (𝑖 = 1 → ((𝑡𝑇 → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖)) ↔ (𝑡𝑇 → ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1))))
65 ovex 7390 . . . . . . . . . . . . . . 15 (1...𝑀) ∈ V
6665mptex 7173 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V
6749fvmpt2 6959 . . . . . . . . . . . . . 14 ((𝑡𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
6866, 67mpan2 689 . . . . . . . . . . . . 13 (𝑡𝑇 → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
6968fveq1d 6844 . . . . . . . . . . . 12 (𝑡𝑇 → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖))
7060, 64, 69vtoclg1f 3524 . . . . . . . . . . 11 (1 ∈ (1...𝑀) → (𝑡𝑇 → ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1)))
7147, 70syl 17 . . . . . . . . . 10 (𝜑 → (𝑡𝑇 → ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1)))
7271imp 407 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1))
73 eqid 2736 . . . . . . . . . 10 (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
74 fveq2 6842 . . . . . . . . . . 11 (𝑖 = 1 → (𝑈𝑖) = (𝑈‘1))
7574fveq1d 6844 . . . . . . . . . 10 (𝑖 = 1 → ((𝑈𝑖)‘𝑡) = ((𝑈‘1)‘𝑡))
7647adantr 481 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 1 ∈ (1...𝑀))
77 fmuldfeq.9 . . . . . . . . . . . . 13 (𝜑𝑈:(1...𝑀)⟶𝑌)
7877, 47ffvelcdmd 7036 . . . . . . . . . . . 12 (𝜑 → (𝑈‘1) ∈ 𝑌)
7978ancli 549 . . . . . . . . . . . 12 (𝜑 → (𝜑 ∧ (𝑈‘1) ∈ 𝑌))
80 eleq1 2825 . . . . . . . . . . . . . . 15 (𝑓 = (𝑈‘1) → (𝑓𝑌 ↔ (𝑈‘1) ∈ 𝑌))
8180anbi2d 629 . . . . . . . . . . . . . 14 (𝑓 = (𝑈‘1) → ((𝜑𝑓𝑌) ↔ (𝜑 ∧ (𝑈‘1) ∈ 𝑌)))
82 feq1 6649 . . . . . . . . . . . . . 14 (𝑓 = (𝑈‘1) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘1):𝑇⟶ℝ))
8381, 82imbi12d 344 . . . . . . . . . . . . 13 (𝑓 = (𝑈‘1) → (((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ)))
84 fmuldfeq.10 . . . . . . . . . . . . . 14 ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ)
8584a1i 11 . . . . . . . . . . . . 13 (𝑓𝑌 → ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ))
8683, 85vtoclga 3534 . . . . . . . . . . . 12 ((𝑈‘1) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ))
8778, 79, 86sylc 65 . . . . . . . . . . 11 (𝜑 → (𝑈‘1):𝑇⟶ℝ)
8887ffvelcdmda 7035 . . . . . . . . . 10 ((𝜑𝑡𝑇) → ((𝑈‘1)‘𝑡) ∈ ℝ)
8973, 75, 76, 88fvmptd3 6971 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1) = ((𝑈‘1)‘𝑡))
9072, 89eqtrd 2776 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝐹𝑡)‘1) = ((𝑈‘1)‘𝑡))
91 seq1 13919 . . . . . . . . . 10 (1 ∈ ℤ → (seq1(𝑃, 𝑈)‘1) = (𝑈‘1))
9241, 91ax-mp 5 . . . . . . . . 9 (seq1(𝑃, 𝑈)‘1) = (𝑈‘1)
9392fveq1i 6843 . . . . . . . 8 ((seq1(𝑃, 𝑈)‘1)‘𝑡) = ((𝑈‘1)‘𝑡)
9490, 93eqtr4di 2794 . . . . . . 7 ((𝜑𝑡𝑇) → ((𝐹𝑡)‘1) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
9543, 94eqtr2id 2789 . . . . . 6 ((𝜑𝑡𝑇) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹𝑡))‘1))
96953adant3 1132 . . . . 5 ((𝜑𝑡𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹𝑡))‘1))
97 simp31 1209 . . . . . . 7 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝜑)
98 simp1 1136 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ ℕ)
99 simp33 1211 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 + 1) ∈ (1...𝑀))
10098, 99jca 512 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)))
101 elnnuz 12807 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
102101biimpi 215 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
103102anim1i 615 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)) → (𝑛 ∈ (ℤ‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)))
104 peano2fzr 13454 . . . . . . . . 9 ((𝑛 ∈ (ℤ‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)) → 𝑛 ∈ (1...𝑀))
105100, 103, 1043syl 18 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ (1...𝑀))
106 simp32 1210 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑡𝑇)
107 simp2 1137 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)))
10897, 106, 105, 107mp3and 1464 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))
109105, 99, 1083jca 1128 . . . . . . 7 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)))
110 nfv 1917 . . . . . . . . 9 𝑓𝜑
111 nfv 1917 . . . . . . . . . 10 𝑓 𝑛 ∈ (1...𝑀)
112 nfv 1917 . . . . . . . . . 10 𝑓(𝑛 + 1) ∈ (1...𝑀)
113 nfcv 2907 . . . . . . . . . . . . . 14 𝑓1
114 fmuldfeq.3 . . . . . . . . . . . . . . 15 𝑃 = (𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
115 nfmpo1 7437 . . . . . . . . . . . . . . 15 𝑓(𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
116114, 115nfcxfr 2905 . . . . . . . . . . . . . 14 𝑓𝑃
117 nfcv 2907 . . . . . . . . . . . . . 14 𝑓𝑈
118113, 116, 117nfseq 13916 . . . . . . . . . . . . 13 𝑓seq1(𝑃, 𝑈)
119 nfcv 2907 . . . . . . . . . . . . 13 𝑓𝑛
120118, 119nffv 6852 . . . . . . . . . . . 12 𝑓(seq1(𝑃, 𝑈)‘𝑛)
121 nfcv 2907 . . . . . . . . . . . 12 𝑓𝑡
122120, 121nffv 6852 . . . . . . . . . . 11 𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
123 nfcv 2907 . . . . . . . . . . 11 𝑓(seq1( · , (𝐹𝑡))‘𝑛)
124122, 123nfeq 2920 . . . . . . . . . 10 𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)
125111, 112, 124nf3an 1904 . . . . . . . . 9 𝑓(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))
126110, 125nfan 1902 . . . . . . . 8 𝑓(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)))
127 nfv 1917 . . . . . . . . 9 𝑔𝜑
128 nfv 1917 . . . . . . . . . 10 𝑔 𝑛 ∈ (1...𝑀)
129 nfv 1917 . . . . . . . . . 10 𝑔(𝑛 + 1) ∈ (1...𝑀)
130 nfcv 2907 . . . . . . . . . . . . . 14 𝑔1
131 nfmpo2 7438 . . . . . . . . . . . . . . 15 𝑔(𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
132114, 131nfcxfr 2905 . . . . . . . . . . . . . 14 𝑔𝑃
133 nfcv 2907 . . . . . . . . . . . . . 14 𝑔𝑈
134130, 132, 133nfseq 13916 . . . . . . . . . . . . 13 𝑔seq1(𝑃, 𝑈)
135 nfcv 2907 . . . . . . . . . . . . 13 𝑔𝑛
136134, 135nffv 6852 . . . . . . . . . . . 12 𝑔(seq1(𝑃, 𝑈)‘𝑛)
137 nfcv 2907 . . . . . . . . . . . 12 𝑔𝑡
138136, 137nffv 6852 . . . . . . . . . . 11 𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
139 nfcv 2907 . . . . . . . . . . 11 𝑔(seq1( · , (𝐹𝑡))‘𝑛)
140138, 139nfeq 2920 . . . . . . . . . 10 𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)
141128, 129, 140nf3an 1904 . . . . . . . . 9 𝑔(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))
142127, 141nfan 1902 . . . . . . . 8 𝑔(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)))
143 fmuldfeq.2 . . . . . . . 8 𝑡𝑌
144 fmuldfeq.7 . . . . . . . . 9 (𝜑𝑇 ∈ V)
145144adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) → 𝑇 ∈ V)
14677adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) → 𝑈:(1...𝑀)⟶𝑌)
147 fmuldfeq.11 . . . . . . . . 9 ((𝜑𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
1481473adant1r 1177 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) ∧ 𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
149 simpr1 1194 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) → 𝑛 ∈ (1...𝑀))
150 simpr2 1195 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) → (𝑛 + 1) ∈ (1...𝑀))
151 simpr3 1196 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))
15284adantlr 713 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) ∧ 𝑓𝑌) → 𝑓:𝑇⟶ℝ)
153126, 142, 143, 114, 49, 145, 146, 148, 149, 150, 151, 152fmuldfeqlem1 43813 . . . . . . 7 (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) ∧ 𝑡𝑇) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1)))
15497, 109, 106, 153syl21anc 836 . . . . . 6 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1)))
1551543exp 1119 . . . . 5 (𝑛 ∈ ℕ → (((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) → ((𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1)))))
15619, 26, 33, 40, 96, 155nnind 12171 . . . 4 (𝑀 ∈ ℕ → ((𝜑𝑡𝑇𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑀)))
15712, 156mpcom 38 . . 3 ((𝜑𝑡𝑇𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
15811, 157mpd3an3 1462 . 2 ((𝜑𝑡𝑇) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
159 fmuldfeq.4 . . . 4 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
160159fveq1i 6843 . . 3 (𝑋𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡)
161160a1i 11 . 2 ((𝜑𝑡𝑇) → (𝑋𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
162 simpr 485 . . 3 ((𝜑𝑡𝑇) → 𝑡𝑇)
163 elnnuz 12807 . . . . . 6 (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ‘1))
1642, 163sylib 217 . . . . 5 (𝜑𝑀 ∈ (ℤ‘1))
165164adantr 481 . . . 4 ((𝜑𝑡𝑇) → 𝑀 ∈ (ℤ‘1))
166 fmuldfeq.1 . . . . . . . 8 𝑖𝜑
167166, 48nfan 1902 . . . . . . 7 𝑖(𝜑𝑡𝑇)
168 nfv 1917 . . . . . . 7 𝑖 𝑘 ∈ (1...𝑀)
169167, 168nfan 1902 . . . . . 6 𝑖((𝜑𝑡𝑇) ∧ 𝑘 ∈ (1...𝑀))
170 nfcv 2907 . . . . . . . 8 𝑖𝑘
17155, 170nffv 6852 . . . . . . 7 𝑖((𝐹𝑡)‘𝑘)
172171nfel1 2923 . . . . . 6 𝑖((𝐹𝑡)‘𝑘) ∈ ℝ
173169, 172nfim 1899 . . . . 5 𝑖(((𝜑𝑡𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑘) ∈ ℝ)
174 eleq1 2825 . . . . . . 7 (𝑖 = 𝑘 → (𝑖 ∈ (1...𝑀) ↔ 𝑘 ∈ (1...𝑀)))
175174anbi2d 629 . . . . . 6 (𝑖 = 𝑘 → (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑𝑡𝑇) ∧ 𝑘 ∈ (1...𝑀))))
176 fveq2 6842 . . . . . . 7 (𝑖 = 𝑘 → ((𝐹𝑡)‘𝑖) = ((𝐹𝑡)‘𝑘))
177176eleq1d 2822 . . . . . 6 (𝑖 = 𝑘 → (((𝐹𝑡)‘𝑖) ∈ ℝ ↔ ((𝐹𝑡)‘𝑘) ∈ ℝ))
178175, 177imbi12d 344 . . . . 5 (𝑖 = 𝑘 → ((((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ∈ ℝ) ↔ (((𝜑𝑡𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑘) ∈ ℝ)))
17969ad2antlr 725 . . . . . 6 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖))
180 simpr 485 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀))
18177ffvelcdmda 7035 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝑌)
182 simpl 483 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → 𝜑)
183182, 181jca 512 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈𝑖) ∈ 𝑌))
184 eleq1 2825 . . . . . . . . . . . . . 14 (𝑓 = (𝑈𝑖) → (𝑓𝑌 ↔ (𝑈𝑖) ∈ 𝑌))
185184anbi2d 629 . . . . . . . . . . . . 13 (𝑓 = (𝑈𝑖) → ((𝜑𝑓𝑌) ↔ (𝜑 ∧ (𝑈𝑖) ∈ 𝑌)))
186 feq1 6649 . . . . . . . . . . . . 13 (𝑓 = (𝑈𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈𝑖):𝑇⟶ℝ))
187185, 186imbi12d 344 . . . . . . . . . . . 12 (𝑓 = (𝑈𝑖) → (((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈𝑖) ∈ 𝑌) → (𝑈𝑖):𝑇⟶ℝ)))
188187, 85vtoclga 3534 . . . . . . . . . . 11 ((𝑈𝑖) ∈ 𝑌 → ((𝜑 ∧ (𝑈𝑖) ∈ 𝑌) → (𝑈𝑖):𝑇⟶ℝ))
189181, 183, 188sylc 65 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
190189adantlr 713 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
191 simplr 767 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡𝑇)
192190, 191ffvelcdmd 7036 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
19373fvmpt2 6959 . . . . . . . 8 ((𝑖 ∈ (1...𝑀) ∧ ((𝑈𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑈𝑖)‘𝑡))
194180, 192, 193syl2anc 584 . . . . . . 7 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑈𝑖)‘𝑡))
195194, 192eqeltrd 2838 . . . . . 6 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) ∈ ℝ)
196179, 195eqeltrd 2838 . . . . 5 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ∈ ℝ)
197173, 178, 196chvarfv 2233 . . . 4 (((𝜑𝑡𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑘) ∈ ℝ)
198 remulcl 11136 . . . . 5 ((𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑘 · 𝑏) ∈ ℝ)
199198adantl 482 . . . 4 (((𝜑𝑡𝑇) ∧ (𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑘 · 𝑏) ∈ ℝ)
200165, 197, 199seqcl 13928 . . 3 ((𝜑𝑡𝑇) → (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ)
201 fmuldfeq.6 . . . 4 𝑍 = (𝑡𝑇 ↦ (seq1( · , (𝐹𝑡))‘𝑀))
202201fvmpt2 6959 . . 3 ((𝑡𝑇 ∧ (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
203162, 200, 202syl2anc 584 . 2 ((𝜑𝑡𝑇) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
204158, 161, 2033eqtr4d 2786 1 ((𝜑𝑡𝑇) → (𝑋𝑡) = (𝑍𝑡))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wnf 1785  wcel 2106  wnfc 2887  Vcvv 3445   class class class wbr 5105  cmpt 5188  wf 6492  cfv 6496  (class class class)co 7357  cmpo 7359  cr 11050  1c1 11052   + caddc 11054   · cmul 11056  cle 11190  cn 12153  cz 12499  cuz 12763  ...cfz 13424  seqcseq 13906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-seq 13907
This theorem is referenced by:  stoweidlem42  44273  stoweidlem48  44279
  Copyright terms: Public domain W3C validator