Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem23 Structured version   Visualization version   GIF version

Theorem poimirlem23 36975
Description: Lemma for poimir 36985, two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem23.1 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
poimirlem23.2 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
poimirlem23.3 (𝜑𝑉 ∈ (0...𝑁))
Assertion
Ref Expression
poimirlem23 (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
Distinct variable groups:   𝑗,𝑝,𝑦,𝜑   𝑗,𝑁,𝑦   𝑇,𝑗,𝑦   𝑈,𝑗,𝑦   𝑗,𝑉,𝑦   𝜑,𝑝   𝑗,𝐾,𝑝   𝑁,𝑝   𝑇,𝑝   𝑈,𝑝   𝑦,𝐾   𝑉,𝑝

Proof of Theorem poimirlem23
StepHypRef Expression
1 ovex 7445 . . . . . 6 (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
21csbex 5311 . . . . 5 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
32rgenw 3064 . . . 4 𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
4 eqid 2731 . . . . 5 (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
5 fveq1 6890 . . . . . . 7 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝𝑁) = (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
65neeq1d 2999 . . . . . 6 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑁) ≠ 0 ↔ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
7 df-ne 2940 . . . . . 6 ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
86, 7bitrdi 287 . . . . 5 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑁) ≠ 0 ↔ ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
94, 8rexrnmptw 7096 . . . 4 (∀𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
103, 9ax-mp 5 . . 3 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
11 rexnal 3099 . . 3 (∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
1210, 11bitri 275 . 2 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
13 poimir.0 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
1413nnzd 12592 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
15 poimirlem23.3 . . . . . . . . . . 11 (𝜑𝑉 ∈ (0...𝑁))
16 elfzelz 13508 . . . . . . . . . . 11 (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
1715, 16syl 17 . . . . . . . . . 10 (𝜑𝑉 ∈ ℤ)
18 zlem1lt 12621 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑁𝑉 ↔ (𝑁 − 1) < 𝑉))
1914, 17, 18syl2anc 583 . . . . . . . . 9 (𝜑 → (𝑁𝑉 ↔ (𝑁 − 1) < 𝑉))
20 elfzle2 13512 . . . . . . . . . . 11 (𝑉 ∈ (0...𝑁) → 𝑉𝑁)
2115, 20syl 17 . . . . . . . . . 10 (𝜑𝑉𝑁)
2217zred 12673 . . . . . . . . . . . 12 (𝜑𝑉 ∈ ℝ)
2313nnred 12234 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℝ)
2422, 23letri3d 11363 . . . . . . . . . . 11 (𝜑 → (𝑉 = 𝑁 ↔ (𝑉𝑁𝑁𝑉)))
2524biimprd 247 . . . . . . . . . 10 (𝜑 → ((𝑉𝑁𝑁𝑉) → 𝑉 = 𝑁))
2621, 25mpand 692 . . . . . . . . 9 (𝜑 → (𝑁𝑉𝑉 = 𝑁))
2719, 26sylbird 260 . . . . . . . 8 (𝜑 → ((𝑁 − 1) < 𝑉𝑉 = 𝑁))
2827necon3ad 2952 . . . . . . 7 (𝜑 → (𝑉𝑁 → ¬ (𝑁 − 1) < 𝑉))
29 nnm1nn0 12520 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
3013, 29syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑁 − 1) ∈ ℕ0)
31 nn0fz0 13606 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℕ0 ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1)))
3230, 31sylib 217 . . . . . . . . . . 11 (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
3332adantr 480 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
34 iffalse 4537 . . . . . . . . . . . . . . . 16 (¬ (𝑁 − 1) < 𝑉 → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = ((𝑁 − 1) + 1))
3513nncnd 12235 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℂ)
36 npcan1 11646 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
3735, 36syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
3834, 37sylan9eqr 2793 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = 𝑁)
3938csbeq1d 3897 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑁 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
40 oveq2 7420 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁))
4140imaeq2d 6059 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑁 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑁)))
4241xpeq1d 5705 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑁)) × {1}))
43 oveq1 7419 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1))
4443oveq1d 7427 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁))
4544imaeq2d 6059 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑁 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑁 + 1)...𝑁)))
4645xpeq1d 5705 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}))
4742, 46uneq12d 4164 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑁 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})))
48 poimirlem23.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
49 f1ofo 6840 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
50 foima 6810 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
5148, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
5251xpeq1d 5705 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑈 “ (1...𝑁)) × {1}) = ((1...𝑁) × {1}))
5323ltp1d 12151 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑁 < (𝑁 + 1))
5414peano2zd 12676 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑁 + 1) ∈ ℤ)
55 fzn 13524 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
5654, 14, 55syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
5753, 56mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑁 + 1)...𝑁) = ∅)
5857imaeq2d 6059 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑈 “ ((𝑁 + 1)...𝑁)) = (𝑈 “ ∅))
5958xpeq1d 5705 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ((𝑈 “ ∅) × {0}))
60 ima0 6076 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈 “ ∅) = ∅
6160xpeq1i 5702 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 “ ∅) × {0}) = (∅ × {0})
62 0xp 5774 . . . . . . . . . . . . . . . . . . . . . 22 (∅ × {0}) = ∅
6361, 62eqtri 2759 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈 “ ∅) × {0}) = ∅
6459, 63eqtrdi 2787 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ∅)
6552, 64uneq12d 4164 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪ ∅))
66 un0 4390 . . . . . . . . . . . . . . . . . . 19 (((1...𝑁) × {1}) ∪ ∅) = ((1...𝑁) × {1})
6765, 66eqtrdi 2787 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
6847, 67sylan9eqr 2793 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 = 𝑁) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
6968oveq2d 7428 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 = 𝑁) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7013, 69csbied 3931 . . . . . . . . . . . . . . 15 (𝜑𝑁 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7170adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → 𝑁 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7239, 71eqtrd 2771 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7372fveq1d 6893 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇f + ((1...𝑁) × {1}))‘𝑁))
74 elfzonn0 13684 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0..^𝐾) → 𝑗 ∈ ℕ0)
75 nn0p1nn 12518 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
7674, 75syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝐾) → (𝑗 + 1) ∈ ℕ)
77 elsni 4645 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {1} → 𝑦 = 1)
7877oveq2d 7428 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ {1} → (𝑗 + 𝑦) = (𝑗 + 1))
7978eleq1d 2817 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {1} → ((𝑗 + 𝑦) ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ))
8076, 79syl5ibrcom 246 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑗 + 𝑦) ∈ ℕ))
8180imp 406 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1}) → (𝑗 + 𝑦) ∈ ℕ)
8281adantl 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1})) → (𝑗 + 𝑦) ∈ ℕ)
83 poimirlem23.1 . . . . . . . . . . . . . . 15 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
84 1ex 11217 . . . . . . . . . . . . . . . . 17 1 ∈ V
8584fconst 6777 . . . . . . . . . . . . . . . 16 ((1...𝑁) × {1}):(1...𝑁)⟶{1}
8685a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ((1...𝑁) × {1}):(1...𝑁)⟶{1})
87 ovexd 7447 . . . . . . . . . . . . . . 15 (𝜑 → (1...𝑁) ∈ V)
88 inidm 4218 . . . . . . . . . . . . . . 15 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
8982, 83, 86, 87, 87, 88off 7692 . . . . . . . . . . . . . 14 (𝜑 → (𝑇f + ((1...𝑁) × {1})):(1...𝑁)⟶ℕ)
90 elfz1end 13538 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
9113, 90sylib 217 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (1...𝑁))
9289, 91ffvelcdmd 7087 . . . . . . . . . . . . 13 (𝜑 → ((𝑇f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
9392adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ((𝑇f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
9473, 93eqeltrd 2832 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ∈ ℕ)
9594nnne0d 12269 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)
96 breq1 5151 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → (𝑦 < 𝑉 ↔ (𝑁 − 1) < 𝑉))
97 id 22 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → 𝑦 = (𝑁 − 1))
98 oveq1 7419 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1))
9996, 97, 98ifbieq12d 4556 . . . . . . . . . . . . . . 15 (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)))
10099csbeq1d 3897 . . . . . . . . . . . . . 14 (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
101100fveq1d 6893 . . . . . . . . . . . . 13 (𝑦 = (𝑁 − 1) → (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
102101neeq1d 2999 . . . . . . . . . . . 12 (𝑦 = (𝑁 − 1) → ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
1037, 102bitr3id 285 . . . . . . . . . . 11 (𝑦 = (𝑁 − 1) → (¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
104103rspcev 3612 . . . . . . . . . 10 (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
10533, 95, 104syl2anc 583 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
106105, 11sylib 217 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
107106ex 412 . . . . . . 7 (𝜑 → (¬ (𝑁 − 1) < 𝑉 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
10828, 107syld 47 . . . . . 6 (𝜑 → (𝑉𝑁 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
109108necon4ad 2958 . . . . 5 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 → 𝑉 = 𝑁))
110109pm4.71rd 562 . . . 4 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)))
11130nn0zd 12591 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℤ)
112 uzid 12844 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
113 peano2uz 12892 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
114111, 112, 1133syl 18 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
11537, 114eqeltrrd 2833 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
116 fzss2 13548 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
117115, 116syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
118117sselda 3982 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
11991adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑁 ∈ (1...𝑁))
12083ffnd 6718 . . . . . . . . . . . . . 14 (𝜑𝑇 Fn (1...𝑁))
121120adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇 Fn (1...𝑁))
12284fconst 6777 . . . . . . . . . . . . . . . . 17 ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
123 c0ex 11215 . . . . . . . . . . . . . . . . . 18 0 ∈ V
124123fconst 6777 . . . . . . . . . . . . . . . . 17 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
125122, 124pm3.2i 470 . . . . . . . . . . . . . . . 16 (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
126 dff1o3 6839 . . . . . . . . . . . . . . . . . . 19 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
127126simprbi 496 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
128 imain 6633 . . . . . . . . . . . . . . . . . 18 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
12948, 127, 1283syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
130 elfzelz 13508 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
131130zred 12673 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
132131ltp1d 12151 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
133 fzdisj 13535 . . . . . . . . . . . . . . . . . . . 20 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
134132, 133syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
135134imaeq2d 6059 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
136135, 60eqtrdi 2787 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
137129, 136sylan9req 2792 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
138 fun 6753 . . . . . . . . . . . . . . . 16 (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
139125, 137, 138sylancr 586 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
140 elfznn0 13601 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
141140, 75syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
142 nnuz 12872 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
143141, 142eleqtrdi 2842 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
144 elfzuz3 13505 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
145 fzsplit2 13533 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
146143, 144, 145syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
147146imaeq2d 6059 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
148 imaundi 6149 . . . . . . . . . . . . . . . . . 18 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
149147, 148eqtr2di 2788 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
150149, 51sylan9eqr 2793 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
151150feq2d 6703 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
152139, 151mpbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
153152ffnd 6718 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
154 ovexd 7447 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
155 eqidd 2732 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → (𝑇𝑁) = (𝑇𝑁))
156 eqidd 2732 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
157121, 153, 154, 154, 88, 155, 156ofval 7685 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
158119, 157mpdan 684 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
159158eqeq1d 2733 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0))
16083, 91ffvelcdmd 7087 . . . . . . . . . . . . . 14 (𝜑 → (𝑇𝑁) ∈ (0..^𝐾))
161 elfzonn0 13684 . . . . . . . . . . . . . 14 ((𝑇𝑁) ∈ (0..^𝐾) → (𝑇𝑁) ∈ ℕ0)
162160, 161syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑁) ∈ ℕ0)
163162nn0red 12540 . . . . . . . . . . . 12 (𝜑 → (𝑇𝑁) ∈ ℝ)
164163adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇𝑁) ∈ ℝ)
165162nn0ge0d 12542 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑇𝑁))
166165adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → 0 ≤ (𝑇𝑁))
167 1re 11221 . . . . . . . . . . . . . 14 1 ∈ ℝ
168 snssi 4811 . . . . . . . . . . . . . 14 (1 ∈ ℝ → {1} ⊆ ℝ)
169167, 168ax-mp 5 . . . . . . . . . . . . 13 {1} ⊆ ℝ
170 0re 11223 . . . . . . . . . . . . . 14 0 ∈ ℝ
171 snssi 4811 . . . . . . . . . . . . . 14 (0 ∈ ℝ → {0} ⊆ ℝ)
172170, 171ax-mp 5 . . . . . . . . . . . . 13 {0} ⊆ ℝ
173169, 172unssi 4185 . . . . . . . . . . . 12 ({1} ∪ {0}) ⊆ ℝ
174152, 119ffvelcdmd 7087 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}))
175173, 174sselid 3980 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ)
176 elun 4148 . . . . . . . . . . . . 13 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) ↔ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}))
177 0le1 11744 . . . . . . . . . . . . . . 15 0 ≤ 1
178 elsni 4645 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 1)
179177, 178breqtrrid 5186 . . . . . . . . . . . . . 14 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
180 0le0 12320 . . . . . . . . . . . . . . 15 0 ≤ 0
181 elsni 4645 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
182180, 181breqtrrid 5186 . . . . . . . . . . . . . 14 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
183179, 182jaoi 854 . . . . . . . . . . . . 13 ((((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
184176, 183sylbi 216 . . . . . . . . . . . 12 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
185174, 184syl 17 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
186 add20 11733 . . . . . . . . . . 11 ((((𝑇𝑁) ∈ ℝ ∧ 0 ≤ (𝑇𝑁)) ∧ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ ∧ 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))) → (((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
187164, 166, 175, 185, 186syl22anc 836 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
188159, 187bitrd 279 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
189118, 188syldan 590 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
190189ralbidva 3174 . . . . . . 7 (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
191190adantr 480 . . . . . 6 ((𝜑𝑉 = 𝑁) → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
192 breq2 5152 . . . . . . . . . . . . . 14 (𝑉 = 𝑁 → (𝑦 < 𝑉𝑦 < 𝑁))
193192ifbid 4551 . . . . . . . . . . . . 13 (𝑉 = 𝑁 → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)))
194 elfzelz 13508 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
195194zred 12673 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
196195adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
19730nn0red 12540 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℝ)
198197adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
19923adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ)
200 elfzle2 13512 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1))
201200adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1))
20223ltm1d 12153 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) < 𝑁)
203202adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
204196, 198, 199, 201, 203lelttrd 11379 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁)
205204iftrued 4536 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)) = 𝑦)
206193, 205sylan9eqr 2793 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑉 = 𝑁) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
207206an32s 649 . . . . . . . . . . 11 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
208207csbeq1d 3897 . . . . . . . . . 10 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
209208fveq1d 6893 . . . . . . . . 9 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
210209eqeq1d 2733 . . . . . . . 8 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
211210ralbidva 3174 . . . . . . 7 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
212 nfv 1916 . . . . . . . 8 𝑦((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
213 nfcsb1v 3918 . . . . . . . . . 10 𝑗𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
214 nfcv 2902 . . . . . . . . . 10 𝑗𝑁
215213, 214nffv 6901 . . . . . . . . 9 𝑗(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)
216215nfeq1 2917 . . . . . . . 8 𝑗(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
217 csbeq1a 3907 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
218217fveq1d 6893 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
219218eqeq1d 2733 . . . . . . . 8 (𝑗 = 𝑦 → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
220212, 216, 219cbvralw 3302 . . . . . . 7 (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
221211, 220bitr4di 289 . . . . . 6 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
222 ne0i 4334 . . . . . . . . . 10 ((𝑁 − 1) ∈ (0...(𝑁 − 1)) → (0...(𝑁 − 1)) ≠ ∅)
223 r19.3rzv 4498 . . . . . . . . . 10 ((0...(𝑁 − 1)) ≠ ∅ → ((𝑇𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0))
22432, 222, 2233syl 18 . . . . . . . . 9 (𝜑 → ((𝑇𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0))
225 elfzelz 13508 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℤ)
226225zred 12673 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℝ)
227226ltp1d 12151 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 < (𝑗 + 1))
228227, 133syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...(𝑁 − 1)) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
229228imaeq2d 6059 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
230229, 60eqtrdi 2787 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
231129, 230sylan9req 2792 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
232231adantlr 712 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
233 simplr 766 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) = 𝑁)
234 f1ofn 6834 . . . . . . . . . . . . . . . . . . 19 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
23548, 234syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 Fn (1...𝑁))
236235adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑈 Fn (1...𝑁))
237 elfznn0 13601 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ0)
238237, 75syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ)
239238, 142eleqtrdi 2842 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ (ℤ‘1))
240 fzss1 13547 . . . . . . . . . . . . . . . . . . 19 ((𝑗 + 1) ∈ (ℤ‘1) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
241239, 240syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
242241adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
24337adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
244 elfzuz3 13505 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑗))
245 eluzp1p1 12857 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 − 1) ∈ (ℤ𝑗) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
247246adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
248243, 247eqeltrrd 2833 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑗 + 1)))
249 eluzfz2 13516 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘(𝑗 + 1)) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
250248, 249syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
251 fnfvima 7237 . . . . . . . . . . . . . . . . 17 ((𝑈 Fn (1...𝑁) ∧ ((𝑗 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑗 + 1)...𝑁)) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
252236, 242, 250, 251syl3anc 1370 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
253252adantlr 712 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
254233, 253eqeltrrd 2833 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
255 fnconstg 6779 . . . . . . . . . . . . . . . 16 (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
25684, 255ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
257 fnconstg 6779 . . . . . . . . . . . . . . . 16 (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)))
258123, 257ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁))
259 fvun2 6983 . . . . . . . . . . . . . . 15 ((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
260256, 258, 259mp3an12 1450 . . . . . . . . . . . . . 14 ((((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
261232, 254, 260syl2anc 583 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
262123fvconst2 7207 . . . . . . . . . . . . . 14 (𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
263254, 262syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
264261, 263eqtrd 2771 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
265264ralrimiva 3145 . . . . . . . . . . 11 ((𝜑 ∧ (𝑈𝑁) = 𝑁) → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
266265ex 412 . . . . . . . . . 10 (𝜑 → ((𝑈𝑁) = 𝑁 → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
26732adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
268 ax-1ne0 11185 . . . . . . . . . . . . . . 15 1 ≠ 0
269 imain 6633 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝑈 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))))
27048, 127, 2693syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))))
271202, 37breqtrrd 5176 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑁 − 1) < ((𝑁 − 1) + 1))
272 fzdisj 13535 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 − 1) < ((𝑁 − 1) + 1) → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
273271, 272syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
274273imaeq2d 6059 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = (𝑈 “ ∅))
275274, 60eqtrdi 2787 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ∅)
276270, 275eqtr3d 2773 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
277276adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
27891adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ (1...𝑁))
279 elimasni 6090 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (𝑈 “ {𝑁}) → 𝑁𝑈𝑁)
280 fnbrfvb 6944 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈 Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑈𝑁) = 𝑁𝑁𝑈𝑁))
281235, 91, 280syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑈𝑁) = 𝑁𝑁𝑈𝑁))
282279, 281imbitrrid 245 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑁 ∈ (𝑈 “ {𝑁}) → (𝑈𝑁) = 𝑁))
283282necon3ad 2952 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ¬ 𝑁 ∈ (𝑈 “ {𝑁})))
284283imp 406 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ¬ 𝑁 ∈ (𝑈 “ {𝑁}))
285278, 284eldifd 3959 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ ((1...𝑁) ∖ (𝑈 “ {𝑁})))
286 imadif 6632 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
28748, 127, 2863syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
288 difun2 4480 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁})
289 elun 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}))
290 velsn 4644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ {𝑁} ↔ 𝑗 = 𝑁)
291290orbi2i 910 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
292289, 291bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
29313, 142eleqtrdi 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑁 ∈ (ℤ‘1))
294 fzm1 13588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
295293, 294syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
296292, 295bitr4id 290 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ 𝑗 ∈ (1...𝑁)))
297296eqrdv 2729 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
298297difeq1d 4121 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...𝑁) ∖ {𝑁}))
299197, 23ltnled 11368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
300202, 299mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
301 elfzle2 13512 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
302300, 301nsyl 140 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
303 difsn 4801 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑁 ∈ (1...(𝑁 − 1)) → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
304302, 303syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
305288, 298, 3043eqtr3a 2795 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
306305imaeq2d 6059 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
30751difeq1d 4121 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})) = ((1...𝑁) ∖ (𝑈 “ {𝑁})))
308287, 306, 3073eqtr3rd 2780 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
309308adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
310285, 309eleqtrd 2834 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))
311 fnconstg 6779 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ V → ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))))
31284, 311ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1)))
313 fnconstg 6779 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ V → ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
314123, 313ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁))
315 fvun1 6982 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))) ∧ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)) ∧ (((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
316312, 314, 315mp3an12 1450 . . . . . . . . . . . . . . . . . 18 ((((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1)))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
317277, 310, 316syl2anc 583 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
31884fvconst2 7207 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
319310, 318syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
320317, 319eqtrd 2771 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = 1)
321320neeq1d 2999 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ 1 ≠ 0))
322268, 321mpbiri 258 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0)
323 df-ne 2940 . . . . . . . . . . . . . . . 16 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
324 oveq2 7420 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑁 − 1) → (1...𝑗) = (1...(𝑁 − 1)))
325324imaeq2d 6059 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑁 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑁 − 1))))
326325xpeq1d 5705 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑁 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑁 − 1))) × {1}))
327 oveq1 7419 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑁 − 1) → (𝑗 + 1) = ((𝑁 − 1) + 1))
328327oveq1d 7427 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑁 − 1) → ((𝑗 + 1)...𝑁) = (((𝑁 − 1) + 1)...𝑁))
329328imaeq2d 6059 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑁 − 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
330329xpeq1d 5705 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑁 − 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))
331326, 330uneq12d 4164 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑁 − 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0})))
332331fveq1d 6893 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑁 − 1) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁))
333332neeq1d 2999 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑁 − 1) → (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
334323, 333bitr3id 285 . . . . . . . . . . . . . . 15 (𝑗 = (𝑁 − 1) → (¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
335334rspcev 3612 . . . . . . . . . . . . . 14 (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
336267, 322, 335syl2anc 583 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
337336ex 412 . . . . . . . . . . . 12 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
338 rexnal 3099 . . . . . . . . . . . 12 (∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
339337, 338imbitrdi 250 . . . . . . . . . . 11 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
340339necon4ad 2958 . . . . . . . . . 10 (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 → (𝑈𝑁) = 𝑁))
341266, 340impbid 211 . . . . . . . . 9 (𝜑 → ((𝑈𝑁) = 𝑁 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
342224, 341anbi12d 630 . . . . . . . 8 (𝜑 → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
343 r19.26 3110 . . . . . . . 8 (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
344342, 343bitr4di 289 . . . . . . 7 (𝜑 → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
345344adantr 480 . . . . . 6 ((𝜑𝑉 = 𝑁) → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
346191, 221, 3453bitr4d 311 . . . . 5 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁)))
347346pm5.32da 578 . . . 4 (𝜑 → ((𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) ↔ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
348110, 347bitrd 279 . . 3 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
349348notbid 318 . 2 (𝜑 → (¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
35012, 349bitrid 283 1 (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844   = wceq 1540  wcel 2105  wne 2939  wral 3060  wrex 3069  Vcvv 3473  csb 3893  cdif 3945  cun 3946  cin 3947  wss 3948  c0 4322  ifcif 4528  {csn 4628   class class class wbr 5148  cmpt 5231   × cxp 5674  ccnv 5675  ran crn 5677  cima 5679  Fun wfun 6537   Fn wfn 6538  wf 6539  ontowfo 6541  1-1-ontowf1o 6542  cfv 6543  (class class class)co 7412  f cof 7672  cc 11114  cr 11115  0cc0 11116  1c1 11117   + caddc 11119   < clt 11255  cle 11256  cmin 11451  cn 12219  0cn0 12479  cz 12565  cuz 12829  ...cfz 13491  ..^cfzo 13634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7674  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-er 8709  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-nn 12220  df-n0 12480  df-z 12566  df-uz 12830  df-fz 13492  df-fzo 13635
This theorem is referenced by:  poimirlem24  36976
  Copyright terms: Public domain W3C validator