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 45538
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 12645 . . . 4 ((𝜑𝑡𝑇) → 1 ∈ ℤ)
2 fmuldfeq.8 . . . . . 6 (𝜑𝑀 ∈ ℕ)
32nnzd 12637 . . . . 5 (𝜑𝑀 ∈ ℤ)
43adantr 480 . . . 4 ((𝜑𝑡𝑇) → 𝑀 ∈ ℤ)
52nnge1d 12311 . . . . 5 (𝜑 → 1 ≤ 𝑀)
65adantr 480 . . . 4 ((𝜑𝑡𝑇) → 1 ≤ 𝑀)
7 nnre 12270 . . . . . 6 (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8 leid 11354 . . . . . 6 (𝑀 ∈ ℝ → 𝑀𝑀)
92, 7, 83syl 18 . . . . 5 (𝜑𝑀𝑀)
109adantr 480 . . . 4 ((𝜑𝑡𝑇) → 𝑀𝑀)
111, 4, 4, 6, 10elfzd 13551 . . 3 ((𝜑𝑡𝑇) → 𝑀 ∈ (1...𝑀))
1223ad2ant1 1132 . . . 4 ((𝜑𝑡𝑇𝑀 ∈ (1...𝑀)) → 𝑀 ∈ ℕ)
13 eleq1 2826 . . . . . . 7 (𝑚 = 1 → (𝑚 ∈ (1...𝑀) ↔ 1 ∈ (1...𝑀)))
14133anbi3d 1441 . . . . . 6 (𝑚 = 1 → ((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) ↔ (𝜑𝑡𝑇 ∧ 1 ∈ (1...𝑀))))
15 fveq2 6906 . . . . . . . 8 (𝑚 = 1 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘1))
1615fveq1d 6908 . . . . . . 7 (𝑚 = 1 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
17 fveq2 6906 . . . . . . 7 (𝑚 = 1 → (seq1( · , (𝐹𝑡))‘𝑚) = (seq1( · , (𝐹𝑡))‘1))
1816, 17eqeq12d 2750 . . . . . 6 (𝑚 = 1 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹𝑡))‘1)))
1914, 18imbi12d 344 . . . . 5 (𝑚 = 1 → (((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚)) ↔ ((𝜑𝑡𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹𝑡))‘1))))
20 eleq1 2826 . . . . . . 7 (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑀) ↔ 𝑛 ∈ (1...𝑀)))
21203anbi3d 1441 . . . . . 6 (𝑚 = 𝑛 → ((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) ↔ (𝜑𝑡𝑇𝑛 ∈ (1...𝑀))))
22 fveq2 6906 . . . . . . . 8 (𝑚 = 𝑛 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑛))
2322fveq1d 6908 . . . . . . 7 (𝑚 = 𝑛 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡))
24 fveq2 6906 . . . . . . 7 (𝑚 = 𝑛 → (seq1( · , (𝐹𝑡))‘𝑚) = (seq1( · , (𝐹𝑡))‘𝑛))
2523, 24eqeq12d 2750 . . . . . 6 (𝑚 = 𝑛 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)))
2621, 25imbi12d 344 . . . . 5 (𝑚 = 𝑛 → (((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚)) ↔ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))))
27 eleq1 2826 . . . . . . 7 (𝑚 = (𝑛 + 1) → (𝑚 ∈ (1...𝑀) ↔ (𝑛 + 1) ∈ (1...𝑀)))
28273anbi3d 1441 . . . . . 6 (𝑚 = (𝑛 + 1) → ((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) ↔ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))))
29 fveq2 6906 . . . . . . . 8 (𝑚 = (𝑛 + 1) → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘(𝑛 + 1)))
3029fveq1d 6908 . . . . . . 7 (𝑚 = (𝑛 + 1) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡))
31 fveq2 6906 . . . . . . 7 (𝑚 = (𝑛 + 1) → (seq1( · , (𝐹𝑡))‘𝑚) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1)))
3230, 31eqeq12d 2750 . . . . . 6 (𝑚 = (𝑛 + 1) → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1))))
3328, 32imbi12d 344 . . . . 5 (𝑚 = (𝑛 + 1) → (((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚)) ↔ ((𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1)))))
34 eleq1 2826 . . . . . . 7 (𝑚 = 𝑀 → (𝑚 ∈ (1...𝑀) ↔ 𝑀 ∈ (1...𝑀)))
35343anbi3d 1441 . . . . . 6 (𝑚 = 𝑀 → ((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) ↔ (𝜑𝑡𝑇𝑀 ∈ (1...𝑀))))
36 fveq2 6906 . . . . . . . 8 (𝑚 = 𝑀 → (seq1(𝑃, 𝑈)‘𝑚) = (seq1(𝑃, 𝑈)‘𝑀))
3736fveq1d 6908 . . . . . . 7 (𝑚 = 𝑀 → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
38 fveq2 6906 . . . . . . 7 (𝑚 = 𝑀 → (seq1( · , (𝐹𝑡))‘𝑚) = (seq1( · , (𝐹𝑡))‘𝑀))
3937, 38eqeq12d 2750 . . . . . 6 (𝑚 = 𝑀 → (((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚) ↔ ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑀)))
4035, 39imbi12d 344 . . . . 5 (𝑚 = 𝑀 → (((𝜑𝑡𝑇𝑚 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑚)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑚)) ↔ ((𝜑𝑡𝑇𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))))
41 1z 12644 . . . . . . . 8 1 ∈ ℤ
42 seq1 14051 . . . . . . . 8 (1 ∈ ℤ → (seq1( · , (𝐹𝑡))‘1) = ((𝐹𝑡)‘1))
4341, 42ax-mp 5 . . . . . . 7 (seq1( · , (𝐹𝑡))‘1) = ((𝐹𝑡)‘1)
44 1zzd 12645 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℤ)
45 1le1 11888 . . . . . . . . . . . . 13 1 ≤ 1
4645a1i 11 . . . . . . . . . . . 12 (𝜑 → 1 ≤ 1)
4744, 3, 44, 46, 5elfzd 13551 . . . . . . . . . . 11 (𝜑 → 1 ∈ (1...𝑀))
48 nfv 1911 . . . . . . . . . . . . 13 𝑖 𝑡𝑇
49 fmuldfeq.5 . . . . . . . . . . . . . . . . 17 𝐹 = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
50 nfcv 2902 . . . . . . . . . . . . . . . . . 18 𝑖𝑇
51 nfmpt1 5255 . . . . . . . . . . . . . . . . . 18 𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
5250, 51nfmpt 5254 . . . . . . . . . . . . . . . . 17 𝑖(𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
5349, 52nfcxfr 2900 . . . . . . . . . . . . . . . 16 𝑖𝐹
54 nfcv 2902 . . . . . . . . . . . . . . . 16 𝑖𝑡
5553, 54nffv 6916 . . . . . . . . . . . . . . 15 𝑖(𝐹𝑡)
56 nfcv 2902 . . . . . . . . . . . . . . 15 𝑖1
5755, 56nffv 6916 . . . . . . . . . . . . . 14 𝑖((𝐹𝑡)‘1)
58 nffvmpt1 6917 . . . . . . . . . . . . . 14 𝑖((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1)
5957, 58nfeq 2916 . . . . . . . . . . . . 13 𝑖((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1)
6048, 59nfim 1893 . . . . . . . . . . . 12 𝑖(𝑡𝑇 → ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1))
61 fveq2 6906 . . . . . . . . . . . . . 14 (𝑖 = 1 → ((𝐹𝑡)‘𝑖) = ((𝐹𝑡)‘1))
62 fveq2 6906 . . . . . . . . . . . . . 14 (𝑖 = 1 → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1))
6361, 62eqeq12d 2750 . . . . . . . . . . . . 13 (𝑖 = 1 → (((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) ↔ ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1)))
6463imbi2d 340 . . . . . . . . . . . 12 (𝑖 = 1 → ((𝑡𝑇 → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖)) ↔ (𝑡𝑇 → ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1))))
65 ovex 7463 . . . . . . . . . . . . . . 15 (1...𝑀) ∈ V
6665mptex 7242 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V
6749fvmpt2 7026 . . . . . . . . . . . . . 14 ((𝑡𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
6866, 67mpan2 691 . . . . . . . . . . . . 13 (𝑡𝑇 → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
6968fveq1d 6908 . . . . . . . . . . . 12 (𝑡𝑇 → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖))
7060, 64, 69vtoclg1f 3569 . . . . . . . . . . 11 (1 ∈ (1...𝑀) → (𝑡𝑇 → ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1)))
7147, 70syl 17 . . . . . . . . . 10 (𝜑 → (𝑡𝑇 → ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1)))
7271imp 406 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝐹𝑡)‘1) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1))
73 eqid 2734 . . . . . . . . . 10 (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
74 fveq2 6906 . . . . . . . . . . 11 (𝑖 = 1 → (𝑈𝑖) = (𝑈‘1))
7574fveq1d 6908 . . . . . . . . . 10 (𝑖 = 1 → ((𝑈𝑖)‘𝑡) = ((𝑈‘1)‘𝑡))
7647adantr 480 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 1 ∈ (1...𝑀))
77 fmuldfeq.9 . . . . . . . . . . . . 13 (𝜑𝑈:(1...𝑀)⟶𝑌)
7877, 47ffvelcdmd 7104 . . . . . . . . . . . 12 (𝜑 → (𝑈‘1) ∈ 𝑌)
7978ancli 548 . . . . . . . . . . . 12 (𝜑 → (𝜑 ∧ (𝑈‘1) ∈ 𝑌))
80 eleq1 2826 . . . . . . . . . . . . . . 15 (𝑓 = (𝑈‘1) → (𝑓𝑌 ↔ (𝑈‘1) ∈ 𝑌))
8180anbi2d 630 . . . . . . . . . . . . . 14 (𝑓 = (𝑈‘1) → ((𝜑𝑓𝑌) ↔ (𝜑 ∧ (𝑈‘1) ∈ 𝑌)))
82 feq1 6716 . . . . . . . . . . . . . 14 (𝑓 = (𝑈‘1) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘1):𝑇⟶ℝ))
8381, 82imbi12d 344 . . . . . . . . . . . . 13 (𝑓 = (𝑈‘1) → (((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ)))
84 fmuldfeq.10 . . . . . . . . . . . . . 14 ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ)
8584a1i 11 . . . . . . . . . . . . 13 (𝑓𝑌 → ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ))
8683, 85vtoclga 3576 . . . . . . . . . . . 12 ((𝑈‘1) ∈ 𝑌 → ((𝜑 ∧ (𝑈‘1) ∈ 𝑌) → (𝑈‘1):𝑇⟶ℝ))
8778, 79, 86sylc 65 . . . . . . . . . . 11 (𝜑 → (𝑈‘1):𝑇⟶ℝ)
8887ffvelcdmda 7103 . . . . . . . . . 10 ((𝜑𝑡𝑇) → ((𝑈‘1)‘𝑡) ∈ ℝ)
8973, 75, 76, 88fvmptd3 7038 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘1) = ((𝑈‘1)‘𝑡))
9072, 89eqtrd 2774 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝐹𝑡)‘1) = ((𝑈‘1)‘𝑡))
91 seq1 14051 . . . . . . . . . 10 (1 ∈ ℤ → (seq1(𝑃, 𝑈)‘1) = (𝑈‘1))
9241, 91ax-mp 5 . . . . . . . . 9 (seq1(𝑃, 𝑈)‘1) = (𝑈‘1)
9392fveq1i 6907 . . . . . . . 8 ((seq1(𝑃, 𝑈)‘1)‘𝑡) = ((𝑈‘1)‘𝑡)
9490, 93eqtr4di 2792 . . . . . . 7 ((𝜑𝑡𝑇) → ((𝐹𝑡)‘1) = ((seq1(𝑃, 𝑈)‘1)‘𝑡))
9543, 94eqtr2id 2787 . . . . . 6 ((𝜑𝑡𝑇) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹𝑡))‘1))
96953adant3 1131 . . . . 5 ((𝜑𝑡𝑇 ∧ 1 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘1)‘𝑡) = (seq1( · , (𝐹𝑡))‘1))
97 simp31 1208 . . . . . . 7 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝜑)
98 simp1 1135 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ ℕ)
99 simp33 1210 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 + 1) ∈ (1...𝑀))
10098, 99jca 511 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)))
101 elnnuz 12919 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
102101biimpi 216 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
103102anim1i 615 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑀)) → (𝑛 ∈ (ℤ‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)))
104 peano2fzr 13573 . . . . . . . . 9 ((𝑛 ∈ (ℤ‘1) ∧ (𝑛 + 1) ∈ (1...𝑀)) → 𝑛 ∈ (1...𝑀))
105100, 103, 1043syl 18 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑛 ∈ (1...𝑀))
106 simp32 1209 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → 𝑡𝑇)
107 simp2 1136 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)))
10897, 106, 105, 107mp3and 1463 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))
109105, 99, 1083jca 1127 . . . . . . 7 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)))
110 nfv 1911 . . . . . . . . 9 𝑓𝜑
111 nfv 1911 . . . . . . . . . 10 𝑓 𝑛 ∈ (1...𝑀)
112 nfv 1911 . . . . . . . . . 10 𝑓(𝑛 + 1) ∈ (1...𝑀)
113 nfcv 2902 . . . . . . . . . . . . . 14 𝑓1
114 fmuldfeq.3 . . . . . . . . . . . . . . 15 𝑃 = (𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
115 nfmpo1 7512 . . . . . . . . . . . . . . 15 𝑓(𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
116114, 115nfcxfr 2900 . . . . . . . . . . . . . 14 𝑓𝑃
117 nfcv 2902 . . . . . . . . . . . . . 14 𝑓𝑈
118113, 116, 117nfseq 14048 . . . . . . . . . . . . 13 𝑓seq1(𝑃, 𝑈)
119 nfcv 2902 . . . . . . . . . . . . 13 𝑓𝑛
120118, 119nffv 6916 . . . . . . . . . . . 12 𝑓(seq1(𝑃, 𝑈)‘𝑛)
121 nfcv 2902 . . . . . . . . . . . 12 𝑓𝑡
122120, 121nffv 6916 . . . . . . . . . . 11 𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
123 nfcv 2902 . . . . . . . . . . 11 𝑓(seq1( · , (𝐹𝑡))‘𝑛)
124122, 123nfeq 2916 . . . . . . . . . 10 𝑓((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)
125111, 112, 124nf3an 1898 . . . . . . . . 9 𝑓(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))
126110, 125nfan 1896 . . . . . . . 8 𝑓(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)))
127 nfv 1911 . . . . . . . . 9 𝑔𝜑
128 nfv 1911 . . . . . . . . . 10 𝑔 𝑛 ∈ (1...𝑀)
129 nfv 1911 . . . . . . . . . 10 𝑔(𝑛 + 1) ∈ (1...𝑀)
130 nfcv 2902 . . . . . . . . . . . . . 14 𝑔1
131 nfmpo2 7513 . . . . . . . . . . . . . . 15 𝑔(𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
132114, 131nfcxfr 2900 . . . . . . . . . . . . . 14 𝑔𝑃
133 nfcv 2902 . . . . . . . . . . . . . 14 𝑔𝑈
134130, 132, 133nfseq 14048 . . . . . . . . . . . . 13 𝑔seq1(𝑃, 𝑈)
135 nfcv 2902 . . . . . . . . . . . . 13 𝑔𝑛
136134, 135nffv 6916 . . . . . . . . . . . 12 𝑔(seq1(𝑃, 𝑈)‘𝑛)
137 nfcv 2902 . . . . . . . . . . . 12 𝑔𝑡
138136, 137nffv 6916 . . . . . . . . . . 11 𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡)
139 nfcv 2902 . . . . . . . . . . 11 𝑔(seq1( · , (𝐹𝑡))‘𝑛)
140138, 139nfeq 2916 . . . . . . . . . 10 𝑔((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)
141128, 129, 140nf3an 1898 . . . . . . . . 9 𝑔(𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))
142127, 141nfan 1896 . . . . . . . 8 𝑔(𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)))
143 fmuldfeq.2 . . . . . . . 8 𝑡𝑌
144 fmuldfeq.7 . . . . . . . . 9 (𝜑𝑇 ∈ V)
145144adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) → 𝑇 ∈ V)
14677adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) → 𝑈:(1...𝑀)⟶𝑌)
147 fmuldfeq.11 . . . . . . . . 9 ((𝜑𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
1481473adant1r 1176 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) ∧ 𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
149 simpr1 1193 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) → 𝑛 ∈ (1...𝑀))
150 simpr2 1194 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) → (𝑛 + 1) ∈ (1...𝑀))
151 simpr3 1195 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))
15284adantlr 715 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) ∧ 𝑓𝑌) → 𝑓:𝑇⟶ℝ)
153126, 142, 143, 114, 49, 145, 146, 148, 149, 150, 151, 152fmuldfeqlem1 45537 . . . . . . 7 (((𝜑 ∧ (𝑛 ∈ (1...𝑀) ∧ (𝑛 + 1) ∈ (1...𝑀) ∧ ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛))) ∧ 𝑡𝑇) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1)))
15497, 109, 106, 153syl21anc 838 . . . . . 6 ((𝑛 ∈ ℕ ∧ ((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) ∧ (𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀))) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1)))
1551543exp 1118 . . . . 5 (𝑛 ∈ ℕ → (((𝜑𝑡𝑇𝑛 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑛)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑛)) → ((𝜑𝑡𝑇 ∧ (𝑛 + 1) ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘(𝑛 + 1))‘𝑡) = (seq1( · , (𝐹𝑡))‘(𝑛 + 1)))))
15619, 26, 33, 40, 96, 155nnind 12281 . . . 4 (𝑀 ∈ ℕ → ((𝜑𝑡𝑇𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑀)))
15712, 156mpcom 38 . . 3 ((𝜑𝑡𝑇𝑀 ∈ (1...𝑀)) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
15811, 157mpd3an3 1461 . 2 ((𝜑𝑡𝑇) → ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
159 fmuldfeq.4 . . . 4 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
160159fveq1i 6907 . . 3 (𝑋𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡)
161160a1i 11 . 2 ((𝜑𝑡𝑇) → (𝑋𝑡) = ((seq1(𝑃, 𝑈)‘𝑀)‘𝑡))
162 simpr 484 . . 3 ((𝜑𝑡𝑇) → 𝑡𝑇)
163 elnnuz 12919 . . . . . 6 (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ‘1))
1642, 163sylib 218 . . . . 5 (𝜑𝑀 ∈ (ℤ‘1))
165164adantr 480 . . . 4 ((𝜑𝑡𝑇) → 𝑀 ∈ (ℤ‘1))
166 fmuldfeq.1 . . . . . . . 8 𝑖𝜑
167166, 48nfan 1896 . . . . . . 7 𝑖(𝜑𝑡𝑇)
168 nfv 1911 . . . . . . 7 𝑖 𝑘 ∈ (1...𝑀)
169167, 168nfan 1896 . . . . . 6 𝑖((𝜑𝑡𝑇) ∧ 𝑘 ∈ (1...𝑀))
170 nfcv 2902 . . . . . . . 8 𝑖𝑘
17155, 170nffv 6916 . . . . . . 7 𝑖((𝐹𝑡)‘𝑘)
172171nfel1 2919 . . . . . 6 𝑖((𝐹𝑡)‘𝑘) ∈ ℝ
173169, 172nfim 1893 . . . . 5 𝑖(((𝜑𝑡𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑘) ∈ ℝ)
174 eleq1 2826 . . . . . . 7 (𝑖 = 𝑘 → (𝑖 ∈ (1...𝑀) ↔ 𝑘 ∈ (1...𝑀)))
175174anbi2d 630 . . . . . 6 (𝑖 = 𝑘 → (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑𝑡𝑇) ∧ 𝑘 ∈ (1...𝑀))))
176 fveq2 6906 . . . . . . 7 (𝑖 = 𝑘 → ((𝐹𝑡)‘𝑖) = ((𝐹𝑡)‘𝑘))
177176eleq1d 2823 . . . . . 6 (𝑖 = 𝑘 → (((𝐹𝑡)‘𝑖) ∈ ℝ ↔ ((𝐹𝑡)‘𝑘) ∈ ℝ))
178175, 177imbi12d 344 . . . . 5 (𝑖 = 𝑘 → ((((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ∈ ℝ) ↔ (((𝜑𝑡𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑘) ∈ ℝ)))
17969ad2antlr 727 . . . . . 6 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖))
180 simpr 484 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑀))
18177ffvelcdmda 7103 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝑌)
182 simpl 482 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → 𝜑)
183182, 181jca 511 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈𝑖) ∈ 𝑌))
184 eleq1 2826 . . . . . . . . . . . . . 14 (𝑓 = (𝑈𝑖) → (𝑓𝑌 ↔ (𝑈𝑖) ∈ 𝑌))
185184anbi2d 630 . . . . . . . . . . . . 13 (𝑓 = (𝑈𝑖) → ((𝜑𝑓𝑌) ↔ (𝜑 ∧ (𝑈𝑖) ∈ 𝑌)))
186 feq1 6716 . . . . . . . . . . . . 13 (𝑓 = (𝑈𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈𝑖):𝑇⟶ℝ))
187185, 186imbi12d 344 . . . . . . . . . . . 12 (𝑓 = (𝑈𝑖) → (((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈𝑖) ∈ 𝑌) → (𝑈𝑖):𝑇⟶ℝ)))
188187, 85vtoclga 3576 . . . . . . . . . . 11 ((𝑈𝑖) ∈ 𝑌 → ((𝜑 ∧ (𝑈𝑖) ∈ 𝑌) → (𝑈𝑖):𝑇⟶ℝ))
189181, 183, 188sylc 65 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
190189adantlr 715 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
191 simplr 769 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡𝑇)
192190, 191ffvelcdmd 7104 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
19373fvmpt2 7026 . . . . . . . 8 ((𝑖 ∈ (1...𝑀) ∧ ((𝑈𝑖)‘𝑡) ∈ ℝ) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑈𝑖)‘𝑡))
194180, 192, 193syl2anc 584 . . . . . . 7 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) = ((𝑈𝑖)‘𝑡))
195194, 192eqeltrd 2838 . . . . . 6 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))‘𝑖) ∈ ℝ)
196179, 195eqeltrd 2838 . . . . 5 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ∈ ℝ)
197173, 178, 196chvarfv 2237 . . . 4 (((𝜑𝑡𝑇) ∧ 𝑘 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑘) ∈ ℝ)
198 remulcl 11237 . . . . 5 ((𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑘 · 𝑏) ∈ ℝ)
199198adantl 481 . . . 4 (((𝜑𝑡𝑇) ∧ (𝑘 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑘 · 𝑏) ∈ ℝ)
200165, 197, 199seqcl 14059 . . 3 ((𝜑𝑡𝑇) → (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ)
201 fmuldfeq.6 . . . 4 𝑍 = (𝑡𝑇 ↦ (seq1( · , (𝐹𝑡))‘𝑀))
202201fvmpt2 7026 . . 3 ((𝑡𝑇 ∧ (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
203162, 200, 202syl2anc 584 . 2 ((𝜑𝑡𝑇) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
204158, 161, 2033eqtr4d 2784 1 ((𝜑𝑡𝑇) → (𝑋𝑡) = (𝑍𝑡))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1536  wnf 1779  wcel 2105  wnfc 2887  Vcvv 3477   class class class wbr 5147  cmpt 5230  wf 6558  cfv 6562  (class class class)co 7430  cmpo 7432  cr 11151  1c1 11153   + caddc 11155   · cmul 11157  cle 11293  cn 12263  cz 12610  cuz 12875  ...cfz 13543  seqcseq 14038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-n0 12524  df-z 12611  df-uz 12876  df-fz 13544  df-seq 14039
This theorem is referenced by:  stoweidlem42  45997  stoweidlem48  46003
  Copyright terms: Public domain W3C validator